A _ function's exits combine exactly as an if's arms do, a refused _ body or loop is collected with every other error, and the placeholder type never leaves the checker
This commit is contained in:
parent
8fdf8513fd
commit
df7078d586
157
lib/check.ml
157
lib/check.ml
@ -218,7 +218,7 @@ type env = {
|
||||
their own, while every error is being collected. Each stands in [fns]
|
||||
as Never, a call to one stands as a poison, and pass two reports the
|
||||
body's errors once. *)
|
||||
infer_failed : (string, unit) Hashtbl.t;
|
||||
infer_failed : (string, Loc.diag option) Hashtbl.t;
|
||||
(* Recovery: checking goes on past a refused subexpression. See [check].
|
||||
[recovering] is on only while a whole-file or session check is collecting
|
||||
every error; [recovered] is what it found, newest first; [poison] counts
|
||||
@ -3690,7 +3690,7 @@ let hash_ty = Types.Int Types.U64
|
||||
address, so no type written anywhere is ever mistaken for it. What each
|
||||
[return] in that body gives is pushed on [infer_seen]. *)
|
||||
let infer_ret = Types.Named "_"
|
||||
let infer_seen : (Types.t * Loc.t) list ref = ref []
|
||||
let infer_seen : (Types.t * Loc.t * bool) list ref = ref []
|
||||
(* What a refused subexpression stands as while recovering. [Zero] of [Never]
|
||||
is a value nothing else builds, so it is recognisable; see [check]. *)
|
||||
let poison loc = { Tast.e = Tast.Zero Types.Never; ty = Types.Never; loc }
|
||||
@ -4788,11 +4788,12 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
(match ctx.in_frames with Some n -> n | None -> assert false)
|
||||
|
||||
| Ast.Return v when ctx.ret == infer_ret ->
|
||||
let lit = match v with Some x -> lone_literal x | None -> false in
|
||||
let v = Option.map (check ctx) v in
|
||||
infer_seen :=
|
||||
(match v with
|
||||
| Some (x : Tast.expr) -> (x.Tast.ty, loc)
|
||||
| None -> (Types.Unit, loc))
|
||||
| Some (x : Tast.expr) -> (x.Tast.ty, loc, lit)
|
||||
| None -> (Types.Unit, loc, false))
|
||||
:: !infer_seen;
|
||||
(match ctx.defers, v with
|
||||
| [], _ -> mk loc Types.Never (Tast.Return v)
|
||||
@ -13644,6 +13645,15 @@ let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn =
|
||||
| None -> ctx.defers
|
||||
| Some s -> guarded_defers s ctx.defers);
|
||||
fenv = None; fparent = None; floc = fn.Ast.nloc }
|
||||
|> fun (tf : Tast.fn) ->
|
||||
if sign = None && ret == infer_ret then
|
||||
(* Pass two over a [_] body pass one could not read: its errors are
|
||||
raised above; a body that checks has the refusal pass one made about
|
||||
its exits, or waited on one that did, and stands as Never. *)
|
||||
match Hashtbl.find_opt env.infer_failed fn.Ast.name with
|
||||
| Some (Some d) -> raise (Loc.Error d)
|
||||
| _ -> { tf with Tast.ret = Types.Never }
|
||||
else tf
|
||||
|
||||
(* The generic body, checked once with its variables abstract. Nothing is kept
|
||||
— the [Tast.fn] it produces is thrown away, and so is anything it lifted —
|
||||
@ -13688,12 +13698,15 @@ and check_generic env (fn : Ast.fn) =
|
||||
them never settles and is refused by name; a body that calls its own name
|
||||
is the cycle of one. *)
|
||||
|
||||
(* The type one body gives, and the form that decided it: the last form and
|
||||
every [return], ignoring what never arrives. All alike give that type;
|
||||
none gives (). When they differ, each one's type is tried as the return
|
||||
type the body is checked against, last form first, so a literal takes the
|
||||
type of the other exits the way an [if]'s arms do; the first that checks
|
||||
is the type. When none does, they meet in dyn. *)
|
||||
(* The type one body gives, and the form that decided it. The exits — the
|
||||
last form and every [return], less what never arrives — combine the way
|
||||
an [if]'s arms do ([check_if_once]): the first one that is not a lone
|
||||
literal decides and the literals take its type, a bool meets a dyn at
|
||||
dyn, and literals alone meet at the wider of their own types. The body is
|
||||
then checked against that type exactly as a written one would be, so
|
||||
whatever [if] refuses between its arms is refused between exits, in the
|
||||
same words. None gives (); no value beside a value is refused, since ()
|
||||
does not take a value's place. *)
|
||||
and read_return env (fn : Ast.fn) params =
|
||||
(* One check of the body against [ret], thrown away: what it lifted goes,
|
||||
and so do the copies it asked for if it failed, as [tolerant] does. *)
|
||||
@ -13732,67 +13745,48 @@ and read_return env (fn : Ast.fn) params =
|
||||
in
|
||||
let tf, returns = attempt infer_ret in
|
||||
let last =
|
||||
match List.rev tf.Tast.body with
|
||||
| (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ]
|
||||
| [] -> []
|
||||
match List.rev tf.Tast.body, List.rev fn.Ast.fbody with
|
||||
| (x : Tast.expr) :: _, (a : Ast.expr) :: _ ->
|
||||
[ (x.Tast.ty, x.Tast.loc, lone_literal a) ]
|
||||
| (x : Tast.expr) :: _, [] -> [ (x.Tast.ty, x.Tast.loc, false) ]
|
||||
| [], _ -> []
|
||||
in
|
||||
let arrive =
|
||||
List.filter (fun (t, _) -> not (Types.equal t Types.Never)) (returns @ last)
|
||||
List.filter (fun (t, _, _) -> not (Types.equal t Types.Never)) (returns @ last)
|
||||
in
|
||||
let unit (t, _, _) = Types.equal t Types.Unit in
|
||||
(match List.find_opt unit arrive, List.find_opt (fun x -> not (unit x)) arrive with
|
||||
| Some (_, bare, _), Some (t, valued, _) ->
|
||||
Loc.failk "check/infer-mixed" bare
|
||||
~notes:[ Loc.note valued ("this gives " ^ Types.to_string t) ]
|
||||
"%s gives no value here and %s on another path, and its return \
|
||||
type is read off its body. Give this path a value too, or write \
|
||||
the return type"
|
||||
fn.Ast.name (Types.to_string t)
|
||||
| _ -> ());
|
||||
match arrive with
|
||||
| [] -> (Types.Unit, fn.Ast.nloc)
|
||||
| (t, l) :: rest
|
||||
when not (List.exists (fun (u, _) -> not (Types.equal t u)) rest) ->
|
||||
| (t, l, _) :: rest
|
||||
when not (List.exists (fun (u, _, _) -> not (Types.equal t u)) rest) ->
|
||||
(t, l)
|
||||
| _ ->
|
||||
let candidates =
|
||||
List.fold_left
|
||||
(fun acc (t, l) ->
|
||||
if List.exists (fun (u, _) -> Types.equal t u) acc then acc
|
||||
else acc @ [ (t, l) ])
|
||||
[] (List.rev arrive)
|
||||
| (t0, l0, _) :: _ ->
|
||||
let decided =
|
||||
match List.filter (fun (_, _, lit) -> not lit) arrive with
|
||||
| (Types.Bool, l, _) :: others
|
||||
when List.exists (fun (u, _, _) -> Types.equal u Types.Dyn) others ->
|
||||
(Types.Dyn, l)
|
||||
| (t, l, _) :: _ -> (t, l)
|
||||
| [] ->
|
||||
let joined =
|
||||
List.fold_left
|
||||
(fun acc (u, _, _) ->
|
||||
match acc with Some a -> Types.join a u | None -> None)
|
||||
(Some t0) arrive
|
||||
in
|
||||
(Option.value joined ~default:t0, l0)
|
||||
in
|
||||
let fits (t, _) =
|
||||
match attempt t with _ -> true | exception Loc.Error _ -> false
|
||||
in
|
||||
(match List.find_opt fits candidates with
|
||||
| Some found -> found
|
||||
| None ->
|
||||
(* Two types meet in dyn only if both box into it, and () and a
|
||||
struct do not: said here, with both ways out, rather than as a
|
||||
boxing refusal at one of them in pass two. *)
|
||||
let boxes (t, _) =
|
||||
match t with
|
||||
| Types.Int _ | Types.Float _ | Types.Bool | Types.String
|
||||
| Types.Dyn -> true
|
||||
| _ -> false
|
||||
in
|
||||
(match List.find_opt (fun x -> not (boxes x)) arrive with
|
||||
| Some (bad, at) ->
|
||||
let other, oloc =
|
||||
List.find (fun (u, _) -> not (Types.equal u bad)) arrive
|
||||
in
|
||||
let notes =
|
||||
[ Loc.note oloc ("this gives " ^ Types.to_string other) ]
|
||||
in
|
||||
if Types.equal bad Types.Unit then
|
||||
Loc.failk "check/infer-mixed" at ~notes
|
||||
"%s gives no value here and %s on another path, and its \
|
||||
return type is read off its body. Give this path a value \
|
||||
too, or write the return type"
|
||||
fn.Ast.name (Types.to_string other)
|
||||
else
|
||||
Loc.failk "check/infer-mixed" at ~notes
|
||||
"%s gives %s here and %s on another path, and its return type \
|
||||
is read off its body. Two types meet only in dyn, and %s does \
|
||||
not box into it. Give every path one type, or write the \
|
||||
return type"
|
||||
fn.Ast.name (Types.to_string bad) (Types.to_string other)
|
||||
(Types.to_string bad)
|
||||
| None ->
|
||||
let t, _ = List.hd arrive in
|
||||
let _, l' = List.find (fun (u, _) -> not (Types.equal t u)) arrive in
|
||||
(Types.Dyn, l')))
|
||||
ignore (attempt (fst decided));
|
||||
decided
|
||||
|
||||
and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
|
||||
(decls : Ast.decl list) =
|
||||
@ -13849,8 +13843,8 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
|
||||
sake; a [_] body that calls it cannot be read either, and waits the
|
||||
same way. *)
|
||||
let failed = env.infer_failed in
|
||||
let fail_quietly (fn : Ast.fn) =
|
||||
Hashtbl.replace failed fn.Ast.name ();
|
||||
let fail_quietly ?refusal (fn : Ast.fn) =
|
||||
Hashtbl.replace failed fn.Ast.name refusal;
|
||||
Hashtbl.replace env.fns fn.Ast.name (params_of fn, Types.Never)
|
||||
in
|
||||
(* Only while every error is collected: a check that stops at the first
|
||||
@ -13862,7 +13856,7 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
|
||||
(match tolerate, previous fn.Ast.name with
|
||||
| Some ok, Some (params, ret) when ok env fn.Ast.name d ->
|
||||
Hashtbl.replace env.fns fn.Ast.name (params, ret)
|
||||
| _ -> if keep_going then fail_quietly fn else raise e)
|
||||
| _ -> if keep_going then fail_quietly ~refusal:d fn else raise e)
|
||||
in
|
||||
let rec rounds left =
|
||||
let still =
|
||||
@ -13972,6 +13966,9 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
|
||||
else Printf.sprintf "%s calls %s here" n callee))
|
||||
cycle
|
||||
in
|
||||
(* Collected like any refusal when every error is: the loop's
|
||||
first member carries it into pass two, the rest stand quietly. *)
|
||||
match
|
||||
(match cycle with
|
||||
| [ n ] ->
|
||||
Loc.failk "check/infer-recursive" fn.Ast.nloc ~notes
|
||||
@ -13984,7 +13981,20 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env
|
||||
them in its signature"
|
||||
(String.concat " and " cycle)
|
||||
(String.concat " → " (cycle @ [ first ]))
|
||||
(if List.length cycle = 2 then "neither" else "none")))
|
||||
(if List.length cycle = 2 then "neither" else "none"))
|
||||
with
|
||||
| () -> ()
|
||||
| exception (Loc.Error d as e) ->
|
||||
if not keep_going then raise e;
|
||||
List.iter
|
||||
(fun n ->
|
||||
fail_quietly
|
||||
?refusal:(if n = first then Some d else None)
|
||||
(List.assoc n byname))
|
||||
cycle;
|
||||
stalled
|
||||
(List.filter
|
||||
(fun (fn : Ast.fn) -> not (List.mem fn.Ast.name cycle)) stuck))
|
||||
in
|
||||
stalled order
|
||||
end
|
||||
@ -15199,6 +15209,17 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) :
|
||||
(Loc.entry ~mark:'~' ~label:"warning: " d.Loc.dloc d.Loc.dmsg))
|
||||
(List.rev !grow_warnings);
|
||||
Loc.finish s;
|
||||
(* The placeholder a [_] body is read against is never a type anything
|
||||
downstream may see; a signature carrying it would be emitted as a
|
||||
struct named _. *)
|
||||
List.iter
|
||||
(fun (f : Tast.fn) ->
|
||||
if f.Tast.ret == infer_ret
|
||||
|| List.exists (fun t -> t == infer_ret) f.Tast.params
|
||||
then
|
||||
fail f.Tast.floc "internal: %s left the checker with its return \
|
||||
type unread" f.Tast.name)
|
||||
fns;
|
||||
(* The handler clauses lifted out along the way. They are ordinary functions
|
||||
from here down; nothing in the backend knows they were written inside
|
||||
something else. *)
|
||||
|
||||
@ -54,8 +54,10 @@ warns about; the new syntax must not inherit it.
|
||||
|
||||
**The return type is inferred when omitted.** Body-local only, as
|
||||
`docs/SPIKE-INFERENCE.md` ("The cheap first step" and "Verdict") scopes it:
|
||||
- the return type is the body's type; a `dyn` body gives `dyn`; `return`s of
|
||||
different types give `dyn`; no value gives `()`.
|
||||
- the return type is the body's type; a `dyn` body gives `dyn`; the exits (the
|
||||
last form and each `return`) combine exactly as an `if`'s arms do, so a
|
||||
literal takes the other exits' type and what `if` refuses is refused; no
|
||||
value gives `()`.
|
||||
- it reads only the function's own body, never a call site.
|
||||
- a self-recursive or mutually recursive function must write its return type.
|
||||
Refuse by name, naming the whole cycle. The corpus has 17 self-recursive
|
||||
@ -361,11 +363,9 @@ Each step lands on its own, with `dune test --root .` green.
|
||||
stale-caller cause. This is independent of steps 1-5 once the marker exists.
|
||||
**Built** (`Check.infer_returns`). `_` is refused outside a `defn`'s return
|
||||
slot, in a generic's, and in `defgeneric`/`defmulti`'s (`defmethod` has no
|
||||
return slot). Two ways out of one body whose types differ and cannot both
|
||||
box (a value and `()`, a number and a struct) are refused rather than made
|
||||
`dyn`. Exits of different types are first tried at each other's type, so a
|
||||
literal `return 0` beside an `i64` gives `i64`. A self- or mutually
|
||||
recursive group whose every exit gives `()` is `()`. A stale
|
||||
return slot). An exit with no value beside one with a value is refused. A
|
||||
self- or mutually recursive group whose every exit gives `()` is `()`. A
|
||||
stale
|
||||
body with `_` keeps the signature it was compiled with.
|
||||
|
||||
Out of scope: dropping macros, built-in replacements for `with-*`/`defedn`,
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
;; Return types read off the body: _ in the return slot here, no arrow in
|
||||
;; main.fln. Each shape the rule has: one type, a call's type, a literal
|
||||
;; that takes the other exit's type, two types (dyn), nothing (()), a return
|
||||
;; that takes the other exit's type, a dyn beside a literal, nothing (()), a return
|
||||
;; that never falls off the end, and a function that calls itself and gives
|
||||
;; nothing.
|
||||
|
||||
@ -14,8 +14,8 @@
|
||||
(when c (return 1))
|
||||
2.5)
|
||||
|
||||
(defn label [c bool] _
|
||||
(when c (return "yes"))
|
||||
(defn label [c bool d dyn] _
|
||||
(when c (return d))
|
||||
0)
|
||||
|
||||
(defn say [x i32] _ (println x))
|
||||
@ -33,7 +33,7 @@
|
||||
(println (quarter 10.0))
|
||||
(println (+ (pick true) 0.5))
|
||||
(println (pick false))
|
||||
(println (label true) (label false))
|
||||
(println (label true "yes") (label false "yes"))
|
||||
(say 4)
|
||||
(println (floor0 -3) (floor0 5))
|
||||
(countdown 2)
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
;; Return types read off the body: no arrow here, _ in the return slot in
|
||||
;; main.flan. Each shape the rule has: one type, a call's type, a literal
|
||||
;; that takes the other exit's type, two types (dyn), nothing (()), a return
|
||||
;; that takes the other exit's type, a dyn beside a literal, nothing (()), a return
|
||||
;; that never falls off the end, and a function that calls itself and gives
|
||||
;; nothing.
|
||||
|
||||
@ -15,9 +15,9 @@ fn pick(c: bool)
|
||||
return 1
|
||||
2.5
|
||||
|
||||
fn label(c: bool)
|
||||
fn label(c: bool, d)
|
||||
if c
|
||||
return "yes"
|
||||
return d
|
||||
0
|
||||
|
||||
fn say(x: i32) = println(x)
|
||||
@ -35,7 +35,7 @@ fn main() -> i32
|
||||
println(quarter(10.0))
|
||||
println(pick(true) + 0.5)
|
||||
println(pick(false))
|
||||
println(label(true), label(false))
|
||||
println(label(true, "yes"), label(false, "yes"))
|
||||
say(4)
|
||||
println(floor0(-3), floor0(5))
|
||||
countdown(2)
|
||||
|
||||
@ -7326,8 +7326,12 @@ let () =
|
||||
("(defn f [x i64] _ (when (< x 0) (return 0)) x)" ^ main) "f" "f [i64] i64";
|
||||
reads_as "a literal return takes an f32"
|
||||
("(defn f [c bool x f32] _ (when c (return 1)) x)" ^ main) "f" "f [bool f32] f32";
|
||||
reads_as "two types give dyn"
|
||||
("(defn f [c bool] _ (when c (return \"s\")) 2)" ^ main) "f" "f [bool] dyn";
|
||||
reads_as "a dyn exit beside a literal gives dyn"
|
||||
("(defn f [d dyn c bool] _ (when c (return d)) 1)" ^ main) "f" "f [dyn bool] dyn";
|
||||
reads_as "a literal before the typed exit still takes its type"
|
||||
("(defn f [x i16] _ (when (< x 0) (return x)) 0)" ^ main) "f" "f [i16] i16";
|
||||
reads_as "an f32 exit and a float literal"
|
||||
("(defn f [x f32] _ (when (< x 0.0) (return x)) 0.0)" ^ main) "f" "f [f32] f32";
|
||||
reads_as "a function that calls itself and gives nothing is ()"
|
||||
("(defn f [n i32] _ (when (> n 0) (println n) (f (- n 1))))" ^ main) "f" "f [i32] ()";
|
||||
reads_as "two that call each other and give nothing are ()"
|
||||
@ -7364,10 +7368,6 @@ let () =
|
||||
rejects_check "no value on one path and a value on another"
|
||||
~needle:"f gives no value here and i32 on another path"
|
||||
"(defn f [x i32] _ (when (> x 0) (return 1)) (println 2))\n(defn main [] ())";
|
||||
rejects_check "a struct on one path and a number on another"
|
||||
~needle:"f gives P here and i32 on another path"
|
||||
"(defstruct P [x i32])\n\
|
||||
(defn f [c bool] _ (when c (return (P {.x 1}))) 2)\n(defn main [] ())";
|
||||
(* Every error in the file is still reported, a [_] body's included, and
|
||||
a call to a [_] function whose body failed adds none of its own. *)
|
||||
(let count src =
|
||||
@ -7392,7 +7392,30 @@ let () =
|
||||
errors "a call to a failed _ body adds nothing"
|
||||
"(defn bad1 [x i32] _ (+ x \"s\"))\n(defn g [x i32] _ (bad1 x))\n\
|
||||
(defn h [x i32] i32 (+ 1 (g x)))\n\
|
||||
(defn main [] i32 (println (bad1 1)) 0)" 1);
|
||||
(defn main [] i32 (println (bad1 1)) 0)" 1;
|
||||
errors "a refused loop does not hide the others"
|
||||
"(defn a [n i32] _ (if (> n 0) (b (- n 1)) 5))\n(defn b [n i32] _ (a n))\n\
|
||||
(defn z [n i32] i32 (+ n \"q\"))\n(defn main [] i32 (a 3) 0)" 2;
|
||||
errors "a refused exit does not hide the others"
|
||||
"(defn u [c bool] _ (when c (return)) 1)\n\
|
||||
(defn z [n i32] i32 (+ n \"q\"))\n(defn main [] i32 (u true) 0)" 2);
|
||||
(* Exits meet as an if's arms do, and are refused where those are. *)
|
||||
rejects_check "a struct exit and a literal exit"
|
||||
~needle:"expected Pt, found the integer literal 1"
|
||||
"(defstruct Pt [x i32 y i32])\n\
|
||||
(defn m [c bool] _ (when c (return (Pt {.x 1 .y 2}))) 1)\n(defn main [] ())";
|
||||
rejects_check "no value on one exit and a value on the other"
|
||||
~needle:"u gives no value here and i32 on another path"
|
||||
"(defn u [c bool] _ (when c (return)) 1)\n(defn main [] ())";
|
||||
rejects_check "an i32 exit and an i64 exit, as if refuses them"
|
||||
~needle:"expected i32, found i64"
|
||||
"(defn f [x i32 y i64 c bool] _ (when c (return x)) y)\n(defn main [] ())";
|
||||
rejects_check "a literal that does not fit the typed exit"
|
||||
~needle:"300 does not fit in u8"
|
||||
"(defn f [c bool] _ (when c (return 300)) (u8 2))\n(defn main [] ())";
|
||||
rejects_check "a string exit and a number exit"
|
||||
~needle:"expected string, found the integer literal 1"
|
||||
"(defn f [c bool] _ (when c (return \"s\")) 1)\n(defn main [] ())";
|
||||
rejects_check "some under an inferred return"
|
||||
~needle:"Write the return type: (Option T)"
|
||||
"(defn f [o (Option i32)] _ (+ 1 (some o)))\n(defn main [] ())";
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user