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/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..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 @@ -38,10 +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. 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 @@ -79,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** @@ -93,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** @@ -106,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, @@ -114,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 929b9fc..ee78e53 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; @@ -67,14 +68,18 @@ 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 bound by the prelude of every generated module: its imports and the abort function *) +val prelude_names = ["dataclass", "Any", "Callable", "functools", "_abort"]; - (* these are symbols we use in addition to the standard reserved words *) - @ ["dataclass", "Any", "Callable", "_unimplemented", "_abort", "functools"];; +(* 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, 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 *) @@ -165,13 +170,12 @@ 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 * 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 *) @@ -187,6 +191,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 @@ -221,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) + (* 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"; (* Create patterns from iterms *) fun pattern_of_iterm vars (IVar NONE) = (PWild, [], [], vars) @@ -233,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 *) @@ -306,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) => @@ -567,16 +576,15 @@ 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 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) @@ -705,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 @@ -735,19 +742,17 @@ 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: - * - functions without any code equations => print `pass` + (* 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 * 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 *) @@ -799,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)) @@ -896,19 +901,19 @@ fun print_python_stmt undefineds const_syntax reserved args_num fun python_program_of_program ctxt module_name reserved identifiers exports program = let - 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; + (* 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 + 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.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 @@ -921,13 +926,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; + + (* Find the module names by a first pass *) + 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 = @@ -985,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 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 of Code_Thingol.Fun (((_, ty), []), _) => (length o fst o Code_Thingol.unfold_fun) ty | Code_Thingol.Fun (((_, ty), ((ts, _), _) :: _), _) => @@ -1039,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)); @@ -1055,6 +1066,25 @@ 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 + 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 + 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 @@ -1064,13 +1094,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 (imports_block :: unimplemented_def :: abort_def :: stmt_ps)) + in ([mod_name ^ ".py"], + Pretty.chunks2 (print_header mod_name :: imports_block :: abort_def :: stmt_ps)) end; val p = map print_one_module module_stmts @@ -1092,6 +1120,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); + #> (fn thy => fold (Code_Target.add_reserved target) + (distinct (op =) (python_names thy @ prelude_names)) 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/test/diff/golden/Python_Examples.Example/Example.py b/test/diff/golden/Python_Examples.Example/Example.py index 70eb3a6..69182e6 100644 --- a/test/diff/golden/Python_Examples.Example/Example.py +++ b/test/diff/golden/Python_Examples.Example/Example.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory Python_Examples.Example; do not edit + 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 78fe428..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 @@ -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 @@ -6,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 ff381e0..50329ea 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/HOL.py @@ -1,15 +1,14 @@ +# Generated by Isabelle from theory HOL.HOL; do not edit + from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @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 77953db..54e02b5 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Int.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Int.py @@ -1,22 +1,21 @@ +# Generated by Isabelle from theory HOL.Int; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools import Orderings import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @functools.cache def equal_int(): - return HOL.equal(equala = lambda a, b: (a == b)) + return HOL.equal(equal_ = lambda a, b: (a == b)) @functools.cache def ord_int(): - return Orderings.ord(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/Num.py b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py index c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Num.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 bf86827..ddbb6b0 100644 --- a/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py +++ b/test/diff/golden/Python_Examples.Example_class_dicts/Orderings.py @@ -1,14 +1,13 @@ +# Generated by Isabelle from theory HOL.Orderings; do not edit + from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class ord: +class ord_: less_eq: Callable less: 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 816caa6..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 @@ -1,17 +1,16 @@ +# Generated by Isabelle from theory HOL.Product_Type; do not edit + from dataclasses import dataclass from typing import Any, Callable import HOL -def _unimplemented(name): - raise NotImplementedError(name) - 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_classrel/Example_classrel.py b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py index c6c9396..65054ca 100644 --- a/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py +++ b/test/diff/golden/Python_Examples.Example_classrel/Example_classrel.py @@ -1,11 +1,10 @@ +# Generated by Isabelle from theory Python_Examples.Example_classrel; do not edit + from dataclasses import dataclass from typing import Any, Callable 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 5a70b24..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory Python_Examples.Example_classrel_base; do not edit + 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 b912cab..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_code_numerals; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_code_numerals/Num.py +++ b/test/diff/golden/Python_Examples.Example_code_numerals/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 f3e0e53..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 @@ -1,11 +1,10 @@ +# 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 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 5935c4c..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.List; do not edit + 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 4477e75..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Product_Type; do not edit + 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 f99cf74..a8cbea7 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Example_iarray.py @@ -1,12 +1,11 @@ +# Generated by Isabelle from theory Python_Examples.Example_iarray; do not edit + from dataclasses import dataclass from typing import Any, Callable import IArray 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 ff381e0..50329ea 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/HOL.py +++ b/test/diff/golden/Python_Examples.Example_iarray/HOL.py @@ -1,15 +1,14 @@ +# Generated by Isabelle from theory HOL.HOL; do not edit + from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @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/IArray.py b/test/diff/golden/Python_Examples.Example_iarray/IArray.py index a5d0f38..666c626 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/IArray.py +++ b/test/diff/golden/Python_Examples.Example_iarray/IArray.py @@ -1,11 +1,10 @@ +# Generated by Isabelle from theory HOL-Library.IArray; do not edit + from dataclasses import dataclass from typing import Any, Callable 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 1aad452..af01ca2 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/List.py +++ b/test/diff/golden/Python_Examples.Example_iarray/List.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory HOL.List; do not edit + from dataclasses import dataclass 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 c0a5572..ddb7ef3 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Nat.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Nat.py @@ -1,14 +1,13 @@ +# Generated by Isabelle from theory HOL.Nat; do not edit + from dataclasses import dataclass from typing import Any, Callable import functools import HOL -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @functools.cache def equal_nat(): - return HOL.equal(equala = lambda a, b: (a == b)) + return HOL.equal(equal_ = lambda a, b: (a == b)) diff --git a/test/diff/golden/Python_Examples.Example_iarray/Num.py b/test/diff/golden/Python_Examples.Example_iarray/Num.py index c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_iarray/Num.py +++ b/test/diff/golden/Python_Examples.Example_iarray/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 9751940..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_int_arith; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_int_arith/Num.py +++ b/test/diff/golden/Python_Examples.Example_int_arith/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 68365d3..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 @@ -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 @@ -5,29 +7,26 @@ import Power import Groups -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @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/Example_integer_bit_ops.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Example_integer_bit_ops.py index 8ce682f..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 @@ -1,11 +1,10 @@ +# 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 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 1553aac..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 @@ -1,16 +1,15 @@ +# Generated by Isabelle from theory HOL.Groups; do not edit + from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @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/Num.py b/test/diff/golden/Python_Examples.Example_integer_bit_ops/Num.py index c4907ac..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 152fd2d..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory HOL.Power; do not edit + from dataclasses import dataclass from typing import Any, Callable import Groups -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @@ -13,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_lambda_case/Example_lambda_case.py b/test/diff/golden/Python_Examples.Example_lambda_case/Example_lambda_case.py index 6e6f61b..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_lambda_case; do not edit + from dataclasses import dataclass from typing import Any, Callable import Option -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @@ -13,7 +12,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) @@ -27,7 +26,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 645d8a0..b48b0c2 100644 --- a/test/diff/golden/Python_Examples.Example_lambda_case/Option.py +++ b/test/diff/golden/Python_Examples.Example_lambda_case/Option.py @@ -1,14 +1,13 @@ +# Generated by Isabelle from theory HOL.Option; do not edit + from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class Nonea: +class None_: pass @dataclass(frozen=True) class Some: 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 77a01ad..8baf75f 100644 --- a/test/diff/golden/Python_Examples.Example_lists/Example_lists.py +++ b/test/diff/golden/Python_Examples.Example_lists/Example_lists.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_lists; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_lists/Num.py +++ b/test/diff/golden/Python_Examples.Example_lists/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 74b6da9..9ce8d1e 100644 --- a/test/diff/golden/Python_Examples.Example_nat/Example_nat.py +++ b/test/diff/golden/Python_Examples.Example_nat/Example_nat.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_nat; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nat/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 dd06d07..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 @@ -1,10 +1,9 @@ +# 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 -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 c4907ac..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 934f9ad..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_nat_pattern; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py +++ b/test/diff/golden/Python_Examples.Example_nat_pattern/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 5e966dd..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_nested_case; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nested_case/Num.py +++ b/test/diff/golden/Python_Examples.Example_nested_case/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 c273e55..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_nested_if; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_nested_if/Num.py +++ b/test/diff/golden/Python_Examples.Example_nested_if/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 b6e32a6..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_no_eqs; do not edit + from dataclasses import dataclass 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_no_eqs/HOL.py b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py index dab8256..754f260 100644 --- a/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py +++ b/test/diff/golden/Python_Examples.Example_no_eqs/HOL.py @@ -1,11 +1,10 @@ +# Generated by Isabelle from theory HOL.HOL; do not edit + 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 3478ecb..d6031c7 100644 --- a/test/diff/golden/Python_Examples.Example_options/Example_options.py +++ b/test/diff/golden/Python_Examples.Example_options/Example_options.py @@ -1,17 +1,16 @@ +# Generated by Isabelle from theory Python_Examples.Example_options; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num import Option -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) def describe_opt(x0): match x0: - case Option.Nonea(): + case Option.None_(): return (0) case Option.Some(x): return ((x + 1)) @@ -22,7 +21,7 @@ def describe_opt(x0): d1 = (describe_opt(o_some)) -o_none = (Option.Nonea()) +o_none = (Option.None_()) d2 = (describe_opt(o_none)) @@ -30,7 +29,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/Num.py b/test/diff/golden/Python_Examples.Example_options/Num.py index c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_options/Num.py +++ b/test/diff/golden/Python_Examples.Example_options/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 645d8a0..b48b0c2 100644 --- a/test/diff/golden/Python_Examples.Example_options/Option.py +++ b/test/diff/golden/Python_Examples.Example_options/Option.py @@ -1,14 +1,13 @@ +# Generated by Isabelle from theory HOL.Option; do not edit + from dataclasses import dataclass from typing import Any, Callable -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class Nonea: +class None_: pass @dataclass(frozen=True) class Some: 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 62419c5..a1d7803 100644 --- a/test/diff/golden/Python_Examples.Example_partial/Example_partial.py +++ b/test/diff/golden/Python_Examples.Example_partial/Example_partial.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_partial; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_partial/Num.py +++ b/test/diff/golden/Python_Examples.Example_partial/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 4993801..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_polymorphic_const; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py +++ b/test/diff/golden/Python_Examples.Example_polymorphic_const/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 013f722..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 @@ -1,32 +1,31 @@ +# Generated by Isabelle from theory Python_Examples.Example_record_ext; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - 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): @@ -34,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_record_ext/Num.py b/test/diff/golden/Python_Examples.Example_record_ext/Num.py index c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_record_ext/Num.py +++ b/test/diff/golden/Python_Examples.Example_record_ext/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 991ce03..db04f04 100644 --- a/test/diff/golden/Python_Examples.Example_records/Example_records.py +++ b/test/diff/golden/Python_Examples.Example_records/Example_records.py @@ -1,38 +1,37 @@ +# Generated by Isabelle from theory Python_Examples.Example_records; do not edit + from dataclasses import dataclass from typing import Any, Callable import Num -def _unimplemented(name): - raise NotImplementedError(name) - 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)) diff --git a/test/diff/golden/Python_Examples.Example_records/Num.py b/test/diff/golden/Python_Examples.Example_records/Num.py index c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_records/Num.py +++ b/test/diff/golden/Python_Examples.Example_records/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 ab75e78..905f21d 100644 --- a/test/diff/golden/Python_Examples.Example_super/Example_super.py +++ b/test/diff/golden/Python_Examples.Example_super/Example_super.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_super; do not edit + from dataclasses import dataclass 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 9a97453..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 @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_super_chain; do not edit + from dataclasses import dataclass 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 105517f..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 @@ -1,14 +1,13 @@ +# 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 -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class ord: +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 a97206b..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 @@ -1,14 +1,13 @@ +# 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 -def _unimplemented(name): - raise NotImplementedError(name) - def _abort(msg, thunk): raise RuntimeError(msg) @dataclass(frozen=True) -class ord: +class ord_: less_eq: Callable less: 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 897a90b..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory Python_Examples.Example_transparent_wrapper; do not edit + 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 a6d17bc..4323f44 100644 --- a/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py +++ b/test/diff/golden/Python_Examples.Example_tuples/Example_tuples.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_tuples; do not edit + from dataclasses import dataclass 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 c4907ac..b751fd5 100644 --- a/test/diff/golden/Python_Examples.Example_tuples/Num.py +++ b/test/diff/golden/Python_Examples.Example_tuples/Num.py @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory HOL.Num; do not edit + 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 0868ed6..4d4fd8f 100644 --- a/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py +++ b/test/diff/golden/Python_Examples.Example_tyclass/Example_tyclass.py @@ -1,10 +1,9 @@ +# Generated by Isabelle from theory Python_Examples.Example_tyclass; do not edit + from dataclasses import dataclass 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 63451dd..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 @@ -1,9 +1,8 @@ +# Generated by Isabelle from theory Python_Examples.Example_unused_arg; do not edit + 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/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"