diff --git a/packages/imandrax-codegen/CHANGELOG.md b/packages/imandrax-codegen/CHANGELOG.md index 54b57c10..f95e9fbc 100644 --- a/packages/imandrax-codegen/CHANGELOG.md +++ b/packages/imandrax-codegen/CHANGELOG.md @@ -4,6 +4,10 @@ Versioning scheme: .. ## [Unreleased] +## [19.0.0] - 2026-03-25 + +- imandrax-api update: qcheck + ## [18.6.1] - 2026-03-23 - Fix duplicated option-lib generation diff --git a/packages/imandrax-codegen/pyproject.toml b/packages/imandrax-codegen/pyproject.toml index 85239ae0..682b83d0 100644 --- a/packages/imandrax-codegen/pyproject.toml +++ b/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", diff --git a/packages/imandrax-codegen/python/imandrax_codegen/code_of_ast/__main__.py b/packages/imandrax-codegen/python/imandrax_codegen/code_of_ast/__main__.py index e1015f5f..500170e5 100755 --- a/packages/imandrax-codegen/python/imandrax_codegen/code_of_ast/__main__.py +++ b/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__': diff --git a/packages/imandrax-codegen/test/e2e/python/dune b/packages/imandrax-codegen/test/e2e/python/dune index 43367af2..f9fb9680 100644 --- a/packages/imandrax-codegen/test/e2e/python/dune +++ b/packages/imandrax-codegen/test/e2e/python/dune @@ -5,4 +5,4 @@ ../../../pyproject.toml ../../../uv.lock ../../../README.md - (glob_files ../../../python/**/*.py))) + (source_tree ../../../python))) diff --git a/packages/imandrax-codegen/test/e2e/python/test_parse_fun_decomp.t b/packages/imandrax-codegen/test/e2e/python/test_parse_fun_decomp.t index 025bd445..8277c3e0 100644 --- a/packages/imandrax-codegen/test/e2e/python/test_parse_fun_decomp.t +++ b/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 diff --git a/packages/imandrax-codegen/test/e2e/python/test_parse_model.t b/packages/imandrax-codegen/test/e2e/python/test_parse_model.t index 26c8a850..a8d3fa81 100644 --- a/packages/imandrax-codegen/test/e2e/python/test_parse_model.t +++ b/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) ``` diff --git a/packages/imandrax-codegen/test/python/test_unparse.py b/packages/imandrax-codegen/test/python/test_unparse.py index d0a92f8d..a50b7870 100644 --- a/packages/imandrax-codegen/test/python/test_unparse.py +++ b/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 ''') diff --git a/packages/imandrax-codegen/uv.lock b/packages/imandrax-codegen/uv.lock index 4c40fde8..a6daa3f5 100644 --- a/packages/imandrax-codegen/uv.lock +++ b/packages/imandrax-codegen/uv.lock @@ -405,7 +405,7 @@ wheels = [ [[package]] name = "imandrax-api" -version = "0.18.0.1" +version = "0.19" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "protobuf" }, @@ -413,7 +413,7 @@ dependencies = [ { name = "structlog" }, ] wheels = [ - { url = "https://files.pythonhosted.org/packages/47/9b/2711a0927bc149dcfb377094a6862d9f062e9737537d74009338a66a8c74/imandrax_api-0.18.0.1-py3-none-any.whl", hash = "sha256:2d98d081daee52ad998afa45acd88188b6116615fc80a315e07e2d1bdfe38e06", size = 62246, upload-time = "2026-01-08T18:19:38.786Z" }, + { url = "https://files.pythonhosted.org/packages/19/0e/0c74a21fa340a2d51d2d70a80b29a98bde943bdbc8ed17699c2b2c0c93b5/imandrax_api-0.19-py3-none-any.whl", hash = "sha256:a0a0f1308db34520e9ecd4c859b5065d63baae569c5a6178402338a8fcae67ba", size = 63637, upload-time = "2026-03-12T22:29:33.038Z" }, ] [package.optional-dependencies] @@ -423,21 +423,21 @@ async = [ [[package]] name = "imandrax-api-models" -version = "18.0.0" +version = "19.0.0" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "devtools" }, { name = "imandrax-api", extra = ["async"] }, { name = "pydantic" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/b3/30/6f899ddb11eddb4d6c408f12188ba73225d98750f1858694cd702a256929/imandrax_api_models-18.0.0.tar.gz", hash = "sha256:ba499542ddfd51745785cfc55c69d983695534f3ae94c0f44c20a73fb39a140d", size = 12703, upload-time = "2025-12-15T14:26:00.969Z" } +sdist = { url = "https://files.pythonhosted.org/packages/ab/87/d20ab9f567bdf088170514793dbf8714f979ad0b341505310e515f713a4d/imandrax_api_models-19.0.0.tar.gz", hash = "sha256:7e8ffa0ad7d07412b0344ea5bd9467030d68d2470f9ad7b724e2635827221d29", size = 15833, upload-time = "2026-03-25T13:01:10.658Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/71/e8/5ee9b5245a86b96d942706e5c80ec81e5ca1f0a9f352c3c32ec6c8233c02/imandrax_api_models-18.0.0-py3-none-any.whl", hash = "sha256:7cf3ceaa152e5d6c03bda81228ec9e545f900d622be45dcdf15665fcee5e58b1", size = 17378, upload-time = "2025-12-15T14:25:59.926Z" }, + { url = "https://files.pythonhosted.org/packages/ca/02/20fe54845c70f1399ca8aaef5c4444b642b1fb64ab4f8536f0fc94e5827a/imandrax_api_models-19.0.0-py3-none-any.whl", hash = "sha256:19d0e59cfdde77e231f30fc3d8c3d81f8d185fd54f8caee6b5671462e7fb9751", size = 21278, upload-time = "2026-03-25T13:01:09.353Z" }, ] [[package]] name = "imandrax-codegen" -version = "18.6.1" +version = "19.0.0" source = { editable = "." } dependencies = [ { name = "devtools" }, @@ -462,8 +462,8 @@ dev = [ requires-dist = [ { name = "devtools", specifier = ">=0.12.2" }, { name = "dotenv", specifier = ">=0.9.9" }, - { name = "imandrax-api", extras = ["async"], specifier = ">=0.18.0.1,<0.19" }, - { name = "imandrax-api-models", specifier = ">=18.0.0,<19" }, + { name = "imandrax-api", extras = ["async"], specifier = ">=0.19,<0.20" }, + { name = "imandrax-api-models", specifier = ">=19,<20" }, { name = "iml-query", specifier = ">=0.8" }, { name = "pydantic", specifier = ">=2.12.3" }, { name = "pyyaml", specifier = ">=6.0.3" }, @@ -871,16 +871,16 @@ wheels = [ [[package]] name = "protobuf" -version = "5.29.5" +version = "5.29.6" source = { registry = "https://pypi.org/simple" } -sdist = { url = "https://files.pythonhosted.org/packages/43/29/d09e70352e4e88c9c7a198d5645d7277811448d76c23b00345670f7c8a38/protobuf-5.29.5.tar.gz", hash = "sha256:bc1463bafd4b0929216c35f437a8e28731a2b7fe3d98bb77a600efced5a15c84", size = 425226, upload-time = "2025-05-28T23:51:59.82Z" } +sdist = { url = "https://files.pythonhosted.org/packages/7e/57/394a763c103e0edf87f0938dafcd918d53b4c011dfc5c8ae80f3b0452dbb/protobuf-5.29.6.tar.gz", hash = "sha256:da9ee6a5424b6b30fd5e45c5ea663aef540ca95f9ad99d1e887e819cdf9b8723", size = 425623, upload-time = "2026-02-04T22:54:40.584Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/5f/11/6e40e9fc5bba02988a214c07cf324595789ca7820160bfd1f8be96e48539/protobuf-5.29.5-cp310-abi3-win32.whl", hash = "sha256:3f1c6468a2cfd102ff4703976138844f78ebd1fb45f49011afc5139e9e283079", size = 422963, upload-time = "2025-05-28T23:51:41.204Z" }, - { url = "https://files.pythonhosted.org/packages/81/7f/73cefb093e1a2a7c3ffd839e6f9fcafb7a427d300c7f8aef9c64405d8ac6/protobuf-5.29.5-cp310-abi3-win_amd64.whl", hash = "sha256:3f76e3a3675b4a4d867b52e4a5f5b78a2ef9565549d4037e06cf7b0942b1d3fc", size = 434818, upload-time = "2025-05-28T23:51:44.297Z" }, - { url = "https://files.pythonhosted.org/packages/dd/73/10e1661c21f139f2c6ad9b23040ff36fee624310dc28fba20d33fdae124c/protobuf-5.29.5-cp38-abi3-macosx_10_9_universal2.whl", hash = "sha256:e38c5add5a311f2a6eb0340716ef9b039c1dfa428b28f25a7838ac329204a671", size = 418091, upload-time = "2025-05-28T23:51:45.907Z" }, - { url = "https://files.pythonhosted.org/packages/6c/04/98f6f8cf5b07ab1294c13f34b4e69b3722bb609c5b701d6c169828f9f8aa/protobuf-5.29.5-cp38-abi3-manylinux2014_aarch64.whl", hash = "sha256:fa18533a299d7ab6c55a238bf8629311439995f2e7eca5caaff08663606e9015", size = 319824, upload-time = "2025-05-28T23:51:47.545Z" }, - { url = "https://files.pythonhosted.org/packages/85/e4/07c80521879c2d15f321465ac24c70efe2381378c00bf5e56a0f4fbac8cd/protobuf-5.29.5-cp38-abi3-manylinux2014_x86_64.whl", hash = "sha256:63848923da3325e1bf7e9003d680ce6e14b07e55d0473253a690c3a8b8fd6e61", size = 319942, upload-time = "2025-05-28T23:51:49.11Z" }, - { url = "https://files.pythonhosted.org/packages/7e/cc/7e77861000a0691aeea8f4566e5d3aa716f2b1dece4a24439437e41d3d25/protobuf-5.29.5-py3-none-any.whl", hash = "sha256:6cf42630262c59b2d8de33954443d94b746c952b01434fc58a417fdbd2e84bd5", size = 172823, upload-time = "2025-05-28T23:51:58.157Z" }, + { url = "https://files.pythonhosted.org/packages/d4/88/9ee58ff7863c479d6f8346686d4636dd4c415b0cbeed7a6a7d0617639c2a/protobuf-5.29.6-cp310-abi3-win32.whl", hash = "sha256:62e8a3114992c7c647bce37dcc93647575fc52d50e48de30c6fcb28a6a291eb1", size = 423357, upload-time = "2026-02-04T22:54:25.805Z" }, + { url = "https://files.pythonhosted.org/packages/1c/66/2dc736a4d576847134fb6d80bd995c569b13cdc7b815d669050bf0ce2d2c/protobuf-5.29.6-cp310-abi3-win_amd64.whl", hash = "sha256:7e6ad413275be172f67fdee0f43484b6de5a904cc1c3ea9804cb6fe2ff366eda", size = 435175, upload-time = "2026-02-04T22:54:28.592Z" }, + { url = "https://files.pythonhosted.org/packages/06/db/49b05966fd208ae3f44dcd33837b6243b4915c57561d730a43f881f24dea/protobuf-5.29.6-cp38-abi3-macosx_10_9_universal2.whl", hash = "sha256:b5a169e664b4057183a34bdc424540e86eea47560f3c123a0d64de4e137f9269", size = 418619, upload-time = "2026-02-04T22:54:30.266Z" }, + { url = "https://files.pythonhosted.org/packages/b7/d7/48cbf6b0c3c39761e47a99cb483405f0fde2be22cf00d71ef316ce52b458/protobuf-5.29.6-cp38-abi3-manylinux2014_aarch64.whl", hash = "sha256:a8866b2cff111f0f863c1b3b9e7572dc7eaea23a7fae27f6fc613304046483e6", size = 320284, upload-time = "2026-02-04T22:54:31.782Z" }, + { url = "https://files.pythonhosted.org/packages/e3/dd/cadd6ec43069247d91f6345fa7a0d2858bef6af366dbd7ba8f05d2c77d3b/protobuf-5.29.6-cp38-abi3-manylinux2014_x86_64.whl", hash = "sha256:e3387f44798ac1106af0233c04fb8abf543772ff241169946f698b3a9a3d3ab9", size = 320478, upload-time = "2026-02-04T22:54:32.909Z" }, + { url = "https://files.pythonhosted.org/packages/5a/cb/e3065b447186cb70aa65acc70c86baf482d82bf75625bf5a2c4f6919c6a3/protobuf-5.29.6-py3-none-any.whl", hash = "sha256:6b9edb641441b2da9fa8f428760fc136a49cf97a52076010cf22a2ff73438a86", size = 173126, upload-time = "2026-02-04T22:54:39.462Z" }, ] [[package]]