JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Literal locals fed through do, let and if arms share one type without extra rounds, a chain past the rounds names the local to annotate, a restart's conversion fix shows the argument as written, and a name's lookup is answered from the last one under the same scope

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-26 11:14:09 +07:00
parent a546bde112
commit c7fb0e5422
6 changed files with 143 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

121
lib/check.ml
View File

@ -1020,7 +1020,21 @@ let bind ctx ?what ?lit name bty ~assignable =
ctx.scope <- (name, { slot; bty; assignable; bwhat = what; blit = lit }) :: ctx.scope;
slot
let lookup ctx name = List.assoc_opt name ctx.scope
(* The last answer for each name, with the scope it was read from. A body is
checked under one scope for long stretches and names the same local
several times per form, so compared by identity this answers most
lookups without walking a scope that, in a long [let], holds thousands of
names. *)
let lookup_cache : (string, (string * binding) list * binding option) Hashtbl.t =
Hashtbl.create 64
let lookup ctx name =
match Hashtbl.find_opt lookup_cache name with
| Some (sc, r) when sc == ctx.scope -> r
| _ ->
let r = List.assoc_opt name ctx.scope in
Hashtbl.replace lookup_cache name (ctx.scope, r);
r
(* Capture, spec-memory.md's case 2: a body lifted into a function of its own —
an [fn] literal or a handler clause — naming a local of the function it was
@ -6089,11 +6103,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
integer type, since the real one is answered again per copy. A local of
the same name shadows it. *)
| Ast.Var name
when (not (List.mem_assoc name ctx.scope))
&& (List.mem name ctx.env.lenvars
|| (match List.assoc_opt name ctx.env.subst with
| Some (Types.Len _) -> true
| _ -> false)) ->
when (List.mem name ctx.env.lenvars
|| (match List.assoc_opt name ctx.env.subst with
| Some (Types.Len _) -> true
| _ -> false))
&& lookup ctx name = None ->
let n =
match List.assoc_opt name ctx.env.subst with
| Some (Types.Len n) -> n
@ -6425,7 +6439,16 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
let t = Printf.sprintf "%g" x in
if String.exists (fun c -> c = '.' || c = 'e' || c = 'n' || c = 'i') t
then t else t ^ ".0"
| _ -> spell_arg "x" a
| _ ->
(* The argument as written, when it is on one line of a file the
checker can read; otherwise an ellipsis. *)
let l = a.Ast.loc in
match Loc.source_line l with
| Some line
when l.Loc.macro = None && l.Loc.eline = l.Loc.line && l.Loc.col >= 1
&& l.Loc.ecol > l.Loc.col && l.Loc.ecol - 1 <= String.length line ->
String.sub line (l.Loc.col - 1) (l.Loc.ecol - l.Loc.col)
| _ -> spell_arg "\u{2026}" a
in
String.concat "\x1f"
(sg :: (if fln_source loc then "i" else "p") :: List.map spell written)
@ -7420,19 +7443,37 @@ and lit_recorded ctx n =
locals are merged with whatever [v] is stored into and the others are
what it brings. *)
and lit_parts ctx (v : Ast.expr) =
let rec go (v : Ast.expr) (vars, others) =
(* [env]: names a [let] inside [v] binds, with what they were bound to, so
(let [t a0] t) passes a0 through as (do a0) and an if's arms do. *)
let rec go env (v : Ast.expr) (vars, others) =
match v.Ast.e with
| Ast.Var n ->
(match lookup ctx n with
| Some { blit = Some k; _ } when lit_kind k <> Some `Box -> (k :: vars, others)
| _ -> (vars, v :: others))
(match List.assoc_opt n env with
| Some (Some (vs, os)) -> (vs @ vars, os @ others)
| Some None -> (vars, v :: others)
| None ->
match lookup ctx n with
| Some { blit = Some k; _ } when lit_kind k <> Some `Box -> (k :: vars, others)
| _ -> (vars, v :: others))
| Ast.Int _ | Ast.Float _ | Ast.Byte _ -> (vars, others)
| Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%" | "min" | "max"); _ }, args)
when args <> [] ->
List.fold_left (fun acc a -> go a acc) (vars, others) args
List.fold_left (fun acc a -> go env a acc) (vars, others) args
| Ast.Do (_ :: _ as xs) -> go env (List.nth xs (List.length xs - 1)) (vars, others)
| Ast.Let (bs, (_ :: _ as xs)) ->
let env =
List.fold_left
(fun env (b : Ast.binding) ->
(b.Ast.bname,
if b.Ast.bty = None then Some (go env b.Ast.bval ([], [])) else None)
:: env)
env bs
in
go env (List.nth xs (List.length xs - 1)) (vars, others)
| Ast.If (_, t, Some e) -> go env e (go env t (vars, others))
| _ -> (vars, v :: others)
in
go v ([], [])
go [] v ([], [])
(* A float literal, or an integer one past i32, anywhere in [v]'s arithmetic. *)
and lit_wide_literals (v : Ast.expr) =
@ -7528,22 +7569,23 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
if !lit_depth = 0 then Phys.reset lit_memo)
@@ fun () ->
let unsettled = Loc.diag ~kind:"check/lit-unsettled" loc "unsettled" in
(* The decisions the uses recorded so far make, and whether any moved. *)
(* The decisions the uses recorded so far make, written into
[s.decided], and the locals whose decision moved. *)
let settle () =
let solved = lit_solve s in
let moved = ref false in
let moved = ref [] in
List.iter
(fun (k, _, r) ->
(fun (k, name, r) ->
match r with
| Ok t ->
let kind = Option.value (lit_kind k) ~default:`Int in
if not (Types.equal t (lit_guess ~subst:ctx.env.subst s k kind)) then begin
moved := true;
moved := (k, name, t) :: !moved;
Phys.replace s.decided k t
end
| Error _ -> ())
solved;
(solved, !moved)
(solved, List.rev !moved)
in
let conflict solved =
List.find_map
@ -7567,6 +7609,9 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
incr lit_recording;
(* A ref, because [trial] is monomorphic inside this recursive group. *)
let answer = ref None in
(* What the settle inside the trial found, which has already written
its decisions: settling again outside would see nothing move. *)
let settled = ref None in
let outcome =
Fun.protect
~finally:(fun () -> decr lit_recording; s.recording <- false)
@ -7574,8 +7619,9 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
trial ctx (fun () ->
let r = run () in
let solved, moved = settle () in
settled := Some (solved, moved);
(* The guesses held: this check is the answer. *)
if moved || s.dirty || conflict solved <> None then
if moved <> [] || s.dirty || conflict solved <> None then
raise (Loc.Error unsettled);
answer := Some r;
poison loc))
@ -7583,11 +7629,19 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
match outcome, !answer with
| Ok _, Some r -> log (); remember (); r
| _ ->
let solved, moved = settle () in
let solved, moved =
match !settled with Some sm -> sm | None -> settle ()
in
(match conflict solved with
| Some (k, name, ((t1, l1), (t2, l2))) -> lit_conflict k name t1 l1 t2 l2
| None -> ());
if moved && n < lit_rounds then round (n + 1)
if moved <> [] && n < lit_rounds then round (n + 1)
else if moved <> [] then begin
(* Still moving: a local fed through more calls than the rounds
follow. It is the local that needs its type written. *)
let k, name, t = List.hd moved in
lit_unsettled k name t
end
else begin
(* Nothing left to learn: checked for real, so a refusal is the
ordinary one and a whole-file check goes on past it. *)
@ -7599,6 +7653,31 @@ and with_lits : 'a. ctx -> Loc.t -> Ast.expr list -> (unit -> 'a) -> 'a =
round 1
end
(* A literal local whose uses kept changing its type past [lit_rounds]. *)
and lit_unsettled (k : Ast.expr) name t =
let lit = lit_spelling k in
let fix =
if fln_source k.Ast.loc then Printf.sprintf "let %s: %s = %s" name (tyname k.Ast.loc t) lit
else Printf.sprintf "(%s %s)" (tyname k.Ast.loc t) lit
in
Loc.failk "check/literal-unsettled" k.Ast.loc
"the type of %s depends on too long a chain of the values stored into it \
to be read off them. Write the type it should have: %s"
name fix
and lit_spelling (k : Ast.expr) =
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 whole = lit <> "" && String.for_all (fun c -> (c >= '0' && c <= '9') || c = '-') lit in
if whole && lit_kind k = Some `Float then lit ^ ".0" else lit
(* Two uses of a literal local that no one type satisfies. *)
and lit_conflict (k : Ast.expr) name t1 l1 t2 l2 =
let lit =

8
runtime/flan_rt.c
View File

@ -1193,10 +1193,14 @@ _Noreturn void flan_restart_args_fail(const uint8_t *loc, int64_t loclen,
if (wrote < 0 || (size_t)wrote >= sizeof fix - used) { ok = 0; break; }
used += (size_t)wrote;
}
/* An argument the compiler could not spell is an ellipsis, and a fix with
* a hole in it is a conversion to make, not code to paste. */
int holed = strstr(fix, "\xe2\x80\xa6") != NULL;
if (ok && used > 0)
flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s. Write %s",
flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s. %s %s",
(int)namelen, (const char *)name, (int)wantlen, (const char *)want,
(int)plen[0], (const char *)part[0], fix);
(int)plen[0], (const char *)part[0],
holed ? "Convert the argument with" : "Write", fix);
else
flan_say(loc, loclen, "restart %.*s takes %.*s, given %.*s", (int)namelen,
(const char *)name, (int)wantlen, (const char *)want, (int)plen[0],

10
test/programs/literal-locals.flan
View File

@ -30,10 +30,14 @@
(set a b)
a))
;; recur rebinds a loop's names the way set does.
;; Two locals fed from each other: i is counted against an i64, and acc
;; sums a literal past i32.
(defn sum-to [n i64] i64
(loop [i 0 acc 0]
(if (< i n) (recur (+ i 1) (+ acc 1000000000)) acc)))
(let [i 0 acc 0]
(while (< i n)
(set acc (+ acc 1000000000))
(set i (+ i 1)))
acc))
;; Inside a generic body the literal takes the type variable.
(defn sum-of [xs [$t]] $t {:where (numeric? $t)}

5
test/programs/restarts.flan
View File

@ -106,6 +106,10 @@
(handler-bind [(AssetMissing [c] (let [big (i64 7)] (invoke-restart 'use-value big)))]
(supplied n)))
(defn doubled [n i32] i32
(handler-bind [(AssetMissing [c] (let [big (i64 7)] (invoke-restart 'use-value (* big 2))))]
(supplied n)))
(defn main [args [str]] i32
;; One argument selects a trap; none runs the table's case.
(if (> (length args) 1)
@ -116,6 +120,7 @@
(= k 3) (print (overfull 92))
(= k 4) (print (mislaid 93))
(= k 5) (print (widened 94))
(= k 6) (print (doubled 95))
:else (println "?"))
(return 0)))

2
test/test_acceptance.ml
View File

@ -1402,6 +1402,8 @@ let () =
"restart use-value takes (str), given (i32)";
refuses "a number of another type is refused with its conversion" "5"
"restart use-value takes (i32), given (i64). Write (i32 big)";
refuses "and the argument as it was written when it is an expression" "6"
"restart use-value takes (i32), given (i64). Write (i32 (* big 2))";
(try Sys.remove exe with Sys_error _ -> ())
in
restart_mismatch ();

23
test/test_flan.ml
View File

@ -1105,6 +1105,29 @@ let () =
~needle:"1e-50 is too small for f32, which rounds it to 0"
"(defn f [] f32 1e-50)";
infers "a literal past f32's range is an f64 like any other" "(+ 1.0 1e300)" "f64";
(* Chains through a second round, and through do, let and if arms that
merge without one. *)
accepts "a literal local fed through do, however long the chain"
"(defn f [x i64] i64 (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0 a6 0 a7 0 a8 0 a9 0 a10 0 \
a11 0 a12 0] (set a0 x) (set a1 (do a0)) (set a2 (do a1)) (set a3 (do a2)) \
(set a4 (do a3)) (set a5 (do a4)) (set a6 (do a5)) (set a7 (do a6)) \
(set a8 (do a7)) (set a9 (do a8)) (set a10 (do a9)) (set a11 (do a10)) \
(set a12 (do a11)) a12))";
accepts "a literal local fed through a let"
"(defn f [x i64] i64 (let [a0 0 a1 0 a2 0] (set a0 x) (set a1 (let [t a0] t)) \
(set a2 (let [t a1] t)) a2))";
accepts "a literal local fed through both arms of an if"
"(defn f [x i64] i64 (let [a0 0 a1 0] (set a0 x) (set a1 (if true a0 a0)) a1))";
accepts "a literal local fed through a generic call settles in rounds"
"(defn same [x $t] $t x) (defn f [x i64] i64 (let [a0 0 a1 0 a2 0] (set a0 x) \
(set a1 (same a0)) (set a2 (same a1)) a2))";
rejects_check "a chain the rounds cannot follow names the local to annotate"
~needle:"the type of a7 depends on too long a chain of the values stored into \
it to be read off them. Write the type it should have: (i64 0)"
"(defn same [x $t] $t x) (defn f [x i64] i64 (let [a0 0 a1 0 a2 0 a3 0 a4 0 a5 0 \
a6 0 a7 0 a8 0 a9 0 a10 0] (set a0 x) (set a1 (same a0)) (set a2 (same a1)) \
(set a3 (same a2)) (set a4 (same a3)) (set a5 (same a4)) (set a6 (same a5)) \
(set a7 (same a6)) (set a8 (same a7)) (set a9 (same a8)) (set a10 (same a9)) a10))";
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)"