A literal arm of an if, a cond or a match takes its type from the arms that are not literals

This commit is contained in:
Joseph Ferano 2026-09-25 11:32:54 +07:00
parent 14bac84f53
commit 315125c677
3 changed files with 72 additions and 8 deletions

View File

@ -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,

View File

@ -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)

View File

@ -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