Keep short-circuit evaluation when hoisting case expressions

ROOT

@@ -40,6 +40,7 @@ session Python_Examples in "examples" = Python +
     Example_class_dicts
     Example_iarray
     Example_tail_calls
+    Example_short_circuit
   export_files (in "python_out") "*:**"
 
 session Python_Test_Quick in "test/quick" = Python +

code_python.ML

@@ -215,7 +215,13 @@ fun print_python_stmt undefineds const_syntax reserved args_num
 
     (* A "preamble" entry is a statement that needs to run before the
        expression that depends on it *)
-    datatype python_preamble = PBind of string * iterm | PRaw of Pretty.T;
+    (* A branch of a short-circuiting connective: a term, or a fixed truth value *)
+    datatype python_branch = BTerm of iterm | BBool of bool;
+
+    datatype python_preamble = PBind of string * iterm | PRaw of Pretty.T
+      (* `x = (cond ? then : else)`, printed as an if statement so that only the
+         branch that is taken gets evaluated *)
+      | PIf of string * iterm * python_branch * python_branch;
 
     val fallthrough_arm = Pretty.chunks
       [Pretty.block [Pretty.str "case ", Pretty.str "_", Pretty.str ":"],
@@ -363,13 +369,35 @@ fun print_python_stmt undefineds const_syntax reserved args_num
         val body = Pretty.chunks (preamble @ [body_pretty vars'])
       in (header, vars', body) end
 
+    (* The connectives are printed as Python's short-circuiting `and`/`or`, so the
+       right operand is only evaluated when the left one does not decide the result.
+       Hoisting statements out of the right operand would evaluate them
+       unconditionally; such a connective is turned into an if statement instead. *)
+    and short_circuit t =
+      case Code_Thingol.unfold_const_app t of
+        SOME ({ sym = Constant c, ... }, [a, b]) =>
+          if is_stmt_free b then NONE
+          else (case c of
+              "HOL.conj" => SOME (a, BTerm b, BBool false)
+            | "HOL.disj" => SOME (a, BBool true, BTerm b)
+            | "HOL.implies" => SOME (a, BTerm b, BBool true)
+            | _ => NONE)
+      | _ => NONE
+
     and anf_term vars (t as IConst _) = ([], vars, t)
       | anf_term vars (t as IVar _) = ([], vars, t)
-      | anf_term vars (t1 `$ t2) =
-          let
-            val (b1, vars1, t1') = anf_term vars t1;
-            val (b2, vars2, t2') = anf_term vars1 t2;
-          in (b1 @ b2, vars2, t1' `$ t2') end
+      | anf_term vars (t as t1 `$ t2) =
+          (case short_circuit t of
+            SOME (cond, t_branch, e_branch) =>
+              let
+                val (bc, vars1, cond') = anf_term vars cond;
+                val (x, vars2) = invent_name vars1 "x";
+              in (bc @ [PIf (x, cond', t_branch, e_branch)], vars2, IVar (SOME x)) end
+          | NONE =>
+              let
+                val (b1, vars1, t1') = anf_term vars t1;
+                val (b2, vars2, t2') = anf_term vars1 t2;
+              in (b1 @ b2, vars2, t1' `$ t2') end)
       | anf_term vars (t as (_, _) `|=> (_, _)) =
           if is_stmt_free t
           then ([], vars, t)
@@ -461,6 +489,19 @@ fun print_python_stmt undefineds const_syntax reserved args_num
 
     and print_preamble some_thm vars (PBind (name, t)) = print_binding some_thm vars (name, t)
       | print_preamble _ _ (PRaw p) = p
+      | print_preamble some_thm vars (PIf (name, cond, t_branch, e_branch)) =
+          let
+            fun branch (BTerm t) = print_binding some_thm vars (name, t)
+              | branch (BBool b) =
+                  Pretty.str (name ^ " = (" ^ (if b then "True" else "False") ^ ")")
+          in
+            Pretty.chunks [
+              Pretty.block [Pretty.str "if (",
+                print_python_expr const_syntax some_thm vars NOBR cond, Pretty.str "):"],
+              indent_block 4 (branch t_branch),
+              Pretty.str "else:",
+              indent_block 4 (branch e_branch)]
+          end
 
     and print_case_block some_thm finish vars target clauses =
       let

examples/Example_short_circuit.thy

@@ -0,0 +1,53 @@
+theory Example_short_circuit
+  imports Main "Python.Python_Setup"
+begin
+
+text \<open>
+  A case expression in the right operand of a short-circuiting connective
+  (conjunction, disjunction, implication) must only be evaluated if the left
+  operand does not already determine the result. Here the left operand guards
+  @{term "hd xs"}, which fails on the empty list.
+\<close>
+
+definition conj_case :: "nat list \<Rightarrow> bool" where
+  "conj_case xs = (xs \<noteq> [] \<and> (case hd xs of 0 \<Rightarrow> True | Suc _ \<Rightarrow> False))"
+
+definition disj_case :: "nat list \<Rightarrow> bool" where
+  "disj_case xs = (xs = [] \<or> (case hd xs of 0 \<Rightarrow> True | Suc _ \<Rightarrow> False))"
+
+definition impl_case :: "nat list \<Rightarrow> bool" where
+  "impl_case xs = (xs \<noteq> [] \<longrightarrow> (case hd xs of 0 \<Rightarrow> True | Suc _ \<Rightarrow> False))"
+
+text \<open>The same with a case on a datatype instead of @{typ nat}.\<close>
+
+definition conj_case_list :: "nat list list \<Rightarrow> bool" where
+  "conj_case_list xss = (xss \<noteq> [] \<and> (case hd xss of [] \<Rightarrow> True | _ \<Rightarrow> False))"
+
+text \<open>Control: the guarded case in a branch of if-then-else.\<close>
+
+definition if_case :: "nat list \<Rightarrow> bool" where
+  "if_case xs = (if xs = [] then False else (case hd xs of 0 \<Rightarrow> True | Suc _ \<Rightarrow> False))"
+
+text \<open>Expected values, checked by Isabelle's own code generator (SML).\<close>
+
+lemma "conj_case [] = False" by eval
+lemma "disj_case [] = True" by eval
+lemma "impl_case [] = True" by eval
+lemma "conj_case_list [] = False" by eval
+lemma "if_case [] = False" by eval
+
+definition conj_case_empty :: bool where "conj_case_empty = conj_case []"
+definition conj_case_zero :: bool where "conj_case_zero = conj_case [0]"
+definition disj_case_empty :: bool where "disj_case_empty = disj_case []"
+definition disj_case_three :: bool where "disj_case_three = disj_case [3]"
+definition impl_case_empty :: bool where "impl_case_empty = impl_case []"
+definition conj_case_list_empty :: bool where "conj_case_list_empty = conj_case_list []"
+definition if_case_empty :: bool where "if_case_empty = if_case []"
+
+export_code
+  conj_case disj_case impl_case conj_case_list if_case
+  conj_case_empty conj_case_zero disj_case_empty disj_case_three
+  impl_case_empty conj_case_list_empty if_case_empty
+  in Python file_prefix "."
+
+end

test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py

@@ -0,0 +1,76 @@
+# Generated by Isabelle from theory Python_Examples.Example_short_circuit; do not edit
+
+from dataclasses import dataclass
+from typing import Any, Callable
+import Num
+import List
+
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
+def if_case(xs):
+    if (List.null(xs)):
+        return (False)
+    else:
+        if ((List.hd(xs) == 0)):
+            return (True)
+        else:
+            return (False)
+
+def conj_case(xs):
+    if (not List.null(xs)):
+        if ((List.hd(xs) == 0)):
+            x = (True)
+        else:
+            x = (False)
+    else:
+        x = (False)
+    return (x)
+
+def disj_case(xs):
+    if (List.null(xs)):
+        x = (True)
+    else:
+        if ((List.hd(xs) == 0)):
+            x = (True)
+        else:
+            x = (False)
+    return (x)
+
+def impl_case(xs):
+    if (not List.null(xs)):
+        if ((List.hd(xs) == 0)):
+            x = (True)
+        else:
+            x = (False)
+    else:
+        x = (True)
+    return (x)
+
+if_case_empty = (if_case([]))
+
+def conj_case_list(xss):
+    if (not List.null(xss)):
+        target = (List.hd(xss))
+        match target:
+            case []:
+                x = (True)
+            case [_, *_]:
+                x = (False)
+            case _:
+                raise RuntimeError("match failed")
+    else:
+        x = (False)
+    return (x)
+
+conj_case_zero = (conj_case([0]))
+
+conj_case_empty = (conj_case([]))
+
+disj_case_empty = (disj_case([]))
+
+disj_case_three = (disj_case([3]))
+
+impl_case_empty = (impl_case([]))
+
+conj_case_list_empty = (conj_case_list([]))

test/diff/golden/Python_Examples.Example_short_circuit/List.py

@@ -0,0 +1,23 @@
+# Generated by Isabelle from theory HOL.List; do not edit
+
+from dataclasses import dataclass
+from typing import Any, Callable
+
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
+def null(x0):
+    match x0:
+        case []:
+            return (True)
+        case [x, *xs]:
+            return (False)
+        case _:
+            raise RuntimeError("match failed")
+
+def hd(x0):
+    match x0:
+        case [x21, *x22]:
+            return (x21)
+        case _:
+            raise RuntimeError("match failed")

test/diff/golden/Python_Examples.Example_short_circuit/Num.py

@@ -0,0 +1,17 @@
+# Generated by Isabelle from theory HOL.Num; do not edit
+
+from dataclasses import dataclass
+from typing import Any, Callable
+
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
+@dataclass(frozen=True)
+class One:
+    pass
+@dataclass(frozen=True)
+class Bit0:
+    a: Any
+@dataclass(frozen=True)
+class Bit1:
+    a: Any