and hands back its deciding operand too, and both forms point refusals at the operand

FIX.org

@@ -444,16 +444,42 @@ rename. typed-flan branch freezes the static language pre-dyn.
    decided going in, one fixed on review and one left as the author's
    call:
 
-   - or's answer used to stay a strict bool where and's already carried a
+   - Neither and nor or handed back the operand that decided it.
-     non-bool dyn value through, Clojure-style — and's short-circuit
+     Clojure's rule is that both do; each answered a bare bool sentinel
-     sentinel sits in the else arm, so the real value's type wins there,
+     on its deciding path instead. and's "false" sat in the else arm, so
-     but or's sat in the then arm, the one check_if types first, so it
+     check_if typed the real branch first and boxed the sentinel to
-     decided the whole expression's type and a later non-bool dyn answer
+     match: an all-truthy and did carry its last dyn operand through,
-     hit the strict bool boundary and trapped. (or nil "x"), the
+     but a falsey one answered false where Clojure answers the falsey
-     canonical (or x default) idiom, crashed rather than answering "x".
+     operand — (and (box 1) (box nil) x) printed false, not nil. or's
-     FIXED, ad0f1fb: or now binds its test to a temp and answers the
+     "true" sat in the then arm, the one check_if types first, so the
-     temp, Clojure's own expansion, evaluating the test once and handing
+     sentinel decided the whole expression's type and a later non-bool
-     back whichever operand actually decided it.
+     dyn answer hit the strict bool boundary and trapped: (or nil "x"),
+     the canonical (or x default) idiom, crashed rather than answering
+     "x". FIXED for or in ad0f1fb and for and in this pass: both now
+     bind the test to a temp and answer the temp on the deciding path,
+     Clojure's own expansion — (let [t a] (if t t b)) for or and (let [t
+     a] (if t b t)) for and — evaluating each test exactly once. The
+     asymmetry between the two forms is fully closed; the survey program
+     (test/programs/dyn-if-truthy.flan) pins both, short-circuit and
+     single-evaluation included, and test_flan.ml pins both desugarings
+     down to the bound name and the bound value.
+
+     Two things came with that pass. The temp binding and the if it
+     feeds now carry the *operand's* loc rather than the whole form's,
+     which ad0f1fb had lost for or: (or (vec-new i32) v) blamed the
+     enclosing form at 3:13 and now points at the operand at 3:18, and
+     and's second operand gained the same precision. And, noted and not
+     acted on: with both arms of the desugared if now holding real
+     values, a dyn operand mixed with a typed bool one makes check_if
+     unify them by the then arm, so a non-bool dyn value on the losing
+     side traps at the strict bool boundary — (or false (box "s")) and
+     (and (box nil) some-bool) both do. Each form used to be safe in
+     exactly one of those directions, because the sentinel it answered
+     was a bool literal that boxed to fit the real branch; neither is
+     now, and they are at least symmetric about it. (and (box nil)
+     some-bool) printing false is the one previously-compiling behaviour
+     this pass changed. Making a bool arm and a dyn arm join as dyn is a
+     check_if question and the author's call, not settled here.
    - A bare keyword condition used to be checked with want:Bool from the
      start and refused by the keyword arm's enum-or-refuse case: ":kw is
      an enum member where an enum is expected and a dyn keyword

lib/check.ml

@@ -3179,8 +3179,9 @@ and check_recur ctx ~tail loc args =
    sugar built out of [Ast.If] in parse.ml, so they get this for free
    without a separate case. [and] and [or] are sugar too, and both their
    tests and their answers get this for free the same way — see
-   [shortcircuit] in parse.ml for how [or] carries its deciding operand
+   [shortcircuit] in parse.ml, where each binds its test to a temp and
-   through, the same way [and] always has.)
+   answers that temp on the path it decides, so the deciding operand
+   itself comes back rather than a bare bool.)
 
    A dyn scrutinee is tested for truthiness, Clojure's rule: nil and false
    are the only falsey values, and everything else — 0, "", an empty vec, an

lib/parse.ml

