From bb2608a787da802f62c088d6e4b5fa42ce2d4ccd Mon Sep 17 00:00:00 2001 From: Nikolaus Huber Date: Mon, 26 Oct 2026 15:31:48 +0000 Subject: [PATCH 1/4] add example for failing short circuit cases --- ROOT | 1 + examples/Example_short_circuit.thy | 53 ++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+) create mode 100644 examples/Example_short_circuit.thy diff --git a/ROOT b/ROOT index db4d24b..593f132 100644 --- a/ROOT +++ b/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 + diff --git a/examples/Example_short_circuit.thy b/examples/Example_short_circuit.thy new file mode 100644 index 0000000..073111a --- /dev/null +++ b/examples/Example_short_circuit.thy @@ -0,0 +1,53 @@ +theory Example_short_circuit + imports Main "Python.Python_Setup" +begin + +text \ + 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. +\ + +definition conj_case :: "nat list \ bool" where + "conj_case xs = (xs \ [] \ (case hd xs of 0 \ True | Suc _ \ False))" + +definition disj_case :: "nat list \ bool" where + "disj_case xs = (xs = [] \ (case hd xs of 0 \ True | Suc _ \ False))" + +definition impl_case :: "nat list \ bool" where + "impl_case xs = (xs \ [] \ (case hd xs of 0 \ True | Suc _ \ False))" + +text \The same with a case on a datatype instead of @{typ nat}.\ + +definition conj_case_list :: "nat list list \ bool" where + "conj_case_list xss = (xss \ [] \ (case hd xss of [] \ True | _ \ False))" + +text \Control: the guarded case in a branch of if-then-else.\ + +definition if_case :: "nat list \ bool" where + "if_case xs = (if xs = [] then False else (case hd xs of 0 \ True | Suc _ \ False))" + +text \Expected values, checked by Isabelle's own code generator (SML).\ + +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 From 60de7b1cf58cec3feaf39a4493ccc6775dc5b84d Mon Sep 17 00:00:00 2001 From: Nikolaus Huber Date: Mon, 26 Oct 2026 15:33:26 +0000 Subject: [PATCH 2/4] add new example to golden --- .../Example_short_circuit.py | 64 +++++++++++++++++++ .../List.py | 23 +++++++ .../Num.py | 17 +++++ 3 files changed, 104 insertions(+) create mode 100644 test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py create mode 100644 test/diff/golden/Python_Examples.Example_short_circuit/List.py create mode 100644 test/diff/golden/Python_Examples.Example_short_circuit/Num.py diff --git a/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py b/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py new file mode 100644 index 0000000..312bf9b --- /dev/null +++ b/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py @@ -0,0 +1,64 @@ +# 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 ((List.hd(xs) == 0)): + x = (True) + else: + x = (False) + return (not List.null(xs) and x) + +def disj_case(xs): + if ((List.hd(xs) == 0)): + x = (True) + else: + x = (False) + return (List.null(xs) or x) + +def impl_case(xs): + if ((List.hd(xs) == 0)): + x = (True) + else: + x = (False) + return ((not (not List.null(xs)) or x)) + +if_case_empty = (if_case([])) + +def conj_case_list(xss): + target = (List.hd(xss)) + match target: + case []: + x = (True) + case [_, *_]: + x = (False) + case _: + raise RuntimeError("match failed") + return (not List.null(xss) and 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([])) diff --git a/test/diff/golden/Python_Examples.Example_short_circuit/List.py b/test/diff/golden/Python_Examples.Example_short_circuit/List.py new file mode 100644 index 0000000..54be781 --- /dev/null +++ b/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") diff --git a/test/diff/golden/Python_Examples.Example_short_circuit/Num.py b/test/diff/golden/Python_Examples.Example_short_circuit/Num.py new file mode 100644 index 0000000..b751fd5 --- /dev/null +++ b/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 From 73e8e111bf256d9c4df3bd40ace3fcc911f258e1 Mon Sep 17 00:00:00 2001 From: Nikolaus Huber Date: Mon, 26 Oct 2026 15:45:27 +0000 Subject: [PATCH 3/4] prevent hoisting of short-circuits --- code_python.ML | 53 ++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 47 insertions(+), 6 deletions(-) diff --git a/code_python.ML b/code_python.ML index ee78e53..6e7906f 100644 --- a/code_python.ML +++ b/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 From e7fb63d7e2ae3582ef03319b8a36c292bfd06d62 Mon Sep 17 00:00:00 2001 From: Nikolaus Huber Date: Mon, 26 Oct 2026 15:46:04 +0000 Subject: [PATCH 4/4] reseed diff tests --- .../Example_short_circuit.py | 50 ++++++++++++------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py b/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py index 312bf9b..4770045 100644 --- a/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py +++ b/test/diff/golden/Python_Examples.Example_short_circuit/Example_short_circuit.py @@ -18,38 +18,50 @@ def if_case(xs): return (False) def conj_case(xs): - if ((List.hd(xs) == 0)): - x = (True) + if (not List.null(xs)): + if ((List.hd(xs) == 0)): + x = (True) + else: + x = (False) else: x = (False) - return (not List.null(xs) and x) + return (x) def disj_case(xs): - if ((List.hd(xs) == 0)): + if (List.null(xs)): x = (True) else: - x = (False) - return (List.null(xs) or x) + if ((List.hd(xs) == 0)): + x = (True) + else: + x = (False) + return (x) def impl_case(xs): - if ((List.hd(xs) == 0)): - x = (True) + if (not List.null(xs)): + if ((List.hd(xs) == 0)): + x = (True) + else: + x = (False) else: - x = (False) - return ((not (not List.null(xs)) or x)) + x = (True) + return (x) if_case_empty = (if_case([])) def conj_case_list(xss): - target = (List.hd(xss)) - match target: - case []: - x = (True) - case [_, *_]: - x = (False) - case _: - raise RuntimeError("match failed") - return (not List.null(xss) and x) + 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]))