A number or character literal bound by let or loop takes its type from its uses in the function
This commit is contained in:
parent
8e8015cb2d
commit
5177586848
3
TODO.org
3
TODO.org
@ -33,6 +33,9 @@ disagree are refused with a request for an annotation. Vector, map and text lite
|
||||
are dyn unless something typed wants them. A typed value is boxed where it goes into
|
||||
dyn, and a dyn unboxed (checked) where typed code needs it; typed beside dyn in an
|
||||
operator gives dyn. Dyn integers stay i64 and dyn floats f64.
|
||||
Local inference is in (check.ml [lit_session]). The f32 default and dyn text and vector
|
||||
literals wait on the author's answers to the phase-1 measurements; =FLAN_LIT=f32,dyn= in
|
||||
check.ml is the measuring switch, to be deleted with them.
|
||||
** DONE Dynamic-first, and the dyn half of the language
|
||||
CLOSED: [2026-09-20]
|
||||
An unannotated parameter or return is =dyn=: a NaN-boxed value over a mark-sweep
|
||||
|
||||
385
lib/check.ml
385
lib/check.ml
@ -70,6 +70,10 @@ type binding = {
|
||||
that the field is already in hand. [None] everywhere else, and a refusal
|
||||
with [None] says exactly what it said before. *)
|
||||
bwhat : string option;
|
||||
(* The literal a [let] or [loop] bound this name to, when its type is read
|
||||
off the uses ([lit_session]). The initialiser's node, by identity, is the
|
||||
key: two expansions of one macro are two nodes. *)
|
||||
blit : Ast.expr option;
|
||||
}
|
||||
|
||||
(* A class slot's type: what a value stored into it is checked against. A
|
||||
@ -725,11 +729,53 @@ type lentry =
|
||||
| Lrecur of (int * Types.t) list
|
||||
| Lbarrier of string
|
||||
|
||||
(* Local inference for a number or character literal bound by a [let] or a
|
||||
[loop]: [(let [t 0.0] ... (set t (+ t x)))] makes [t] x's type. The uses
|
||||
are read by checking the form once with the literal locals at their current
|
||||
guess and every hook below recording instead of refusing, then undoing that
|
||||
check; the guesses are solved, and the form is checked for real. A guess
|
||||
that moved is checked again, at most [lit_rounds] times, so a local fed by
|
||||
another settles. One session per function context, opened by its outermost
|
||||
such [let], so a lambda or a generic's copy is inferred on its own and a
|
||||
literal's type never depends on another function.
|
||||
|
||||
What a use says about the local:
|
||||
- [Up t]: the local flows into a [t] — a parameter, a return, a field, an
|
||||
index. The local has to widen into [t].
|
||||
- [Down t]: a [t] is [set] into it, or passed to [recur] for it. [t] has to
|
||||
widen into the local.
|
||||
- [Hint t]: an operator's other operand, which meets it at either.
|
||||
A [set] of one such local into another links the two, and a group of
|
||||
linked locals takes one type. *)
|
||||
type lit_con = Up | Down | Hint
|
||||
|
||||
type lit_session = {
|
||||
(* The type each literal local is checked at, by its initialiser's node. *)
|
||||
mutable decided : (Ast.expr * Types.t) list;
|
||||
(* On during the recording check and off for the real one. *)
|
||||
mutable recording : bool;
|
||||
mutable cons : (Ast.expr * (lit_con * Types.t * Loc.t)) list;
|
||||
mutable links : (Ast.expr * Ast.expr) list;
|
||||
(* Each literal local the recording check bound, with its name. *)
|
||||
mutable seen : (Ast.expr * string) list;
|
||||
}
|
||||
|
||||
(* Nonzero while any recording check runs: the refusal memos ([arm_failed],
|
||||
[if_failed], [truthy_failed]) are not written then, since a refusal made
|
||||
at a guessed type must not be replayed at the decided one. *)
|
||||
let lit_recording = ref 0
|
||||
|
||||
(* Set around the one check of an operator's operand that is a literal local,
|
||||
so its use is recorded as a [Hint] and not an [Up]. *)
|
||||
let lit_hint = ref false
|
||||
|
||||
(* Per-function state. Slots are never reused, so [slots] is also the frame
|
||||
size — the interpreter allocates one array of this length per call. *)
|
||||
type ctx = {
|
||||
env : env;
|
||||
ret : Types.t;
|
||||
(* The literal-inference session of this function, while one is open. *)
|
||||
mutable lits : lit_session option;
|
||||
mutable slots : int;
|
||||
(* The type of each slot, newest first. A backend needs it to size the
|
||||
frame — nothing else records it, since the IR refers to slots by index. *)
|
||||
@ -910,7 +956,7 @@ let render_ctx ctx (emit : Render.emitter) : Render.ctx =
|
||||
variables properly means emitting a [!DILexicalBlock] per [Let] and moving
|
||||
the [llvm.dbg.declare]s out of the entry block to the binding sites, which
|
||||
needs block structure this IR does not carry. *)
|
||||
let bind ctx ?what name bty ~assignable =
|
||||
let bind ctx ?what ?lit name bty ~assignable =
|
||||
let taken n = List.exists (fun s -> s = Some n) ctx.slot_names in
|
||||
let name' =
|
||||
if not (taken name) then name
|
||||
@ -924,7 +970,7 @@ let bind ctx ?what name bty ~assignable =
|
||||
let slot = fresh_slot ~name:name' ctx bty in
|
||||
(* [ctx.scope] keeps the *source* name: the suffix is a debug-info artifact
|
||||
and resolving [v] must still find the innermost binding. *)
|
||||
ctx.scope <- (name, { slot; bty; assignable; bwhat = what }) :: ctx.scope;
|
||||
ctx.scope <- (name, { slot; bty; assignable; bwhat = what; blit = lit }) :: ctx.scope;
|
||||
slot
|
||||
|
||||
let lookup ctx name = List.assoc_opt name ctx.scope
|
||||
@ -956,7 +1002,7 @@ let rec capture ctx loc name =
|
||||
a [let] inside the body restores what it displaced, and the copy's
|
||||
binding goes with it. One field, not two: the environment is keyed by the
|
||||
source name. *)
|
||||
| Some (outer, slot) -> Some { slot; bty = outer.bty; assignable = false; bwhat = None }
|
||||
| Some (outer, slot) -> Some { slot; bty = outer.bty; assignable = false; bwhat = None; blit = None }
|
||||
| None ->
|
||||
let from_parent () =
|
||||
(* Not a local of the body directly around this one, so ask whether that
|
||||
@ -977,7 +1023,7 @@ let rec capture ctx loc name =
|
||||
| Some _, Some (outer : binding) ->
|
||||
let slot = bind ctx name outer.bty ~assignable:false in
|
||||
ctx.caught <- ctx.caught @ [ (name, (outer, slot)) ];
|
||||
Some { slot; bty = outer.bty; assignable = false; bwhat = None }
|
||||
Some { slot; bty = outer.bty; assignable = false; bwhat = None; blit = None }
|
||||
| _ -> None
|
||||
|
||||
(* The one thing [capture] does not answer for. A captured name is a copy, so
|
||||
@ -997,7 +1043,7 @@ and peek_outer ctx name =
|
||||
if ctx.outer_what = None then None
|
||||
else
|
||||
match List.assoc_opt name ctx.caught with
|
||||
| Some ((b : binding), slot) -> Some { slot; bty = b.bty; assignable = false; bwhat = None }
|
||||
| Some ((b : binding), slot) -> Some { slot; bty = b.bty; assignable = false; bwhat = None; blit = None }
|
||||
| None ->
|
||||
match List.assoc_opt name ctx.outer with
|
||||
| Some b -> Some b
|
||||
@ -3585,6 +3631,114 @@ let restart_sig tys =
|
||||
let dyn_i64 = Types.Int Types.I64
|
||||
let dyn_f64 = Types.Float Types.F64
|
||||
|
||||
(* PROTOTYPE switch for measuring the literal rules; removed before merge. *)
|
||||
let lit_mode = try Sys.getenv "FLAN_LIT" with Not_found -> ""
|
||||
let lit_has m = List.mem m (String.split_on_char ',' lit_mode)
|
||||
let float_default () = if lit_has "f32" then Types.F32 else Types.F64
|
||||
|
||||
(* ── Literal locals ([lit_session]) ────────────────────────────────── *)
|
||||
|
||||
(* The literal a [let] or [loop] initialiser is, when its type is to be read
|
||||
off the uses: a number or a character, negated or not. A bool has one type
|
||||
and a wide literal one (u64), so neither has anything to infer. *)
|
||||
let lit_kind (e : Ast.expr) =
|
||||
match e.Ast.e with
|
||||
| Ast.Int _ -> Some `Int
|
||||
| Ast.Byte _ -> Some `Char
|
||||
| Ast.Float _ -> Some `Float
|
||||
| Ast.Call ({ Ast.e = Ast.Var "-"; _ }, [ { Ast.e = Ast.Int _; _ } ]) -> Some `Int
|
||||
| Ast.Call ({ Ast.e = Ast.Var "-"; _ }, [ { Ast.e = Ast.Float _; _ } ]) -> Some `Float
|
||||
| _ -> None
|
||||
|
||||
(* What the literal is with no use to say otherwise. *)
|
||||
let lit_default = function
|
||||
| `Int -> Types.Int Types.I32
|
||||
| `Char -> Types.Int Types.U8
|
||||
| `Float -> Types.Float (float_default ())
|
||||
|
||||
(* The types a use can give it: any number for an integer or a character,
|
||||
since an untyped integer constant is usable where a float is wanted, and
|
||||
only a float for a float. A type variable is admitted and left to
|
||||
[int_literal] to judge against its bound. Anything else — dyn, a struct —
|
||||
says nothing about the literal's type; the local keeps its guess and the
|
||||
use is checked as it always was. *)
|
||||
let lit_admits kind (t : Types.t) =
|
||||
match kind, t with
|
||||
| (`Int | `Char), (Types.Int _ | Types.Float _ | Types.Var _) -> true
|
||||
| `Float, (Types.Float _ | Types.Var _) -> true
|
||||
| _ -> false
|
||||
|
||||
let lit_rounds = 3
|
||||
|
||||
(* Every literal local the recording check bound, with the type the uses
|
||||
decide for it, and the first pair of uses that no one type satisfies. *)
|
||||
let lit_solve (s : lit_session) =
|
||||
let keys =
|
||||
List.fold_left
|
||||
(fun acc (k, n) -> if List.exists (fun (k', _) -> k' == k) acc then acc else (k, n) :: acc)
|
||||
[] s.seen
|
||||
in
|
||||
(* The linked group of [k]: a [set] of one literal local into another. *)
|
||||
let group k =
|
||||
let rec go seen = function
|
||||
| [] -> seen
|
||||
| k :: rest when List.memq k seen -> go seen rest
|
||||
| k :: rest ->
|
||||
let next =
|
||||
List.filter_map
|
||||
(fun (a, b) -> if a == k then Some b else if b == k then Some a else None)
|
||||
s.links
|
||||
in
|
||||
go (k :: seen) (next @ rest)
|
||||
in
|
||||
go [] [ k ]
|
||||
in
|
||||
let widens a b = Types.equal a b || Types.widens_to ~from:a ~into:b in
|
||||
List.map
|
||||
(fun (k, name) ->
|
||||
let members = List.filter (fun m -> List.exists (fun (k', _) -> k' == m) keys) (group k) in
|
||||
let kind =
|
||||
if List.exists (fun m -> lit_kind m = Some `Float) members then `Float
|
||||
else Option.value (lit_kind k) ~default:`Int
|
||||
in
|
||||
let cons =
|
||||
List.filter_map
|
||||
(fun (k', c) -> if List.memq k' members then Some c else None)
|
||||
s.cons
|
||||
|> List.filter (fun (_, t, _) -> lit_admits kind t)
|
||||
|> List.rev
|
||||
in
|
||||
let pick c = List.filter_map (fun (c', t, l) -> if c' = c then Some (t, l) else None) cons in
|
||||
let ups = pick Up and downs = pick Down and hints = pick Hint in
|
||||
let res =
|
||||
match ups with
|
||||
| (u0, l0) :: _ ->
|
||||
(match List.find_opt (fun (u, _) -> List.for_all (fun (u', _) -> widens u u') ups) ups with
|
||||
| None ->
|
||||
let (u1, l1) =
|
||||
List.find (fun (u, _) -> not (widens u u0 || widens u0 u)) ups
|
||||
in
|
||||
Error ((u0, l0), (u1, l1))
|
||||
| Some (c, lc) ->
|
||||
(match List.find_opt (fun (d, _) -> not (widens d c)) downs with
|
||||
| None -> Ok c
|
||||
| Some (d, ld) -> Error ((c, lc), (d, ld))))
|
||||
| [] ->
|
||||
(match downs @ hints with
|
||||
| [] -> Ok (lit_default kind)
|
||||
| (t0, l0) :: rest ->
|
||||
let rec fold (t, l) = function
|
||||
| [] -> Ok t
|
||||
| (t', l') :: rest ->
|
||||
(match Types.join t t' with
|
||||
| Some j -> fold ((j, if Types.equal j t then l else l')) rest
|
||||
| None -> Error ((t, l), (t', l')))
|
||||
in
|
||||
fold (t0, l0) rest)
|
||||
in
|
||||
(k, name, res))
|
||||
keys
|
||||
|
||||
(* Converting to whatever width the other side of the boundary wants, with a
|
||||
[Cast] and not a silent reinterpretation. The name is for the direction it
|
||||
was written for: runtime/flan_dyn.h boxes integers as [i64] and floats as
|
||||
@ -4763,7 +4917,7 @@ let with_recovery env ~on f =
|
||||
end
|
||||
|
||||
let invented_ctx env ret =
|
||||
{ env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
|
||||
{ env; ret; lits = None; slots = 0; slot_tys = []; slot_names = []; scope = [];
|
||||
defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
|
||||
in_defer = false; defer_ok = false; defer_block = "a nested form";
|
||||
owner = "<none>" }
|
||||
@ -5711,9 +5865,10 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
| Some other when other <> Types.Never ->
|
||||
Loc.failk literal_at_want loc "expected %s, found the float literal %g"
|
||||
(tyname loc other) x
|
||||
| _ -> Types.F64
|
||||
| _ -> float_default ()
|
||||
in
|
||||
mk loc (Types.Float k) (Tast.Float (x, k))
|
||||
| Ast.Str s when want = None && lit_has "dyn" -> box loc (mk loc Types.String (Tast.Str s))
|
||||
| Ast.Str s -> expect ctx loc ~want (mk loc Types.String (Tast.Str s))
|
||||
| Ast.Kw k ->
|
||||
(* Two keywords in one spelling, told apart by the expectation. Where an
|
||||
@ -5962,6 +6117,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
let v = check ctx ~want:Types.Dyn v in
|
||||
expect ctx loc ~want
|
||||
(rt loc Types.Unit "flan_dyn_slot_set" [ target; k; v; here loc ])
|
||||
| Ast.Set ((Ast.Pvar n as p), v) when lit_recorded ctx n <> None ->
|
||||
let key = Option.get (lit_recorded ctx n) in
|
||||
let p, pty = check_place ctx loc p in
|
||||
let v = lit_down ctx key pty v in
|
||||
expect ctx loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
|
||||
| Ast.Set (p, v) ->
|
||||
let p, pty = check_place ctx loc p in
|
||||
let v = check ctx ~want:pty v in
|
||||
@ -5984,6 +6144,8 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
fixed-array literal they always were. *)
|
||||
| Ast.Arr items when want = Some Types.Dyn ->
|
||||
dyn_vec ctx loc (map_lr (fun x -> check ctx ~want:Types.Dyn x) items)
|
||||
| Ast.Arr items when want = None && lit_has "dyn" ->
|
||||
dyn_vec ctx loc (map_lr (fun x -> check ctx ~want:Types.Dyn x) items)
|
||||
| Ast.Arr items -> check_arr ctx ~want loc items
|
||||
(* (array 4 rl/Vector2). Parse already assembled the whole array type, so
|
||||
there is nothing to infer: resolve it and hand back its all-bytes-zero
|
||||
@ -6338,6 +6500,16 @@ and var ctx ?(qualified = false) loc ~want name =
|
||||
defn to pass that" builtin_prefix name name builtin_prefix name
|
||||
| _ ->
|
||||
match lookup ctx name with
|
||||
(* A literal local while its uses are being recorded: the use is noted
|
||||
and read at the type it asks for, so the recording check goes on past
|
||||
a use its guess would have refused. That check is thrown away. *)
|
||||
| Some ({ blit = Some key; _ } as b)
|
||||
when (match ctx.lits, want with
|
||||
| Some s, Some t -> s.recording && lit_admits (Option.value (lit_kind key) ~default:`Int) t
|
||||
| _ -> false) ->
|
||||
let s = Option.get ctx.lits and t = Option.get want in
|
||||
s.cons <- (key, ((if !lit_hint then Hint else Up), t, loc)) :: s.cons;
|
||||
mk loc t (Tast.Local b.slot)
|
||||
| Some b ->
|
||||
expect ctx loc ~want (mk loc b.bty (Tast.Local b.slot))
|
||||
(* A local of the enclosing function, in a body that was lifted out of it:
|
||||
@ -7050,12 +7222,140 @@ and defer_counter_zero slot loc =
|
||||
(* [defer_ok] says whether *this* let has the function's extent. If it does, so
|
||||
does every form in its body, including a nested let — which is why the flag
|
||||
is handed to the body rather than consumed here. *)
|
||||
(* The literal local [n] names, while its uses are being recorded. *)
|
||||
and lit_recorded ctx n =
|
||||
match ctx.lits, lookup ctx n with
|
||||
| Some s, Some { blit = Some key; _ } when s.recording -> Some key
|
||||
| _ -> None
|
||||
|
||||
(* [v] stored into the literal local [key] (a [set] or a [recur]), while
|
||||
recording: checked on its own terms, so its type is what it brings rather
|
||||
than the guess. Another literal local links the two; a float literal says
|
||||
only that it is a float. *)
|
||||
and lit_down ctx key pty (v : Ast.expr) =
|
||||
let s = Option.get ctx.lits in
|
||||
let other =
|
||||
match v.Ast.e with
|
||||
| Ast.Var m -> (match lookup ctx m with Some { blit = Some k; _ } -> Some k | _ -> None)
|
||||
| _ -> None
|
||||
in
|
||||
match other with
|
||||
| Some k -> s.links <- (key, k) :: s.links; check ctx v
|
||||
| None ->
|
||||
match lit_kind v with
|
||||
| Some `Float ->
|
||||
s.cons <- (key, (Hint, Types.Float (float_default ()), v.Ast.loc)) :: s.cons;
|
||||
check ctx v
|
||||
(* An integer literal fits wherever its value does; one past i32 says
|
||||
the local is at least an i64. *)
|
||||
| Some _ ->
|
||||
(match v.Ast.e with
|
||||
| Ast.Int n when Int64.compare n (Int64.of_int32 Int32.max_int) > 0
|
||||
|| Int64.compare n (Int64.of_int32 Int32.min_int) < 0 ->
|
||||
s.cons <- (key, (Hint, Types.Int Types.I64, v.Ast.loc)) :: s.cons;
|
||||
check ctx ~want:(Types.Int Types.I64) v
|
||||
| _ -> check ctx ~want:pty v)
|
||||
| None ->
|
||||
(match trial ctx (fun () -> check ctx v) with
|
||||
| Ok e ->
|
||||
s.cons <- (key, (Down, e.Tast.ty, v.Ast.loc)) :: s.cons;
|
||||
e
|
||||
| Error _ -> check ctx ~want:pty v)
|
||||
|
||||
(* The type a literal initialiser is checked at while a session is open —
|
||||
its current guess, or the decision — noting it as seen while recording.
|
||||
[None] for anything that is not a literal, or with no session open. *)
|
||||
and lit_local ctx name (e : Ast.expr) =
|
||||
match ctx.lits, lit_kind e with
|
||||
| Some s, Some kind ->
|
||||
if s.recording then s.seen <- (e, name) :: s.seen;
|
||||
Some (match List.assq_opt e s.decided with Some t -> t | None -> lit_default kind)
|
||||
| _ -> None
|
||||
|
||||
(* [run] is a [let] or a [loop] with some of [inits] literals, and the
|
||||
outermost such form of this function: the session opens here. See
|
||||
[lit_session]. *)
|
||||
and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
|
||||
fun ctx loc inits run ->
|
||||
if ctx.lits <> None || not (List.exists (fun e -> lit_kind e <> None) inits)
|
||||
then run ()
|
||||
else begin
|
||||
let s = { decided = []; recording = false; cons = []; links = []; seen = [] } in
|
||||
ctx.lits <- Some s;
|
||||
Fun.protect ~finally:(fun () -> ctx.lits <- None) @@ fun () ->
|
||||
let undo = Loc.diag ~kind:"check/lit-undo" loc "undone" in
|
||||
let rec round n =
|
||||
s.cons <- []; s.links <- []; s.seen <- [];
|
||||
s.recording <- true;
|
||||
incr lit_recording;
|
||||
Fun.protect
|
||||
~finally:(fun () -> decr lit_recording; s.recording <- false)
|
||||
(fun () -> ignore (trial ctx (fun () -> ignore (run ()); raise (Loc.Error undo))));
|
||||
let solved = lit_solve s in
|
||||
let guess k =
|
||||
match List.assq_opt k s.decided with
|
||||
| Some t -> t
|
||||
| None -> lit_default (Option.value (lit_kind k) ~default:`Int)
|
||||
in
|
||||
let decided =
|
||||
List.map (fun (k, _, r) -> (k, match r with Ok t -> t | Error _ -> guess k)) solved
|
||||
in
|
||||
let moved = List.exists (fun (k, t) -> not (Types.equal t (guess k))) decided in
|
||||
s.decided <- decided;
|
||||
if moved && n < lit_rounds then round (n + 1)
|
||||
else
|
||||
match List.find_opt (fun (_, _, r) -> Result.is_error r) solved with
|
||||
| Some (k, name, Error ((t1, l1), (t2, l2))) -> lit_conflict k name t1 l1 t2 l2
|
||||
| _ -> ()
|
||||
in
|
||||
round 1;
|
||||
if lit_has "log" then
|
||||
List.iter
|
||||
(fun (k, t) ->
|
||||
let d = lit_default (Option.value (lit_kind k) ~default:`Int) in
|
||||
if not (Types.equal t d) then
|
||||
Printf.eprintf "LITINF %s:%d:%d %s -> %s\n" k.Ast.loc.Loc.file
|
||||
k.Ast.loc.Loc.line k.Ast.loc.Loc.col (tyname loc d) (tyname loc t))
|
||||
s.decided;
|
||||
run ()
|
||||
end
|
||||
|
||||
(* Two uses of a literal local that no one type satisfies. *)
|
||||
and lit_conflict (k : Ast.expr) name t1 l1 t2 l2 =
|
||||
let lit =
|
||||
match k.Ast.e with
|
||||
| Ast.Int n -> Int64.to_string n
|
||||
| Ast.Float x -> Printf.sprintf "%g" x
|
||||
| Ast.Byte b -> Printf.sprintf "\\%c" (Char.chr b)
|
||||
| Ast.Call (_, [ { Ast.e = Ast.Int n; _ } ]) -> Int64.to_string (Int64.neg n)
|
||||
| Ast.Call (_, [ { Ast.e = Ast.Float x; _ } ]) -> Printf.sprintf "%g" (-.x)
|
||||
| _ -> "..."
|
||||
in
|
||||
let lit = if String.length lit > 0 && lit.[0] <> '-' && not (String.contains lit '.') && lit_kind k = Some `Float then lit ^ ".0" else lit in
|
||||
let fix =
|
||||
if fln_source k.Ast.loc then Printf.sprintf "let %s: %s = %s" name (tyname l1 t1) lit
|
||||
else Printf.sprintf "(%s %s)" (tyname l1 t1) lit
|
||||
in
|
||||
Loc.failk "check/literal-uses" k.Ast.loc
|
||||
~notes:[ Loc.note l1 (Printf.sprintf "%s is used as %s here" name (tyname l1 t1));
|
||||
Loc.note l2 (Printf.sprintf "and as %s here" (tyname l2 t2)) ]
|
||||
"%s is used as %s and as %s, and %s can have only one type. Write the \
|
||||
one it should have: %s"
|
||||
name (tyname l1 t1) (tyname l2 t2) lit fix
|
||||
|
||||
and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
|
||||
with_lits ctx loc
|
||||
(List.filter_map
|
||||
(fun (b : Ast.binding) -> if b.Ast.bty = None then Some b.Ast.bval else None)
|
||||
bs)
|
||||
@@ fun () ->
|
||||
scoped ctx (fun () ->
|
||||
let bs =
|
||||
map_lr
|
||||
(fun (b : Ast.binding) ->
|
||||
let want = Option.map (resolve ctx.env) b.Ast.bty in
|
||||
let lit = if b.Ast.bty = None then lit_local ctx b.Ast.bname b.Ast.bval else None in
|
||||
let want = match lit with Some t -> Some t | None -> want in
|
||||
let v = check ctx ?want b.Ast.bval in
|
||||
(match v.Tast.ty with
|
||||
(* A refused initialiser, already reported: the name is bound to
|
||||
@ -7066,7 +7366,10 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
|
||||
b.Ast.bname (tyname loc v.Tast.ty)
|
||||
| _ -> ());
|
||||
(* Locals are assignable places; parameters are not. *)
|
||||
let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
|
||||
let slot =
|
||||
bind ctx b.Ast.bname v.Tast.ty ~assignable:true
|
||||
?lit:(Option.map (fun _ -> b.Ast.bval) lit)
|
||||
in
|
||||
(slot, v))
|
||||
bs
|
||||
in
|
||||
@ -7281,6 +7584,7 @@ and check_dotimes ctx ~want loc label name (b : Ast.bounds) body =
|
||||
below and every [continue] a [recur] mints count from the same stack [emit]
|
||||
indexes. *)
|
||||
and check_loop ctx ?want loc bs body =
|
||||
with_lits ctx loc (List.map snd bs) @@ fun () ->
|
||||
scoped ctx (fun () ->
|
||||
(* Each initial value is evaluated once, before the loop, exactly as a
|
||||
[let]'s is and as [dotimes]'s bound is — and bound before the next is
|
||||
@ -7288,8 +7592,9 @@ and check_loop ctx ?want loc bs body =
|
||||
name. *)
|
||||
let binds =
|
||||
map_lr
|
||||
(fun (n, v) ->
|
||||
let v = check ctx v in
|
||||
(fun (n, v0) ->
|
||||
let lit = lit_local ctx n v0 in
|
||||
let v = check ctx ?want:lit v0 in
|
||||
(match v.Tast.ty with
|
||||
(* A refused initialiser, already reported: the name is bound to
|
||||
the poison so that what follows is still checked. *)
|
||||
@ -7298,7 +7603,8 @@ and check_loop ctx ?want loc bs body =
|
||||
fail v.Tast.loc "%s would be bound to %s, which is not a value" n
|
||||
(tyname loc v.Tast.ty)
|
||||
| _ -> ());
|
||||
(bind ctx n v.Tast.ty ~assignable:true, v))
|
||||
(bind ctx n v.Tast.ty ~assignable:true
|
||||
?lit:(Option.map (fun _ -> v0) lit), v))
|
||||
bs
|
||||
in
|
||||
let names = List.map (fun (slot, v) -> (slot, v.Tast.ty)) binds in
|
||||
@ -7371,7 +7677,18 @@ and check_recur ctx ~tail loc args =
|
||||
if want <> got then
|
||||
fail loc "this loop binds %d name%s and this recur passes %d" want
|
||||
(if want = 1 then "" else "s") got;
|
||||
let vals = List.map2 (fun a (_, ty) -> check ctx ~want:ty a) args names in
|
||||
let vals =
|
||||
List.map2
|
||||
(fun a (slot, ty) ->
|
||||
match
|
||||
List.find_opt (fun (_, (b : binding)) -> b.slot = slot) ctx.scope
|
||||
with
|
||||
| Some (_, { blit = Some key; _ })
|
||||
when (match ctx.lits with Some s -> s.recording | None -> false) ->
|
||||
lit_down ctx key ty a
|
||||
| _ -> check ctx ~want:ty a)
|
||||
args names
|
||||
in
|
||||
(* Every name is rebound at once. The new values go into temporaries first,
|
||||
so that (recur y x) swaps rather than writing y over x and then reading it
|
||||
back — the same reason Clojure's recur is simultaneous. *)
|
||||
@ -7486,7 +7803,7 @@ and check_truthy ctx c =
|
||||
(fun () ->
|
||||
try check_truthy_once ctx c
|
||||
with Loc.Error d as ex ->
|
||||
truthy_failed := (c, scope, ctx.ret, d) :: !truthy_failed;
|
||||
if !lit_recording = 0 then truthy_failed := (c, scope, ctx.ret, d) :: !truthy_failed;
|
||||
raise ex)
|
||||
|
||||
and check_truthy_once ctx c =
|
||||
@ -7564,7 +7881,7 @@ and check_if ctx ?(tail = false) ?want loc c t e =
|
||||
(fun () ->
|
||||
try check_if_once ctx ~tail ?want loc c t e
|
||||
with Loc.Error d as ex ->
|
||||
Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d);
|
||||
if !lit_recording = 0 then Hashtbl.add if_failed c.Ast.loc (c, (scope, ctx.ret), want, d);
|
||||
raise ex)
|
||||
|
||||
and check_if_once ctx ~tail ?want loc c t e =
|
||||
@ -7653,7 +7970,7 @@ and check_if_once ctx ~tail ?want loc c t e =
|
||||
with
|
||||
| Ok v -> Ok v
|
||||
| Error d ->
|
||||
Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d);
|
||||
if !lit_recording = 0 then Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d);
|
||||
Error d
|
||||
in
|
||||
let meet v =
|
||||
@ -7843,7 +8160,7 @@ and generic_ctor ctx ~want loc name given =
|
||||
(* A literal's own type, the one it has with nothing expected of it. *)
|
||||
let literal_type (a : Ast.expr) =
|
||||
match a.Ast.e with
|
||||
| Ast.Float _ -> Types.Float Types.F64
|
||||
| Ast.Float _ -> Types.Float (float_default ())
|
||||
| Ast.UInt _ -> Types.Int Types.U64
|
||||
| Ast.Byte _ -> Types.Int Types.U8
|
||||
| _ -> Types.Int Types.I32
|
||||
@ -9241,7 +9558,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
|
||||
(match trial ctx (at (Some w)) with
|
||||
| Ok b -> Ok b
|
||||
| Error d ->
|
||||
Hashtbl.add arm_failed head.Ast.loc
|
||||
if !lit_recording = 0 then Hashtbl.add arm_failed head.Ast.loc
|
||||
(head, (ctx.scope, ctx.ret), w, d);
|
||||
Error d)
|
||||
in
|
||||
@ -14144,7 +14461,7 @@ and trial ctx f =
|
||||
Only [Loc.Error] is caught. A timeout or a stack overflow is not a
|
||||
refusal to reconsider, and silently continuing past one would turn a
|
||||
resource failure into a wrong answer. *)
|
||||
let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
|
||||
let[@warning "+9"] { env = _; ret = _; lits = _; slots; slot_tys; slot_names; scope;
|
||||
defers; defer_slot; defer_ok; defer_block; outer = _;
|
||||
outer_what; caught; place_ok; envslot; parent = _;
|
||||
in_frames; loops; tail; in_defer;
|
||||
@ -14207,7 +14524,7 @@ and trial_at ctx (y : Ast.expr) (w : Types.t) =
|
||||
(match trial ctx (fun () -> check ctx ~want:w y) with
|
||||
| Ok b -> Ok b
|
||||
| Error d ->
|
||||
Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
|
||||
if !lit_recording = 0 then Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d);
|
||||
Error d)
|
||||
|
||||
and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
|
||||
@ -14227,7 +14544,35 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
|
||||
let needs_want (f : Ast.expr) =
|
||||
is_literal f || (match f.Ast.e with Ast.Kw _ -> true | _ -> false)
|
||||
in
|
||||
if y_decides then begin
|
||||
(* While a literal local's uses are recorded, the operand beside it
|
||||
decides and the local is recorded as meeting it ([lit_session]). *)
|
||||
let lv (f : Ast.expr) =
|
||||
match f.Ast.e with Ast.Var n -> lit_recorded ctx n <> None | _ -> false
|
||||
in
|
||||
let hinted f =
|
||||
lit_hint := true;
|
||||
Fun.protect ~finally:(fun () -> lit_hint := false) f
|
||||
in
|
||||
let float_lit (f : Ast.expr) = lit_kind f = Some `Float in
|
||||
if lv x && float_lit y then begin
|
||||
let a = hinted (fun () -> check ctx ~want:(Types.Float (float_default ())) x) in
|
||||
a, check ctx ~want:a.Tast.ty y
|
||||
end
|
||||
else if lv y && float_lit x then begin
|
||||
let b = hinted (fun () -> check ctx ~want:(Types.Float (float_default ())) y) in
|
||||
check ctx ~want:b.Tast.ty x, b
|
||||
end
|
||||
else if lv x && not (lv y) && not (needs_want y) then begin
|
||||
let b = check ctx ?want y in
|
||||
let a = hinted (fun () -> check ctx ~want:b.Tast.ty x) in
|
||||
a, b
|
||||
end
|
||||
else if lv y && not (lv x) && not (needs_want x) then begin
|
||||
let a = check ctx ?want x in
|
||||
let b = hinted (fun () -> check ctx ~want:a.Tast.ty y) in
|
||||
a, b
|
||||
end
|
||||
else if y_decides then begin
|
||||
let b = check ctx ?want y in
|
||||
let a = check ctx ~want:b.Tast.ty x in
|
||||
a, b
|
||||
|
||||
59
test/programs/literal-locals.flan
Normal file
59
test/programs/literal-locals.flan
Normal file
@ -0,0 +1,59 @@
|
||||
;;;; A number literal bound by let or loop takes its type from its uses in
|
||||
;;;; the function. Each line's expected output is beside it.
|
||||
|
||||
;; A set of an i64 sum makes the accumulator an i64.
|
||||
(defn total [xs [i64]] i64
|
||||
(let [t 0]
|
||||
(dotimes [i (length xs)]
|
||||
(set t (+ t (at xs i))))
|
||||
t))
|
||||
|
||||
;; The operand beside it: an f64 accumulator from a float literal.
|
||||
(defn mean [xs [f64]] f64
|
||||
(let [s 0.0]
|
||||
(dotimes [i (length xs)]
|
||||
(set s (+ s (at xs i))))
|
||||
(/ s (f64 (length xs)))))
|
||||
|
||||
;; A counter compared with an i64 bound counts past i32.
|
||||
(defn count-to [n i64] i64
|
||||
(let [i 0]
|
||||
(while (< i n)
|
||||
(set i (+ i 1000000000)))
|
||||
i))
|
||||
|
||||
;; A set of one literal local into another links them: b holds a value past
|
||||
;; i32, so a is an i64 too.
|
||||
(defn linked [] i64
|
||||
(let [a 0 b 0]
|
||||
(set b 3000000000)
|
||||
(set a b)
|
||||
a))
|
||||
|
||||
;; recur rebinds a loop's names the way set does.
|
||||
(defn sum-to [n i64] i64
|
||||
(loop [i 0 acc 0]
|
||||
(if (< i n) (recur (+ i 1) (+ acc 1000000000)) acc)))
|
||||
|
||||
;; Inside a generic body the literal takes the type variable.
|
||||
(defn sum-of [xs [$t]] $t {:where (numeric? $t)}
|
||||
(let [acc 0]
|
||||
(dotimes [i (length xs)]
|
||||
(set acc (+ acc (at xs i))))
|
||||
acc))
|
||||
|
||||
(defn main [] i32
|
||||
(let [xs (the [3 i64] [3000000000 4 5])
|
||||
fs (the [2 f64] [0.5 0.25])
|
||||
gs (the [2 u8] [200 50])]
|
||||
(println (total (slice xs 0 3))) ; 3000000009
|
||||
(println (mean (slice fs 0 2))) ; 0.375
|
||||
(println (count-to 5000000000)) ; 5000000000
|
||||
(println (linked)) ; 3000000000
|
||||
(println (sum-to 3)) ; 3000000000
|
||||
(println (sum-of (slice xs 0 3))) ; 3000000009
|
||||
(println (sum-of (slice fs 0 2)))) ; 0.75
|
||||
;; Nothing says otherwise: an i32 and an f64.
|
||||
(let [n 7 f 1.5]
|
||||
(println n f)) ; 7 1.5
|
||||
0)
|
||||
@ -389,6 +389,14 @@ let () =
|
||||
outputs "value semantics" "programs/values.flan" values_out;
|
||||
outputs "machine surface" "programs/machine.flan" machine_out;
|
||||
outputs "unit main exits 0" "programs/unit-main.flan" "ok\n";
|
||||
let literal_locals_out =
|
||||
"3000000009\n0.375\n5000000000\n3000000000\n3000000000\n3000000009\n\
|
||||
0.75\n7 1.5\n"
|
||||
in
|
||||
outputs "literal locals take their uses' type" "programs/literal-locals.flan"
|
||||
literal_locals_out;
|
||||
outputs ~x86:true "literal locals take their uses' type, --x86"
|
||||
"programs/literal-locals.flan" literal_locals_out;
|
||||
(* Comparisons over three operands and more. The lines that carry the
|
||||
whole claim are the tag transcripts: [abc -> false] is a chain whose
|
||||
*first* link already decided the answer and whose middle operand —
|
||||
|
||||
@ -1086,6 +1086,21 @@ let () =
|
||||
two [infers] above still hold — and this is the position that had no way
|
||||
to say it. *)
|
||||
infers "array constructor" "(array 4 f32)" "[4 f32]";
|
||||
(* A literal bound by a let takes its type from its uses in the function,
|
||||
and two uses no one type satisfies are refused with the annotation. *)
|
||||
accepts "a literal local takes the type set into it"
|
||||
"(defn f [x i64] i64 (let [t 0] (set t (+ t x)) t))";
|
||||
accepts "a literal local takes an operand's type"
|
||||
"(defn f [x f64] f64 (let [s 0.0] (set s (+ s x)) s))";
|
||||
accepts "recur rebinds a literal local at the type it brings"
|
||||
"(defn f [n i64] i64 (loop [i 0 acc 0] (if (< i n) (recur (+ i 1) (+ acc n)) acc)))";
|
||||
accepts "a set links two literal locals"
|
||||
"(defn f [] i64 (let [a 0 b 0] (set b 3000000000) (set a b) a))";
|
||||
rejects_check "two uses of a literal local disagree"
|
||||
~needle:"x is used as u32 and as i32, and 0 can have only one type. \
|
||||
Write the one it should have: (u32 0)"
|
||||
"(defn u [x u32] u32 x) (defn i [x i32] i32 x) \
|
||||
(defn f [] i32 (let [x 0] (u x) (i x)) 0)";
|
||||
infers "array of a struct" "(array 2 i32)" "[2 i32]";
|
||||
infers "array of an array" "(array 2 [3 u8])" "[2 [3 u8]]";
|
||||
(* (array-fill [r c] v): the same type at any rank, with the element type
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user