include _abort as an expression

Python.thy

@@ -9,9 +9,9 @@ declare [[default_code_width = 2000]]
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (Python) Arith
 
-(* Panic *)
+(* Panic, by a helper function, since Code.abort occurs in expression position *)
 code_printing
-  constant Code.abort \<rightharpoonup> (Python) "raise RuntimeError(\"_\")"
+  constant Code.abort \<rightharpoonup> (Python) "'_abort"
 
 (* unit *)
 code_printing

code_python.ML

@@ -74,7 +74,7 @@ val python_reserved_words =
    "raise", "return", "try", "while", "with", "yield", "match", "case"]
 
   (* these are symbols we use in addition to the standard reserved words *) 
-  @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];;
+  @ ["dataclass", "Any", "Callable", "_unimplemented", "_abort", "functools"];;
 
 type eqtn = { 
   patterns: iterm list,       (* left hand side pattern list *)
@@ -1067,7 +1067,10 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms,
         val unimplemented_def = Pretty.chunks
           [Pretty.str "def _unimplemented(name):",
            indent_block 4 (Pretty.str "raise NotImplementedError(name)")]
-      in ([mod_name ^ ".py"], Pretty.chunks2 (imports_block :: unimplemented_def :: stmt_ps))
+        val abort_def = Pretty.chunks
+          [Pretty.str "def _abort(msg, thunk):",
+           indent_block 4 (Pretty.str "raise RuntimeError(msg)")]
+      in ([mod_name ^ ".py"], Pretty.chunks2 (imports_block :: unimplemented_def :: abort_def :: stmt_ps))
       end;
 
     val p = map print_one_module module_stmts

test/diff/golden/Python_Examples.Example/Example.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Red:
     pass

test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py

@@ -9,6 +9,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def weight(a_dict, x, xa1):
     match (x, xa1):
         case (xa, []):

test/diff/golden/Python_Examples.Example_class_dicts/HOL.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class equal:
     equala: Callable

test/diff/golden/Python_Examples.Example_class_dicts/Int.py

@@ -7,6 +7,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @functools.cache
 def equal_int():
     return HOL.equal(equala = lambda a, b: (a == b))

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class ord:
     less_eq: Callable

test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def equal_proda(a_dict, b_dict, x0, x1):
     match (x0, x1):
         case ((x1a, x2), (y1, y2)):

test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py

@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def sup_apply_bool(b):
     return (b)
 

test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class super_op:
     sup_apply: Callable

test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def cn_add(x, y):
     return ((x + y))
 

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py

@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def swap(x0):
     match x0:
         case Product_Type.Pair(x, y):

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Nil:
     pass

test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Pair:
     a: Any

test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py

@@ -7,6 +7,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def sum_ends(a):
     return (((a[0]) + (a[(max(0, (len(a)) - 1))])))
 

test/diff/golden/Python_Examples.Example_iarray/HOL.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class equal:
     equala: Callable

test/diff/golden/Python_Examples.Example_iarray/IArray.py

@@ -6,5 +6,8 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def equal_iarray(a_dict, asa, bs):
     return (List.equal_list(a_dict, (list(asa)), (list(bs))))

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

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def equal_list(a_dict, x0, x1):
     match (x0, x1):
         case ([], [x21, *x22]):

test/diff/golden/Python_Examples.Example_iarray/Nat.py

@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @functools.cache
 def equal_nat():
     return HOL.equal(equala = lambda a, b: (a == b))

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 product = ((6 * 7))
 
 def checksum(x, y):

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py

@@ -8,6 +8,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @functools.cache
 def one_integer():
     return Groups.one(onea = lambda : 1)

test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py

@@ -6,6 +6,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 test_bit = (Arith.bit_integer(10, 1))
 
 test_sgn = (Arith.sgn_integer(-42))

test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class one:
     onea: Callable

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class power:
     one_power: Any

test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def doubled(xs):
     return (list(map(lambda n: (n + n), xs)))
 

test/diff/golden/Python_Examples.Example_lambda_case/Option.py

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class Nonea:
     pass

test/diff/golden/Python_Examples.Example_lists/Example_lists.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 example = ([1, 2, 3])
 
 def prepend(x, xs):

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_nat/Example_nat.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 nat_sum = ((6 + 7))
 
 nat_eq_test = ((4 == 4))

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def peel_positive_head(x0):
     match x0:
         case []:

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

@@ -4,6 +4,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 @dataclass(frozen=True)
 class One:
     pass

test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py

@@ -5,6 +5,9 @@
 def _unimplemented(name):
     raise NotImplementedError(name)
 
+def _abort(msg, thunk):
+    raise RuntimeError(msg)
+
 def fact(n):
     if ((n == 0)):
         return (1)