A self-containing or runaway generic struct and a where clause over a length are each one error among the file's others, and a literal that does not fit a variable a typed field decided names that field
This commit is contained in:
parent
2f321fd061
commit
ff8b61e44c
102
lib/check.ml
102
lib/check.ml
@ -251,6 +251,15 @@ type env = {
|
|||||||
(* The struct copies this env made, by key, and whether each is one at
|
(* The struct copies this env made, by key, and whether each is one at
|
||||||
variables — those are left out of the program. *)
|
variables — those are left out of the program. *)
|
||||||
copies : (string, bool) Hashtbl.t;
|
copies : (string, bool) Hashtbl.t;
|
||||||
|
(* Templates whose own check was refused while [deferred] was collecting:
|
||||||
|
a use of one is a copy with no fields, so the refusal is said once, at
|
||||||
|
the defstruct, and nothing downstream repeats it. *)
|
||||||
|
broken : (string, unit) Hashtbl.t;
|
||||||
|
(* While a whole-file check collects every error, the refusals [collect]
|
||||||
|
can go on past — a generic struct's template, a where clause over a
|
||||||
|
length — are kept here instead of ending the pass. [None] everywhere
|
||||||
|
else, where they raise as before. *)
|
||||||
|
mutable deferred : Loc.diag list option;
|
||||||
(* A generic defn's length variables, by name: the ones of its [gsigs]
|
(* A generic defn's length variables, by name: the ones of its [gsigs]
|
||||||
variables that are lengths. *)
|
variables that are lengths. *)
|
||||||
glens : (string, string list) Hashtbl.t;
|
glens : (string, string list) Hashtbl.t;
|
||||||
@ -329,6 +338,8 @@ let new_env () = {
|
|||||||
refused_generics = Hashtbl.create 4;
|
refused_generics = Hashtbl.create 4;
|
||||||
gstructs = Hashtbl.create 4;
|
gstructs = Hashtbl.create 4;
|
||||||
copies = Hashtbl.create 8;
|
copies = Hashtbl.create 8;
|
||||||
|
broken = Hashtbl.create 2;
|
||||||
|
deferred = None;
|
||||||
glens = Hashtbl.create 8;
|
glens = Hashtbl.create 8;
|
||||||
lenvars = [];
|
lenvars = [];
|
||||||
len_placeholder = false;
|
len_placeholder = false;
|
||||||
@ -343,6 +354,13 @@ let new_env () = {
|
|||||||
guard_next = false;
|
guard_next = false;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
(* A refusal [collect] can go on past: kept while a whole-file check is
|
||||||
|
collecting, in the order found, and raised otherwise. *)
|
||||||
|
let defer_or_raise env (d : Loc.diag) =
|
||||||
|
match env.deferred with
|
||||||
|
| Some l -> env.deferred <- Some (d :: l)
|
||||||
|
| None -> Loc.raise_diag d
|
||||||
|
|
||||||
(* Where a named type was declared, and what it has, as a note.
|
(* Where a named type was declared, and what it has, as a note.
|
||||||
|
|
||||||
This is the second half of the two-place messages: a refusal that says
|
This is the second half of the two-place messages: a refusal that says
|
||||||
@ -1599,9 +1617,14 @@ and struct_len_arg env name p (a : Ast.texpr) =
|
|||||||
|
|
||||||
(* The copy of generic struct [name] at [targs], made on first use and
|
(* The copy of generic struct [name] at [targs], made on first use and
|
||||||
registered as an ordinary struct under its key. *)
|
registered as an ordinary struct under its key. *)
|
||||||
and struct_copy env loc name targs =
|
and struct_copy ?(at_definition = false) env loc name targs =
|
||||||
let key = struct_app name targs in
|
let key = struct_app name targs in
|
||||||
if Hashtbl.mem env.copies key then key
|
if Hashtbl.mem env.copies key then key
|
||||||
|
else if Hashtbl.mem env.broken name then begin
|
||||||
|
Hashtbl.replace env.copies key (List.exists generic_arg targs);
|
||||||
|
Hashtbl.replace env.structs key { Tast.sname = key; fields = [] };
|
||||||
|
key
|
||||||
|
end
|
||||||
else begin
|
else begin
|
||||||
if Hashtbl.mem env.structs key || Hashtbl.mem env.datas key
|
if Hashtbl.mem env.structs key || Hashtbl.mem env.datas key
|
||||||
|| Hashtbl.mem env.unions key then
|
|| Hashtbl.mem env.unions key then
|
||||||
@ -1673,7 +1696,7 @@ and struct_copy env loc name targs =
|
|||||||
(* A field refused inside the template says nothing about which use
|
(* A field refused inside the template says nothing about which use
|
||||||
asked for this copy; the note names it, one per level of copies. *)
|
asked for this copy; the note names it, one per level of copies. *)
|
||||||
(match e with
|
(match e with
|
||||||
| Loc.Error d when d.Loc.dloc <> loc ->
|
| Loc.Error d when d.Loc.dloc <> loc && not at_definition ->
|
||||||
Loc.raise_diag
|
Loc.raise_diag
|
||||||
{ d with
|
{ d with
|
||||||
Loc.notes =
|
Loc.notes =
|
||||||
@ -6810,9 +6833,37 @@ and generic_ctor ctx ~want loc name given =
|
|||||||
them, as a generic call's literal arguments meet at the wider type —
|
them, as a generic call's literal arguments meet at the wider type —
|
||||||
[(Pair 1 2.5)] is a [(Pair f64)]. *)
|
[(Pair 1 2.5)] is a [(Pair f64)]. *)
|
||||||
let lit_only = ref [] in
|
let lit_only = ref [] in
|
||||||
|
(* Which field's value decided each variable, for the refusal of a
|
||||||
|
literal that does not fit what it decided. *)
|
||||||
|
let decided_by = ref [] in
|
||||||
List.iter
|
List.iter
|
||||||
(fun ((f : Tast.field), (a : Ast.expr)) ->
|
(fun ((f : Tast.field), (a : Ast.expr)) ->
|
||||||
match f.Tast.fty with
|
match f.Tast.fty with
|
||||||
|
(* A literal at a variable a typed field already decided: it has to
|
||||||
|
be usable at that type, and when it is not the refusal names the
|
||||||
|
field that decided it. *)
|
||||||
|
| Types.Var v
|
||||||
|
when literal a && List.mem_assoc v !subst
|
||||||
|
&& not (List.mem v !lit_only) ->
|
||||||
|
let b = List.assoc v !subst in
|
||||||
|
(match a.Ast.e, b with
|
||||||
|
| Ast.Float x, Types.Int _ ->
|
||||||
|
let notes =
|
||||||
|
match List.assoc_opt v !decided_by with
|
||||||
|
| Some (fname, at) ->
|
||||||
|
[ Loc.note at
|
||||||
|
(Printf.sprintf ".%s is %s here, which decides $%s" fname
|
||||||
|
(Types.to_string b) v) ]
|
||||||
|
| None -> []
|
||||||
|
in
|
||||||
|
Loc.failk "check/generic-struct-field" a.Ast.loc ~notes
|
||||||
|
"%s's .%s is $%s, which is %s here, and %g is a float literal. \
|
||||||
|
Write .%s as an integer, or give .%s a float type"
|
||||||
|
name f.Tast.fname v (Types.to_string b) x f.Tast.fname
|
||||||
|
(match List.assoc_opt v !decided_by with
|
||||||
|
| Some (fname, _) -> fname
|
||||||
|
| None -> f.Tast.fname)
|
||||||
|
| _ -> ())
|
||||||
| Types.Var v when literal a && not (List.mem_assoc v !subst && not (List.mem v !lit_only)) ->
|
| Types.Var v when literal a && not (List.mem_assoc v !subst && not (List.mem v !lit_only)) ->
|
||||||
let t = (literal_type a) in
|
let t = (literal_type a) in
|
||||||
(match List.assoc_opt v !subst with
|
(match List.assoc_opt v !subst with
|
||||||
@ -6841,7 +6892,14 @@ and generic_ctor ctx ~want loc name given =
|
|||||||
nothing. *)
|
nothing. *)
|
||||||
| None -> Option.iter (fun d -> unsure := d :: !unsure) refusal
|
| None -> Option.iter (fun d -> unsure := d :: !unsure) refusal
|
||||||
| Some t ->
|
| Some t ->
|
||||||
if not (bind_ty subst f.Tast.fty t) then
|
let before = !subst in
|
||||||
|
if bind_ty subst f.Tast.fty t then
|
||||||
|
List.iter
|
||||||
|
(fun (v, _) ->
|
||||||
|
if not (List.mem_assoc v before) then
|
||||||
|
decided_by := (v, (f.Tast.fname, a.Ast.loc)) :: !decided_by)
|
||||||
|
!subst
|
||||||
|
else
|
||||||
fail a.Ast.loc "%s's .%s is %s here, and this is %s"
|
fail a.Ast.loc "%s's .%s is %s here, and this is %s"
|
||||||
(Types.to_string (Types.Named open_key)) f.Tast.fname
|
(Types.to_string (Types.Named open_key)) f.Tast.fname
|
||||||
(Types.to_string (subst_ty !subst f.Tast.fty))
|
(Types.to_string (subst_ty !subst f.Tast.fty))
|
||||||
@ -13370,9 +13428,14 @@ let collect env (decls : Ast.decl list) =
|
|||||||
type in a field is refused at the defstruct rather than at the
|
type in a field is refused at the defstruct rather than at the
|
||||||
first use of it. *)
|
first use of it. *)
|
||||||
let g = Hashtbl.find env.gstructs n in
|
let g = Hashtbl.find env.gstructs n in
|
||||||
ignore
|
(match
|
||||||
(struct_copy env loc n
|
struct_copy ~at_definition:true env loc n
|
||||||
(List.map (fun (p, _) -> Types.Var p) g.gparams))
|
(List.map (fun (p, _) -> Types.Var p) g.gparams)
|
||||||
|
with
|
||||||
|
| _ -> ()
|
||||||
|
| exception Loc.Error d ->
|
||||||
|
Hashtbl.replace env.broken n ();
|
||||||
|
defer_or_raise env d)
|
||||||
| Ast.Defstruct (n, fs, parent) ->
|
| Ast.Defstruct (n, fs, parent) ->
|
||||||
let names = List.map (fun (f : Ast.field) -> f.Ast.fname) fs in
|
let names = List.map (fun (f : Ast.field) -> f.Ast.fname) fs in
|
||||||
if List.length (List.sort_uniq compare names) <> List.length names then
|
if List.length (List.sort_uniq compare names) <> List.length names then
|
||||||
@ -13517,10 +13580,22 @@ let collect env (decls : Ast.decl list) =
|
|||||||
an open question in TODO.org, not an accident to fall out
|
an open question in TODO.org, not an accident to fall out
|
||||||
of this. *)
|
of this. *)
|
||||||
if List.mem p.Ast.pvar lens then
|
if List.mem p.Ast.pvar lens then
|
||||||
Loc.failk "check/length-predicate" p.Ast.ploc
|
defer_or_raise env
|
||||||
"$%s is a length, and a where clause takes type predicates \
|
(Loc.diag ~kind:"check/length-predicate" p.Ast.ploc
|
||||||
only — %s is about a type" p.Ast.pvar p.Ast.pname)
|
(Printf.sprintf
|
||||||
|
"$%s is a length, and a where clause takes type \
|
||||||
|
predicates only — %s is about a type"
|
||||||
|
p.Ast.pvar p.Ast.pname)))
|
||||||
fn.Ast.fwhere;
|
fn.Ast.fwhere;
|
||||||
|
(* A predicate over a length was refused above; what is left is the
|
||||||
|
clause every copy is judged against. *)
|
||||||
|
let fn =
|
||||||
|
{ fn with
|
||||||
|
Ast.fwhere =
|
||||||
|
List.filter
|
||||||
|
(fun (p : Ast.pred) -> not (List.mem p.Ast.pvar lens))
|
||||||
|
fn.Ast.fwhere }
|
||||||
|
in
|
||||||
env.tyvars <- vars;
|
env.tyvars <- vars;
|
||||||
env.lenvars <- lens;
|
env.lenvars <- lens;
|
||||||
env.tvpreds <- fn.Ast.fwhere;
|
env.tvpreds <- fn.Ast.fwhere;
|
||||||
@ -13623,7 +13698,10 @@ let collect env (decls : Ast.decl list) =
|
|||||||
out or a zero value is built for it — which would not fail, it would hang. *)
|
out or a zero value is built for it — which would not fail, it would hang. *)
|
||||||
let check_finite env =
|
let check_finite env =
|
||||||
let walk _ n = finite_from env n in
|
let walk _ n = finite_from env n in
|
||||||
Hashtbl.iter (fun n _ -> walk [] n) env.structs;
|
(* A generic struct's copy was asked this when it was made. *)
|
||||||
|
Hashtbl.iter
|
||||||
|
(fun n _ -> if not (Hashtbl.mem env.copies n) then walk [] n)
|
||||||
|
env.structs;
|
||||||
Hashtbl.iter (fun n _ -> walk [] n) env.datas;
|
Hashtbl.iter (fun n _ -> walk [] n) env.datas;
|
||||||
Hashtbl.iter (fun n _ -> walk [] n) env.unions
|
Hashtbl.iter (fun n _ -> walk [] n) env.unions
|
||||||
|
|
||||||
@ -14978,10 +15056,14 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) :
|
|||||||
time it runs every signature is sound, so a body that fails to check
|
time it runs every signature is sound, so a body that fails to check
|
||||||
cannot make the next body fail — which is what makes a declaration a
|
cannot make the next body fail — which is what makes a declaration a
|
||||||
resync point that needs no resynchronising. *)
|
resync point that needs no resynchronising. *)
|
||||||
|
if keep_going then env.deferred <- Some [];
|
||||||
let decls = collect env decls in
|
let decls = collect env decls in
|
||||||
check_finite env;
|
check_finite env;
|
||||||
check_union_members env;
|
check_union_members env;
|
||||||
let s = Loc.sink ~on:keep_going in
|
let s = Loc.sink ~on:keep_going in
|
||||||
|
(match env.deferred with
|
||||||
|
| Some ds -> s.Loc.found <- ds; env.deferred <- None
|
||||||
|
| None -> ());
|
||||||
ignore (Loc.caught s (fun () -> check_main env decls));
|
ignore (Loc.caught s (fun () -> check_main env decls));
|
||||||
(* Every generic body, checked once with its variables left abstract, and
|
(* Every generic body, checked once with its variables left abstract, and
|
||||||
the result thrown away. This is the pass plan.org's rule needs and Odin
|
the result thrown away. This is the pass plan.org's rule needs and Odin
|
||||||
|
|||||||
@ -6017,6 +6017,47 @@ let () =
|
|||||||
= [ "show is instantiated at $t = (CFn [] i32) here";
|
= [ "show is instantiated at $t = (CFn [] i32) here";
|
||||||
"outer is instantiated at $t = (CFn [] i32) here" ]));
|
"outer is instantiated at $t = (CFn [] i32) here" ]));
|
||||||
|
|
||||||
|
(* A refusal made while collecting declarations — a generic struct that
|
||||||
|
holds itself, one that grows without end, a where clause over a length —
|
||||||
|
is one error among the rest of the file's, not the end of the check. *)
|
||||||
|
let all_lines src =
|
||||||
|
match Check.program_all (Parse.program_all (read src)) with
|
||||||
|
| _ -> []
|
||||||
|
| exception Loc.Errors ds ->
|
||||||
|
List.map (fun (d : Loc.diag) -> d.Loc.dloc.Loc.line) ds
|
||||||
|
in
|
||||||
|
check "a self-containing generic struct is one error of several"
|
||||||
|
(all_lines
|
||||||
|
"(defstruct Loop [next (Loop $t)])\n\
|
||||||
|
(defn g [] i32 (let [p (the (Loop i32) (zeroed))] nope1))\n\
|
||||||
|
(defn h [] i32 nope2)\n"
|
||||||
|
= [ 1; 2; 3 ]);
|
||||||
|
check "a generic struct that grows without end is one error of several"
|
||||||
|
(all_lines
|
||||||
|
"(defstruct Grow [next (Ptr (Grow [$t]))])\n\
|
||||||
|
(defn g [] i32 (let [p (the (Grow i32) (zeroed))] nope1))\n\
|
||||||
|
(defn h [] i32 nope2)\n"
|
||||||
|
= [ 1; 2; 3 ]);
|
||||||
|
check "a where clause over a length is one error of several"
|
||||||
|
(all_lines
|
||||||
|
"(defn f [a [$n i32]] i32 {:where (numeric? $n)} nope1)\n\
|
||||||
|
(defn h [] i32 nope2)\n"
|
||||||
|
= [ 1; 1; 2 ]);
|
||||||
|
(* A literal that does not fit what a typed field decided names that field. *)
|
||||||
|
(match
|
||||||
|
checked
|
||||||
|
"(defstruct Pair [a $t b $t]) \
|
||||||
|
(defn main [] i32 (let [p (Pair (the i32 1) 2.5)] 0))"
|
||||||
|
with
|
||||||
|
| _ -> check "a float literal where a typed field decided i32" false
|
||||||
|
| exception Loc.Error d ->
|
||||||
|
check "the refusal names the field that decided the variable"
|
||||||
|
(contains d.Loc.dmsg "Pair's .b is $t, which is i32 here"
|
||||||
|
&& List.exists
|
||||||
|
(fun (n : Loc.note) ->
|
||||||
|
contains n.Loc.nmsg ".a is i32 here, which decides $t")
|
||||||
|
d.Loc.notes));
|
||||||
|
|
||||||
(* A copy that cannot be built at a closure's type: the zeroed value in the
|
(* A copy that cannot be built at a closure's type: the zeroed value in the
|
||||||
body is refused there, and the call that asked is named. *)
|
body is refused there, and the call that asked is named. *)
|
||||||
(match
|
(match
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user