From 69255d0c593a2f629a4b22925befaa35ea37a4b2 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 07:09:11 +0100 Subject: [PATCH 01/30] Native characters, reserved builtins and undefined as stub Python_Setup imports Code_Abstract_Char and prints char as a one-character string, with chr and ord for the abstract constructor and projection, each character constant as a string literal, and explode and implode as list and join. Python's builtins are reserved in the generator, so a generated name no longer shadows int, str, ord or filter in its module; the per-theory code_reserved lines go. HOL.undefined is an intentionally unimplemented symbol, printed as a stub without the warning for a function without code equations. --- Python.thy | 5 +++ Python_IArray.thy | 2 - Python_Setup.thy | 25 ++++++++++++- README.md | 5 ++- ROOT | 2 + code_python.ML | 27 +++++++++++++- examples/Example_builtin_names.thy | 16 ++++++++ examples/Example_chars.thy | 25 +++++++++++++ .../Example_builtin_names.py | 37 +++++++++++++++++++ .../Num.py | 15 ++++++++ .../Python_Examples.Example_chars/Arith.py | 8 ++++ .../Example_chars.py | 20 ++++++++++ .../Int.py | 2 +- .../Orderings.py | 2 +- .../Example_no_eqs.py | 2 +- .../Example_tail_calls.py | 2 +- .../loops/Example_tail_calls_loops.py | 2 +- test/quick/Quick_Test.thy | 14 +++++++ test/quick/run_test.py | 26 +++++++++++++ 19 files changed, 225 insertions(+), 12 deletions(-) create mode 100644 examples/Example_builtin_names.thy create mode 100644 examples/Example_chars.thy create mode 100644 test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py create mode 100644 test/diff/golden/Python_Examples.Example_builtin_names/Num.py create mode 100644 test/diff/golden/Python_Examples.Example_chars/Arith.py create mode 100644 test/diff/golden/Python_Examples.Example_chars/Example_chars.py diff --git a/Python.thy b/Python.thy index 278b140..4932f8d 100644 --- a/Python.thy +++ b/Python.thy @@ -13,6 +13,11 @@ code_identifier code_printing constant Code.abort \ (Python) "raise RuntimeError(\"_\")" +(* Print undefined as an unimplemented stub, without the warning for a function without code equations *) +setup \ + Code_Python.add_undefined_sym \<^const_name>\HOL.undefined\ +\ + (* unit *) code_printing type_constructor Product_Type.unit \ (Python) "None" diff --git a/Python_IArray.thy b/Python_IArray.thy index bdb2d6a..328896a 100644 --- a/Python_IArray.thy +++ b/Python_IArray.thy @@ -12,8 +12,6 @@ text \ depend on HOL-Library.IArray. \ -code_reserved (Python) tuple range all any - code_printing type_constructor iarray \ (Python) "_ tuple" | constant IArray \ (Python) "tuple'(_')" diff --git a/Python_Setup.thy b/Python_Setup.thy index 69499d9..9ac9c9f 100644 --- a/Python_Setup.thy +++ b/Python_Setup.thy @@ -1,5 +1,6 @@ theory Python_Setup imports Python "HOL-Library.Code_Target_Int" "HOL-Library.Code_Target_Nat" + "HOL-Library.Code_Abstract_Char" begin code_identifier @@ -122,8 +123,28 @@ setup \ \ -(* Python builtins used by the printings in this theory; generated names must not shadow them *) -code_reserved (Python) len list map max min abs divmod +(* Characters, as one-character strings *) +code_printing + type_constructor char \ (Python) "str" + | constant Code_Abstract_Char.Chr \ (Python) "chr'(_')" + | constant String.integer_of_char \ (Python) "ord'(_')" + | constant "HOL.equal :: char \ char \ bool" \ (Python) infix 4 "==" + | constant "(\) :: char \ char \ bool" \ (Python) infixl 35 "<=" + | constant "(<) :: char \ char \ bool" \ (Python) infixl 35 "<" + | constant String.explode \ (Python) "list'(_')" + | constant String.implode \ (Python) "\"\".join'(_')" + +(* Each character constant of Code_Abstract_Char as a string literal *) +setup \ + let + fun literal n = + if 32 <= n andalso n < 127 then Code_Python.print_python_string (String.str (Char.chr n)) + else quote ("\\x" ^ align_right "0" 2 (Int.fmt StringCvt.HEX n)); + fun printing n = Code_Target.set_printings (Code_Symbol.Constant + ("Code_Abstract_Char.Char_" ^ String_Syntax.hex n, + [("Python", SOME (Code_Printer.plain_const_syntax (literal n)))])); + in fold printing (0 upto 255) end +\ (* Lists *) code_printing diff --git a/README.md b/README.md index 6da392c..beaaecb 100644 --- a/README.md +++ b/README.md @@ -40,8 +40,9 @@ things. `Python.Python_Setup` includes additional custom code printers to utilise Python native integers for `int` and `nat`, as well as using Python's own -list and tuple data types. Most people will probably want to use this setup for -code generation. +list and tuple data types, and one-character strings for `char`, so that a +`string` is a list of one-character strings. Most people will probably want to +use this setup for code generation. ### Tail calls as loops diff --git a/ROOT b/ROOT index db4d24b..c660d6d 100644 --- a/ROOT +++ b/ROOT @@ -40,6 +40,8 @@ session Python_Examples in "examples" = Python + Example_class_dicts Example_iarray Example_tail_calls + Example_chars + Example_builtin_names export_files (in "python_out") "*:**" session Python_Test_Quick in "test/quick" = Python + diff --git a/code_python.ML b/code_python.ML index de72bae..2b031f7 100644 --- a/code_python.ML +++ b/code_python.ML @@ -4,6 +4,7 @@ sig val add_transparent_wrapper_sym: string -> theory -> theory val add_undefined_sym: string -> theory -> theory val enable_native_encoding: string -> theory -> theory + val print_python_string: string -> string val tail_calls: bool Config.T end; @@ -76,6 +77,30 @@ val python_reserved_words = (* these are symbols we use in addition to the standard reserved words *) @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];; +(* Python builtins, which a generated name must not shadow in its module *) +val python_builtins = + ["ArithmeticError", "AssertionError", "AttributeError", "BaseException", "BaseExceptionGroup", + "BlockingIOError", "BrokenPipeError", "BufferError", "BytesWarning", "ChildProcessError", + "ConnectionAbortedError", "ConnectionError", "ConnectionRefusedError", "ConnectionResetError", + "DeprecationWarning", "EOFError", "Ellipsis", "EncodingWarning", "EnvironmentError", "Exception", + "ExceptionGroup", "FileExistsError", "FileNotFoundError", "FloatingPointError", "FutureWarning", + "GeneratorExit", "IOError", "ImportError", "ImportWarning", "IndentationError", "IndexError", + "InterruptedError", "IsADirectoryError", "KeyError", "KeyboardInterrupt", "LookupError", "MemoryError", + "ModuleNotFoundError", "NameError", "NotADirectoryError", "NotImplemented", "NotImplementedError", + "OSError", "OverflowError", "PendingDeprecationWarning", "PermissionError", "ProcessLookupError", + "PythonFinalizationError", "RecursionError", "ReferenceError", "ResourceWarning", "RuntimeError", + "RuntimeWarning", "StopAsyncIteration", "StopIteration", "SyntaxError", "SyntaxWarning", "SystemError", + "SystemExit", "TabError", "TimeoutError", "TypeError", "UnboundLocalError", "UnicodeDecodeError", + "UnicodeEncodeError", "UnicodeError", "UnicodeTranslateError", "UnicodeWarning", "UserWarning", + "ValueError", "Warning", "ZeroDivisionError", "abs", "aiter", "all", "anext", "any", "ascii", "bin", + "bool", "breakpoint", "bytearray", "bytes", "callable", "chr", "classmethod", "compile", "complex", + "copyright", "credits", "delattr", "dict", "dir", "divmod", "enumerate", "eval", "exec", "exit", + "filter", "float", "format", "frozenset", "getattr", "globals", "hasattr", "hash", "help", "hex", "id", + "input", "int", "isinstance", "issubclass", "iter", "len", "license", "list", "locals", "map", "max", + "memoryview", "min", "next", "object", "oct", "open", "ord", "pow", "print", "property", "quit", "range", + "repr", "reversed", "round", "set", "setattr", "slice", "sorted", "staticmethod", "str", "sum", "super", + "tuple", "type", "vars", "zip"]; + type eqtn = { patterns: iterm list, (* left hand side pattern list *) rhs: iterm, (* rhs expr *) @@ -1089,6 +1114,6 @@ val _ = Theory.setup run_command = Code_Target.run_command_bash (fn module_name => "python3 -m py_compile " ^ Bash.string module_name ^ "/*.py")}, evaluation_args = []}) - #> fold (Code_Target.add_reserved target) python_reserved_words); + #> fold (Code_Target.add_reserved target) (python_reserved_words @ python_builtins)); end; (* struct *) diff --git a/examples/Example_builtin_names.thy b/examples/Example_builtin_names.thy new file mode 100644 index 0000000..1a5a2c1 --- /dev/null +++ b/examples/Example_builtin_names.thy @@ -0,0 +1,16 @@ +theory Example_builtin_names + imports Main "Python.Python_Setup" +begin + +datatype prim = int | str | object + +fun len :: "prim list \ nat" where + "len [] = 0" | + "len (_ # ps) = Suc (len ps)" + +definition hash :: "prim \ nat" where + "hash p = (case p of int \ 0 | str \ 1 | object \ 2)" + +export_code len hash in Python file_prefix "." + +end diff --git a/examples/Example_chars.thy b/examples/Example_chars.thy new file mode 100644 index 0000000..169419f --- /dev/null +++ b/examples/Example_chars.thy @@ -0,0 +1,25 @@ +theory Example_chars + imports Main "Python.Python_Setup" +begin + +definition greeting :: string where + "greeting = ''hello''" + +definition is_digit :: "char \ bool" where + "is_digit c = (CHR ''0'' \ c \ c \ CHR ''9'')" + +definition code :: "char \ nat" where + "code c = of_char c" + +definition literal :: String.literal where + "literal = String.implode greeting" + +definition chars :: string where + "chars = String.explode (STR ''hi'')" + +definition newline :: char where + "newline = CHR 0x0A" + +export_code greeting is_digit code literal chars newline in Python file_prefix "." + +end diff --git a/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py b/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py new file mode 100644 index 0000000..7202343 --- /dev/null +++ b/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py @@ -0,0 +1,37 @@ +from dataclasses import dataclass +from typing import Any, Callable +import Num + +def _unimplemented(name): + raise NotImplementedError(name) + +@dataclass(frozen=True) +class inta: + pass +@dataclass(frozen=True) +class stra: + pass +@dataclass(frozen=True) +class objecta: + pass + +def lena(x0): + match x0: + case []: + return (0) + case [uu, *ps]: + return ((lena(ps) + 1)) + case _: + raise RuntimeError("match failed") + +def hasha(p): + target = (p) + match target: + case inta(): + return (0) + case stra(): + return (1) + case objecta(): + return (2) + case _: + raise RuntimeError("match failed") diff --git a/test/diff/golden/Python_Examples.Example_builtin_names/Num.py b/test/diff/golden/Python_Examples.Example_builtin_names/Num.py new file mode 100644 index 0000000..fc191a7 --- /dev/null +++ b/test/diff/golden/Python_Examples.Example_builtin_names/Num.py @@ -0,0 +1,15 @@ +from dataclasses import dataclass +from typing import Any, Callable + +def _unimplemented(name): + raise NotImplementedError(name) + +@dataclass(frozen=True) +class One: + pass +@dataclass(frozen=True) +class Bit0: + a: Any +@dataclass(frozen=True) +class Bit1: + a: Any diff --git a/test/diff/golden/Python_Examples.Example_chars/Arith.py b/test/diff/golden/Python_Examples.Example_chars/Arith.py new file mode 100644 index 0000000..e096457 --- /dev/null +++ b/test/diff/golden/Python_Examples.Example_chars/Arith.py @@ -0,0 +1,8 @@ +from dataclasses import dataclass +from typing import Any, Callable + +def _unimplemented(name): + raise NotImplementedError(name) + +def nat_of_char(c): + return ((ord(c))) diff --git a/test/diff/golden/Python_Examples.Example_chars/Example_chars.py b/test/diff/golden/Python_Examples.Example_chars/Example_chars.py new file mode 100644 index 0000000..d961a55 --- /dev/null +++ b/test/diff/golden/Python_Examples.Example_chars/Example_chars.py @@ -0,0 +1,20 @@ +from dataclasses import dataclass +from typing import Any, Callable +import Arith + +def _unimplemented(name): + raise NotImplementedError(name) + +def code(c): + return (Arith.nat_of_char(c)) + +chars = (list("hi")) + +greeting = (["h", "e", "l", "l", "o"]) + +literal = ("".join(greeting)) + +newline = ("\x0A") + +def is_digit(c): + return ("0" <= c and c <= "9") diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py index d828248..c917cb9 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py @@ -13,7 +13,7 @@ def equal_int(): @functools.cache def ord_int(): - return Orderings.ord(less_eq = lambda a, b: (a <= b ), less = lambda a, b: (a < b)) + return Orderings.orda(less_eq = lambda a, b: (a <= b ), less = lambda a, b: (a < b)) @functools.cache def preorder_int(): diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py index 3ec0149..cca9ae9 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class ord: +class orda: less_eq: Callable less: Callable diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py index bdb77e2..2a3fafb 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py @@ -5,4 +5,4 @@ def _unimplemented(name): raise NotImplementedError(name) -uses_undefined = (HOL.undefined()) +uses_undefined = (_unimplemented("undefined")) diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py index ed0efe7..3d725aa 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class ord: +class orda: less_eq: Callable less: Callable diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py index 1cd3db1..7e60feb 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class ord: +class orda: less_eq: Callable less: Callable diff --git a/test/quick/Quick_Test.thy b/test/quick/Quick_Test.thy index b9a8d20..e7d5659 100644 --- a/test/quick/Quick_Test.thy +++ b/test/quick/Quick_Test.thy @@ -264,6 +264,19 @@ definition twice_twice :: "'a::plus \ 'a" where "twice_twice = (\x. x + x) \ (\x. x + x)" definition e_twice_twice :: int where "e_twice_twice = twice_twice 3" +section \Characters\ + +definition ch_greeting :: string where "ch_greeting = ''hi''" +definition ch_is_digit :: "char \ bool" where "ch_is_digit c = (CHR ''0'' \ c \ c \ CHR ''9'')" +definition ch_digit_yes :: bool where "ch_digit_yes = ch_is_digit (CHR ''7'')" +definition ch_digit_no :: bool where "ch_digit_no = ch_is_digit (CHR ''x'')" +definition ch_code_A :: nat where "ch_code_A = of_char (CHR ''A'')" +definition ch_literal :: String.literal where "ch_literal = String.implode ch_greeting" +definition ch_chars :: string where "ch_chars = String.explode (STR ''ab'')" +definition ch_newline :: char where "ch_newline = CHR 0x0A" +definition ch_quote :: char where "ch_quote = CHR 0x22" +definition ch_high :: char where "ch_high = CHR 0xE9" + export_code t_point t_swap t_add_points t_points_sum i_quotient_neg i_remainder_neg i_checksum @@ -286,6 +299,7 @@ export_code ia_nth ia_grid ia_get ia_rows ia_head ia_any_neg z_int_div z_int_mod z_nat_div z_nat_mod z_int_floor l_shadow_none l_shadow_some c_boxed e_twice_twice + ch_greeting ch_digit_yes ch_digit_no ch_code_A ch_literal ch_chars ch_newline ch_quote ch_high in Python file_prefix "." end diff --git a/test/quick/run_test.py b/test/quick/run_test.py index 7feb210..5a77829 100644 --- a/test/quick/run_test.py +++ b/test/quick/run_test.py @@ -315,3 +315,29 @@ def test_tail_calls_with_closures_stay_recursive(): tc = _load_tail_calls() assert tc.tc_shift_small == 13 assert tc.tc_shift(3, lambda x: x)(0) == 3 + + +# ---- characters ---- + +def test_string_is_list_of_characters(): + assert m.ch_greeting == ["h", "i"] + + +def test_character_comparison(): + assert m.ch_digit_yes is True + assert m.ch_digit_no is False + + +def test_character_code(): + assert m.ch_code_A == 65 + + +def test_implode_and_explode(): + assert m.ch_literal == "hi" + assert m.ch_chars == ["a", "b"] + + +def test_escaped_characters(): + assert m.ch_newline == "\n" + assert m.ch_quote == '"' + assert m.ch_high == "\xe9" From 1f83418e96e698738eb3e6c7fc53a4f3ff42e5f1 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 07:23:26 +0100 Subject: [PATCH 02/30] Trailing underscore for a name clashing with a keyword or builtin Following PEP 8, rather than Isabelle's appended letter, so the primitive type constructors print as int_ and str_ and the option constructor as None_. --- code_python.ML | 13 ++++++++++--- .../Example_builtin_names.py | 18 +++++++++--------- .../Python_Examples.Example_class_dicts/Int.py | 2 +- .../Orderings.py | 2 +- .../Example_lambda_case.py | 4 ++-- .../Option.py | 2 +- .../Example_options.py | 6 +++--- .../Python_Examples.Example_options/Option.py | 2 +- .../Example_tail_calls.py | 2 +- .../loops/Example_tail_calls_loops.py | 2 +- 10 files changed, 30 insertions(+), 23 deletions(-) diff --git a/code_python.ML b/code_python.ML index 2b031f7..15601e9 100644 --- a/code_python.ML +++ b/code_python.ML @@ -128,7 +128,8 @@ datatype python_stmt = eqs: eqtn list (* code equations, see above *) } - (* A datatype definition (turns into one `@dataclass` per constructor) *) + (* A datatype definition (turns into one `@dataclass` per constructor, also when every constructor is + nullary, since PurePy has no enumerations) *) | Datatype of { typarams: vname list, (* type parameter names *) cnstrs: cnstr list (* constructor list, see above *) @@ -921,9 +922,15 @@ fun print_python_stmt undefineds const_syntax reserved args_num fun python_program_of_program ctxt module_name reserved identifiers exports program = let + (* A name clashing with a keyword or builtin gets a trailing underscore, following PEP 8; Name.variant + would append a letter, and treats a trailing underscore as marking an internal name *) fun namify_common base ((nsp_class, nsp_object), nsp_common) = - let val (base', nsp_common') = Name.variant base nsp_common - in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end; + let + val base' = if Name.is_declared reserved base then base ^ "_" else base; + val (base'', nsp_common') = + if Name.is_declared nsp_common base' then Name.variant base' nsp_common + else (base', Name.declare base' nsp_common); + in (base'', ((Name.declare base'' nsp_class, Name.declare base'' nsp_object), nsp_common')) end; (* Python doesn't really have any naming restrictions relating to upper/lowercase etc. *) fun namify_stmt (Code_Thingol.Fun _) = namify_common diff --git a/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py b/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py index 7202343..dbf8065 100644 --- a/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py +++ b/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py @@ -6,32 +6,32 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class inta: +class int_: pass @dataclass(frozen=True) -class stra: +class str_: pass @dataclass(frozen=True) -class objecta: +class object_: pass -def lena(x0): +def len_(x0): match x0: case []: return (0) case [uu, *ps]: - return ((lena(ps) + 1)) + return ((len_(ps) + 1)) case _: raise RuntimeError("match failed") -def hasha(p): +def hash_(p): target = (p) match target: - case inta(): + case int_(): return (0) - case stra(): + case str_(): return (1) - case objecta(): + case object_(): return (2) case _: raise RuntimeError("match failed") diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py index c917cb9..ada97b4 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py @@ -13,7 +13,7 @@ def equal_int(): @functools.cache def ord_int(): - return Orderings.orda(less_eq = lambda a, b: (a <= b ), less = lambda a, b: (a < b)) + return Orderings.ord_(less_eq = lambda a, b: (a <= b ), less = lambda a, b: (a < b)) @functools.cache def preorder_int(): diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py index cca9ae9..6555326 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class orda: +class ord_: less_eq: Callable less: Callable diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py index e213bf6..5a7e9d6 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py @@ -10,7 +10,7 @@ def doubled(xs): def sum_or_zero(x0): match x0: - case Option.Nonea(): + case Option.None_(): return (0) case Option.Some(n): return (n) @@ -24,7 +24,7 @@ def sum_options_inline(xs): def lam(a): target = (a) match target: - case Option.Nonea(): + case Option.None_(): return (0) case Option.Some(n): return (n) diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py index e4fcff2..be2279e 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class Nonea: +class None_: pass @dataclass(frozen=True) class Some: diff --git a/test/diff/golden/Python_Examples.Example_options/Example_options.py b/test/diff/golden/Python_Examples.Example_options/Example_options.py index be05357..bbf8ef6 100644 --- a/test/diff/golden/Python_Examples.Example_options/Example_options.py +++ b/test/diff/golden/Python_Examples.Example_options/Example_options.py @@ -8,7 +8,7 @@ def _unimplemented(name): def describe_opt(x0): match x0: - case Option.Nonea(): + case Option.None_(): return (0) case Option.Some(x): return ((x + 1)) @@ -19,7 +19,7 @@ def describe_opt(x0): d1 = (describe_opt(o_some)) -o_none = (Option.Nonea()) +o_none = (Option.None_()) d2 = (describe_opt(o_none)) @@ -27,7 +27,7 @@ def describe_opt2(x0): match x0: case Option.Some(x): return ((x + 100)) - case Option.Nonea(): + case Option.None_(): return ((- 1)) case _: raise RuntimeError("match failed") diff --git a/test/diff/golden/Python_Examples.Example_options/Option.py b/test/diff/golden/Python_Examples.Example_options/Option.py index e4fcff2..be2279e 100644 --- a/test/diff/golden/Python_Examples.Example_options/Option.py +++ b/test/diff/golden/Python_Examples.Example_options/Option.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class Nonea: +class None_: pass @dataclass(frozen=True) class Some: diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py index 3d725aa..c1ecaae 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class orda: +class ord_: less_eq: Callable less: Callable diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py index 7e60feb..59bc054 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py @@ -5,7 +5,7 @@ def _unimplemented(name): raise NotImplementedError(name) @dataclass(frozen=True) -class orda: +class ord_: less_eq: Callable less: Callable From 90b6d25e6dea5f5747e79c223671842e3001e30c Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 07:27:58 +0100 Subject: [PATCH 03/30] Example of names clashing with builtins deleted, since other examples show the renaming --- ROOT | 1 - examples/Example_builtin_names.thy | 16 -------- .../Example_builtin_names.py | 37 ------------------- .../Num.py | 15 -------- 4 files changed, 69 deletions(-) delete mode 100644 examples/Example_builtin_names.thy delete mode 100644 test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py delete mode 100644 test/diff/golden/Python_Examples.Example_builtin_names/Num.py diff --git a/ROOT b/ROOT index c660d6d..4628ae1 100644 --- a/ROOT +++ b/ROOT @@ -41,7 +41,6 @@ session Python_Examples in "examples" = Python + Example_iarray Example_tail_calls Example_chars - Example_builtin_names export_files (in "python_out") "*:**" session Python_Test_Quick in "test/quick" = Python + diff --git a/examples/Example_builtin_names.thy b/examples/Example_builtin_names.thy deleted file mode 100644 index 1a5a2c1..0000000 --- a/examples/Example_builtin_names.thy +++ /dev/null @@ -1,16 +0,0 @@ -theory Example_builtin_names - imports Main "Python.Python_Setup" -begin - -datatype prim = int | str | object - -fun len :: "prim list \ nat" where - "len [] = 0" | - "len (_ # ps) = Suc (len ps)" - -definition hash :: "prim \ nat" where - "hash p = (case p of int \ 0 | str \ 1 | object \ 2)" - -export_code len hash in Python file_prefix "." - -end diff --git a/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py b/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py deleted file mode 100644 index dbf8065..0000000 --- a/test/diff/golden/Python_Examples.Example_builtin_names/Example_builtin_names.py +++ /dev/null @@ -1,37 +0,0 @@ -from dataclasses import dataclass -from typing import Any, Callable -import Num - -def _unimplemented(name): - raise NotImplementedError(name) - -@dataclass(frozen=True) -class int_: - pass -@dataclass(frozen=True) -class str_: - pass -@dataclass(frozen=True) -class object_: - pass - -def len_(x0): - match x0: - case []: - return (0) - case [uu, *ps]: - return ((len_(ps) + 1)) - case _: - raise RuntimeError("match failed") - -def hash_(p): - target = (p) - match target: - case int_(): - return (0) - case str_(): - return (1) - case object_(): - return (2) - case _: - raise RuntimeError("match failed") diff --git a/test/diff/golden/Python_Examples.Example_builtin_names/Num.py b/test/diff/golden/Python_Examples.Example_builtin_names/Num.py deleted file mode 100644 index fc191a7..0000000 --- a/test/diff/golden/Python_Examples.Example_builtin_names/Num.py +++ /dev/null @@ -1,15 +0,0 @@ -from dataclasses import dataclass -from typing import Any, Callable - -def _unimplemented(name): - raise NotImplementedError(name) - -@dataclass(frozen=True) -class One: - pass -@dataclass(frozen=True) -class Bit0: - a: Any -@dataclass(frozen=True) -class Bit1: - a: Any From 33d02c73dc031e8027d9ce53311650c2aaca51be Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 07:29:27 +0100 Subject: [PATCH 04/30] Example of characters deleted, since the quick test checks the same definitions --- ROOT | 1 - examples/Example_chars.thy | 25 ------------------- .../Python_Examples.Example_chars/Arith.py | 8 ------ .../Example_chars.py | 20 --------------- 4 files changed, 54 deletions(-) delete mode 100644 examples/Example_chars.thy delete mode 100644 test/diff/golden/Python_Examples.Example_chars/Arith.py delete mode 100644 test/diff/golden/Python_Examples.Example_chars/Example_chars.py diff --git a/ROOT b/ROOT index 4628ae1..db4d24b 100644 --- a/ROOT +++ b/ROOT @@ -40,7 +40,6 @@ session Python_Examples in "examples" = Python + Example_class_dicts Example_iarray Example_tail_calls - Example_chars export_files (in "python_out") "*:**" session Python_Test_Quick in "test/quick" = Python + diff --git a/examples/Example_chars.thy b/examples/Example_chars.thy deleted file mode 100644 index 169419f..0000000 --- a/examples/Example_chars.thy +++ /dev/null @@ -1,25 +0,0 @@ -theory Example_chars - imports Main "Python.Python_Setup" -begin - -definition greeting :: string where - "greeting = ''hello''" - -definition is_digit :: "char \ bool" where - "is_digit c = (CHR ''0'' \ c \ c \ CHR ''9'')" - -definition code :: "char \ nat" where - "code c = of_char c" - -definition literal :: String.literal where - "literal = String.implode greeting" - -definition chars :: string where - "chars = String.explode (STR ''hi'')" - -definition newline :: char where - "newline = CHR 0x0A" - -export_code greeting is_digit code literal chars newline in Python file_prefix "." - -end diff --git a/test/diff/golden/Python_Examples.Example_chars/Arith.py b/test/diff/golden/Python_Examples.Example_chars/Arith.py deleted file mode 100644 index e096457..0000000 --- a/test/diff/golden/Python_Examples.Example_chars/Arith.py +++ /dev/null @@ -1,8 +0,0 @@ -from dataclasses import dataclass -from typing import Any, Callable - -def _unimplemented(name): - raise NotImplementedError(name) - -def nat_of_char(c): - return ((ord(c))) diff --git a/test/diff/golden/Python_Examples.Example_chars/Example_chars.py b/test/diff/golden/Python_Examples.Example_chars/Example_chars.py deleted file mode 100644 index d961a55..0000000 --- a/test/diff/golden/Python_Examples.Example_chars/Example_chars.py +++ /dev/null @@ -1,20 +0,0 @@ -from dataclasses import dataclass -from typing import Any, Callable -import Arith - -def _unimplemented(name): - raise NotImplementedError(name) - -def code(c): - return (Arith.nat_of_char(c)) - -chars = (list("hi")) - -greeting = (["h", "e", "l", "l", "o"]) - -literal = ("".join(greeting)) - -newline = ("\x0A") - -def is_digit(c): - return ("0" <= c and c <= "9") From 8f50d4daf31f4088bda408df44dad3bbdbc97327 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 07:38:40 +0100 Subject: [PATCH 05/30] Header naming the source theories of each generated file --- code_python.ML | 19 ++++++++++++++++++- .../golden/Python_Examples.Example/Example.py | 2 ++ .../Example_class_dicts.py | 2 ++ .../HOL.py | 2 ++ .../Int.py | 2 ++ .../Num.py | 2 ++ .../Orderings.py | 2 ++ .../Product_Type.py | 2 ++ .../Example_classrel.py | 2 ++ .../Example_classrel_base.py | 2 ++ .../Example_code_numerals.py | 2 ++ .../Num.py | 2 ++ .../Example_generic_list_pair.py | 2 ++ .../List.py | 2 ++ .../Product_Type.py | 2 ++ .../Example_iarray.py | 2 ++ .../Python_Examples.Example_iarray/HOL.py | 2 ++ .../Python_Examples.Example_iarray/IArray.py | 2 ++ .../Python_Examples.Example_iarray/List.py | 2 ++ .../Python_Examples.Example_iarray/Nat.py | 2 ++ .../Python_Examples.Example_iarray/Num.py | 2 ++ .../Example_int_arith.py | 2 ++ .../Python_Examples.Example_int_arith/Num.py | 2 ++ .../Arith.py | 2 ++ .../Example_integer_bit_ops.py | 2 ++ .../Groups.py | 2 ++ .../Num.py | 2 ++ .../Power.py | 2 ++ .../Example_lambda_case.py | 2 ++ .../Option.py | 2 ++ .../Example_lists.py | 2 ++ .../Python_Examples.Example_lists/Num.py | 2 ++ .../Example_nat.py | 2 ++ .../golden/Python_Examples.Example_nat/Num.py | 2 ++ .../Example_nat_edge_cases.py | 2 ++ .../Num.py | 2 ++ .../Example_nat_pattern.py | 2 ++ .../Num.py | 2 ++ .../Example_nested_case.py | 2 ++ .../Num.py | 2 ++ .../Example_nested_if.py | 2 ++ .../Python_Examples.Example_nested_if/Num.py | 2 ++ .../Example_no_eqs.py | 2 ++ .../Python_Examples.Example_no_eqs/HOL.py | 2 ++ .../Example_options.py | 2 ++ .../Python_Examples.Example_options/Num.py | 2 ++ .../Python_Examples.Example_options/Option.py | 2 ++ .../Example_partial.py | 2 ++ .../Python_Examples.Example_partial/Num.py | 2 ++ .../Example_polymorphic_const.py | 2 ++ .../Num.py | 2 ++ .../Example_record_ext.py | 2 ++ .../Python_Examples.Example_record_ext/Num.py | 2 ++ .../Example_records.py | 2 ++ .../Python_Examples.Example_records/Num.py | 2 ++ .../Example_super.py | 2 ++ .../Example_super_chain.py | 2 ++ .../Example_tail_calls.py | 2 ++ .../loops/Example_tail_calls_loops.py | 2 ++ .../Example_transparent_wrapper.py | 2 ++ .../Example_tuples.py | 2 ++ .../Python_Examples.Example_tuples/Num.py | 2 ++ .../Example_tyclass.py | 2 ++ .../Example_unused_arg.py | 2 ++ 64 files changed, 144 insertions(+), 1 deletion(-) diff --git a/code_python.ML b/code_python.ML index 15601e9..b630b28 100644 --- a/code_python.ML +++ b/code_python.ML @@ -1087,6 +1087,22 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, | _ => false)) stmt_gr false end; + (* Full names of the theories defining the symbols of a module *) + fun source_theories mod_name = + let + val (stmt_gr, _) = Graph.get_node python_program mod_name; + val long_name = Symtab.make (map (fn thy => (Context.theory_base_name thy, + Context.theory_long_name thy)) (Theory.nodes_of (Proof_Context.theory_of ctxt))); + val base_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) + stmt_gr []; + in sort_strings (map (fn name => the_default name (Symtab.lookup long_name name)) base_names) end; + + fun print_header mod_name = + let val thys = source_theories mod_name + in Pretty.str ("# Generated by Isabelle from " ^ (if length thys = 1 then "theory " else "theories ") ^ + commas thys ^ "; do not edit") + end; + fun print_one_module (mod_name, imports, stmt_ps) = let val import_ps = imports @@ -1099,7 +1115,8 @@ 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)) + in ([mod_name ^ ".py"], + Pretty.chunks2 (print_header mod_name :: imports_block :: unimplemented_def :: stmt_ps)) end; val p = map print_one_module module_stmts diff --git a/test/diff/golden/Python_Examples.Example/Example.py b/test/diff/golden/Python_Examples.Example/Example.py index 2bbabeb..ba318dc 100644 --- a/test/diff/golden/Python_Examples.Example/Example.py +++ b/test/diff/golden/Python_Examples.Example/Example.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py b/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py index 83c83ec..d9ad1db 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_class_dicts; do not edit + from dataclasses import dataclass from typing import Any, Callable import Product_Type diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py index 0134fe9..dc7ad39 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.HOL; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py index ada97b4..a370e12 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Int; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py index 6555326..df803f2 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Orderings; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py index 8e3911a..ad8f49b 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Product_Type; do not edit + from dataclasses import dataclass from typing import Any, Callable import HOL diff --git a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py index 02d9206..59b72f2 100644 --- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py +++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_classrel; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py index 8d4bdb7..d5f3c91 100644 --- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py +++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_classrel_base; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py b/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py index 8ab5c8f..a983422 100644 --- a/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py +++ b/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_code_numerals; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py +++ b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py index 03938a0..3b9fa50 100644 --- a/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py +++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_generic_list_pair; do not edit + from dataclasses import dataclass from typing import Any, Callable import List diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py index 61b9c7b..94e5277 100644 --- a/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py +++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.List; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py index 9d91185..2b3d083 100644 --- a/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py +++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Product_Type; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py index b35bb0d..801e229 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_iarray; do not edit + from dataclasses import dataclass from typing import Any, Callable import IArray diff --git a/test/diff/golden/Python_Examples.Example_iarray/HOL.py b/test/diff/golden/Python_Examples.Example_iarray/HOL.py index 0134fe9..dc7ad39 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/HOL.py +++ b/test/diff/golden/Python_Examples.Example_iarray/HOL.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.HOL; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_iarray/IArray.py b/test/diff/golden/Python_Examples.Example_iarray/IArray.py index 4403b0e..d4b7546 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/IArray.py +++ b/test/diff/golden/Python_Examples.Example_iarray/IArray.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL-Library.IArray; do not edit + from dataclasses import dataclass from typing import Any, Callable import List diff --git a/test/diff/golden/Python_Examples.Example_iarray/List.py b/test/diff/golden/Python_Examples.Example_iarray/List.py index 7b82d6e..c51eb3f 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/List.py +++ b/test/diff/golden/Python_Examples.Example_iarray/List.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.List; do not edit + from dataclasses import dataclass from typing import Any, Callable import HOL diff --git a/test/diff/golden/Python_Examples.Example_iarray/Nat.py b/test/diff/golden/Python_Examples.Example_iarray/Nat.py index 04009cc..46ff8e8 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Nat.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Nat.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Nat; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_iarray/Num.py b/test/diff/golden/Python_Examples.Example_iarray/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Num.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py b/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py index 14f06f6..9c5d7af 100644 --- a/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py +++ b/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_int_arith; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_int_arith/Num.py b/test/diff/golden/Python_Examples.Example_int_arith/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_int_arith/Num.py +++ b/test/diff/golden/Python_Examples.Example_int_arith/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py index 475f11a..68fb4ba 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Code_Numeral; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py index 666f41f..e069b67 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_integer_bit_ops; do not edit + from dataclasses import dataclass from typing import Any, Callable import Arith diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py index 1172389..eeb31a6 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Groups; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py index 9da25a7..3d33384 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Power; do not edit + from dataclasses import dataclass from typing import Any, Callable import Groups diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py index 5a7e9d6..bd1c761 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_lambda_case; do not edit + from dataclasses import dataclass from typing import Any, Callable import Option diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py index be2279e..93548f9 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Option; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py index 1f08ca9..5ca4082 100644 --- a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py +++ b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_lists; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_lists/Num.py b/test/diff/golden/Python_Examples.Example_lists/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_lists/Num.py +++ b/test/diff/golden/Python_Examples.Example_lists/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py index caefc81..bae9725 100644 --- a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py +++ b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_nat; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_nat/Num.py b/test/diff/golden/Python_Examples.Example_nat/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_nat/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py index 494a942..9ced0f5 100644 --- a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py +++ b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_nat_edge_cases; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py b/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py index 2f9657a..86c25d1 100644 --- a/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py +++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_nat_pattern; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py b/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py index 83c2d13..0b57ab4 100644 --- a/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py +++ b/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_nested_case; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_nested_case/Num.py b/test/diff/golden/Python_Examples.Example_nested_case/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_nested_case/Num.py +++ b/test/diff/golden/Python_Examples.Example_nested_case/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py b/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py index cbc70de..f1ef2ff 100644 --- a/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py +++ b/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_nested_if; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_nested_if/Num.py b/test/diff/golden/Python_Examples.Example_nested_if/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_nested_if/Num.py +++ b/test/diff/golden/Python_Examples.Example_nested_if/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py index 2a3fafb..3e12890 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_no_eqs; do not edit + from dataclasses import dataclass from typing import Any, Callable import HOL diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py index bf23ee4..323d707 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.HOL; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_options/Example_options.py b/test/diff/golden/Python_Examples.Example_options/Example_options.py index bbf8ef6..1109254 100644 --- a/test/diff/golden/Python_Examples.Example_options/Example_options.py +++ b/test/diff/golden/Python_Examples.Example_options/Example_options.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_options; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_options/Num.py b/test/diff/golden/Python_Examples.Example_options/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_options/Num.py +++ b/test/diff/golden/Python_Examples.Example_options/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_options/Option.py b/test/diff/golden/Python_Examples.Example_options/Option.py index be2279e..93548f9 100644 --- a/test/diff/golden/Python_Examples.Example_options/Option.py +++ b/test/diff/golden/Python_Examples.Example_options/Option.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Option; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py index 8fa829e..32db794 100644 --- a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py +++ b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_partial; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_partial/Num.py b/test/diff/golden/Python_Examples.Example_partial/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_partial/Num.py +++ b/test/diff/golden/Python_Examples.Example_partial/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py b/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py index 0409c7c..308678d 100644 --- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py +++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_polymorphic_const; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py +++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py index 722a393..c77bf21 100644 --- a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py +++ b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_record_ext; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Num.py b/test/diff/golden/Python_Examples.Example_record_ext/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_record_ext/Num.py +++ b/test/diff/golden/Python_Examples.Example_record_ext/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_records/Example_records.py b/test/diff/golden/Python_Examples.Example_records/Example_records.py index 7001c66..31dc109 100644 --- a/test/diff/golden/Python_Examples.Example_records/Example_records.py +++ b/test/diff/golden/Python_Examples.Example_records/Example_records.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_records; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_records/Num.py b/test/diff/golden/Python_Examples.Example_records/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_records/Num.py +++ b/test/diff/golden/Python_Examples.Example_records/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_super/Example_super.py b/test/diff/golden/Python_Examples.Example_super/Example_super.py index 6a3501d..211ed70 100644 --- a/test/diff/golden/Python_Examples.Example_super/Example_super.py +++ b/test/diff/golden/Python_Examples.Example_super/Example_super.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_super; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py b/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py index a26386f..2f0c36e 100644 --- a/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py +++ b/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_super_chain; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py index c1ecaae..9591c09 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theories HOL.HOL, HOL.Orderings, Pure, Python_Examples.Example_tail_calls; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py index 59bc054..3c227bb 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theories HOL.HOL, HOL.Orderings, Pure, Python_Examples.Example_tail_calls; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py b/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py index 254cc68..afe3e92 100644 --- a/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py +++ b/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_transparent_wrapper; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py index 5d3e48f..c0b7268 100644 --- a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py +++ b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_tuples; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num diff --git a/test/diff/golden/Python_Examples.Example_tuples/Num.py b/test/diff/golden/Python_Examples.Example_tuples/Num.py index fc191a7..648ca75 100644 --- a/test/diff/golden/Python_Examples.Example_tuples/Num.py +++ b/test/diff/golden/Python_Examples.Example_tuples/Num.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + from dataclasses import dataclass from typing import Any, Callable diff --git a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py index 748b17e..eafe119 100644 --- a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py +++ b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_tyclass; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools diff --git a/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py b/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py index 9a55018..a966771 100644 --- a/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py +++ b/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py @@ -1,3 +1,5 @@ +# Generated by Isabelle from theory Python_Examples.Example_unused_arg; do not edit + from dataclasses import dataclass from typing import Any, Callable From 47dd03d595d25f46d112e861ac4a203c5ea1bed0 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 09:30:38 +0100 Subject: [PATCH 06/30] Characters section of quick test in the style of the others --- test/quick/Quick_Test.thy | 2 +- test/quick/run_test.py | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/quick/Quick_Test.thy b/test/quick/Quick_Test.thy index e7d5659..f709322 100644 --- a/test/quick/Quick_Test.thy +++ b/test/quick/Quick_Test.thy @@ -264,7 +264,7 @@ definition twice_twice :: "'a::plus \ 'a" where "twice_twice = (\x. x + x) \ (\x. x + x)" definition e_twice_twice :: int where "e_twice_twice = twice_twice 3" -section \Characters\ +section \characters\ definition ch_greeting :: string where "ch_greeting = ''hi''" definition ch_is_digit :: "char \ bool" where "ch_is_digit c = (CHR ''0'' \ c \ c \ CHR ''9'')" diff --git a/test/quick/run_test.py b/test/quick/run_test.py index 5a77829..f3036cb 100644 --- a/test/quick/run_test.py +++ b/test/quick/run_test.py @@ -324,8 +324,8 @@ def test_string_is_list_of_characters(): def test_character_comparison(): - assert m.ch_digit_yes is True - assert m.ch_digit_no is False + assert m.ch_digit_yes + assert not m.ch_digit_no def test_character_code(): From e16b72cae5569678c50ac58282200dcf7d7be662 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 12:44:55 +0100 Subject: [PATCH 07/30] README paragraph on the setup theory as one sentence --- README.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index beaaecb..bec1509 100644 --- a/README.md +++ b/README.md @@ -38,11 +38,9 @@ In order to use this generator you have to import one of the following theories: Strings), and relies on the automatically extracted HOL definitions for other things. -`Python.Python_Setup` includes additional custom code printers to utilise -Python native integers for `int` and `nat`, as well as using Python's own -list and tuple data types, and one-character strings for `char`, so that a -`string` is a list of one-character strings. Most people will probably want to -use this setup for code generation. +`Python.Python_Setup` extends `Python.Python` by printing `int` and `nat` as +Python integers, lists as Python lists, pairs as tuples and `char` as +one-character strings. ### Tail calls as loops From 6c5aaecba5b475ff37c52023fb09bf8ac209060b Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 12:46:43 +0100 Subject: [PATCH 08/30] Single blank lines between character tests, as elsewhere in the file --- test/quick/run_test.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/test/quick/run_test.py b/test/quick/run_test.py index f3036cb..f4bf27b 100644 --- a/test/quick/run_test.py +++ b/test/quick/run_test.py @@ -322,21 +322,17 @@ def test_tail_calls_with_closures_stay_recursive(): def test_string_is_list_of_characters(): assert m.ch_greeting == ["h", "i"] - def test_character_comparison(): assert m.ch_digit_yes assert not m.ch_digit_no - def test_character_code(): assert m.ch_code_A == 65 - def test_implode_and_explode(): assert m.ch_literal == "hi" assert m.ch_chars == ["a", "b"] - def test_escaped_characters(): assert m.ch_newline == "\n" assert m.ch_quote == '"' From 98ad16ba89226760cbf5d030605d7967706f77c1 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 12:51:20 +0100 Subject: [PATCH 09/30] Reserved builtins read from the builtins module of the Python on the path --- code_python.ML | 30 ++++++------------------------ 1 file changed, 6 insertions(+), 24 deletions(-) diff --git a/code_python.ML b/code_python.ML index b630b28..a40ce7a 100644 --- a/code_python.ML +++ b/code_python.ML @@ -77,29 +77,10 @@ val python_reserved_words = (* these are symbols we use in addition to the standard reserved words *) @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];; -(* Python builtins, which a generated name must not shadow in its module *) -val python_builtins = - ["ArithmeticError", "AssertionError", "AttributeError", "BaseException", "BaseExceptionGroup", - "BlockingIOError", "BrokenPipeError", "BufferError", "BytesWarning", "ChildProcessError", - "ConnectionAbortedError", "ConnectionError", "ConnectionRefusedError", "ConnectionResetError", - "DeprecationWarning", "EOFError", "Ellipsis", "EncodingWarning", "EnvironmentError", "Exception", - "ExceptionGroup", "FileExistsError", "FileNotFoundError", "FloatingPointError", "FutureWarning", - "GeneratorExit", "IOError", "ImportError", "ImportWarning", "IndentationError", "IndexError", - "InterruptedError", "IsADirectoryError", "KeyError", "KeyboardInterrupt", "LookupError", "MemoryError", - "ModuleNotFoundError", "NameError", "NotADirectoryError", "NotImplemented", "NotImplementedError", - "OSError", "OverflowError", "PendingDeprecationWarning", "PermissionError", "ProcessLookupError", - "PythonFinalizationError", "RecursionError", "ReferenceError", "ResourceWarning", "RuntimeError", - "RuntimeWarning", "StopAsyncIteration", "StopIteration", "SyntaxError", "SyntaxWarning", "SystemError", - "SystemExit", "TabError", "TimeoutError", "TypeError", "UnboundLocalError", "UnicodeDecodeError", - "UnicodeEncodeError", "UnicodeError", "UnicodeTranslateError", "UnicodeWarning", "UserWarning", - "ValueError", "Warning", "ZeroDivisionError", "abs", "aiter", "all", "anext", "any", "ascii", "bin", - "bool", "breakpoint", "bytearray", "bytes", "callable", "chr", "classmethod", "compile", "complex", - "copyright", "credits", "delattr", "dict", "dir", "divmod", "enumerate", "eval", "exec", "exit", - "filter", "float", "format", "frozenset", "getattr", "globals", "hasattr", "hash", "help", "hex", "id", - "input", "int", "isinstance", "issubclass", "iter", "len", "license", "list", "locals", "map", "max", - "memoryview", "min", "next", "object", "oct", "open", "ord", "pow", "print", "property", "quit", "range", - "repr", "reversed", "round", "set", "setattr", "slice", "sorted", "staticmethod", "str", "sum", "super", - "tuple", "type", "vars", "zip"]; +(* Names in the builtins module of the Python on the path, which a generated name must not shadow *) +fun python_builtins () = + let val (out, rc) = Isabelle_System.bash_output "python3 -c 'import builtins; print(*dir(builtins))'" + in if rc = 0 then space_explode " " (trim_line out) else error ("No Python builtins: " ^ out) end; type eqtn = { patterns: iterm list, (* left hand side pattern list *) @@ -1138,6 +1119,7 @@ val _ = Theory.setup run_command = Code_Target.run_command_bash (fn module_name => "python3 -m py_compile " ^ Bash.string module_name ^ "/*.py")}, evaluation_args = []}) - #> fold (Code_Target.add_reserved target) (python_reserved_words @ python_builtins)); + #> (fn thy => fold (Code_Target.add_reserved target) + (distinct (op =) (python_reserved_words @ python_builtins ())) thy)); end; (* struct *) From 4cd0c09cd65e4f74d7646bee75926d2a5dabfef5 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:03:37 +0100 Subject: [PATCH 10/30] Target Python version from the spec repository, used throughout .python-version is 3.12, as in pure-py-spec. The generator reads its reserved builtins from that Python through uv, and pyproject.toml, the README and CI use the same version. --- .github/workflows/ci.yml | 26 ++++++++++---------------- .python-version | 2 +- README.md | 14 +++++++------- code_python.ML | 14 +++++++++----- pyproject.toml | 2 +- uv.lock | 2 +- 6 files changed, 29 insertions(+), 31 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 75d6290..72a8db7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,17 +16,14 @@ jobs: steps: - uses: actions/checkout@v4 - - name: Install python3/pip and pytest - run: | - apt-get update - apt-get install -y --no-install-recommends python3 python3-pip - pip3 install --break-system-packages pytest 2>/dev/null || pip3 install pytest + - name: Install uv + uses: astral-sh/setup-uv@v6 - name: extract Python code run: /home/isabelle/Isabelle/bin/isabelle build -v -d . -e Python_Test_Quick - name: Run quick test suite - run: pytest test/quick/run_test.py + run: uv run pytest test/quick/run_test.py diff: runs-on: ubuntu-latest @@ -36,17 +33,14 @@ jobs: steps: - uses: actions/checkout@v4 - - name: Install python3/pip and pytest - run: | - apt-get update - apt-get install -y --no-install-recommends python3 python3-pip - pip3 install --break-system-packages pytest 2>/dev/null || pip3 install pytest + - name: Install uv + uses: astral-sh/setup-uv@v6 - name: extract Python code run: /home/isabelle/Isabelle/bin/isabelle build -v -d . -e Python_Examples - name: Run diff test suite - run: pytest test/diff/run_test.py + run: uv run pytest test/diff/run_test.py slow: runs-on: ubuntu-latest @@ -56,14 +50,14 @@ jobs: steps: - uses: actions/checkout@v4 - - name: Install python3 - run: apt-get update && apt-get install -y --no-install-recommends python3 + - name: Install uv + uses: astral-sh/setup-uv@v6 - name: extract Python code run: ISABELLE_PYTHON=1 /home/isabelle/Isabelle/bin/isabelle build -v -d . -e Python_Test_Slow - name: syntax check generated code run: | - python3 -m py_compile test/slow/generated_basic/*.py - python3 -m py_compile test/slow/generated_full/*.py + uv run python -m py_compile test/slow/generated_basic/*.py + uv run python -m py_compile test/slow/generated_full/*.py diff --git a/.python-version b/.python-version index 6324d40..e4fba21 100644 --- a/.python-version +++ b/.python-version @@ -1 +1 @@ -3.14 +3.12 diff --git a/README.md b/README.md index bec1509..2bd0c34 100644 --- a/README.md +++ b/README.md @@ -7,8 +7,8 @@ Python 3. - A recent Isabelle/HOL release (with `isabelle` on your `PATH`, currently only `Isabelle2025-2` has been tested) -- Python 3.10+ (generated pattern-matching code uses `match`/`case`) -- `pytest`, if you want to run the tests +- [uv](https://docs.astral.sh/uv/), which runs Python at the version in `.python-version`, the target version of + the generated code ## Installing as a component @@ -78,7 +78,7 @@ and runs various tests defined in `/test/quick/run_test.py`. ```bash isabelle build -d . -e Python_Test_Quick -pytest test/quick/run_test.py -v +uv run pytest test/quick/run_test.py -v ``` - **slow** @@ -92,8 +92,8 @@ with `Python.Python_Setup`. Unfortunately, we can currently not use Isabelle's ```bash isabelle build -d . -e Python_Test_Slow -python3 -m py_compile test/slow/generated_basic/*.py -python3 -m py_compile test/slow/generated_full/*.py +uv run python -m py_compile test/slow/generated_basic/*.py +uv run python -m py_compile test/slow/generated_full/*.py ``` - **diff** @@ -105,7 +105,7 @@ suite holds golden reference files under `test/diff/golden/`. ```bash isabelle build -d . -e Python_Examples -pytest test/diff/run_test.py +uv run pytest test/diff/run_test.py ``` If a new example is added, or the output has changed and is confirmed correct, @@ -113,7 +113,7 @@ the golden files can be recreated by ```bash isabelle build -d . -e Python_Examples -python3 test/diff/reseed_goldens.py +uv run python test/diff/reseed_goldens.py ``` ## Known limitations diff --git a/code_python.ML b/code_python.ML index a40ce7a..e73f028 100644 --- a/code_python.ML +++ b/code_python.ML @@ -77,10 +77,14 @@ val python_reserved_words = (* these are symbols we use in addition to the standard reserved words *) @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];; -(* Names in the builtins module of the Python on the path, which a generated name must not shadow *) -fun python_builtins () = - let val (out, rc) = Isabelle_System.bash_output "python3 -c 'import builtins; print(*dir(builtins))'" - in if rc = 0 then space_explode " " (trim_line out) else error ("No Python builtins: " ^ out) end; +(* Names in the builtins module of the target Python, given by the version file in the directory of thy; + a generated name must not shadow them *) +fun python_builtins thy = + let + val version = trim_line (File.read (Resources.master_directory thy + Path.basic ".python-version")); + val (out, rc) = Isabelle_System.bash_output ("uv run -q --no-project --python " ^ Bash.string version ^ + " python -c 'import builtins; print(*dir(builtins))'"); + in if rc = 0 then space_explode " " (trim_line out) else error ("No builtins of Python " ^ version) end; type eqtn = { patterns: iterm list, (* left hand side pattern list *) @@ -1120,6 +1124,6 @@ val _ = Theory.setup "python3 -m py_compile " ^ Bash.string module_name ^ "/*.py")}, evaluation_args = []}) #> (fn thy => fold (Code_Target.add_reserved target) - (distinct (op =) (python_reserved_words @ python_builtins ())) thy)); + (distinct (op =) (python_reserved_words @ python_builtins thy)) thy)); end; (* struct *) diff --git a/pyproject.toml b/pyproject.toml index 78c1bfb..c4818bc 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -3,7 +3,7 @@ name = "isabelle-python-codegen" version = "0.1.0" description = "Add your description here" readme = "README.md" -requires-python = ">=3.14" +requires-python = ">=3.12" dependencies = [ "pytest>=9.1.1", ] diff --git a/uv.lock b/uv.lock index f72a733..d543f47 100644 --- a/uv.lock +++ b/uv.lock @@ -1,6 +1,6 @@ version = 1 revision = 3 -requires-python = ">=3.14" +requires-python = ">=3.12" [[package]] name = "colorama" From f80a8cbc354e3fe4aaa58772fe29b4eb26066557 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:07:35 +0100 Subject: [PATCH 11/30] Shorter comment on reserved builtins --- code_python.ML | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/code_python.ML b/code_python.ML index e73f028..44764fe 100644 --- a/code_python.ML +++ b/code_python.ML @@ -77,8 +77,7 @@ val python_reserved_words = (* these are symbols we use in addition to the standard reserved words *) @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];; -(* Names in the builtins module of the target Python, given by the version file in the directory of thy; - a generated name must not shadow them *) +(* Names in the builtins module of the target Python *) fun python_builtins thy = let val version = trim_line (File.read (Resources.master_directory thy + Path.basic ".python-version")); From 2da05313c7524c36ec46a9742e567ad0e17b1518 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 14:58:16 +0100 Subject: [PATCH 12/30] Comment on reserved builtins states their purpose --- code_python.ML | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/code_python.ML b/code_python.ML index 44764fe..b3697df 100644 --- a/code_python.ML +++ b/code_python.ML @@ -77,7 +77,7 @@ val python_reserved_words = (* these are symbols we use in addition to the standard reserved words *) @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];; -(* Names in the builtins module of the target Python *) +(* Names in the builtins module of the target Python; generated names must not hide these. *) fun python_builtins thy = let val version = trim_line (File.read (Resources.master_directory thy + Path.basic ".python-version")); From 74143a6bfc6f4abdb9082a02a5d75edc34e2e7dc Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 15:02:49 +0100 Subject: [PATCH 13/30] Keywords read from the target Python, and header names defined once The reserved keywords come from Python's keyword module, in the same call as the builtins, leaving out the wildcard _. The names bound by the header of a generated module are defined once, for both the header printer and the reserved names. --- code_python.ML | 38 ++++++++++++++++++++------------------ 1 file changed, 20 insertions(+), 18 deletions(-) diff --git a/code_python.ML b/code_python.ML index b3697df..e7ca516 100644 --- a/code_python.ML +++ b/code_python.ML @@ -68,22 +68,24 @@ fun enable_native_encoding name = Native_Encoding_Data.map (Symtab.update (name, fun use_native_encoding thy name = Symtab.defined (Native_Encoding_Data.get thy) name; -val python_reserved_words = - ["False", "None", "True", "and", "as", "assert", "await", "break", "class", - "continue", "def", "del", "elif", "else", "except", "finally", "for", "from", - "global", "if", "import", "in", "is", "lambda", "nonlocal", "not", "or", "pass", - "raise", "return", "try", "while", "with", "yield", "match", "case"] +(* Names imported by the header of every generated module, with their modules *) +val header_imports = [("dataclasses", ["dataclass"]), ("typing", ["Any", "Callable"])]; - (* these are symbols we use in addition to the standard reserved words *) - @ ["dataclass", "Any", "Callable", "_unimplemented", "functools"];; +(* Module imported by a generated module with a cached instance *) +val functools = "functools"; -(* Names in the builtins module of the target Python; generated names must not hide these. *) -fun python_builtins thy = +(* Function defined by the header of every generated module, called for a constant without code equations *) +val unimplemented = "_unimplemented"; + +(* Keywords and builtins of the target Python, except the wildcard _ printed by the generator; generated names + must not hide these. *) +fun python_names thy = let val version = trim_line (File.read (Resources.master_directory thy + Path.basic ".python-version")); val (out, rc) = Isabelle_System.bash_output ("uv run -q --no-project --python " ^ Bash.string version ^ - " python -c 'import builtins; print(*dir(builtins))'"); - in if rc = 0 then space_explode " " (trim_line out) else error ("No builtins of Python " ^ version) end; + " python -c 'import builtins, keyword; " ^ + "print(*keyword.kwlist, *(k for k in keyword.softkwlist if k != \"_\"), *dir(builtins))'"); + in if rc = 0 then space_explode " " (trim_line out) else error ("No names of Python " ^ version) end; type eqtn = { patterns: iterm list, (* left hand side pattern list *) @@ -584,7 +586,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num and print_app const_syntax some_thm vars fxy (const as { sym, ... }, ts) = if List.exists (fn name => sym = Constant name) undefineds - then Pretty.block [Pretty.str "_unimplemented(", + then Pretty.block [Pretty.str (unimplemented ^ "("), Pretty.str (print_python_string (Code_Symbol.default_base sym)), Pretty.str ")"] else let @@ -691,7 +693,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num Pretty.enum "," "(" ")" dict_args, Pretty.str ":"] (* an instance without dictionary arguments always builds the same (frozen) dictionary, so build it once *) - val decorator = if null dict_args then [Pretty.str "@functools.cache"] else [] + val decorator = if null dict_args then [Pretty.str ("@" ^ functools ^ ".cache")] else [] in Pretty.chunks (decorator @ [head, indent_block 4 body]) end; fun print_func_head const vctxt dicts params = @@ -1092,12 +1094,12 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, val import_ps = imports |> filter (fn (imported_name, _) => member (op =) nonempty_names imported_name) |> map (fn (imported_name, _) => concat [Pretty.str "import", Pretty.str imported_name]); - val imports_block = Pretty.chunks (Pretty.str "from dataclasses import dataclass" - :: Pretty.str "from typing import Any, Callable" - :: (if needs_functools mod_name then [Pretty.str "import functools"] else []) + val imports_block = Pretty.chunks + (map (fn (m, names) => Pretty.str ("from " ^ m ^ " import " ^ commas names)) header_imports + @ (if needs_functools mod_name then [Pretty.str ("import " ^ functools)] else []) @ import_ps) val unimplemented_def = Pretty.chunks - [Pretty.str "def _unimplemented(name):", + [Pretty.str ("def " ^ unimplemented ^ "(name):"), indent_block 4 (Pretty.str "raise NotImplementedError(name)")] in ([mod_name ^ ".py"], Pretty.chunks2 (print_header mod_name :: imports_block :: unimplemented_def :: stmt_ps)) @@ -1123,6 +1125,6 @@ val _ = Theory.setup "python3 -m py_compile " ^ Bash.string module_name ^ "/*.py")}, evaluation_args = []}) #> (fn thy => fold (Code_Target.add_reserved target) - (distinct (op =) (python_reserved_words @ python_builtins thy)) thy)); + (distinct (op =) (python_names thy @ maps snd header_imports @ [functools, unimplemented])) thy)); end; (* struct *) From 6c7061a3d991fee49e04d73b8b7d9ce944d4b1e2 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 17:04:01 +0100 Subject: [PATCH 14/30] Header names as one list again --- code_python.ML | 24 +++++++++--------------- 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/code_python.ML b/code_python.ML index e7ca516..ae2b28a 100644 --- a/code_python.ML +++ b/code_python.ML @@ -68,14 +68,8 @@ fun enable_native_encoding name = Native_Encoding_Data.map (Symtab.update (name, fun use_native_encoding thy name = Symtab.defined (Native_Encoding_Data.get thy) name; -(* Names imported by the header of every generated module, with their modules *) -val header_imports = [("dataclasses", ["dataclass"]), ("typing", ["Any", "Callable"])]; - -(* Module imported by a generated module with a cached instance *) -val functools = "functools"; - -(* Function defined by the header of every generated module, called for a constant without code equations *) -val unimplemented = "_unimplemented"; +(* Names bound by the header of a generated module; generated names must not hide these. *) +val header_names = ["dataclass", "Any", "Callable", "functools", "_unimplemented"]; (* Keywords and builtins of the target Python, except the wildcard _ printed by the generator; generated names must not hide these. *) @@ -586,7 +580,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num and print_app const_syntax some_thm vars fxy (const as { sym, ... }, ts) = if List.exists (fn name => sym = Constant name) undefineds - then Pretty.block [Pretty.str (unimplemented ^ "("), + then Pretty.block [Pretty.str "_unimplemented(", Pretty.str (print_python_string (Code_Symbol.default_base sym)), Pretty.str ")"] else let @@ -693,7 +687,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num Pretty.enum "," "(" ")" dict_args, Pretty.str ":"] (* an instance without dictionary arguments always builds the same (frozen) dictionary, so build it once *) - val decorator = if null dict_args then [Pretty.str ("@" ^ functools ^ ".cache")] else [] + val decorator = if null dict_args then [Pretty.str "@functools.cache"] else [] in Pretty.chunks (decorator @ [head, indent_block 4 body]) end; fun print_func_head const vctxt dicts params = @@ -1094,12 +1088,12 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, val import_ps = imports |> filter (fn (imported_name, _) => member (op =) nonempty_names imported_name) |> map (fn (imported_name, _) => concat [Pretty.str "import", Pretty.str imported_name]); - val imports_block = Pretty.chunks - (map (fn (m, names) => Pretty.str ("from " ^ m ^ " import " ^ commas names)) header_imports - @ (if needs_functools mod_name then [Pretty.str ("import " ^ functools)] else []) + val imports_block = Pretty.chunks (Pretty.str "from dataclasses import dataclass" + :: Pretty.str "from typing import Any, Callable" + :: (if needs_functools mod_name then [Pretty.str "import functools"] else []) @ import_ps) val unimplemented_def = Pretty.chunks - [Pretty.str ("def " ^ unimplemented ^ "(name):"), + [Pretty.str "def _unimplemented(name):", indent_block 4 (Pretty.str "raise NotImplementedError(name)")] in ([mod_name ^ ".py"], Pretty.chunks2 (print_header mod_name :: imports_block :: unimplemented_def :: stmt_ps)) @@ -1125,6 +1119,6 @@ val _ = Theory.setup "python3 -m py_compile " ^ Bash.string module_name ^ "/*.py")}, evaluation_args = []}) #> (fn thy => fold (Code_Target.add_reserved target) - (distinct (op =) (python_names thy @ maps snd header_imports @ [functools, unimplemented])) thy)); + (distinct (op =) (python_names thy @ header_names)) thy)); end; (* struct *) From 93470f43a0e338e23eec51a12dc2a74f79a6c806 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 17:14:23 +0100 Subject: [PATCH 15/30] Error for a definition with the name of a module imported by its module --- code_python.ML | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/code_python.ML b/code_python.ML index ae2b28a..d31964a 100644 --- a/code_python.ML +++ b/code_python.ML @@ -1058,6 +1058,25 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, val nonempty_names = map #1 module_stmts; + (* Stop if a definition has the name of a module imported by its module, which it would hide *) + fun check_imports (mod_name, imports, _) = + let + val (stmt_gr, _) = Graph.get_node python_program mod_name; + fun binds (sym as Constant _) = not (is_class_param sym) + | binds (Type_Class _) = true + | binds (Class_Instance _) = true + | binds _ = false; + val names = Code_Symbol.Graph.fold (fn (sym, ((base, _), _)) => + if binds sym then insert (op =) base else I) stmt_gr []; + in + case filter (fn (imported, _) => + member (op =) nonempty_names imported andalso member (op =) names imported) imports + of [] => () + | (imported, _) :: _ => + error ("Definition " ^ imported ^ " of module " ^ mod_name ^ " hides imported module " ^ imported) + end; + val _ = List.app check_imports module_stmts; + (* modules that print a cached (dictionary-free) instance need functools *) fun needs_functools mod_name = let val (stmt_gr, _) = Graph.get_node python_program mod_name From 2b1bf36d98bc8336b39febbe66a80a30702278e9 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 17:47:03 +0100 Subject: [PATCH 16/30] Abort helper for constants without code, with the constant's full name The header function for constants without code equations goes; their uses and stub functions call the abort helper instead, with the full name of the constant as message. --- Python.thy | 2 +- code_python.ML | 24 +++++++++---------- .../golden/Python_Examples.Example/Example.py | 3 --- .../Example_class_dicts.py | 3 --- .../HOL.py | 3 --- .../Int.py | 3 --- .../Num.py | 3 --- .../Orderings.py | 3 --- .../Product_Type.py | 3 --- .../Example_classrel.py | 3 --- .../Example_classrel_base.py | 3 --- .../Example_code_numerals.py | 3 --- .../Num.py | 3 --- .../Example_generic_list_pair.py | 3 --- .../List.py | 3 --- .../Product_Type.py | 3 --- .../Example_iarray.py | 3 --- .../Python_Examples.Example_iarray/HOL.py | 3 --- .../Python_Examples.Example_iarray/IArray.py | 3 --- .../Python_Examples.Example_iarray/List.py | 3 --- .../Python_Examples.Example_iarray/Nat.py | 3 --- .../Python_Examples.Example_iarray/Num.py | 3 --- .../Example_int_arith.py | 3 --- .../Python_Examples.Example_int_arith/Num.py | 3 --- .../Arith.py | 3 --- .../Example_integer_bit_ops.py | 3 --- .../Groups.py | 3 --- .../Num.py | 3 --- .../Power.py | 3 --- .../Example_lambda_case.py | 3 --- .../Option.py | 3 --- .../Example_lists.py | 3 --- .../Python_Examples.Example_lists/Num.py | 3 --- .../Example_nat.py | 3 --- .../golden/Python_Examples.Example_nat/Num.py | 3 --- .../Example_nat_edge_cases.py | 3 --- .../Num.py | 3 --- .../Example_nat_pattern.py | 3 --- .../Num.py | 3 --- .../Example_nested_case.py | 3 --- .../Num.py | 3 --- .../Example_nested_if.py | 3 --- .../Python_Examples.Example_nested_if/Num.py | 3 --- .../Example_no_eqs.py | 5 +--- .../Python_Examples.Example_no_eqs/HOL.py | 5 +--- .../Example_options.py | 3 --- .../Python_Examples.Example_options/Num.py | 3 --- .../Python_Examples.Example_options/Option.py | 3 --- .../Example_partial.py | 3 --- .../Python_Examples.Example_partial/Num.py | 3 --- .../Example_polymorphic_const.py | 3 --- .../Num.py | 3 --- .../Example_record_ext.py | 3 --- .../Python_Examples.Example_record_ext/Num.py | 3 --- .../Example_records.py | 3 --- .../Python_Examples.Example_records/Num.py | 3 --- .../Example_super.py | 3 --- .../Example_super_chain.py | 3 --- .../Example_tail_calls.py | 3 --- .../loops/Example_tail_calls_loops.py | 3 --- .../Example_transparent_wrapper.py | 3 --- .../Example_tuples.py | 3 --- .../Python_Examples.Example_tuples/Num.py | 3 --- .../Example_tyclass.py | 3 --- .../Example_unused_arg.py | 3 --- 65 files changed, 14 insertions(+), 205 deletions(-) diff --git a/Python.thy b/Python.thy index ce2639a..9120990 100644 --- a/Python.thy +++ b/Python.thy @@ -13,7 +13,7 @@ code_identifier code_printing constant Code.abort \ (Python) "'_abort" -(* Print undefined as an unimplemented stub, without the warning for a function without code equations *) +(* Print undefined as an abort, without the warning for a function without code equations *) setup \ Code_Python.add_undefined_sym \<^const_name>\HOL.undefined\ \ diff --git a/code_python.ML b/code_python.ML index 73b136a..c86c302 100644 --- a/code_python.ML +++ b/code_python.ML @@ -69,7 +69,7 @@ fun enable_native_encoding name = Native_Encoding_Data.map (Symtab.update (name, fun use_native_encoding thy name = Symtab.defined (Native_Encoding_Data.get thy) name; (* Names bound by the header of a generated module; generated names must not hide these. *) -val header_names = ["dataclass", "Any", "Callable", "functools", "_unimplemented", "_abort"]; +val header_names = ["dataclass", "Any", "Callable", "functools", "_abort"]; (* Keywords and builtins of the target Python, except the wildcard _ printed by the generator; generated names must not hide these. *) @@ -171,8 +171,7 @@ fun invent_names vars prefix n = (* * arguments: - * undefineds: intentionally unimplemented symbols, turn into - * `raise NotImplementedError(...)` + * undefineds: intentionally unimplemented symbols, turn into `_abort(...)` * const_syntax: custom registered code_printing declarations for constants * reserved: context of names that are not useable as new names * args_num: how many arguments needed by the current stmt for saturation @@ -193,6 +192,10 @@ fun print_python_stmt undefineds const_syntax reserved args_num deresolve may rename (`equal` -> `equala`) or module-qualify. *) fun attr_name sym = Long_Name.base_name (deresolve sym); + (* Abort for a constant without code, named by its full name *) + fun print_abort const = + Pretty.block [Pretty.str "_abort(", Pretty.str (print_python_string const), Pretty.str ", None)"]; + (* extract the theory from the context *) val thy = Proof_Context.theory_of ctxt @@ -579,10 +582,9 @@ fun print_python_stmt undefineds const_syntax reserved args_num end and print_app const_syntax some_thm vars fxy (const as { sym, ... }, ts) = - if List.exists (fn name => sym = Constant name) undefineds - then Pretty.block [Pretty.str "_unimplemented(", - Pretty.str (print_python_string (Code_Symbol.default_base sym)), Pretty.str ")"] - else + case find_first (fn name => sym = Constant name) undefineds of + SOME name => print_abort name + | NONE => let fun stock fxy' ts' = gen_print_app (print_app_expr const_syntax) (print_python_expr const_syntax) @@ -711,8 +713,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num val dict_params = print_dict_args vs val head = print_func_head const vctxt dict_params (map SOME params) in Pretty.chunks [head, - indent_block 4 (Pretty.block [Pretty.str "raise NotImplementedError(", - Pretty.str (print_python_string const), Pretty.str ")"])] + indent_block 4 (Pretty.block [Pretty.str "return ", print_abort const])] end (* A pattern-less equation whose rhs is a constant (`f_int = f`) can't be an @@ -1111,14 +1112,11 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, :: Pretty.str "from typing import Any, Callable" :: (if needs_functools mod_name then [Pretty.str "import functools"] else []) @ import_ps) - val unimplemented_def = Pretty.chunks - [Pretty.str "def _unimplemented(name):", - indent_block 4 (Pretty.str "raise NotImplementedError(name)")] 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 (print_header mod_name :: imports_block :: unimplemented_def :: abort_def :: stmt_ps)) + Pretty.chunks2 (print_header mod_name :: imports_block :: abort_def :: stmt_ps)) end; val p = map print_one_module module_stmts diff --git a/test/diff/golden/Python_Examples.Example/Example.py b/test/diff/golden/Python_Examples.Example/Example.py index db5aa3f..69182e6 100644 --- a/test/diff/golden/Python_Examples.Example/Example.py +++ b/test/diff/golden/Python_Examples.Example/Example.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py b/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py index 1d5cc7f..7985deb 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Example_class_dicts.py @@ -8,9 +8,6 @@ import HOL import Orderings -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py index 13a6b23..295414d 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py index 5d4e4a2..da1ce1c 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py @@ -6,9 +6,6 @@ import Orderings import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py index 7061b45..ddbb6b0 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py index 7ffd9ba..355e314 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py @@ -4,9 +4,6 @@ from typing import Any, Callable import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py index f6edf11..65054ca 100644 --- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py +++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py @@ -5,9 +5,6 @@ import functools import Example_classrel_base -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py index 20a0c13..db6ef20 100644 --- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py +++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel_base.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py b/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py index 4a6a858..92f6f83 100644 --- a/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py +++ b/test/diff/golden/Python_Examples.Example_code_numerals/Example_code_numerals.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py +++ b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py index 4bcc279..35eaab6 100644 --- a/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py +++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/Example_generic_list_pair.py @@ -5,9 +5,6 @@ import List import Product_Type -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py index 0da1110..3965e1d 100644 --- a/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py +++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/List.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py b/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py index c53a22c..7cbe8fe 100644 --- a/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py +++ b/test/diff/golden/Python_Examples.Example_generic_list_pair/Product_Type.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py index 904e987..a8cbea7 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py @@ -6,9 +6,6 @@ import Num import Nat -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_iarray/HOL.py b/test/diff/golden/Python_Examples.Example_iarray/HOL.py index 13a6b23..295414d 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/HOL.py +++ b/test/diff/golden/Python_Examples.Example_iarray/HOL.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_iarray/IArray.py b/test/diff/golden/Python_Examples.Example_iarray/IArray.py index f83c743..666c626 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/IArray.py +++ b/test/diff/golden/Python_Examples.Example_iarray/IArray.py @@ -5,9 +5,6 @@ import List import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_iarray/List.py b/test/diff/golden/Python_Examples.Example_iarray/List.py index 8dbbc76..af01ca2 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/List.py +++ b/test/diff/golden/Python_Examples.Example_iarray/List.py @@ -4,9 +4,6 @@ from typing import Any, Callable import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_iarray/Nat.py b/test/diff/golden/Python_Examples.Example_iarray/Nat.py index 2cc85a1..dcf9e15 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Nat.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Nat.py @@ -5,9 +5,6 @@ import functools import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_iarray/Num.py b/test/diff/golden/Python_Examples.Example_iarray/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Num.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py b/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py index d7a3453..9352d20 100644 --- a/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py +++ b/test/diff/golden/Python_Examples.Example_int_arith/Example_int_arith.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_int_arith/Num.py b/test/diff/golden/Python_Examples.Example_int_arith/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_int_arith/Num.py +++ b/test/diff/golden/Python_Examples.Example_int_arith/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py index 9495284..6cefa6b 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py @@ -7,9 +7,6 @@ import Power import Groups -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py index 5907deb..5714cb1 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py @@ -5,9 +5,6 @@ import Arith import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py index 89a738e..d08587a 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py index 730debc..3408c37 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Groups -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py index 2167a10..4bb8e35 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Option -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py index 7c9a46a..b48b0c2 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py index ee9d695..8baf75f 100644 --- a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py +++ b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_lists/Num.py b/test/diff/golden/Python_Examples.Example_lists/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_lists/Num.py +++ b/test/diff/golden/Python_Examples.Example_lists/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py index 59d3e5d..9ce8d1e 100644 --- a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py +++ b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nat/Num.py b/test/diff/golden/Python_Examples.Example_nat/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nat/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py index fe78a55..2e45c53 100644 --- a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py +++ b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Example_nat_edge_cases.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat_edge_cases/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py b/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py index f233a14..adbca63 100644 --- a/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py +++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Example_nat_pattern.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py b/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py index ee9a013..ccce21a 100644 --- a/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py +++ b/test/diff/golden/Python_Examples.Example_nested_case/Example_nested_case.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nested_case/Num.py b/test/diff/golden/Python_Examples.Example_nested_case/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nested_case/Num.py +++ b/test/diff/golden/Python_Examples.Example_nested_case/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py b/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py index 3c1c016..31c486b 100644 --- a/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py +++ b/test/diff/golden/Python_Examples.Example_nested_if/Example_nested_if.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_nested_if/Num.py b/test/diff/golden/Python_Examples.Example_nested_if/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nested_if/Num.py +++ b/test/diff/golden/Python_Examples.Example_nested_if/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py index 0716b49..fc856ac 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py @@ -4,10 +4,7 @@ from typing import Any, Callable import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) -uses_undefined = (_unimplemented("undefined")) +uses_undefined = (_abort("HOL.undefined", None)) diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py index 1127818..754f260 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py @@ -3,11 +3,8 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) def undefined(): - raise NotImplementedError("HOL.undefined") + return _abort("HOL.undefined", None) diff --git a/test/diff/golden/Python_Examples.Example_options/Example_options.py b/test/diff/golden/Python_Examples.Example_options/Example_options.py index 413162d..d6031c7 100644 --- a/test/diff/golden/Python_Examples.Example_options/Example_options.py +++ b/test/diff/golden/Python_Examples.Example_options/Example_options.py @@ -5,9 +5,6 @@ import Num import Option -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_options/Num.py b/test/diff/golden/Python_Examples.Example_options/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_options/Num.py +++ b/test/diff/golden/Python_Examples.Example_options/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_options/Option.py b/test/diff/golden/Python_Examples.Example_options/Option.py index 7c9a46a..b48b0c2 100644 --- a/test/diff/golden/Python_Examples.Example_options/Option.py +++ b/test/diff/golden/Python_Examples.Example_options/Option.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py index 911b320..a1d7803 100644 --- a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py +++ b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_partial/Num.py b/test/diff/golden/Python_Examples.Example_partial/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_partial/Num.py +++ b/test/diff/golden/Python_Examples.Example_partial/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py b/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py index f434726..2e75fc1 100644 --- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py +++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Example_polymorphic_const.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py +++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py index ce74aea..ad25afe 100644 --- a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py +++ b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Num.py b/test/diff/golden/Python_Examples.Example_record_ext/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_record_ext/Num.py +++ b/test/diff/golden/Python_Examples.Example_record_ext/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_records/Example_records.py b/test/diff/golden/Python_Examples.Example_records/Example_records.py index eddbbef..ae7063d 100644 --- a/test/diff/golden/Python_Examples.Example_records/Example_records.py +++ b/test/diff/golden/Python_Examples.Example_records/Example_records.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_records/Num.py b/test/diff/golden/Python_Examples.Example_records/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_records/Num.py +++ b/test/diff/golden/Python_Examples.Example_records/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_super/Example_super.py b/test/diff/golden/Python_Examples.Example_super/Example_super.py index ddea563..905f21d 100644 --- a/test/diff/golden/Python_Examples.Example_super/Example_super.py +++ b/test/diff/golden/Python_Examples.Example_super/Example_super.py @@ -4,9 +4,6 @@ from typing import Any, Callable import functools -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py b/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py index 291b4fe..c1df7d7 100644 --- a/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py +++ b/test/diff/golden/Python_Examples.Example_super_chain/Example_super_chain.py @@ -4,9 +4,6 @@ from typing import Any, Callable import functools -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py index d285d29..7af571d 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/Example_tail_calls.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py index 722a913..47a0930 100644 --- a/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py +++ b/test/diff/golden/Python_Examples.Example_tail_calls/loops/Example_tail_calls_loops.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py b/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py index 286419d..f59286b 100644 --- a/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py +++ b/test/diff/golden/Python_Examples.Example_transparent_wrapper/Example_transparent_wrapper.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py index b441dfb..4323f44 100644 --- a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py +++ b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py @@ -4,9 +4,6 @@ from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_tuples/Num.py b/test/diff/golden/Python_Examples.Example_tuples/Num.py index 9437a5a..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_tuples/Num.py +++ b/test/diff/golden/Python_Examples.Example_tuples/Num.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py index fd6a3b5..4d4fd8f 100644 --- a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py +++ b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py @@ -4,9 +4,6 @@ from typing import Any, Callable import functools -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) diff --git a/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py b/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py index e5b9513..91bed1a 100644 --- a/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py +++ b/test/diff/golden/Python_Examples.Example_unused_arg/Example_unused_arg.py @@ -3,9 +3,6 @@ from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) From a4ce2a6bdd49ce0faf248df6eee9716aef1226d0 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 17:52:18 +0100 Subject: [PATCH 17/30] No warning for a constant without code equations Isabelle leaves a constant without code equations only when it is declared to abort, so every such constant is meant to have no code. The declaration that exempted undefined from the warning goes with it. --- Python.thy | 5 ----- code_python.ML | 6 ++---- .../golden/Python_Examples.Example_no_eqs/Example_no_eqs.py | 2 +- 3 files changed, 3 insertions(+), 10 deletions(-) diff --git a/Python.thy b/Python.thy index 9120990..ead5b8f 100644 --- a/Python.thy +++ b/Python.thy @@ -13,11 +13,6 @@ code_identifier code_printing constant Code.abort \ (Python) "'_abort" -(* Print undefined as an abort, without the warning for a function without code equations *) -setup \ - Code_Python.add_undefined_sym \<^const_name>\HOL.undefined\ -\ - (* unit *) code_printing type_constructor Product_Type.unit \ (Python) "None" diff --git a/code_python.ML b/code_python.ML index c86c302..429cc3f 100644 --- a/code_python.ML +++ b/code_python.ML @@ -743,7 +743,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num | eta_expand_alias _ _ eq = eq; (* This functions needs to distinguish different cases: - * - functions without any code equations => print `pass` + * - functions without any code equations, which are declared to abort => print a stub that aborts * - value definitions (i.e., nullary functions), should not be printed as * python functions, but as simple assignments * - simple functions (i.e., functions that only have one equations, and @@ -752,9 +752,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num * - functions that have multiple equations, or where there is a pattern * in the arguments, these have to use match/case *) - fun print_python_func const (f as { eqs = [], ... }) = - let val _ = warning ("function " ^ const ^ " has no code equations") - in print_undefined_func_stub const f end + fun print_python_func const (f as { eqs = [], ... }) = print_undefined_func_stub const f | print_python_func const { vs, ty, eqs = eqs0 } = let (* same as above, register typevar names to avoid name clashes *) diff --git a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py index fc856ac..c30f789 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py @@ -7,4 +7,4 @@ def _abort(msg, thunk): raise RuntimeError(msg) -uses_undefined = (_abort("HOL.undefined", None)) +uses_undefined = (HOL.undefined()) From 75b68c6ce7c04358b6fa93afe368bf127842e46b Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:00:32 +0100 Subject: [PATCH 18/30] Trailing underscore for a definition with the name of a module An imported module and a definition share the namespace of a module, so a definition named after a module of the program is renamed, as for reserved names, in place of the error. A first pass finds the module names, which don't depend on the names of definitions. --- code_python.ML | 56 +++++++++++++-------------------------- test/quick/Quick_Test.thy | 7 +++++ test/quick/run_test.py | 5 ++++ 3 files changed, 30 insertions(+), 38 deletions(-) diff --git a/code_python.ML b/code_python.ML index 429cc3f..06456ac 100644 --- a/code_python.ML +++ b/code_python.ML @@ -901,25 +901,21 @@ fun print_python_stmt undefineds const_syntax reserved args_num fun python_program_of_program ctxt module_name reserved identifiers exports program = let - (* A name clashing with a keyword or builtin gets a trailing underscore, following PEP 8; Name.variant - would append a letter, and treats a trailing underscore as marking an internal name *) - fun namify_common base ((nsp_class, nsp_object), nsp_common) = + (* A name clashing with a reserved name or a module gets a trailing underscore, following PEP 8, since + an imported module and a definition share the namespace of a module; Name.variant would append a + letter, and treats a trailing underscore as marking an internal name *) + fun namify_common module_names base ((nsp_class, nsp_object), nsp_common) = let - val base' = if Name.is_declared reserved base then base ^ "_" else base; + val base' = + if Name.is_declared reserved base orelse member (op =) module_names base then base ^ "_" else base; val (base'', nsp_common') = if Name.is_declared nsp_common base' then Name.variant base' nsp_common else (base', Name.declare base' nsp_common); in (base'', ((Name.declare base'' nsp_class, Name.declare base'' nsp_object), nsp_common')) end; (* Python doesn't really have any naming restrictions relating to upper/lowercase etc. *) - fun namify_stmt (Code_Thingol.Fun _) = namify_common - | namify_stmt (Code_Thingol.Datatype _) = namify_common - | namify_stmt (Code_Thingol.Datatypecons _) = namify_common - | namify_stmt (Code_Thingol.Class _) = namify_common - | namify_stmt (Code_Thingol.Classrel _) = namify_common - | namify_stmt (Code_Thingol.Classparam _) = namify_common - | namify_stmt (Code_Thingol.Classinst _) = namify_common - | namify_stmt (Code_Thingol.NoStmt) = raise Fail "should not be reached"; + fun namify_stmt _ (Code_Thingol.NoStmt) = raise Fail "should not be reached" + | namify_stmt module_names _ = namify_common module_names; (* Code_Thingol.stmt -> python_stmt option *) fun modify_stmt (Code_Thingol.Fun (_, SOME _)) = NONE @@ -932,13 +928,16 @@ fun python_program_of_program ctxt module_name reserved identifiers exports prog | modify_stmt (Code_Thingol.Classparam _) = NONE | modify_stmt (stmt as Code_Thingol.Classinst _) = SOME stmt | modify_stmt (Code_Thingol.NoStmt) = raise Fail "should not be reached"; - in - Code_Namespace.flat_program ctxt - { module_prefix = "", module_name = module_name, reserved = reserved, - identifiers = identifiers, empty_nsp = ((reserved, reserved), reserved), - namify_stmt = namify_stmt, modify_stmt = modify_stmt } - exports program - end; + fun flat_program module_names = + Code_Namespace.flat_program ctxt + { module_prefix = "", module_name = module_name, reserved = reserved, + identifiers = identifiers, empty_nsp = ((reserved, reserved), reserved), + namify_stmt = namify_stmt module_names, modify_stmt = modify_stmt } + exports program; + + (* Module names don't depend on the names of definitions, so a first pass finds them *) + val module_names = Graph.keys (#flat_program (flat_program [])); + in flat_program module_names end; fun serialize_python undefineds _ ctxt { module_name, reserved_syms, identifiers, includes, const_syntax, ... } program exports = @@ -1057,25 +1056,6 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, val nonempty_names = map #1 module_stmts; - (* Stop if a definition has the name of a module imported by its module, which it would hide *) - fun check_imports (mod_name, imports, _) = - let - val (stmt_gr, _) = Graph.get_node python_program mod_name; - fun binds (sym as Constant _) = not (is_class_param sym) - | binds (Type_Class _) = true - | binds (Class_Instance _) = true - | binds _ = false; - val names = Code_Symbol.Graph.fold (fn (sym, ((base, _), _)) => - if binds sym then insert (op =) base else I) stmt_gr []; - in - case filter (fn (imported, _) => - member (op =) nonempty_names imported andalso member (op =) names imported) imports - of [] => () - | (imported, _) :: _ => - error ("Definition " ^ imported ^ " of module " ^ mod_name ^ " hides imported module " ^ imported) - end; - val _ = List.app check_imports module_stmts; - (* modules that print a cached (dictionary-free) instance need functools *) fun needs_functools mod_name = let val (stmt_gr, _) = Graph.get_node python_program mod_name diff --git a/test/quick/Quick_Test.thy b/test/quick/Quick_Test.thy index 09df44b..fdb606c 100644 --- a/test/quick/Quick_Test.thy +++ b/test/quick/Quick_Test.thy @@ -264,6 +264,12 @@ definition twice_twice :: "'a::plus \ 'a" where "twice_twice = (\x. x + x) \ (\x. x + x)" definition e_twice_twice :: int where "e_twice_twice = twice_twice 3" +section \names of modules\ + +definition Option :: "int option \ int" where + "Option x = (case x of None \ 0 | Some n \ n)" +definition nm_option :: int where "nm_option = Option (map_option (\n. n + 1) (Some 1))" + section \characters\ definition ch_greeting :: string where "ch_greeting = ''hi''" @@ -308,6 +314,7 @@ export_code ia_nth ia_grid ia_get ia_rows ia_head ia_any_neg z_int_div z_int_mod z_nat_div z_nat_mod z_int_floor l_shadow_none l_shadow_some c_boxed e_twice_twice + nm_option ch_greeting ch_digit_yes ch_digit_no ch_code_A ch_literal ch_chars ch_newline ch_quote ch_high in Python file_prefix "." diff --git a/test/quick/run_test.py b/test/quick/run_test.py index dda57ec..ca02087 100644 --- a/test/quick/run_test.py +++ b/test/quick/run_test.py @@ -329,6 +329,11 @@ def test_tail_calls_with_closures_stay_recursive(): assert tc.tc_shift(3, lambda x: x)(0) == 3 +# ---- names of modules ---- + +def test_definition_named_after_module(): + assert m.nm_option == 2 + # ---- characters ---- def test_string_is_list_of_characters(): From f7636c9ad116b59ca21bbaa8a224b7a71e824b0c Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:06:11 +0100 Subject: [PATCH 19/30] Prelude names, in place of header names --- code_python.ML | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/code_python.ML b/code_python.ML index 06456ac..11a0c37 100644 --- a/code_python.ML +++ b/code_python.ML @@ -68,8 +68,8 @@ fun enable_native_encoding name = Native_Encoding_Data.map (Symtab.update (name, fun use_native_encoding thy name = Symtab.defined (Native_Encoding_Data.get thy) name; -(* Names bound by the header of a generated module; generated names must not hide these. *) -val header_names = ["dataclass", "Any", "Callable", "functools", "_abort"]; +(* Names bound by the prelude of every generated module: its imports and the abort function *) +val prelude_names = ["dataclass", "Any", "Callable", "functools", "_abort"]; (* Keywords and builtins of the target Python, except the wildcard _ printed by the generator; generated names must not hide these. *) @@ -1117,6 +1117,6 @@ val _ = Theory.setup "python3 -m py_compile " ^ Bash.string module_name ^ "/*.py")}, evaluation_args = []}) #> (fn thy => fold (Code_Target.add_reserved target) - (distinct (op =) (python_names thy @ header_names)) thy)); + (distinct (op =) (python_names thy @ prelude_names)) thy)); end; (* struct *) From 5f5d5882975476a67630db5cf8a357b946c466a0 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:09:42 +0100 Subject: [PATCH 20/30] Character tests deleted, pending the oracle of #4 --- test/quick/Quick_Test.thy | 14 -------------- test/quick/run_test.py | 21 --------------------- 2 files changed, 35 deletions(-) diff --git a/test/quick/Quick_Test.thy b/test/quick/Quick_Test.thy index fdb606c..48136f4 100644 --- a/test/quick/Quick_Test.thy +++ b/test/quick/Quick_Test.thy @@ -270,19 +270,6 @@ definition Option :: "int option \ int" where "Option x = (case x of None \ 0 | Some n \ n)" definition nm_option :: int where "nm_option = Option (map_option (\n. n + 1) (Some 1))" -section \characters\ - -definition ch_greeting :: string where "ch_greeting = ''hi''" -definition ch_is_digit :: "char \ bool" where "ch_is_digit c = (CHR ''0'' \ c \ c \ CHR ''9'')" -definition ch_digit_yes :: bool where "ch_digit_yes = ch_is_digit (CHR ''7'')" -definition ch_digit_no :: bool where "ch_digit_no = ch_is_digit (CHR ''x'')" -definition ch_code_A :: nat where "ch_code_A = of_char (CHR ''A'')" -definition ch_literal :: String.literal where "ch_literal = String.implode ch_greeting" -definition ch_chars :: string where "ch_chars = String.explode (STR ''ab'')" -definition ch_newline :: char where "ch_newline = CHR 0x0A" -definition ch_quote :: char where "ch_quote = CHR 0x22" -definition ch_high :: char where "ch_high = CHR 0xE9" - section \Code.abort in expression position\ definition a_checked :: "int \ int" where @@ -315,7 +302,6 @@ export_code z_int_div z_int_mod z_nat_div z_nat_mod z_int_floor l_shadow_none l_shadow_some c_boxed e_twice_twice nm_option - ch_greeting ch_digit_yes ch_digit_no ch_code_A ch_literal ch_chars ch_newline ch_quote ch_high in Python file_prefix "." end diff --git a/test/quick/run_test.py b/test/quick/run_test.py index ca02087..9eff5a2 100644 --- a/test/quick/run_test.py +++ b/test/quick/run_test.py @@ -333,24 +333,3 @@ def test_tail_calls_with_closures_stay_recursive(): def test_definition_named_after_module(): assert m.nm_option == 2 - -# ---- characters ---- - -def test_string_is_list_of_characters(): - assert m.ch_greeting == ["h", "i"] - -def test_character_comparison(): - assert m.ch_digit_yes - assert not m.ch_digit_no - -def test_character_code(): - assert m.ch_code_A == 65 - -def test_implode_and_explode(): - assert m.ch_literal == "hi" - assert m.ch_chars == ["a", "b"] - -def test_escaped_characters(): - assert m.ch_newline == "\n" - assert m.ch_quote == '"' - assert m.ch_high == "\xe9" From 8121eed38c3a2a274ab8f3c4858ceaf37cf34f75 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:10:06 +0100 Subject: [PATCH 21/30] Test of a definition named after a module deleted --- test/quick/Quick_Test.thy | 7 ------- test/quick/run_test.py | 6 ------ 2 files changed, 13 deletions(-) diff --git a/test/quick/Quick_Test.thy b/test/quick/Quick_Test.thy index 48136f4..841eb56 100644 --- a/test/quick/Quick_Test.thy +++ b/test/quick/Quick_Test.thy @@ -264,12 +264,6 @@ definition twice_twice :: "'a::plus \ 'a" where "twice_twice = (\x. x + x) \ (\x. x + x)" definition e_twice_twice :: int where "e_twice_twice = twice_twice 3" -section \names of modules\ - -definition Option :: "int option \ int" where - "Option x = (case x of None \ 0 | Some n \ n)" -definition nm_option :: int where "nm_option = Option (map_option (\n. n + 1) (Some 1))" - section \Code.abort in expression position\ definition a_checked :: "int \ int" where @@ -301,7 +295,6 @@ export_code ia_nth ia_grid ia_get ia_rows ia_head ia_any_neg z_int_div z_int_mod z_nat_div z_nat_mod z_int_floor l_shadow_none l_shadow_some c_boxed e_twice_twice - nm_option in Python file_prefix "." end diff --git a/test/quick/run_test.py b/test/quick/run_test.py index 9eff5a2..8cddd9b 100644 --- a/test/quick/run_test.py +++ b/test/quick/run_test.py @@ -327,9 +327,3 @@ def test_tail_calls_with_closures_stay_recursive(): tc = _load_tail_calls() assert tc.tc_shift_small == 13 assert tc.tc_shift(3, lambda x: x)(0) == 3 - - -# ---- names of modules ---- - -def test_definition_named_after_module(): - assert m.nm_option == 2 From 7da3102e9d218b0b185f4b5cfa29fda622eda303 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:17:54 +0100 Subject: [PATCH 22/30] Comment on datatypes as before --- code_python.ML | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/code_python.ML b/code_python.ML index 11a0c37..ab631e1 100644 --- a/code_python.ML +++ b/code_python.ML @@ -108,8 +108,7 @@ datatype python_stmt = eqs: eqtn list (* code equations, see above *) } - (* A datatype definition (turns into one `@dataclass` per constructor, also when every constructor is - nullary, since PurePy has no enumerations) *) + (* A datatype definition (turns into one `@dataclass` per constructor) *) | Datatype of { typarams: vname list, (* type parameter names *) cnstrs: cnstr list (* constructor list, see above *) From afe24790579481d0a63dfc8b01163f865f746b4b Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:19:45 +0100 Subject: [PATCH 23/30] Typos in comment on function printer --- code_python.ML | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/code_python.ML b/code_python.ML index ab631e1..12b4b41 100644 --- a/code_python.ML +++ b/code_python.ML @@ -741,11 +741,11 @@ fun print_python_stmt undefineds const_syntax reserved args_num in { patterns = vars, rhs = rhs `$$ vars, thm = thm } end | eta_expand_alias _ _ eq = eq; - (* This functions needs to distinguish different cases: + (* This function needs to distinguish different cases: * - functions without any code equations, which are declared to abort => print a stub that aborts * - value definitions (i.e., nullary functions), should not be printed as * python functions, but as simple assignments - * - simple functions (i.e., functions that only have one equations, and + * - simple functions (i.e., functions that only have one equation, and * where all the argument patterns are simple variables), * these should be printed as standard python functions * - functions that have multiple equations, or where there is a pattern From bcab221d6df8b1b977f9fa09476acfd61af92e4c Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:23:17 +0100 Subject: [PATCH 24/30] Shorter comment on renaming --- code_python.ML | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/code_python.ML b/code_python.ML index 12b4b41..c3c955b 100644 --- a/code_python.ML +++ b/code_python.ML @@ -900,9 +900,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num fun python_program_of_program ctxt module_name reserved identifiers exports program = let - (* A name clashing with a reserved name or a module gets a trailing underscore, following PEP 8, since - an imported module and a definition share the namespace of a module; Name.variant would append a - letter, and treats a trailing underscore as marking an internal name *) + (* Add a trailing underscore to a name clashing with a reserved name or a module, following PEP 8 *) fun namify_common module_names base ((nsp_class, nsp_object), nsp_common) = let val base' = From 6162de2c8fe0c8b90e0eb4777e19b01ace3df1d5 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:29:28 +0100 Subject: [PATCH 25/30] Trailing underscores for every clash, including duplicate names --- code_python.ML | 14 +++++++------- .../Python_Examples.Example_class_dicts/HOL.py | 4 ++-- .../Python_Examples.Example_class_dicts/Int.py | 2 +- .../Product_Type.py | 4 ++-- .../golden/Python_Examples.Example_iarray/HOL.py | 4 ++-- .../golden/Python_Examples.Example_iarray/Nat.py | 2 +- .../Arith.py | 8 ++++---- .../Groups.py | 4 ++-- .../Power.py | 6 +++--- .../Example_record_ext.py | 16 ++++++++-------- .../Example_records.py | 12 ++++++------ 11 files changed, 38 insertions(+), 38 deletions(-) diff --git a/code_python.ML b/code_python.ML index c3c955b..13e67e4 100644 --- a/code_python.ML +++ b/code_python.ML @@ -900,15 +900,15 @@ fun print_python_stmt undefineds const_syntax reserved args_num fun python_program_of_program ctxt module_name reserved identifiers exports program = let - (* Add a trailing underscore to a name clashing with a reserved name or a module, following PEP 8 *) + (* Add trailing underscores to a name until it is unused and not a module name, following PEP 8 *) fun namify_common module_names base ((nsp_class, nsp_object), nsp_common) = let - val base' = - if Name.is_declared reserved base orelse member (op =) module_names base then base ^ "_" else base; - val (base'', nsp_common') = - if Name.is_declared nsp_common base' then Name.variant base' nsp_common - else (base', Name.declare base' nsp_common); - in (base'', ((Name.declare base'' nsp_class, Name.declare base'' nsp_object), nsp_common')) end; + fun fresh x = + if Name.is_declared nsp_common x orelse member (op =) module_names x then fresh (x ^ "_") else x; + val base' = fresh base; + in + (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), Name.declare base' nsp_common)) + end; (* Python doesn't really have any naming restrictions relating to upper/lowercase etc. *) fun namify_stmt _ (Code_Thingol.NoStmt) = raise Fail "should not be reached" diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py index 295414d..50329ea 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py @@ -8,7 +8,7 @@ def _abort(msg, thunk): @dataclass(frozen=True) class equal: - equala: Callable + equal_: Callable def eq(a_dict, aa, b): - return (a_dict.equala(aa, b)) + return (a_dict.equal_(aa, b)) diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py index da1ce1c..54e02b5 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py @@ -11,7 +11,7 @@ def _abort(msg, thunk): @functools.cache def equal_int(): - return HOL.equal(equala = lambda a, b: (a == b)) + return HOL.equal(equal_ = lambda a, b: (a == b)) @functools.cache def ord_int(): diff --git a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py index 355e314..51679ff 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Product_Type.py @@ -7,10 +7,10 @@ def _abort(msg, thunk): raise RuntimeError(msg) -def equal_proda(a_dict, b_dict, x0, x1): +def equal_prod_(a_dict, b_dict, x0, x1): match (x0, x1): case ((x1a, x2), (y1, y2)): return (HOL.eq(a_dict, x1a, y1) and HOL.eq(b_dict, x2, y2)) def equal_prod(a_dict, b_dict): - return HOL.equal(equala = lambda a, b: equal_proda(a_dict, b_dict, a, b)) + return HOL.equal(equal_ = lambda a, b: equal_prod_(a_dict, b_dict, a, b)) diff --git a/test/diff/golden/Python_Examples.Example_iarray/HOL.py b/test/diff/golden/Python_Examples.Example_iarray/HOL.py index 295414d..50329ea 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/HOL.py +++ b/test/diff/golden/Python_Examples.Example_iarray/HOL.py @@ -8,7 +8,7 @@ def _abort(msg, thunk): @dataclass(frozen=True) class equal: - equala: Callable + equal_: Callable def eq(a_dict, aa, b): - return (a_dict.equala(aa, b)) + return (a_dict.equal_(aa, b)) diff --git a/test/diff/golden/Python_Examples.Example_iarray/Nat.py b/test/diff/golden/Python_Examples.Example_iarray/Nat.py index dcf9e15..ddb7ef3 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Nat.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Nat.py @@ -10,4 +10,4 @@ def _abort(msg, thunk): @functools.cache def equal_nat(): - return HOL.equal(equala = lambda a, b: (a == b)) + return HOL.equal(equal_ = lambda a, b: (a == b)) diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py index 6cefa6b..a69c90b 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Arith.py @@ -12,21 +12,21 @@ def _abort(msg, thunk): @functools.cache def one_integer(): - return Groups.one(onea = lambda : 1) + return Groups.one(one_ = lambda : 1) @functools.cache def times_integer(): - return Groups.times(timesa = lambda a, b: (a * b)) + return Groups.times(times_ = lambda a, b: (a * b)) @functools.cache def power_integer(): return Power.power(one_power = one_integer(), times_power = times_integer()) def drop_bit(i, k): - return ((lambda a, b: a // b if b else 0)(k, Power.powera(power_integer(), 2, (abs(i))))) + return ((lambda a, b: a // b if b else 0)(k, Power.power_(power_integer(), 2, (abs(i))))) def push_bit(i, k): - return ((k * Power.powera(power_integer(), 2, (abs(i))))) + return ((k * Power.power_(power_integer(), 2, (abs(i))))) def sgn_integer(k): if ((k == 0)): diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py index d08587a..76cd8f2 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Groups.py @@ -8,8 +8,8 @@ def _abort(msg, thunk): @dataclass(frozen=True) class one: - onea: Callable + one_: Callable @dataclass(frozen=True) class times: - timesa: Callable + times_: Callable diff --git a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py index 3408c37..da8e6d9 100644 --- a/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py +++ b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Power.py @@ -12,8 +12,8 @@ class power: one_power: Any times_power: Any -def powera(a_dict, aa, n): +def power_(a_dict, aa, n): if ((n == 0)): - return (a_dict.one_power.onea()) + return (a_dict.one_power.one_()) else: - return (a_dict.times_power.timesa(aa, powera(a_dict, aa, (max(0, n - 1))))) + return (a_dict.times_power.times_(aa, power_(a_dict, aa, (max(0, n - 1))))) diff --git a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py index ad25afe..798abf9 100644 --- a/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py +++ b/test/diff/golden/Python_Examples.Example_record_ext/Example_record_ext.py @@ -8,24 +8,24 @@ def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class point_exta: +class point_ext_: px: Any py: Any more: Any @dataclass(frozen=True) -class point3d_exta: +class point3d_ext_: pz: Any more: Any def pz_update(pza, x1): match (pza, x1): - case (pzaa, point_exta(px, py, point3d_exta(pz, more))): - return (point_exta(px, py, point3d_exta((pzaa(pz)), more))) + case (pzaa, point_ext_(px, py, point3d_ext_(pz, more))): + return (point_ext_(px, py, point3d_ext_((pzaa(pz)), more))) def pz(x0): match x0: - case point_exta(px, py, point3d_exta(pz, more)): + case point_ext_(px, py, point3d_ext_(pz, more)): return (pz) def move_z(p, dz): @@ -33,18 +33,18 @@ def move_z(p, dz): def py(x0): match x0: - case point_exta(px, py, more): + case point_ext_(px, py, more): return (py) def px(x0): match x0: - case point_exta(px, py, more): + case point_ext_(px, py, more): return (px) def point3d_sum(p): return ((((px(p) + py(p))) + pz(p))) -origin3d = (point_exta(0, 0, point3d_exta(0, None))) +origin3d = (point_ext_(0, 0, point3d_ext_(0, None))) shifted3d = (move_z(origin3d, 7)) diff --git a/test/diff/golden/Python_Examples.Example_records/Example_records.py b/test/diff/golden/Python_Examples.Example_records/Example_records.py index ae7063d..db04f04 100644 --- a/test/diff/golden/Python_Examples.Example_records/Example_records.py +++ b/test/diff/golden/Python_Examples.Example_records/Example_records.py @@ -8,30 +8,30 @@ def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class point_exta: +class point_ext_: px: Any py: Any more: Any def py(x0): match x0: - case point_exta(px, py, more): + case point_ext_(px, py, more): return (py) def px(x0): match x0: - case point_exta(px, py, more): + case point_ext_(px, py, more): return (px) def point_sum(p, q): return ((((((px(p) + py(p))) + px(q))) + py(q))) -origin = (point_exta(0, 0, None)) +origin = (point_ext_(0, 0, None)) def px_update(pxa, x1): match (pxa, x1): - case (pxaa, point_exta(px, py, more)): - return (point_exta((pxaa(px)), py, more)) + case (pxaa, point_ext_(px, py, more)): + return (point_ext_((pxaa(px)), py, more)) def move_x(p, dx): return (px_update(lambda _: (px(p) + dx), p)) From 59ddfab173f97faa09cb3245f0c288f4e405f358 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:33:24 +0100 Subject: [PATCH 26/30] Comment on first naming pass as an operation --- code_python.ML | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/code_python.ML b/code_python.ML index 13e67e4..85f6c94 100644 --- a/code_python.ML +++ b/code_python.ML @@ -932,7 +932,7 @@ fun python_program_of_program ctxt module_name reserved identifiers exports prog namify_stmt = namify_stmt module_names, modify_stmt = modify_stmt } exports program; - (* Module names don't depend on the names of definitions, so a first pass finds them *) + (* Find the module names by a first pass *) val module_names = Graph.keys (#flat_program (flat_program [])); in flat_program module_names end; From 0616e6090955e8260c957d00396bbda465d06d5d Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:37:15 +0100 Subject: [PATCH 27/30] No fallback for an unknown theory name; table of theory names built once --- code_python.ML | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/code_python.ML b/code_python.ML index 85f6c94..c607eff 100644 --- a/code_python.ML +++ b/code_python.ML @@ -1062,15 +1062,18 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, | _ => false)) stmt_gr false end; + (* Full names of the theories in the context, by short name *) + val theory_long_names = Symtab.make (map (fn thy => (Context.theory_base_name thy, + Context.theory_long_name thy)) (Theory.nodes_of (Proof_Context.theory_of ctxt))); + (* Full names of the theories defining the symbols of a module *) fun source_theories mod_name = - let - val (stmt_gr, _) = Graph.get_node python_program mod_name; - val long_name = Symtab.make (map (fn thy => (Context.theory_base_name thy, - Context.theory_long_name thy)) (Theory.nodes_of (Proof_Context.theory_of ctxt))); - val base_names = Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) - stmt_gr []; - in sort_strings (map (fn name => the_default name (Symtab.lookup long_name name)) base_names) end; + let val (stmt_gr, _) = Graph.get_node python_program mod_name + in + Code_Symbol.Graph.fold (insert (op =) o Code_Symbol.default_prefix ctxt o fst) stmt_gr [] + |> map (the o Symtab.lookup theory_long_names) + |> sort_strings + end; fun print_header mod_name = let val thys = source_theories mod_name From 0b011685e876555e0df3f6ada951197c7cc488a9 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:41:10 +0100 Subject: [PATCH 28/30] Explicit tests in place of caught exceptions for printed constants A constructor replaced by a printing is absent from the program, which the constructor test now checks, and the arity of a constant with a printing is the number of arguments the printing requires. --- code_python.ML | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/code_python.ML b/code_python.ML index c607eff..95ccd78 100644 --- a/code_python.ML +++ b/code_python.ML @@ -175,7 +175,7 @@ fun invent_names vars prefix n = * reserved: context of names that are not useable as new names * args_num: how many arguments needed by the current stmt for saturation * is_class_param: true if the current symbol is a type-class method - * is_constr: true for any datatype constructor + * is_constr: true for a datatype constructor without a printing * ctxt: thoery context (neede to look up record field names) * deresolve: module relative naming resolver *) @@ -229,8 +229,9 @@ fun print_python_stmt undefineds const_syntax reserved args_num in (x :: es, tail) end | _ => ([], t); - (* Allows us to detect constructors that have been pruned by custom printers *) - fun safe_is_constr sym = (case try is_constr sym of SOME b => b | NONE => false) + (* Number of arguments of a constant, as required by its printing if it has one *) + fun const_arity (sym as Constant c) = (case const_syntax c of SOME (k, _) => k | NONE => args_num sym) + | const_arity _ = raise Fail "should never be reached"; (* Create patterns from iterms *) fun pattern_of_iterm vars (IVar NONE) = (PWild, [], [], vars) @@ -241,7 +242,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num if sym = Constant "List.list.Nil" andalso use_native_encoding thy "list" then (PLiteral (Pretty.str "[]"), [], [], vars) - else if safe_is_constr sym andalso args_num sym = 0 + else if is_constr sym andalso args_num sym = 0 then (PClass (deresolve sym, []), [], [], vars) else (* fallback, create a new name + attach guards *) @@ -314,7 +315,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num fun exhaustive (IVar _) = true | exhaustive (IConst { sym, ... }) = - safe_is_constr sym andalso args_num sym = 0 andalso is_sole_constr sym + is_constr sym andalso args_num sym = 0 andalso is_sole_constr sym | exhaustive t = (case Code_Thingol.unfold_const_app t of SOME ({ sym, ... }, args) => @@ -575,7 +576,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num let (* constructors take no dictionaries (as in SML), even when the type has sort constraints, e.g. the abstype morphism vec_lambda of ('a, 'b::finite) vec *) - val dict_pretty = if safe_is_constr sym then [] + val dict_pretty = if is_constr sym then [] else map_filter (print_dicts some_thm vars BR) dictss in call_with ((Pretty.str o deresolve) sym) dict_pretty end end @@ -803,8 +804,8 @@ fun print_python_stmt undefineds const_syntax reserved args_num | creates_closure (ICase { term, clauses, ... }) = creates_closure term orelse exists (creates_closure o snd) clauses | creates_closure t = (case Code_Thingol.unfold_const_app t of - SOME ({ sym, dictss, dom, ... }, ts) => - let val arity = the_default (length dom) (try args_num sym) + SOME ({ sym, dictss, ... }, ts) => + let val arity = const_arity sym in exists creates_closure ts orelse (length ts < arity andalso not (null ts andalso forall null dictss andalso arity = 1)) @@ -992,6 +993,9 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, Code_Thingol.Class (_, (_, classparams)) => classparams | _ => raise Fail "should never be reached"; + (* Datatype constructor, unless replaced by a printing and so absent from the program *) + fun is_constr sym = Code_Symbol.Graph.defined program sym andalso Code_Thingol.is_constr program sym; + fun args_num (sym as Constant const) = (case Code_Symbol.Graph.get_node program sym of Code_Thingol.Fun (((_, ty), []), _) => (length o fst o Code_Thingol.unfold_fun) ty | Code_Thingol.Fun (((_, ty), ((ts, _), _) :: _), _) => @@ -1046,7 +1050,7 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, | (_, SOME (export, stmt)) => SOME (print_python_stmt undefineds const_syntax (make_vars reserved_syms) args_num is_class_param is_value - (Code_Thingol.is_constr program) ctxt (deresolver mod_name) + is_constr ctxt (deresolver mod_name) (sym, (export, python_stmt_of_thingol stmt)))); in (mod_name, imports, stmt_ps) end) |> filter (fn (_, _, stmt_ps) => not (null stmt_ps)); From 6de7f3f3fbd53164d17f985834229597228f7b37 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:43:04 +0100 Subject: [PATCH 29/30] Shorter comment on constant arity --- code_python.ML | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/code_python.ML b/code_python.ML index 95ccd78..c390b45 100644 --- a/code_python.ML +++ b/code_python.ML @@ -229,7 +229,7 @@ fun print_python_stmt undefineds const_syntax reserved args_num in (x :: es, tail) end | _ => ([], t); - (* Number of arguments of a constant, as required by its printing if it has one *) + (* Arity of a constant, or of its printing if it has one *) fun const_arity (sym as Constant c) = (case const_syntax c of SOME (k, _) => k | NONE => args_num sym) | const_arity _ = raise Fail "should never be reached"; From e8bdc123ba38250c613ab522f753f11ff323cb05 Mon Sep 17 00:00:00 2001 From: rolyp's Claude bot <286931723+rolyp-claude-bot@users.noreply.github.com> Date: Sat, 24 Oct 2026 18:44:42 +0100 Subject: [PATCH 30/30] Shorter comment on constructor test --- code_python.ML | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/code_python.ML b/code_python.ML index c390b45..ee78e53 100644 --- a/code_python.ML +++ b/code_python.ML @@ -993,7 +993,7 @@ fun serialize_python undefineds _ ctxt { module_name, reserved_syms, Code_Thingol.Class (_, (_, classparams)) => classparams | _ => raise Fail "should never be reached"; - (* Datatype constructor, unless replaced by a printing and so absent from the program *) + (* Datatype constructor without a printing *) fun is_constr sym = Code_Symbol.Graph.defined program sym andalso Code_Thingol.is_constr program sym; fun args_num (sym as Constant const) = (case Code_Symbol.Graph.get_node program sym