codegen: bump imandrax-api

packages/imandrax-codegen/CHANGELOG.md

@@ -4,6 +4,10 @@ Versioning scheme: <IMANDRAX_API_VERSION>.<MINOR>.<PATCH>
 
 ## [Unreleased]
 
+## [19.0.0] - 2026-03-25
+
+- imandrax-api update: qcheck
+
 ## [18.6.1] - 2026-03-23
 
 - Fix duplicated option-lib generation

packages/imandrax-codegen/pyproject.toml

@@ -1,6 +1,6 @@
 [project]
 name = "imandrax-codegen"
-version = "18.6.1"
+version = "19.0.0"
 description = "Code generator for ImandraX artifact"
 readme = "README.md"
 authors = [
@@ -10,8 +10,8 @@ requires-python = ">=3.12"
 dependencies = [
     "devtools>=0.12.2",
     "dotenv>=0.9.9",
-    "imandrax-api-models>=18.0.0,<19",
-    "imandrax-api[async]>=0.18.0.1,<0.19",
+    "imandrax-api-models>=19,<20",
+    "imandrax-api[async]>=0.19,<0.20",
     "iml-query>=0.8",
     "pydantic>=2.12.3",
     "pyyaml>=6.0.3",

packages/imandrax-codegen/python/imandrax_codegen/code_of_ast/__main__.py

@@ -7,7 +7,7 @@
 
 import typer
 from imandrax_codegen.ast_deserialize import stmts_of_json
-from imandrax_codegen.unparse import unparse
+from imandrax_codegen.unparse import format_code, gen_preamble, unparse
 
 app = typer.Typer()
 
@@ -48,18 +48,20 @@ def code_of_ocaml_ast(
     stmts = stmts_of_json(json_str)
 
     # Generate Python code
-    python_code = unparse(
+    code = unparse(
         stmts,
-        alias_real_to_float=include_real_to_float_alias,
     )
+    code = unparse(stmts)
+    premable = gen_preamble(code, alias_real_to_float=include_real_to_float_alias)
+    code = format_code(premable + '\n' + code)
 
     # Write output
     if output:
         with Path(output).open('w') as f:
-            f.write(python_code)
+            f.write(code)
             f.write('\n')
     else:
-        typer.echo(python_code)
+        typer.echo(code)
 
 
 if __name__ == '__main__':

packages/imandrax-codegen/test/e2e/python/dune

@@ -5,4 +5,4 @@
   ../../../pyproject.toml
   ../../../uv.lock
   ../../../README.md
-  (glob_files ../../../python/**/*.py)))
+  (source_tree ../../../python)))

packages/imandrax-codegen/test/e2e/python/test_parse_fun_decomp.t

@@ -173,6 +173,50 @@ composite_tuple
 
   ```
 
+infeasible_region_in_trivial_forall
+  $ run_test infeasible_region_in_trivial_forall.yaml
+  ```python
+  from __future__ import annotations
+
+  from dataclasses import dataclass
+  from typing import Generic, TypeAlias, TypeVar
+
+  T = TypeVar('T')
+
+
+  @dataclass
+  class Some(Generic[T]):
+      value: T
+
+
+  option: TypeAlias = Some[T] | None
+
+
+  def test_1():
+      """test_1
+
+      - invariant: None
+      - constraints:
+          - not (List.for_all always_true xs)
+      """
+      raise Exception(
+          'Infeasible region: { reason = "max number of steps (100) reached" }'
+      )
+
+
+  def test_2():
+      """test_2
+
+      - invariant: Some xs
+      - constraints:
+          - List.for_all always_true xs
+      """
+      result: option[list[int]] = check(xs=[])
+      expected: option[list[int]] = Some([])
+      assert result == expected
+
+  ```
+
 list_operations
   $ run_test list_operations.yaml
   ```python

packages/imandrax-codegen/test/e2e/python/test_parse_model.t

@@ -144,6 +144,7 @@ int option none
 
 
   option: TypeAlias = Some[T] | None
+
   a = TypeVar('a')
   w: option[a] = None
 
@@ -166,6 +167,7 @@ int option
 
 
   option: TypeAlias = Some[T] | None
+
   w: option[int] = Some(2)
 
   ```

packages/imandrax-codegen/test/python/test_unparse.py

@@ -134,7 +134,7 @@ def test_2():
         - y >= 1
         - x <= 0
     """
-    result: int = nested_check(y=1, x=0)
+    result: int = nested_check(x=0, y=1)
     expected: int = 1
     assert result == expected
 
@@ -414,7 +414,7 @@ def test_1():
         - not (a = b)
         - not (b = c)
     """
-    result: int = calculate(b=1, c=2, a=0)
+    result: int = calculate(a=0, b=1, c=2)
     expected: int = 0
     assert result == expected
 
@@ -428,7 +428,7 @@ def test_2():
         - a <= b
         - not (a = b)
     """
-    result: int = calculate(a=0, c=1, b=1)
+    result: int = calculate(a=0, b=1, c=1)
     expected: int = 0
     assert result == expected
 
@@ -441,7 +441,7 @@ def test_3():
         - a = b
         - a <= b
     """
-    result: int = calculate(b=0, a=0, c=0)
+    result: int = calculate(a=0, b=0, c=0)
     expected: int = 0
     assert result == expected
 
@@ -456,7 +456,7 @@ def test_4():
         - not (a = b)
         - not (b = c)
     """
-    result: int = calculate(b=0, a=1, c=1)
+    result: int = calculate(a=1, b=0, c=1)
     expected: int = 0
     assert result == expected
 
@@ -471,7 +471,7 @@ def test_5():
         - b <= c
         - not (a = b)
     """
-    result: int = calculate(a=0, c=-1, b=-1)
+    result: int = calculate(a=0, b=-1, c=-1)
     expected: int = 0
     assert result == expected
 
@@ -484,7 +484,7 @@ def test_6():
         - not (a <= b)
         - not (b <= c)
     """
-    result: int = calculate(a=1, c=-1, b=0)
+    result: int = calculate(a=1, b=0, c=-1)
     expected: int = 0
     assert result == expected
 ''')
@@ -768,7 +768,7 @@ def test_3():
         - x >= 1
         - y >= 1
     """
-    result: int = classify(y=1, x=1)
+    result: int = classify(x=1, y=1)
     expected: int = 3
     assert result == expected
 
@@ -783,7 +783,7 @@ def test_4():
         - x >= 1
         - y >= 1
     """
-    result: int = classify(y=2, x=1)
+    result: int = classify(x=1, y=2)
     expected: int = 2
     assert result == expected
 
@@ -797,7 +797,7 @@ def test_5():
         - x >= 1
         - y >= 1
     """
-    result: int = classify(y=1, x=2)
+    result: int = classify(x=2, y=1)
     expected: int = 1
     assert result == expected
 ''')