Widening happens at expect, and the wider operand decides a binary op
This commit is contained in:
parent
080d294bc9
commit
0c50f34916
141
lib/check.ml
141
lib/check.ml
@ -2192,14 +2192,43 @@ let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
|
|||||||
mk loc oty
|
mk loc oty
|
||||||
(Tast.Let ([ (s, got) ], [ mk loc oty (Tast.If (not_nil, some, none)) ]))
|
(Tast.Let ([ (s, got) ], [ mk loc oty (Tast.If (not_nil, some, none)) ]))
|
||||||
|
|
||||||
|
(* What a numeric mismatch has left to say, now that widening is silent.
|
||||||
|
FIX.org 2026-09-20, "Implicit widening": every conversion that cannot change
|
||||||
|
the number happens by itself, so a numeric pair that still reaches a refusal
|
||||||
|
is one of exactly two things, and this tells them apart.
|
||||||
|
|
||||||
|
Either the wanted type is *narrower* — the conversion can lose, which is
|
||||||
|
what the language has always refused to do without being told, and the
|
||||||
|
sentence names the cast and points out that the other direction needed
|
||||||
|
nothing. Or there is no direction at all: i32 and u32 are the same width and
|
||||||
|
each holds values the other cannot, so neither widens and the program has to
|
||||||
|
say which half it means to keep.
|
||||||
|
|
||||||
|
Written once and used by both refusals that can report one — [expect]'s, and
|
||||||
|
the binary operators' when their two operands have no join. *)
|
||||||
|
let numeric_note ~(want : Types.t) ~(got : Types.t) =
|
||||||
|
if not (Types.is_numeric want && Types.is_numeric got) then ""
|
||||||
|
else if Types.widens_to ~from:want ~into:got then
|
||||||
|
Printf.sprintf
|
||||||
|
" — %s into %s can lose, so it has to be written: (%s x). The other way \
|
||||||
|
round, %s widens into %s by itself"
|
||||||
|
(Types.to_string got) (Types.to_string want) (Types.to_string want)
|
||||||
|
(Types.to_string want) (Types.to_string got)
|
||||||
|
else
|
||||||
|
Printf.sprintf
|
||||||
|
" — neither widens into the other, so the conversion has to be written: \
|
||||||
|
(%s x)"
|
||||||
|
(Types.to_string want)
|
||||||
|
|
||||||
let expect ctx loc ~want (got : Tast.expr) =
|
let expect ctx loc ~want (got : Tast.expr) =
|
||||||
match want with
|
match want with
|
||||||
| None -> got
|
| None -> got
|
||||||
| Some w ->
|
| Some w ->
|
||||||
(* The boundary, and the only implicit conversion in the language. It runs
|
(* The boundary: where a wanted type meets a produced one, and the one
|
||||||
before [fits] rather than instead of it: what comes back is an ordinary
|
place the language's implicit conversions live. It runs before [fits]
|
||||||
expression of the wanted type, and if the coercion did not produce one
|
rather than instead of it: what comes back is an ordinary expression of
|
||||||
the usual message is still the one that reports it. *)
|
the wanted type, and if the coercion did not produce one the usual
|
||||||
|
message is still the one that reports it. *)
|
||||||
let got =
|
let got =
|
||||||
match w, got.Tast.ty with
|
match w, got.Tast.ty with
|
||||||
| Types.Dyn, Types.Dyn -> got
|
| Types.Dyn, Types.Dyn -> got
|
||||||
@ -2217,6 +2246,19 @@ let expect ctx loc ~want (got : Tast.expr) =
|
|||||||
(Types.to_string w)
|
(Types.to_string w)
|
||||||
| _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
|
| _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
|
||||||
| _, Types.Dyn -> unbox loc w got
|
| _, Types.Dyn -> unbox loc w got
|
||||||
|
(* Implicit widening, and this single arm is the whole of its surface.
|
||||||
|
[expect] is called by every site that annotates and by nothing else,
|
||||||
|
so an argument, a return, a let or defvar with a type, a struct field
|
||||||
|
initialiser, a push into a Vec and a C import's parameter all get it
|
||||||
|
here at once and none of them had to learn about it.
|
||||||
|
|
||||||
|
The conversion is performed, not waved through: [widen] emits the same
|
||||||
|
[Cast] node the written (i64 x) emits, so the backends sext or zext by
|
||||||
|
the *source* type's signedness and nothing downstream sees a node
|
||||||
|
whose type disagrees with its bits. [widens_to] is what keeps that
|
||||||
|
honest — it admits only conversions that cannot change the number, so
|
||||||
|
the cast this inserts is one no program can tell happened. *)
|
||||||
|
| _ when Types.widens_to ~from:got.Tast.ty ~into:w -> widen loc w got
|
||||||
| _ -> got
|
| _ -> got
|
||||||
in
|
in
|
||||||
if Types.fits ~expected:w ~actual:got.Tast.ty then got
|
if Types.fits ~expected:w ~actual:got.Tast.ty then got
|
||||||
@ -2224,9 +2266,15 @@ let expect ctx loc ~want (got : Tast.expr) =
|
|||||||
(* Kinded so that the one caller who knows more — a call argument, which
|
(* Kinded so that the one caller who knows more — a call argument, which
|
||||||
can name the function and the parameter — can recognise this exact
|
can name the function and the parameter — can recognise this exact
|
||||||
refusal at this exact span and say the rest. Every other reader of a
|
refusal at this exact span and say the rest. Every other reader of a
|
||||||
diagnostic ignores [kind]. *)
|
diagnostic ignores [kind].
|
||||||
Loc.failk "check/type-mismatch" loc "expected %s, found %s"
|
|
||||||
|
[numeric_note] is the rest of the sentence when both sides are
|
||||||
|
numbers, and it is on this message rather than beside it because a
|
||||||
|
reader who has just been told i64 and i32 are different types needs
|
||||||
|
to be told, in the same breath, which direction needed nothing. *)
|
||||||
|
Loc.failk "check/type-mismatch" loc "expected %s, found %s%s"
|
||||||
(Types.to_string w) (Types.to_string got.Tast.ty)
|
(Types.to_string w) (Types.to_string got.Tast.ty)
|
||||||
|
(numeric_note ~want:w ~got:got.Tast.ty)
|
||||||
|
|
||||||
(* Something a [break] may not jump out of, named so the refusal can say which.
|
(* Something a [break] may not jump out of, named so the refusal can say which.
|
||||||
See [lentry]: it is a barrier and not a blanket refusal, so a loop written
|
See [lentry]: it is a barrier and not a blanket refusal, so a loop written
|
||||||
@ -5448,8 +5496,10 @@ and named_call ctx ~want loc name args =
|
|||||||
(* Same truthiness as [if]: a dyn argument is negated on nil/false vs.
|
(* Same truthiness as [if]: a dyn argument is negated on nil/false vs.
|
||||||
everything else, not narrowed to a strict bool first. *)
|
everything else, not narrowed to a strict bool first. *)
|
||||||
prim Tast.Not Types.Bool [ check_truthy ctx (List.hd args) ]
|
prim Tast.Not Types.Bool [ check_truthy ctx (List.hd args) ]
|
||||||
(* Bitwise operators are integers-only, and the shift count has the same type
|
(* Bitwise operators are integers-only. They take the ordinary join — an
|
||||||
as the value shifted — there is no implicit widening anywhere else either. *)
|
operand that widens into the other does, so (bit-and u8-flags u32-mask) is
|
||||||
|
a u32 and — and the shifts below do not, which is the one carve-out
|
||||||
|
widening has (FIX.org 2026-09-20). *)
|
||||||
| "bit-and" | "bit-or" | "bit-xor" ->
|
| "bit-and" | "bit-or" | "bit-xor" ->
|
||||||
let p = match name with
|
let p = match name with
|
||||||
| "bit-and" -> Tast.BitAnd | "bit-or" -> Tast.BitOr
|
| "bit-and" -> Tast.BitAnd | "bit-or" -> Tast.BitOr
|
||||||
@ -5460,11 +5510,20 @@ and named_call ctx ~want loc name args =
|
|||||||
(function Types.Int _ -> true | _ -> false) "integers" args
|
(function Types.Int _ -> true | _ -> false) "integers" args
|
||||||
(* The shifts stay at two, and not only because a shift chain reads badly:
|
(* The shifts stay at two, and not only because a shift chain reads badly:
|
||||||
each count would be checked against the same width below, so (<< x 30 30)
|
each count would be checked against the same width below, so (<< x 30 30)
|
||||||
would pass two legal shifts and still shift the value away entirely. *)
|
would pass two legal shifts and still shift the value away entirely.
|
||||||
|
|
||||||
|
[~join:false] is the one place widening is deliberately not symmetric.
|
||||||
|
The count still widens *to* the value's type — (<< i64-x u8-n) is fine —
|
||||||
|
but the value never widens to the count's, which the general rule would do
|
||||||
|
for (<< u8-x i32-n). It would be the wrong answer twice over: the result's
|
||||||
|
type and the width the shift wraps at would be taken from a number that is
|
||||||
|
only saying how far, and the range check just below, along with [emit]'s
|
||||||
|
mask, is keyed to the *value's* width. A count wider than the value is
|
||||||
|
refused and is told to write the cast. *)
|
||||||
| "<<" | ">>" ->
|
| "<<" | ">>" ->
|
||||||
let p = if String.equal name "<<" then Tast.Shl else Tast.Shr in
|
let p = if String.equal name "<<" then Tast.Shl else Tast.Shr in
|
||||||
arity ctx loc name 2 args;
|
arity ctx loc name 2 args;
|
||||||
let a, b = binary ctx name loc ~want:(numeric_want want) args in
|
let a, b = binary ctx ~join:false name loc ~want:(numeric_want want) args in
|
||||||
(match a.Tast.ty with
|
(match a.Tast.ty with
|
||||||
| Types.Int _ -> ()
|
| Types.Int _ -> ()
|
||||||
| other -> fail loc "%s takes integers, found %s" name
|
| other -> fail loc "%s takes integers, found %s" name
|
||||||
@ -7434,11 +7493,48 @@ and byte_slice ctx (a : Ast.expr) =
|
|||||||
and numeric_want want =
|
and numeric_want want =
|
||||||
match want with Some (Types.Int _ | Types.Float _) -> want | _ -> None
|
match want with Some (Types.Int _ | Types.Float _) -> want | _ -> None
|
||||||
|
|
||||||
(* Both operands of a binary operator have one type, and there is no implicit
|
(* Both operands of a binary operator have one type, so one side has to decide
|
||||||
widening, so one side has to decide it. Check the side that carries the most
|
it. Check the side that carries the most information first: a non-literal
|
||||||
information first: a non-literal over a literal, and a float literal over an
|
over a literal, and a float literal over an integer one, since an integer
|
||||||
integer one, since an integer constant converts to a float and not back. *)
|
constant converts to a float and not back.
|
||||||
and binary ctx ?(dyn_ok = false) name loc ~want args =
|
|
||||||
|
Widening (FIX.org 2026-09-20) does not retire that rule, it finishes it.
|
||||||
|
Three things decide, in this order:
|
||||||
|
|
||||||
|
1. An expectation, if the site has one, and it reaches *both* operands. So
|
||||||
|
(defn f [] i64 (+ a b)) over two i32s widens each operand and adds at
|
||||||
|
i64, rather than adding at i32 and widening the sum. That is the better
|
||||||
|
of the two readings and it costs nothing to prefer it, because no program
|
||||||
|
that compiled before can reach it — the pair used to be a refusal.
|
||||||
|
2. A literal, exactly as before: it takes its width from the other operand,
|
||||||
|
so (+ x 1) over a u64 x is still u64 arithmetic and (let [h fnv-offset])
|
||||||
|
over a u64 defconst still means what it meant. [needs_want] is what marks
|
||||||
|
the forms this applies to and it is untouched.
|
||||||
|
3. Otherwise the *wider* side decides — [Types.join], whichever operand the
|
||||||
|
other widens into, with a [Cast] put on the narrower one. (+ i32-var
|
||||||
|
i64-var) is an i64 add. Equal width across signedness has no join, by
|
||||||
|
construction: neither i32 nor u32 widens into the other, and the refusal
|
||||||
|
says which cast to write.
|
||||||
|
|
||||||
|
[join_pair] is reached only when the *first* operand turned out to be the
|
||||||
|
narrower one. The other order needs nothing here: checking y against an i64
|
||||||
|
x already widens an i32 y inside [expect]. *)
|
||||||
|
and join_pair ctx (a : Tast.expr) (y : Ast.expr) exn =
|
||||||
|
(* Asking y for [a]'s type failed. Either y is genuinely wrong, or y is
|
||||||
|
simply the wider operand and this is the one direction [expect] cannot
|
||||||
|
serve on its own. Check y on its own terms to find out; if it decides a
|
||||||
|
type that a widens into, a is the one that moves. Anything else re-raises
|
||||||
|
the original refusal, so an error inside y is still reported as itself and
|
||||||
|
no form that cannot check without an expectation — None, (zeroed) — loses
|
||||||
|
the expectation it used to get. *)
|
||||||
|
match check ctx y with
|
||||||
|
| exception _ -> raise exn
|
||||||
|
| b ->
|
||||||
|
if Types.widens_to ~from:a.Tast.ty ~into:b.Tast.ty then
|
||||||
|
widen a.Tast.loc b.Tast.ty a, b
|
||||||
|
else raise exn
|
||||||
|
|
||||||
|
and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
|
||||||
match args with
|
match args with
|
||||||
| [ x; y ] ->
|
| [ x; y ] ->
|
||||||
let y_decides =
|
let y_decides =
|
||||||
@ -7484,12 +7580,21 @@ and binary ctx ?(dyn_ok = false) name loc ~want args =
|
|||||||
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
|
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
|
||||||
|| Types.equal a.Tast.ty b.Tast.ty
|
|| Types.equal a.Tast.ty b.Tast.ty
|
||||||
then a, b
|
then a, b
|
||||||
else a, check ctx ~want:a.Tast.ty y
|
(* Both operands are already in hand here, so the join is read off
|
||||||
|
directly rather than through [join_pair]'s retry. Whichever one the
|
||||||
|
other widens into is the pair's type; with no join, the re-check
|
||||||
|
produces the refusal, which names the cast at y's own line. *)
|
||||||
|
else
|
||||||
|
(match Types.join a.Tast.ty b.Tast.ty with
|
||||||
|
| Some t ->
|
||||||
|
widen a.Tast.loc t a, widen b.Tast.loc t b
|
||||||
|
| None -> a, check ctx ~want:a.Tast.ty y)
|
||||||
end
|
end
|
||||||
else begin
|
else begin
|
||||||
let a = check ctx ?want x in
|
let a = check ctx ?want x in
|
||||||
let b = check ctx ~want:a.Tast.ty y in
|
match check ctx ~want:a.Tast.ty y with
|
||||||
a, b
|
| b -> a, b
|
||||||
|
| exception e -> if join then join_pair ctx a y e else raise e
|
||||||
end
|
end
|
||||||
| _ -> fail loc "%s takes two arguments" name
|
| _ -> fail loc "%s takes two arguments" name
|
||||||
|
|
||||||
|
|||||||
109
test/programs/widening.flan
Normal file
109
test/programs/widening.flan
Normal file
@ -0,0 +1,109 @@
|
|||||||
|
;;;; Implicit widening, and the only thing worth pinning about it: the bits.
|
||||||
|
;;;; FIX.org 2026-09-20, "Implicit widening".
|
||||||
|
;;;;
|
||||||
|
;;;; A widening conversion is admitted exactly when it cannot change the
|
||||||
|
;;;; number, so every row here has an answer that is also the answer the source
|
||||||
|
;;;; type had. Which means the test is entirely about the *emitted* cast being
|
||||||
|
;;;; the right one: a sign-extension where the source is signed, a
|
||||||
|
;;;; zero-extension where it is not, and the float conversions picking sitofp
|
||||||
|
;;;; against uitofp by the same rule. Each of those is a separate instruction
|
||||||
|
;;;; on both backends and choosing the wrong one gives a wrong number rather
|
||||||
|
;;;; than a wrong type, which no type test would catch.
|
||||||
|
;;;;
|
||||||
|
;;;; The rows are picked so that a mistake is visible in the printed value:
|
||||||
|
;;;;
|
||||||
|
;;;; -5 i8 to i64 sext; a zext prints 251
|
||||||
|
;;;; -1 i32 to i64 sext; a zext prints 4294967295
|
||||||
|
;;;; 255 u8 to i16 zext; a sext prints -1
|
||||||
|
;;;; 4000000000 u32 zext to i64; a sext prints -294967296
|
||||||
|
;;;; 4294967295 u32 to f64, exact; a signed conversion prints -1
|
||||||
|
;;;; -2000000000 i32 to f64; a uitofp prints 2294967296
|
||||||
|
;;;;
|
||||||
|
;;;; Everything goes through a global rather than a literal, because a literal
|
||||||
|
;;;; is built at the wanted width by the literal rule and would never reach a
|
||||||
|
;;;; cast at all.
|
||||||
|
|
||||||
|
(defvar i8-neg i8 -5)
|
||||||
|
(defvar i8-pos i8 127)
|
||||||
|
(defvar i16-neg i16 -300)
|
||||||
|
(defvar i32-neg i32 -2000000000)
|
||||||
|
(defvar i32-one i32 1)
|
||||||
|
(defvar i32-all i32 -1)
|
||||||
|
(defvar u8-max u8 255)
|
||||||
|
(defvar u16-max u16 65535)
|
||||||
|
(defvar u32-big u32 4000000000)
|
||||||
|
(defvar u32-max u32 4294967295)
|
||||||
|
(defvar i64-big i64 5000000000)
|
||||||
|
(defvar f32-half f32 0.5)
|
||||||
|
|
||||||
|
;; Widening at a parameter. Each of these is a plain typed function and the
|
||||||
|
;; call sites below hand it a narrower type with no cast written anywhere.
|
||||||
|
(defn take-i64 [x i64] i64 x)
|
||||||
|
(defn take-i16 [x i16] i16 x)
|
||||||
|
(defn take-u64 [x u64] u64 x)
|
||||||
|
(defn take-f64 [x f64] f64 x)
|
||||||
|
(defn take-f32 [x f32] f32 x)
|
||||||
|
|
||||||
|
;; Widening at a return position: the body is an i32 and the signature is i64.
|
||||||
|
(defn ret-widened [] i64 i32-neg)
|
||||||
|
|
||||||
|
;; Widening in a binary operator, both orders. The first is the direction
|
||||||
|
;; [expect] already served; the second is the one the join rule added.
|
||||||
|
(defn add-wide-first [] i64 (+ i64-big i32-one))
|
||||||
|
(defn add-narrow-first [] i64 (+ i32-one i64-big))
|
||||||
|
|
||||||
|
(defn main [args [string]] i32
|
||||||
|
;; ── integer to integer ──────────────────────────────────────────
|
||||||
|
(println (take-i64 i8-neg)) ;; -5
|
||||||
|
(println (take-i64 i8-pos)) ;; 127
|
||||||
|
(println (take-i64 i16-neg)) ;; -300
|
||||||
|
(println (take-i64 i32-all)) ;; -1
|
||||||
|
(println (take-i64 i32-neg)) ;; -2000000000
|
||||||
|
(println (take-i16 u8-max)) ;; 255
|
||||||
|
(println (take-i64 u8-max)) ;; 255
|
||||||
|
(println (take-i64 u16-max)) ;; 65535
|
||||||
|
(println (take-i64 u32-big)) ;; 4000000000
|
||||||
|
(println (take-i64 u32-max)) ;; 4294967295
|
||||||
|
(println (take-u64 u32-big)) ;; 4000000000
|
||||||
|
(println (take-u64 u8-max)) ;; 255
|
||||||
|
|
||||||
|
;; ── a widened return ────────────────────────────────────────────
|
||||||
|
(println (ret-widened)) ;; -2000000000
|
||||||
|
|
||||||
|
;; ── integer to float, exact only ────────────────────────────────
|
||||||
|
(println (take-f64 i32-neg)) ;; -2000000000.0
|
||||||
|
(println (take-f64 u32-max)) ;; 4294967295.0
|
||||||
|
(println (take-f64 i8-neg)) ;; -5.0
|
||||||
|
(println (take-f32 i16-neg)) ;; -300.0
|
||||||
|
(println (take-f32 u16-max)) ;; 65535.0
|
||||||
|
|
||||||
|
;; The printer answers %g, which rounds an f64 long before the bits it is
|
||||||
|
;; carrying run out, so the exactness the int-to-float boundary is chosen for
|
||||||
|
;; is asserted by subtraction rather than by reading the digits. Each of
|
||||||
|
;; these is the difference between the widened value and the number it is
|
||||||
|
;; supposed to be, and a conversion that lost anything answers something
|
||||||
|
;; other than the last unit.
|
||||||
|
(println (- (take-f64 u32-max) 4294967294.0)) ;; 1
|
||||||
|
(println (- (take-f64 i32-neg) -1999999999.0)) ;; -1
|
||||||
|
(println (- (take-f32 u16-max) 65534.0)) ;; 1
|
||||||
|
|
||||||
|
;; ── float to float ──────────────────────────────────────────────
|
||||||
|
(println (take-f64 f32-half)) ;; 0.5
|
||||||
|
|
||||||
|
;; ── the binary join, both operand orders ────────────────────────
|
||||||
|
(println (add-wide-first)) ;; 5000000001
|
||||||
|
(println (add-narrow-first)) ;; 5000000001
|
||||||
|
;; The narrower operand is the first one, and the sum is an i64 even though
|
||||||
|
;; nothing on this line is annotated.
|
||||||
|
(println (+ i32-neg i64-big)) ;; 3000000000
|
||||||
|
;; A comparison joins the same way, and the widened -1 must still be -1.
|
||||||
|
(println (< i32-all i64-big)) ;; true
|
||||||
|
;; min and max over two widths answer at the wider one.
|
||||||
|
(println (max i8-neg i16-neg)) ;; -5
|
||||||
|
(println (min i8-neg i32-neg)) ;; -2000000000
|
||||||
|
;; A count narrower than the value widens to it; the value's width decides.
|
||||||
|
(println (<< i64-big i8-pos)) ;; 0 -- masked to 127 mod 64 = 63
|
||||||
|
;; An expectation reaches the operands, so this adds at i64 rather than
|
||||||
|
;; wrapping at i32 and widening the sum afterwards.
|
||||||
|
(println (take-i64 (+ i32-neg i32-neg))) ;; -4000000000
|
||||||
|
0)
|
||||||
@ -542,6 +542,58 @@ let () =
|
|||||||
outputs "the rest of libm, both widths" "programs/math3.flan" math3_out;
|
outputs "the rest of libm, both widths" "programs/math3.flan" math3_out;
|
||||||
outputs ~opt:"-O0" "the rest of libm, both widths, -O0"
|
outputs ~opt:"-O0" "the rest of libm, both widths, -O0"
|
||||||
"programs/math3.flan" math3_out;
|
"programs/math3.flan" math3_out;
|
||||||
|
(* Implicit widening, FIX.org 2026-09-20. The type side of it needs no
|
||||||
|
program — a refusal that stopped happening is a compile that succeeds —
|
||||||
|
so what this asserts is the *bits*: every row is a value whose printed
|
||||||
|
form differs depending on which extension instruction the backend chose.
|
||||||
|
-5 as an i8 reaching an i64 prints 251 under a zero-extension; a u8 255
|
||||||
|
reaching an i16 prints -1 under a sign-extension; a u32 four billion
|
||||||
|
reaching an i64 prints a negative number under a sign-extension. The
|
||||||
|
three subtraction rows are the int-to-float boundary, asserted by
|
||||||
|
difference because %g rounds long before an f64's bits run out.
|
||||||
|
|
||||||
|
Run on both backends and on the unoptimised build, because the choice is
|
||||||
|
made three separate times: emit.ml picks sext/zext/sitofp/uitofp by the
|
||||||
|
source type's signedness, and x86.ml gets there by a load that extends
|
||||||
|
by the same rule and a cvtsi2sd on the register it left behind. *)
|
||||||
|
let widening_out =
|
||||||
|
"-5\n\
|
||||||
|
127\n\
|
||||||
|
-300\n\
|
||||||
|
-1\n\
|
||||||
|
-2000000000\n\
|
||||||
|
255\n\
|
||||||
|
255\n\
|
||||||
|
65535\n\
|
||||||
|
4000000000\n\
|
||||||
|
4294967295\n\
|
||||||
|
4000000000\n\
|
||||||
|
255\n\
|
||||||
|
-2000000000\n\
|
||||||
|
-2e+09\n\
|
||||||
|
4.29497e+09\n\
|
||||||
|
-5\n\
|
||||||
|
-300\n\
|
||||||
|
65535\n\
|
||||||
|
1\n\
|
||||||
|
-1\n\
|
||||||
|
1\n\
|
||||||
|
0.5\n\
|
||||||
|
5000000001\n\
|
||||||
|
5000000001\n\
|
||||||
|
3000000000\n\
|
||||||
|
true\n\
|
||||||
|
-5\n\
|
||||||
|
-2000000000\n\
|
||||||
|
0\n\
|
||||||
|
-4000000000\n"
|
||||||
|
in
|
||||||
|
outputs "implicit widening, and which extension it emits"
|
||||||
|
"programs/widening.flan" widening_out;
|
||||||
|
outputs ~opt:"-O0" "implicit widening, -O0" "programs/widening.flan"
|
||||||
|
widening_out;
|
||||||
|
outputs ~x86:true "implicit widening, --x86" "programs/widening.flan"
|
||||||
|
widening_out;
|
||||||
(* The clock and the environment. Every line of that program's output is
|
(* The clock and the environment. Every line of that program's output is
|
||||||
an invariant — a monotonicity, a date range, a sleep that did not
|
an invariant — a monotonicity, a date range, a sleep that did not
|
||||||
return early — and not a reading, because the same file is in the
|
return early — and not a reading, because the same file is in the
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user