Native characters, reserved builtins and undefined as stub

.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
 

.python-version

@@ -1 +1 @@
-3.14
+3.12

Python_IArray.thy

@@ -12,8 +12,6 @@ text \<open>
   depend on HOL-Library.IArray.
 \<close>
 
-code_reserved (Python) tuple range all any
-
 code_printing
     type_constructor iarray \<rightharpoonup> (Python) "_ tuple"
   | constant IArray \<rightharpoonup> (Python) "tuple'(_')"

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 \<open>
 \<close>
 
 
-(* 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 \<rightharpoonup> (Python) "str"
+  | constant Code_Abstract_Char.Chr \<rightharpoonup> (Python) "chr'(_')"
+  | constant String.integer_of_char \<rightharpoonup> (Python) "ord'(_')"
+  | constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> (Python) infix 4 "=="
+  | constant "(\<le>) :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> (Python) infixl 35 "<="
+  | constant "(<) :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup> (Python) infixl 35 "<"
+  | constant String.explode \<rightharpoonup> (Python) "list'(_')"
+  | constant String.implode \<rightharpoonup> (Python) "\"\".join'(_')"
+
+(* Each character constant of Code_Abstract_Char as a string literal *)
+setup \<open>
+  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
+\<close>
 
 (* Lists *)
 code_printing

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,15 +105,15 @@ 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,
 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