@@ -883,35 +883,55 @@ and cond f (args : Form.t list) : Ast.expr =
 
 (* Every test here is an [if]'s condition, so a dyn operand is truthy-tested
    (check.ml's check_truthy) exactly the way a bare [if]'s is, for both
-   [and] and [or]. The *answer* used to be asymmetric between them: [and]'s
+   [and] and [or]. The *answer* is the operand that decided the form, which
-   "false" sentinel sits in the else arm, so check_if picks the real
+   is Clojure's rule and needs the operand a second time: [(or a b)] is
-   branch's type first and boxes "false" to match it, which lets [and] hand
+   [(let [t a] (if t t b))] and [(and a b)] is [(let [t a] (if t b t))].
-   back the actual last dyn value, Clojure-style. [or] used to put its
+   The temp is what makes that a single evaluation — writing the operand
-   "true" sentinel in the then arm instead — the one check_if types first —
+   itself into the arm, as [(if a a b)] would, evaluates it twice.
-   so that sentinel decided the whole expression's type, and a later
+
+   Both used to answer a bare bool sentinel on the deciding path instead.
+   [and]'s "false" sentinel sat in the else arm, so check_if typed the real
+   branch first and boxed the sentinel to match: an all-truthy [and] did
+   hand back its last operand, but a falsey one answered [false] where
+   Clojure answers the falsey operand itself — (and 1 nil) said false, not
+   nil. [or]'s "true" sentinel sat in the then arm, the one check_if types
+   first, so the sentinel decided the whole expression's type and a later
    non-bool dyn answer hit the strict bool boundary instead of surviving as
-   itself: (or nil "x") traps rather than answering "x", exactly the
+   itself: (or nil "x") trapped rather than answering "x", exactly the
    canonical (or x default) idiom Clojure is reached for.
 
-   [or] now binds its test to a temp and asks the temp itself, the way
+   The locs are the operand's own, not the whole form's, because the temp's
-   Clojure's own or expands: [(or a b)] is [(let [t a] (if t t b))], not
+   [Var] node is what lands in the [if] condition and check_truthy reports
-   [(if a true b)]. The temp is what lets the answer be [a] itself without
+   the condition's loc when a typed operand is not a bool. Pointing that at
-   writing [a] a second time as the then arm — [(if a a b)] would evaluate
+   [f.loc] would blame the enclosing (and ...) for whichever operand is
-   it twice, once for the test and again for the answer — and it is the
+   actually wrong.
-   temp's own type check_if sees first, so [or] hands back the actual
+
-   truthy value the same way [and] hands back its own. *)
+   What answering the operand costs, for both forms alike: the two arms are
+   now both real values, so mixing a dyn operand with a typed bool one makes
+   check_if unify them, and the then arm decides. A non-bool dyn value on
+   the losing side then meets the strict bool boundary at run time —
+   (or false (box "s")) and (and (box nil) some-bool) both trap, verified on
+   this tree. Each form used to be safe in exactly one of those directions,
+   because the sentinel it answered was a bool literal that boxed to fit
+   whatever the real branch was; neither is now, and they are at least
+   symmetric about it. Making bool and dyn arms join as dyn is a check_if
+   question, noted in FIX.org under item 7 and not decided here. *)
 and shortcircuit f (args : Form.t list) ~is_and : Ast.expr =
   let mk e = { Ast.e; loc = f.loc } in
   let rec go = function
     | [] -> mk (Ast.Var (if is_and then "true" else "false"))
     | [ last ] -> expr last
     | x :: rest ->
-      if is_and then mk (Ast.If (expr x, go rest, Some (mk (Ast.Var "false"))))
+      let ex = expr x in
-      else
+      let t = fresh_temp () in
-        let t = fresh_temp () in
+      let tvar = { Ast.e = Ast.Var t; loc = ex.Ast.loc } in
-        let tvar = mk (Ast.Var t) in
+      let bind = { Ast.bname = t; bty = None; bval = ex; bloc = ex.Ast.loc } in
-        let bind = { Ast.bname = t; bty = None; bval = expr x; bloc = f.loc } in
+      let rest = go rest in
-        mk (Ast.Let ([ bind ], [ mk (Ast.If (tvar, tvar, Some (go rest))) ]))
+      let body =
+        if is_and then mk (Ast.If (tvar, rest, Some tvar))
+        else mk (Ast.If (tvar, tvar, Some rest))
+      in
+      mk (Ast.Let ([ bind ], [ body ]))
   in
   go args
 

test/programs/dyn-if-truthy.flan

@@ -7,18 +7,21 @@
 ;;;; The rule reaches every form built out of [if] under the hood -- [when],
 ;;;; [cond], [and] and [or] all desugar to it in parse.ml -- so their *tests*
 ;;;; need no separate case in check.ml and get exercised below through their
