Repository navigation
Native characters, reserved builtins and undefined as stub - #9
Merged
Merged
Conversation
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.
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_.
… show the renaming
.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.
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.
# Conflicts: # code_python.ML # test/diff/golden/Python_Examples.Example_no_eqs/Example_no_eqs.py # test/quick/Quick_Test.thy
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.
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.
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.
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.
rolyp
approved these changes
Oct 24, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.