diff --git a/lib/check.ml b/lib/check.ml index 6d06c7cd..278c614c 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1991,6 +1991,12 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc } let unit_at loc = mk loc Types.Unit Tast.Unit +(* The compiler temp an [and] leaves in its else arm; see [check_if]. *) +let and_sentinel (x : Ast.expr) = + match x.Ast.e with + | Ast.Var n -> String.length n > 4 && String.sub n 0 4 = "and~" + | _ -> false + (* Integer arithmetic over literals alone, folded. Unlike [const_int] no name is read: a defconst has a type of its own, and only an untyped constant may stand at a type variable. *) @@ -2015,6 +2021,10 @@ let rec literal_arith (e : Ast.expr) : int64 option = (literal_arith x) (y :: rest) | _ -> None +(* A value with no type until one is asked of it: a literal, or arithmetic + over literals alone. *) +let lone_literal (e : Ast.expr) = is_literal e || literal_arith e <> None + (* The environment for a lifted body, built once its own body has been checked and [caught] is therefore final. spec-memory.md's case 2, and the whole of @@ -5102,6 +5112,16 @@ and check_if ctx ?(tail = false) ?want loc c t e = no value on the missing side. `when` desugars to this. *) let t = branch ctx (fun () -> in_tail (fun () -> check ctx t)) in expect ctx loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc))) + | Some e when want = None && lone_literal t && not (lone_literal e) + && not (and_sentinel e) -> + (* A literal has no type of its own until something asks, so with no + expectation the other arm decides: [(if c 4000000 n)] over an i64 [n] + is an i64, as [(+ 4000000 n)] is. *) + let e = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in + let twant = if e.Tast.ty = Types.Never then None else Some e.Tast.ty in + let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want:twant t)) in + let ty = if e.Tast.ty = Types.Never then t.Tast.ty else e.Tast.ty in + mk loc ty (Tast.If (c, t, e)) | Some e -> let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in (* With no expectation the then-branch supplies one for the else-branch, @@ -5125,12 +5145,6 @@ and check_if ctx ?(tail = false) ?want loc c t e = sentinel in the then arm, so every operand is already blamed at its own location; and with an expectation in hand both arms are checked against it rather than against each other, so nothing here runs. *) - let and_sentinel (x : Ast.expr) = - match x.Ast.e with - | Ast.Var n -> - String.length n > 4 && String.sub n 0 4 = "and~" - | _ -> false - in let e = match branch ctx (fun () -> in_tail (fun () -> check ctx ?want:ewant e)) with | v -> v @@ -5840,7 +5854,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let want = ref want in let seen = Hashtbl.create 8 in let saw_wild = ref false in - let arms = + let resolved = map_lr (fun (a : Ast.arm) -> let ctor, binds = resolve_pat a in @@ -5850,6 +5864,28 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = if Hashtbl.mem seen c then fail a.Ast.aloc "this match has two %s arms" c; Hashtbl.add seen c ()); + (a, ctor, binds)) + arms + in + (* With nothing expected of the match, the first arm's type is every arm's — + unless that arm is a bare literal, which has no type until asked. So the + arms whose value is a literal are checked last, and take their type from + the others, as an [if]'s literal arm does. The order is only the order + they are checked in; they are put back in source order below. *) + let literal_arm ((a : Ast.arm), _, _) = + match List.rev a.Ast.body with last :: _ -> lone_literal last | [] -> false + in + let order = + let idx = List.mapi (fun i r -> (i, r)) resolved in + if !want <> None then idx + else + List.filter (fun (_, r) -> not (literal_arm r)) idx + @ List.filter (fun (_, r) -> literal_arm r) idx + in + let checked = + map_lr + (fun (i, ((a : Ast.arm), ctor, binds)) -> + i, branch ctx (fun () -> (* What each name in this arm is, in words, for the one refusal that needs it: a case pattern binds fields positionally, so the @@ -5885,7 +5921,10 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = if !want = None && body.Tast.ty <> Types.Never then want := Some body.Tast.ty; { Tast.acase = ctor; binds; abody = [ body ] })) - arms + order + in + let arms = + List.map snd (List.sort (fun (i, _) (j, _) -> compare i j) checked) in (* Exhaustiveness is refused, not defaulted. A match that silently fell through would have to produce a value of the match's type out of nothing, diff --git a/test/programs/literal-arm.flan b/test/programs/literal-arm.flan new file mode 100644 index 00000000..5459e906 --- /dev/null +++ b/test/programs/literal-arm.flan @@ -0,0 +1,18 @@ +;;;; A literal arm takes its type from the arm that is not a literal, in an +;;;; if, a cond and a match alike, as a literal operand of + does. +(defn g [c bool n i64] i64 (let [x (if c 4000000 n)] x)) +(defn h [k i32 n i64] i64 + (let [x (cond (= k 0) 5000000000 (= k 1) 7 :else n)] x)) +(defn m [o (Option i64)] i64 + (let [x (match o None 3 (Some v) v)] x)) +(defn f32s [c bool y f32] f32 (let [x (if c 2.5 y)] x)) +(defn main [] i32 + (println (g true (i64 3))) + (println (g false (i64 9000000000))) + (println (h 0 (i64 1))) + (println (h 1 (i64 1))) + (println (h 2 (i64 9000000000))) + (println (m None)) + (println (m (Some (i64 9000000000)))) + (println (f32s true (f32 1.0))) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index a88787ea..8466b85e 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -558,6 +558,13 @@ let () = "programs/array-first-element.flan" first_out; outputs ~x86:true "an array literal's first element types the rest, x86" "programs/array-first-element.flan" first_out; + (* A literal arm takes the other arm's type. *) + let arm_out = + "4000000\n9000000000\n5000000000\n7\n9000000000\n3\n9000000000\n2.5\n" in + outputs "a literal arm takes the other arm's type" + "programs/literal-arm.flan" arm_out; + outputs ~x86:true "a literal arm takes the other arm's type, x86" + "programs/literal-arm.flan" arm_out; (* into. The count of pulls is the assertion a unit test cannot make: one pass, one call per element per stage it reaches, and no intermediate collection anywhere. The two show lines either side of it are the same