-;;;; own syntax rather than by inspecting the desugaring. [and]'s *answer*
+;;;; own syntax rather than by inspecting the desugaring. Their *answers*
-;;;; carries a non-bool dyn value through too, Clojure-style, because its
+;;;; are covered here too: both [and] and [or] hand back the operand that
-;;;; short-circuit sentinel is the else arm and the real value's type wins.
+;;;; decided them, Clojure-style, rather than a bare bool. Each used to
-;;;; [or] used to put its sentinel in the then arm instead, so a non-bool
+;;;; answer a sentinel on its deciding path instead -- [and]'s "false" sat
-;;;; dyn answer hit the strict bool boundary and traps -- (or nil "x"), the
+;;;; in the else arm, so an all-truthy [and] did carry its last dyn operand
-;;;; canonical Clojure (or x default) idiom, used to crash. [or] now binds
+;;;; through but a falsey one answered [false] where Clojure answers the
-;;;; its test to a temp and answers the temp itself, Clojure's own
+;;;; falsey operand itself, and [or]'s "true" sat in the then arm, the one
-;;;; expansion, so its answer carries a non-bool dyn value through exactly
+;;;; the checker types first, so a non-bool dyn answer hit the strict bool
-;;;; the way [and]'s does; both are exercised below, including the case
+;;;; boundary and trapped: (or nil "x"), the canonical Clojure (or x
-;;;; that used to be excluded here for being unsafe. [not] and [while] are
+;;;; default) idiom, used to crash. Both now bind the test to a temp and
-;;;; not [if] in disguise, so check_truthy is called at their own sites by
+;;;; answer the temp on the deciding path, Clojure's own expansion, which
-;;;; hand, and get their own coverage too.
+;;;; also evaluates each test exactly once -- pinned below, including the
+;;;; case that used to be excluded here for being unsafe. [not] and [while]
+;;;; are not [if] in disguise, so check_truthy is called at their own sites
+;;;; by hand, and get their own coverage too.
 ;;;;
 ;;;; A typed if keeps needing a strict bool -- that refusal, and its message,
 ;;;; is a checker test in test_flan.ml, not a row here, since a program that
@@ -33,6 +36,11 @@
 
 (defn truthy? [x] dyn (if x "truthy" "falsey"))
 
+;; Prints its tag, then answers its value unchanged. An operand written this
+;; way leaves a mark when it is evaluated, which is how the short-circuit
+;; rows below prove that a skipped operand really was skipped.
+(defn loud [tag x] dyn (println tag) x)
+
 (defn main [] i32
   ;; nil and false: the only two falsey dyn values. Everything else Clojure
   ;; calls truthy that C or Python would not: 0, "", an empty vec, an empty
@@ -68,11 +76,15 @@
   ;; and/or: also if in disguise, so each test along the chain is
   ;; truthy-tested the same way if's own is -- 0 and "" do not stop and,
   ;; only nil and false do; 0 does stop or, the way any truthy value does.
-  ;; Both hand back the actual operand that decided them, Clojure-style --
+  ;; Both hand back the actual operand that decided them, Clojure-style:
-  ;; and's answer is the last truthy operand itself (:kw here); or's is the
+  ;; and's is the falsey one that stopped it, or the last operand if none
-  ;; first truthy one (0, then "x") rather than a bare true.
+  ;; did; or's is the first truthy one, or the last operand if none was.
   (println (and (box 1) (box "") (box :kw)))
   (println (and (box 1) (box false) (box "unreached")))
+  ;; The falsey operand itself, not a bare false: nil comes back as nil.
+  (println (and (box 1) (box nil) (box "unreached")))
+  ;; 0 and "" are truthy, so neither stops and -- the last operand answers.
+  (println (and (box 0) (box "")))
   (println (or (box 0) (box false)))
   (println (or (box nil) (box false)))
   ;; The case excluded before the fix: a non-bool value stopping or and
@@ -81,6 +93,31 @@
   (println (or (box nil) (box "x")))
   (println (or (box 5) (box "unreached")))
 
+  ;; One operand is that operand, whatever it is -- no test, no sentinel.
+  (println (and (box nil)))
+  (println (and (box "")))
+  (println (or (box nil)))
+  (println (or (box 0)))
+  ;; No operands at all: the identity of each, and the one place a bare
+  ;; sentinel is still the answer -- (and) is true, (or) is false.
+  (println (and))
+  (println (or))
+
+  ;; Short-circuit proof. [loud] prints its tag before answering, so an
+  ;; operand that is never evaluated is an absent line, not a wrong value.
+  ;; and stops at the first falsey operand and or at the first truthy one,
+  ;; so the "unreached" tags below must never appear.
+  (println (and (box nil) (loud "and-unreached" 1)))
+  (println (and (loud "and-reached" 1) (box 2)))
+  (println (or (box 7) (loud "or-unreached" 1)))
+  (println (or (box nil) (loud "or-reached" 1)))
+  ;; The test is evaluated once, not twice. Here the loud operand is the one
+  ;; that decides the form, so it is both the test and the answer -- and it
+  ;; still prints exactly one line, which is what the temp binding buys over
+  ;; writing the operand into the arm a second time.
+  (println (and (loud "and-decider" nil) (box 3)))
+  (println (or (loud "or-decider" 9) (box 4)))
+
   ;; not: truthiness, negated -- true only for nil and false.
   (println (not (box nil)))
   (println (not (box false)))

test/test_acceptance.ml

@@ -1256,16 +1256,30 @@ let () =
        along for free because their tests desugar to [if] in parse.ml;
        [not] and [while] get the same treatment by hand in check.ml's
        check_truthy. [and] and [or] both hand back the actual operand that
-       decided them, Clojure-style -- [or] used to answer a bare bool
+       decided them, Clojure-style. Each used to answer a bare bool on its
-       instead, its short-circuit sentinel sitting in the arm check_if
+       deciding path instead: [and]'s "false" sentinel sat in the else arm,
-       types first, and a non-bool dyn value reaching that position (the
+       so an all-truthy [and] carried its last dyn operand through but a
-       canonical (or x default) idiom) used to trap rather than survive as
+       falsey one answered [false] rather than the falsey operand, and
-       itself; [or] now binds its test to a temp and answers the temp,
+       [or]'s "true" sentinel sat in the then arm, the one check_if types
-       fixing that. *)
+       first, so a non-bool dyn value reaching that position (the canonical
+       (or x default) idiom) trapped rather than surviving as itself. Both
+       now bind the test to a temp and answer the temp.
+
+       The empty lines in the middle are answers, not spacing: "" is a
+       truthy dyn value that [and] can hand back, and println prints it as
+       an empty line. The "loud" rows print a tag when an operand is
+       evaluated, so the tags that are absent here -- and-unreached,
+       or-unreached -- are the short-circuit proof, and each tag that is
+       present appears exactly once, which is the test-evaluated-once
+       proof. *)
     let dyn_if_truthy_out =
       "falsey\nfalsey\ntruthy\ntruthy\ntruthy\ntruthy\ntruthy\ntruthy\ntruthy\n\
-       truthy\ntruthy\ntruthy\nwhen 0 ran\nwhen empty-string ran\nb\nb\n:kw\n\
+       truthy\ntruthy\ntruthy\nwhen 0 ran\nwhen empty-string ran\nb\nb\n\
-       false\n0\nfalse\nx\n5\ntrue\ntrue\nfalse\nfalse\nfalse\n3\n2\n1\n"
+       :kw\nfalse\nnil\n\n0\nfalse\nx\n5\n\
+       nil\n\nnil\n0\ntrue\nfalse\n\
+       nil\nand-reached\n2\n7\nor-reached\n1\n\
+       and-decider\nnil\nor-decider\n9\n\
+       true\ntrue\nfalse\nfalse\nfalse\n3\n2\n1\n"
     in
     outputs "dyn if truthiness" "programs/dyn-if-truthy.flan" dyn_if_truthy_out;
     outputs ~opt:"-O0" "dyn if truthiness, -O0" "programs/dyn-if-truthy.flan"

test/test_flan.ml

@@ -350,17 +350,30 @@ let () =
    | If (_, _, Some { e = If (_, _, Some { e = Int 3L; _ }); _ }) -> ()
    | _ -> check "cond -> nested if with :else last" false);
 
-  (* and/or short-circuit, so they must not become calls *)
+  (* and/or short-circuit, so they must not become calls. Both bind the test
+     to a temp and answer the temp on the deciding path -- Clojure's own
+     expansion, (let [t a] (if t b t)) for and and (let [t a] (if t t b))
+     for or -- which is what hands back the actual deciding operand rather
+     than a bare bool, and what evaluates the test exactly once (M2 queue
+     item 7 and its review pass).
+
+     The bound name, the bound value and the arm are all pinned, not just
+     the shape: a desugaring that dropped the temp and wrote the operand
+     into the arm twice, (if a b a), would still match a pattern that left
+     the binding as [_]. *)
   (match (parse1 "(and a b)").e with
-   | If (_, _, Some { e = Var "false"; _ }) -> ()
+   | Let ([ { bname; bval = { e = Var "a"; _ }; _ } ],
+          [ { e = If ({ e = Var t1; _ },
+                      { e = Var "b"; _ },
+                      Some { e = Var t2; _ }); _ } ])
+     when bname = t1 && t1 = t2 -> ()
    | _ -> check "and short-circuits" false);
-  (* or binds its test to a temp and answers the temp itself -- Clojure's
-     own expansion, and what lets or hand back the actual truthy operand
-     rather than a bare true (M2 queue item 7's review pass). *)
   (match (parse1 "(or a b)").e with
-   | Let ([ _ ],
+   | Let ([ { bname; bval = { e = Var "a"; _ }; _ } ],
-          [ { e = If ({ e = Var t1; _ }, { e = Var t2; _ }, Some _); _ } ])
+          [ { e = If ({ e = Var t1; _ },
-     when t1 = t2 -> ()
+                      { e = Var t2; _ },
+                      Some { e = Var "b"; _ }); _ } ])
+     when bname = t1 && t1 = t2 -> ()
    | _ -> check "or short-circuits" false);
 
   (* ── Forms that bind or alter control are never calls ──────────── *)