diff --git a/kimp/k-src/imp-verification.k b/kimp/k-src/imp-verification.k index 988d353..00a5644 100644 --- a/kimp/k-src/imp-verification.k +++ b/kimp/k-src/imp-verification.k @@ -1,4 +1,4 @@ -requires "calls.k" +requires "statements.k" module IMP-VERIFICATION-SYNTAX imports ID-SYNTAX @@ -13,7 +13,7 @@ endmodule module IMP-VERIFICATION imports IMP-VERIFICATION-SYNTAX - imports CALLS + imports STATEMENTS // inequality sign normalization rule A >Int B => B =5.3)"] -dev = ["attrs[docs,tests]", "pre-commit"] +dev = ["attrs[tests]", "pre-commit"] docs = ["furo", "myst-parser", "sphinx", "sphinx-notfound-page", "sphinxcontrib-towncrier", "towncrier", "zope-interface"] tests = ["attrs[tests-no-zope]", "zope-interface"] -tests-no-zope = ["cloudpickle", "hypothesis", "mypy (>=1.1.1)", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"] +tests-mypy = ["mypy (>=1.6)", "pytest-mypy-plugins"] +tests-no-zope = ["attrs[tests-mypy]", "cloudpickle", "hypothesis", "pympler", "pytest (>=4.3.0)", "pytest-xdist[psutil]"] [[package]] name = "autoflake" -version = "2.1.1" +version = "2.3.0" description = "Removes unused imports and unused variables" category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "autoflake-2.1.1-py3-none-any.whl", hash = "sha256:94e330a2bcf5ac01384fb2bf98bea60c6383eaa59ea62be486e376622deba985"}, - {file = "autoflake-2.1.1.tar.gz", hash = "sha256:75524b48d42d6537041d91f17573b8a98cb645642f9f05c7fcc68de10b1cade3"}, + {file = "autoflake-2.3.0-py3-none-any.whl", hash = "sha256:79a51eb8c0744759d2efe052455ab20aa6a314763510c3fd897499a402126327"}, + {file = "autoflake-2.3.0.tar.gz", hash = "sha256:8c2011fa34701b9d7dcf05b9873bc4859d4fce4e62dfea90dffefd1576f5f01d"}, ] [package.dependencies] @@ -37,37 +38,34 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} [[package]] name = "black" -version = "23.3.0" +version = "24.2.0" description = "The uncompromising code formatter." category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "black-23.3.0-cp310-cp310-macosx_10_16_arm64.whl", hash = "sha256:0945e13506be58bf7db93ee5853243eb368ace1c08a24c65ce108986eac65915"}, - {file = "black-23.3.0-cp310-cp310-macosx_10_16_universal2.whl", hash = "sha256:67de8d0c209eb5b330cce2469503de11bca4085880d62f1628bd9972cc3366b9"}, - {file = "black-23.3.0-cp310-cp310-macosx_10_16_x86_64.whl", hash = "sha256:7c3eb7cea23904399866c55826b31c1f55bbcd3890ce22ff70466b907b6775c2"}, - {file = "black-23.3.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:32daa9783106c28815d05b724238e30718f34155653d4d6e125dc7daec8e260c"}, - {file = "black-23.3.0-cp310-cp310-win_amd64.whl", hash = "sha256:35d1381d7a22cc5b2be2f72c7dfdae4072a3336060635718cc7e1ede24221d6c"}, - {file = "black-23.3.0-cp311-cp311-macosx_10_16_arm64.whl", hash = "sha256:a8a968125d0a6a404842fa1bf0b349a568634f856aa08ffaff40ae0dfa52e7c6"}, - {file = "black-23.3.0-cp311-cp311-macosx_10_16_universal2.whl", hash = "sha256:c7ab5790333c448903c4b721b59c0d80b11fe5e9803d8703e84dcb8da56fec1b"}, - {file = "black-23.3.0-cp311-cp311-macosx_10_16_x86_64.whl", hash = "sha256:a6f6886c9869d4daae2d1715ce34a19bbc4b95006d20ed785ca00fa03cba312d"}, - {file = "black-23.3.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6f3c333ea1dd6771b2d3777482429864f8e258899f6ff05826c3a4fcc5ce3f70"}, - {file = "black-23.3.0-cp311-cp311-win_amd64.whl", hash = "sha256:11c410f71b876f961d1de77b9699ad19f939094c3a677323f43d7a29855fe326"}, - {file = "black-23.3.0-cp37-cp37m-macosx_10_16_x86_64.whl", hash = "sha256:1d06691f1eb8de91cd1b322f21e3bfc9efe0c7ca1f0e1eb1db44ea367dff656b"}, - {file = "black-23.3.0-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:50cb33cac881766a5cd9913e10ff75b1e8eb71babf4c7104f2e9c52da1fb7de2"}, - {file = "black-23.3.0-cp37-cp37m-win_amd64.whl", hash = "sha256:e114420bf26b90d4b9daa597351337762b63039752bdf72bf361364c1aa05925"}, - {file = "black-23.3.0-cp38-cp38-macosx_10_16_arm64.whl", hash = "sha256:48f9d345675bb7fbc3dd85821b12487e1b9a75242028adad0333ce36ed2a6d27"}, - {file = "black-23.3.0-cp38-cp38-macosx_10_16_universal2.whl", hash = "sha256:714290490c18fb0126baa0fca0a54ee795f7502b44177e1ce7624ba1c00f2331"}, - {file = "black-23.3.0-cp38-cp38-macosx_10_16_x86_64.whl", hash = "sha256:064101748afa12ad2291c2b91c960be28b817c0c7eaa35bec09cc63aa56493c5"}, - {file = "black-23.3.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:562bd3a70495facf56814293149e51aa1be9931567474993c7942ff7d3533961"}, - {file = "black-23.3.0-cp38-cp38-win_amd64.whl", hash = "sha256:e198cf27888ad6f4ff331ca1c48ffc038848ea9f031a3b40ba36aced7e22f2c8"}, - {file = "black-23.3.0-cp39-cp39-macosx_10_16_arm64.whl", hash = "sha256:3238f2aacf827d18d26db07524e44741233ae09a584273aa059066d644ca7b30"}, - {file = "black-23.3.0-cp39-cp39-macosx_10_16_universal2.whl", hash = "sha256:f0bd2f4a58d6666500542b26354978218a9babcdc972722f4bf90779524515f3"}, - {file = "black-23.3.0-cp39-cp39-macosx_10_16_x86_64.whl", hash = "sha256:92c543f6854c28a3c7f39f4d9b7694f9a6eb9d3c5e2ece488c327b6e7ea9b266"}, - {file = "black-23.3.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3a150542a204124ed00683f0db1f5cf1c2aaaa9cc3495b7a3b5976fb136090ab"}, - {file = "black-23.3.0-cp39-cp39-win_amd64.whl", hash = "sha256:6b39abdfb402002b8a7d030ccc85cf5afff64ee90fa4c5aebc531e3ad0175ddb"}, - {file = "black-23.3.0-py3-none-any.whl", hash = "sha256:ec751418022185b0c1bb7d7736e6933d40bbb14c14a0abcf9123d1b159f98dd4"}, - {file = "black-23.3.0.tar.gz", hash = "sha256:1c7b8d606e728a41ea1ccbd7264677e494e87cf630e399262ced92d4a8dac940"}, + {file = "black-24.2.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:6981eae48b3b33399c8757036c7f5d48a535b962a7c2310d19361edeef64ce29"}, + {file = "black-24.2.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:d533d5e3259720fdbc1b37444491b024003e012c5173f7d06825a77508085430"}, + {file = "black-24.2.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:61a0391772490ddfb8a693c067df1ef5227257e72b0e4108482b8d41b5aee13f"}, + {file = "black-24.2.0-cp310-cp310-win_amd64.whl", hash = "sha256:992e451b04667116680cb88f63449267c13e1ad134f30087dec8527242e9862a"}, + {file = "black-24.2.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:163baf4ef40e6897a2a9b83890e59141cc8c2a98f2dda5080dc15c00ee1e62cd"}, + {file = "black-24.2.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:e37c99f89929af50ffaf912454b3e3b47fd64109659026b678c091a4cd450fb2"}, + {file = "black-24.2.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4f9de21bafcba9683853f6c96c2d515e364aee631b178eaa5145fc1c61a3cc92"}, + {file = "black-24.2.0-cp311-cp311-win_amd64.whl", hash = "sha256:9db528bccb9e8e20c08e716b3b09c6bdd64da0dd129b11e160bf082d4642ac23"}, + {file = "black-24.2.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:d84f29eb3ee44859052073b7636533ec995bd0f64e2fb43aeceefc70090e752b"}, + {file = "black-24.2.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:1e08fb9a15c914b81dd734ddd7fb10513016e5ce7e6704bdd5e1251ceee51ac9"}, + {file = "black-24.2.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:810d445ae6069ce64030c78ff6127cd9cd178a9ac3361435708b907d8a04c693"}, + {file = "black-24.2.0-cp312-cp312-win_amd64.whl", hash = "sha256:ba15742a13de85e9b8f3239c8f807723991fbfae24bad92d34a2b12e81904982"}, + {file = "black-24.2.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:7e53a8c630f71db01b28cd9602a1ada68c937cbf2c333e6ed041390d6968faf4"}, + {file = "black-24.2.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:93601c2deb321b4bad8f95df408e3fb3943d85012dddb6121336b8e24a0d1218"}, + {file = "black-24.2.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a0057f800de6acc4407fe75bb147b0c2b5cbb7c3ed110d3e5999cd01184d53b0"}, + {file = "black-24.2.0-cp38-cp38-win_amd64.whl", hash = "sha256:faf2ee02e6612577ba0181f4347bcbcf591eb122f7841ae5ba233d12c39dcb4d"}, + {file = "black-24.2.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:057c3dc602eaa6fdc451069bd027a1b2635028b575a6c3acfd63193ced20d9c8"}, + {file = "black-24.2.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:08654d0797e65f2423f850fc8e16a0ce50925f9337fb4a4a176a7aa4026e63f8"}, + {file = "black-24.2.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ca610d29415ee1a30a3f30fab7a8f4144e9d34c89a235d81292a1edb2b55f540"}, + {file = "black-24.2.0-cp39-cp39-win_amd64.whl", hash = "sha256:4dd76e9468d5536abd40ffbc7a247f83b2324f0c050556d9c371c2b9a9a95e31"}, + {file = "black-24.2.0-py3-none-any.whl", hash = "sha256:e8a6ae970537e67830776488bca52000eaa37fa63b9988e8c487458d9cd5ace6"}, + {file = "black-24.2.0.tar.gz", hash = "sha256:bce4f25c27c3435e4dace4815bcb2008b87e167e3bf4ee47ccdc5ce906eb4894"}, ] [package.dependencies] @@ -77,10 +75,11 @@ packaging = ">=22.0" pathspec = ">=0.9.0" platformdirs = ">=2" tomli = {version = ">=1.1.0", markers = "python_version < \"3.11\""} +typing-extensions = {version = ">=4.0.1", markers = "python_version < \"3.11\""} [package.extras] colorama = ["colorama (>=0.4.3)"] -d = ["aiohttp (>=3.7.4)"] +d = ["aiohttp (>=3.7.4)", "aiohttp (>=3.7.4,!=3.9.0)"] jupyter = ["ipython (>=7.8.0)", "tokenize-rt (>=3.2.0)"] uvloop = ["uvloop (>=0.15.2)"] @@ -98,14 +97,14 @@ files = [ [[package]] name = "click" -version = "8.1.3" +version = "8.1.7" description = "Composable command line interface toolkit" category = "dev" optional = false python-versions = ">=3.7" files = [ - {file = "click-8.1.3-py3-none-any.whl", hash = "sha256:bb4d8133cb15a609f44e8213d9b391b0809795062913b383c62be0ee95b1db48"}, - {file = "click-8.1.3.tar.gz", hash = "sha256:7682dc8afb30297001674575ea00d1814d808d6a36af415a82bd481d37ba7b8e"}, + {file = "click-8.1.7-py3-none-any.whl", hash = "sha256:ae74fb96c20a0277a1d615f1e4d73c8414f5a98db8b799a7931d1582f3390c28"}, + {file = "click-8.1.7.tar.gz", hash = "sha256:ca9853ad459e787e2192211578cc907e7594e294c7ccc834310722b41b9ca6de"}, ] [package.dependencies] @@ -166,63 +165,64 @@ cron = ["capturer (>=2.4)"] [[package]] name = "coverage" -version = "7.2.5" +version = "7.4.3" description = "Code coverage measurement for Python" category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "coverage-7.2.5-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:883123d0bbe1c136f76b56276074b0c79b5817dd4238097ffa64ac67257f4b6c"}, - {file = "coverage-7.2.5-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:d2fbc2a127e857d2f8898aaabcc34c37771bf78a4d5e17d3e1f5c30cd0cbc62a"}, - {file = "coverage-7.2.5-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:5f3671662dc4b422b15776cdca89c041a6349b4864a43aa2350b6b0b03bbcc7f"}, - {file = "coverage-7.2.5-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:780551e47d62095e088f251f5db428473c26db7829884323e56d9c0c3118791a"}, - {file = "coverage-7.2.5-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:066b44897c493e0dcbc9e6a6d9f8bbb6607ef82367cf6810d387c09f0cd4fe9a"}, - {file = "coverage-7.2.5-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:b9a4ee55174b04f6af539218f9f8083140f61a46eabcaa4234f3c2a452c4ed11"}, - {file = "coverage-7.2.5-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:706ec567267c96717ab9363904d846ec009a48d5f832140b6ad08aad3791b1f5"}, - {file = "coverage-7.2.5-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:ae453f655640157d76209f42c62c64c4d4f2c7f97256d3567e3b439bd5c9b06c"}, - {file = "coverage-7.2.5-cp310-cp310-win32.whl", hash = "sha256:f81c9b4bd8aa747d417407a7f6f0b1469a43b36a85748145e144ac4e8d303cb5"}, - {file = "coverage-7.2.5-cp310-cp310-win_amd64.whl", hash = "sha256:dc945064a8783b86fcce9a0a705abd7db2117d95e340df8a4333f00be5efb64c"}, - {file = "coverage-7.2.5-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:40cc0f91c6cde033da493227797be2826cbf8f388eaa36a0271a97a332bfd7ce"}, - {file = "coverage-7.2.5-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:a66e055254a26c82aead7ff420d9fa8dc2da10c82679ea850d8feebf11074d88"}, - {file = "coverage-7.2.5-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c10fbc8a64aa0f3ed136b0b086b6b577bc64d67d5581acd7cc129af52654384e"}, - {file = "coverage-7.2.5-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9a22cbb5ede6fade0482111fa7f01115ff04039795d7092ed0db43522431b4f2"}, - {file = "coverage-7.2.5-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:292300f76440651529b8ceec283a9370532f4ecba9ad67d120617021bb5ef139"}, - {file = "coverage-7.2.5-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:7ff8f3fb38233035028dbc93715551d81eadc110199e14bbbfa01c5c4a43f8d8"}, - {file = "coverage-7.2.5-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:a08c7401d0b24e8c2982f4e307124b671c6736d40d1c39e09d7a8687bddf83ed"}, - {file = "coverage-7.2.5-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:ef9659d1cda9ce9ac9585c045aaa1e59223b143f2407db0eaee0b61a4f266fb6"}, - {file = "coverage-7.2.5-cp311-cp311-win32.whl", hash = "sha256:30dcaf05adfa69c2a7b9f7dfd9f60bc8e36b282d7ed25c308ef9e114de7fc23b"}, - {file = "coverage-7.2.5-cp311-cp311-win_amd64.whl", hash = "sha256:97072cc90f1009386c8a5b7de9d4fc1a9f91ba5ef2146c55c1f005e7b5c5e068"}, - {file = "coverage-7.2.5-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:bebea5f5ed41f618797ce3ffb4606c64a5de92e9c3f26d26c2e0aae292f015c1"}, - {file = "coverage-7.2.5-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:828189fcdda99aae0d6bf718ea766b2e715eabc1868670a0a07bf8404bf58c33"}, - {file = "coverage-7.2.5-cp37-cp37m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:6e8a95f243d01ba572341c52f89f3acb98a3b6d1d5d830efba86033dd3687ade"}, - {file = "coverage-7.2.5-cp37-cp37m-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e8834e5f17d89e05697c3c043d3e58a8b19682bf365048837383abfe39adaed5"}, - {file = "coverage-7.2.5-cp37-cp37m-musllinux_1_1_aarch64.whl", hash = "sha256:d1f25ee9de21a39b3a8516f2c5feb8de248f17da7eead089c2e04aa097936b47"}, - {file = "coverage-7.2.5-cp37-cp37m-musllinux_1_1_i686.whl", hash = "sha256:1637253b11a18f453e34013c665d8bf15904c9e3c44fbda34c643fbdc9d452cd"}, - {file = "coverage-7.2.5-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:8e575a59315a91ccd00c7757127f6b2488c2f914096077c745c2f1ba5b8c0969"}, - {file = "coverage-7.2.5-cp37-cp37m-win32.whl", hash = "sha256:509ecd8334c380000d259dc66feb191dd0a93b21f2453faa75f7f9cdcefc0718"}, - {file = "coverage-7.2.5-cp37-cp37m-win_amd64.whl", hash = "sha256:12580845917b1e59f8a1c2ffa6af6d0908cb39220f3019e36c110c943dc875b0"}, - {file = "coverage-7.2.5-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:b5016e331b75310610c2cf955d9f58a9749943ed5f7b8cfc0bb89c6134ab0a84"}, - {file = "coverage-7.2.5-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:373ea34dca98f2fdb3e5cb33d83b6d801007a8074f992b80311fc589d3e6b790"}, - {file = "coverage-7.2.5-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a063aad9f7b4c9f9da7b2550eae0a582ffc7623dca1c925e50c3fbde7a579771"}, - {file = "coverage-7.2.5-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:38c0a497a000d50491055805313ed83ddba069353d102ece8aef5d11b5faf045"}, - {file = "coverage-7.2.5-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a2b3b05e22a77bb0ae1a3125126a4e08535961c946b62f30985535ed40e26614"}, - {file = "coverage-7.2.5-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:0342a28617e63ad15d96dca0f7ae9479a37b7d8a295f749c14f3436ea59fdcb3"}, - {file = "coverage-7.2.5-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:cf97ed82ca986e5c637ea286ba2793c85325b30f869bf64d3009ccc1a31ae3fd"}, - {file = "coverage-7.2.5-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:c2c41c1b1866b670573657d584de413df701f482574bad7e28214a2362cb1fd1"}, - {file = "coverage-7.2.5-cp38-cp38-win32.whl", hash = "sha256:10b15394c13544fce02382360cab54e51a9e0fd1bd61ae9ce012c0d1e103c813"}, - {file = "coverage-7.2.5-cp38-cp38-win_amd64.whl", hash = "sha256:a0b273fe6dc655b110e8dc89b8ec7f1a778d78c9fd9b4bda7c384c8906072212"}, - {file = "coverage-7.2.5-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:5c587f52c81211d4530fa6857884d37f514bcf9453bdeee0ff93eaaf906a5c1b"}, - {file = "coverage-7.2.5-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4436cc9ba5414c2c998eaedee5343f49c02ca93b21769c5fdfa4f9d799e84200"}, - {file = "coverage-7.2.5-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6599bf92f33ab041e36e06d25890afbdf12078aacfe1f1d08c713906e49a3fe5"}, - {file = "coverage-7.2.5-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:857abe2fa6a4973f8663e039ead8d22215d31db613ace76e4a98f52ec919068e"}, - {file = "coverage-7.2.5-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f6f5cab2d7f0c12f8187a376cc6582c477d2df91d63f75341307fcdcb5d60303"}, - {file = "coverage-7.2.5-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:aa387bd7489f3e1787ff82068b295bcaafbf6f79c3dad3cbc82ef88ce3f48ad3"}, - {file = "coverage-7.2.5-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:156192e5fd3dbbcb11cd777cc469cf010a294f4c736a2b2c891c77618cb1379a"}, - {file = "coverage-7.2.5-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:bd3b4b8175c1db502adf209d06136c000df4d245105c8839e9d0be71c94aefe1"}, - {file = "coverage-7.2.5-cp39-cp39-win32.whl", hash = "sha256:ddc5a54edb653e9e215f75de377354e2455376f416c4378e1d43b08ec50acc31"}, - {file = "coverage-7.2.5-cp39-cp39-win_amd64.whl", hash = "sha256:338aa9d9883aaaad53695cb14ccdeb36d4060485bb9388446330bef9c361c252"}, - {file = "coverage-7.2.5-pp37.pp38.pp39-none-any.whl", hash = "sha256:8877d9b437b35a85c18e3c6499b23674684bf690f5d96c1006a1ef61f9fdf0f3"}, - {file = "coverage-7.2.5.tar.gz", hash = "sha256:f99ef080288f09ffc687423b8d60978cf3a465d3f404a18d1a05474bd8575a47"}, + {file = "coverage-7.4.3-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:8580b827d4746d47294c0e0b92854c85a92c2227927433998f0d3320ae8a71b6"}, + {file = "coverage-7.4.3-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:718187eeb9849fc6cc23e0d9b092bc2348821c5e1a901c9f8975df0bc785bfd4"}, + {file = "coverage-7.4.3-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:767b35c3a246bcb55b8044fd3a43b8cd553dd1f9f2c1eeb87a302b1f8daa0524"}, + {file = "coverage-7.4.3-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ae7f19afe0cce50039e2c782bff379c7e347cba335429678450b8fe81c4ef96d"}, + {file = "coverage-7.4.3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ba3a8aaed13770e970b3df46980cb068d1c24af1a1968b7818b69af8c4347efb"}, + {file = "coverage-7.4.3-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:ee866acc0861caebb4f2ab79f0b94dbfbdbfadc19f82e6e9c93930f74e11d7a0"}, + {file = "coverage-7.4.3-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:506edb1dd49e13a2d4cac6a5173317b82a23c9d6e8df63efb4f0380de0fbccbc"}, + {file = "coverage-7.4.3-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:fd6545d97c98a192c5ac995d21c894b581f1fd14cf389be90724d21808b657e2"}, + {file = "coverage-7.4.3-cp310-cp310-win32.whl", hash = "sha256:f6a09b360d67e589236a44f0c39218a8efba2593b6abdccc300a8862cffc2f94"}, + {file = "coverage-7.4.3-cp310-cp310-win_amd64.whl", hash = "sha256:18d90523ce7553dd0b7e23cbb28865db23cddfd683a38fb224115f7826de78d0"}, + {file = "coverage-7.4.3-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:cbbe5e739d45a52f3200a771c6d2c7acf89eb2524890a4a3aa1a7fa0695d2a47"}, + {file = "coverage-7.4.3-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:489763b2d037b164846ebac0cbd368b8a4ca56385c4090807ff9fad817de4113"}, + {file = "coverage-7.4.3-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:451f433ad901b3bb00184d83fd83d135fb682d780b38af7944c9faeecb1e0bfe"}, + {file = "coverage-7.4.3-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:fcc66e222cf4c719fe7722a403888b1f5e1682d1679bd780e2b26c18bb648cdc"}, + {file = "coverage-7.4.3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b3ec74cfef2d985e145baae90d9b1b32f85e1741b04cd967aaf9cfa84c1334f3"}, + {file = "coverage-7.4.3-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:abbbd8093c5229c72d4c2926afaee0e6e3140de69d5dcd918b2921f2f0c8baba"}, + {file = "coverage-7.4.3-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:35eb581efdacf7b7422af677b92170da4ef34500467381e805944a3201df2079"}, + {file = "coverage-7.4.3-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:8249b1c7334be8f8c3abcaaa996e1e4927b0e5a23b65f5bf6cfe3180d8ca7840"}, + {file = "coverage-7.4.3-cp311-cp311-win32.whl", hash = "sha256:cf30900aa1ba595312ae41978b95e256e419d8a823af79ce670835409fc02ad3"}, + {file = "coverage-7.4.3-cp311-cp311-win_amd64.whl", hash = "sha256:18c7320695c949de11a351742ee001849912fd57e62a706d83dfc1581897fa2e"}, + {file = "coverage-7.4.3-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:b51bfc348925e92a9bd9b2e48dad13431b57011fd1038f08316e6bf1df107d10"}, + {file = "coverage-7.4.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:d6cdecaedea1ea9e033d8adf6a0ab11107b49571bbb9737175444cea6eb72328"}, + {file = "coverage-7.4.3-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3b2eccb883368f9e972e216c7b4c7c06cabda925b5f06dde0650281cb7666a30"}, + {file = "coverage-7.4.3-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:6c00cdc8fa4e50e1cc1f941a7f2e3e0f26cb2a1233c9696f26963ff58445bac7"}, + {file = "coverage-7.4.3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b9a4a8dd3dcf4cbd3165737358e4d7dfbd9d59902ad11e3b15eebb6393b0446e"}, + {file = "coverage-7.4.3-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:062b0a75d9261e2f9c6d071753f7eef0fc9caf3a2c82d36d76667ba7b6470003"}, + {file = "coverage-7.4.3-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:ebe7c9e67a2d15fa97b77ea6571ce5e1e1f6b0db71d1d5e96f8d2bf134303c1d"}, + {file = "coverage-7.4.3-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:c0a120238dd71c68484f02562f6d446d736adcc6ca0993712289b102705a9a3a"}, + {file = "coverage-7.4.3-cp312-cp312-win32.whl", hash = "sha256:37389611ba54fd6d278fde86eb2c013c8e50232e38f5c68235d09d0a3f8aa352"}, + {file = "coverage-7.4.3-cp312-cp312-win_amd64.whl", hash = "sha256:d25b937a5d9ffa857d41be042b4238dd61db888533b53bc76dc082cb5a15e914"}, + {file = "coverage-7.4.3-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:28ca2098939eabab044ad68850aac8f8db6bf0b29bc7f2887d05889b17346454"}, + {file = "coverage-7.4.3-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:280459f0a03cecbe8800786cdc23067a8fc64c0bd51dc614008d9c36e1659d7e"}, + {file = "coverage-7.4.3-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6c0cdedd3500e0511eac1517bf560149764b7d8e65cb800d8bf1c63ebf39edd2"}, + {file = "coverage-7.4.3-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9a9babb9466fe1da12417a4aed923e90124a534736de6201794a3aea9d98484e"}, + {file = "coverage-7.4.3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:dec9de46a33cf2dd87a5254af095a409ea3bf952d85ad339751e7de6d962cde6"}, + {file = "coverage-7.4.3-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:16bae383a9cc5abab9bb05c10a3e5a52e0a788325dc9ba8499e821885928968c"}, + {file = "coverage-7.4.3-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:2c854ce44e1ee31bda4e318af1dbcfc929026d12c5ed030095ad98197eeeaed0"}, + {file = "coverage-7.4.3-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:ce8c50520f57ec57aa21a63ea4f325c7b657386b3f02ccaedeccf9ebe27686e1"}, + {file = "coverage-7.4.3-cp38-cp38-win32.whl", hash = "sha256:708a3369dcf055c00ddeeaa2b20f0dd1ce664eeabde6623e516c5228b753654f"}, + {file = "coverage-7.4.3-cp38-cp38-win_amd64.whl", hash = "sha256:1bf25fbca0c8d121a3e92a2a0555c7e5bc981aee5c3fdaf4bb7809f410f696b9"}, + {file = "coverage-7.4.3-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:3b253094dbe1b431d3a4ac2f053b6d7ede2664ac559705a704f621742e034f1f"}, + {file = "coverage-7.4.3-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:77fbfc5720cceac9c200054b9fab50cb2a7d79660609200ab83f5db96162d20c"}, + {file = "coverage-7.4.3-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6679060424faa9c11808598504c3ab472de4531c571ab2befa32f4971835788e"}, + {file = "coverage-7.4.3-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:4af154d617c875b52651dd8dd17a31270c495082f3d55f6128e7629658d63765"}, + {file = "coverage-7.4.3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8640f1fde5e1b8e3439fe482cdc2b0bb6c329f4bb161927c28d2e8879c6029ee"}, + {file = "coverage-7.4.3-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:69b9f6f66c0af29642e73a520b6fed25ff9fd69a25975ebe6acb297234eda501"}, + {file = "coverage-7.4.3-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:0842571634f39016a6c03e9d4aba502be652a6e4455fadb73cd3a3a49173e38f"}, + {file = "coverage-7.4.3-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:a78ed23b08e8ab524551f52953a8a05d61c3a760781762aac49f8de6eede8c45"}, + {file = "coverage-7.4.3-cp39-cp39-win32.whl", hash = "sha256:c0524de3ff096e15fcbfe8f056fdb4ea0bf497d584454f344d59fce069d3e6e9"}, + {file = "coverage-7.4.3-cp39-cp39-win_amd64.whl", hash = "sha256:0209a6369ccce576b43bb227dc8322d8ef9e323d089c6f3f26a597b09cb4d2aa"}, + {file = "coverage-7.4.3-pp38.pp39.pp310-none-any.whl", hash = "sha256:7cbde573904625509a3f37b6fecea974e363460b556a627c60dc2f47e2fffa51"}, + {file = "coverage-7.4.3.tar.gz", hash = "sha256:276f6077a5c61447a48d133ed13e759c09e62aff0dc84274a68dc18660104d52"}, ] [package.dependencies] @@ -233,14 +233,14 @@ toml = ["tomli"] [[package]] name = "exceptiongroup" -version = "1.1.1" +version = "1.2.0" description = "Backport of PEP 654 (exception groups)" category = "dev" optional = false python-versions = ">=3.7" files = [ - {file = "exceptiongroup-1.1.1-py3-none-any.whl", hash = "sha256:232c37c63e4f682982c8b6459f33a8981039e5fb8756b2074364e5055c498c9e"}, - {file = "exceptiongroup-1.1.1.tar.gz", hash = "sha256:d484c3090ba2889ae2928419117447a14daf3c1231d5e30d0aae34f354f01785"}, + {file = "exceptiongroup-1.2.0-py3-none-any.whl", hash = "sha256:4bfd3996ac73b41e9b9628b04e079f193850720ea5945fc96a08633c66912f14"}, + {file = "exceptiongroup-1.2.0.tar.gz", hash = "sha256:91f5c769735f051a4290d52edd0858999b57e5876e9f85937691bd4c9fa3ed68"}, ] [package.extras] @@ -248,62 +248,63 @@ test = ["pytest (>=6)"] [[package]] name = "execnet" -version = "1.9.0" +version = "2.0.2" description = "execnet: rapid multi-Python deployment" category = "dev" optional = false -python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" +python-versions = ">=3.7" files = [ - {file = "execnet-1.9.0-py2.py3-none-any.whl", hash = "sha256:a295f7cc774947aac58dde7fdc85f4aa00c42adf5d8f5468fc630c1acf30a142"}, - {file = "execnet-1.9.0.tar.gz", hash = "sha256:8f694f3ba9cc92cab508b152dcfe322153975c29bda272e2fd7f3f00f36e47c5"}, + {file = "execnet-2.0.2-py3-none-any.whl", hash = "sha256:88256416ae766bc9e8895c76a87928c0012183da3cc4fc18016e6f050e025f41"}, + {file = "execnet-2.0.2.tar.gz", hash = "sha256:cc59bc4423742fd71ad227122eb0dd44db51efb3dc4095b45ac9a08c770096af"}, ] [package.extras] -testing = ["pre-commit"] +testing = ["hatch", "pre-commit", "pytest", "tox"] [[package]] name = "filelock" -version = "3.12.0" +version = "3.13.1" description = "A platform independent file lock." category = "main" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "filelock-3.12.0-py3-none-any.whl", hash = "sha256:ad98852315c2ab702aeb628412cbf7e95b7ce8c3bf9565670b4eaecf1db370a9"}, - {file = "filelock-3.12.0.tar.gz", hash = "sha256:fc03ae43288c013d2ea83c8597001b1129db351aad9c57fe2409327916b8e718"}, + {file = "filelock-3.13.1-py3-none-any.whl", hash = "sha256:57dbda9b35157b05fb3e58ee91448612eb674172fab98ee235ccb0b5bee19a1c"}, + {file = "filelock-3.13.1.tar.gz", hash = "sha256:521f5f56c50f8426f5e03ad3b281b490a87ef15bc6c526f168290f0c7148d44e"}, ] [package.extras] -docs = ["furo (>=2023.3.27)", "sphinx (>=6.1.3)", "sphinx-autodoc-typehints (>=1.23,!=1.23.4)"] -testing = ["covdefaults (>=2.3)", "coverage (>=7.2.3)", "diff-cover (>=7.5)", "pytest (>=7.3.1)", "pytest-cov (>=4)", "pytest-mock (>=3.10)", "pytest-timeout (>=2.1)"] +docs = ["furo (>=2023.9.10)", "sphinx (>=7.2.6)", "sphinx-autodoc-typehints (>=1.24)"] +testing = ["covdefaults (>=2.3)", "coverage (>=7.3.2)", "diff-cover (>=8)", "pytest (>=7.4.3)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)", "pytest-timeout (>=2.2)"] +typing = ["typing-extensions (>=4.8)"] [[package]] name = "flake8" -version = "6.0.0" +version = "7.0.0" description = "the modular source code checker: pep8 pyflakes and co" category = "dev" optional = false python-versions = ">=3.8.1" files = [ - {file = "flake8-6.0.0-py2.py3-none-any.whl", hash = "sha256:3833794e27ff64ea4e9cf5d410082a8b97ff1a06c16aa3d2027339cd0f1195c7"}, - {file = "flake8-6.0.0.tar.gz", hash = "sha256:c61007e76655af75e6785a931f452915b371dc48f56efd765247c8fe68f2b181"}, + {file = "flake8-7.0.0-py2.py3-none-any.whl", hash = "sha256:a6dfbb75e03252917f2473ea9653f7cd799c3064e54d4c8140044c5c065f53c3"}, + {file = "flake8-7.0.0.tar.gz", hash = "sha256:33f96621059e65eec474169085dc92bf26e7b2d47366b70be2f67ab80dc25132"}, ] [package.dependencies] mccabe = ">=0.7.0,<0.8.0" -pycodestyle = ">=2.10.0,<2.11.0" -pyflakes = ">=3.0.0,<3.1.0" +pycodestyle = ">=2.11.0,<2.12.0" +pyflakes = ">=3.2.0,<3.3.0" [[package]] name = "flake8-bugbear" -version = "23.3.23" +version = "24.2.6" description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle." category = "dev" optional = false python-versions = ">=3.8.1" files = [ - {file = "flake8-bugbear-23.3.23.tar.gz", hash = "sha256:ea565bdb87b96b56dc499edd6cc3ba7f695373d902a5f56c989b74fad7c7719d"}, - {file = "flake8_bugbear-23.3.23-py3-none-any.whl", hash = "sha256:8a218d13abd6904800970381057ce8e72cde8eea743240c4ef3ede4dd0bc9cfb"}, + {file = "flake8-bugbear-24.2.6.tar.gz", hash = "sha256:f9cb5f2a9e792dd80ff68e89a14c12eed8620af8b41a49d823b7a33064ac9658"}, + {file = "flake8_bugbear-24.2.6-py3-none-any.whl", hash = "sha256:663ef5de80cd32aacd39d362212983bc4636435a6f83700b4ed35acbd0b7d1b8"}, ] [package.dependencies] @@ -315,14 +316,14 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest", [[package]] name = "flake8-comprehensions" -version = "3.12.0" +version = "3.14.0" description = "A flake8 plugin to help you write better list/set/dict comprehensions." category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "flake8_comprehensions-3.12.0-py3-none-any.whl", hash = "sha256:013234637ec7dfcb7cd2900578fb53c512f81db909cefe371c019232695c362d"}, - {file = "flake8_comprehensions-3.12.0.tar.gz", hash = "sha256:419ef1a6e8de929203791a5e8ff5e3906caeba13eb3290eebdbf88a9078d502e"}, + {file = "flake8_comprehensions-3.14.0-py3-none-any.whl", hash = "sha256:7b9d07d94aa88e62099a6d1931ddf16c344d4157deedf90fe0d8ee2846f30e97"}, + {file = "flake8_comprehensions-3.14.0.tar.gz", hash = "sha256:81768c61bfc064e1a06222df08a2580d97de10cb388694becaf987c331c6c0cf"}, ] [package.dependencies] @@ -330,28 +331,29 @@ flake8 = ">=3.0,<3.2.0 || >3.2.0" [[package]] name = "flake8-quotes" -version = "3.3.2" +version = "3.4.0" description = "Flake8 lint for quotes." category = "dev" optional = false python-versions = "*" files = [ - {file = "flake8-quotes-3.3.2.tar.gz", hash = "sha256:6e26892b632dacba517bf27219c459a8396dcfac0f5e8204904c5a4ba9b480e1"}, + {file = "flake8-quotes-3.4.0.tar.gz", hash = "sha256:aad8492fb710a2d3eabe68c5f86a1428de650c8484127e14c43d0504ba30276c"}, ] [package.dependencies] flake8 = "*" +setuptools = "*" [[package]] name = "flake8-type-checking" -version = "2.4.0" +version = "2.9.0" description = "A flake8 plugin for managing type-checking imports & forward references" category = "dev" optional = false python-versions = ">=3.8" files = [ - {file = "flake8_type_checking-2.4.0-py3-none-any.whl", hash = "sha256:2dee127f300bb95b7f17b7c3fff4f6336f5e4ba92082c15928c6e19b666cfba4"}, - {file = "flake8_type_checking-2.4.0.tar.gz", hash = "sha256:9ea96d01e6557a47835acf04020c48fabb9c3d4664c15f2920915e09e65c1d55"}, + {file = "flake8_type_checking-2.9.0-py3-none-any.whl", hash = "sha256:b63e1745f6e7deee1403d7e0150a5bca378315e9fe4d4cdaa7b71338034dbcc3"}, + {file = "flake8_type_checking-2.9.0.tar.gz", hash = "sha256:6fcc0e8a63f6a87b5b26b776388c21907e66c4efbd15dcc1bcbd96fe884da93d"}, ] [package.dependencies] @@ -392,23 +394,23 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "importlib-metadata" -version = "4.13.0" +version = "7.0.1" description = "Read metadata from Python packages" category = "main" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "importlib_metadata-4.13.0-py3-none-any.whl", hash = "sha256:8a8a81bcf996e74fee46f0d16bd3eaa382a7eb20fd82445c3ad11f4090334116"}, - {file = "importlib_metadata-4.13.0.tar.gz", hash = "sha256:dd0173e8f150d6815e098fd354f6414b0f079af4644ddfe90c71e2fc6174346d"}, + {file = "importlib_metadata-7.0.1-py3-none-any.whl", hash = "sha256:4805911c3a4ec7c3966410053e9ec6a1fecd629117df5adee56dfc9432a1081e"}, + {file = "importlib_metadata-7.0.1.tar.gz", hash = "sha256:f238736bb06590ae52ac1fab06a3a9ef1d8dce2b7a35b5ab329371d6c8f5d2cc"}, ] [package.dependencies] zipp = ">=0.5" [package.extras] -docs = ["furo", "jaraco.packaging (>=9)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)"] +docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (<7.2.5)", "sphinx (>=3.5)", "sphinx-lint"] perf = ["ipython"] -testing = ["flake8 (<5)", "flufl.flake8", "importlib-resources (>=1.3)", "packaging", "pyfakefs", "pytest (>=6)", "pytest-black (>=0.3.7)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=1.3)", "pytest-flake8", "pytest-mypy (>=0.9.1)", "pytest-perf (>=0.9.2)"] +testing = ["flufl.flake8", "importlib-resources (>=1.3)", "packaging", "pyfakefs", "pytest (>=6)", "pytest-black (>=0.3.7)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-mypy (>=0.9.1)", "pytest-perf (>=0.9.2)", "pytest-ruff"] [[package]] name = "iniconfig" @@ -424,21 +426,39 @@ files = [ [[package]] name = "isort" -version = "5.12.0" +version = "5.13.2" description = "A Python utility / library to sort Python imports." category = "dev" optional = false python-versions = ">=3.8.0" files = [ - {file = "isort-5.12.0-py3-none-any.whl", hash = "sha256:f84c2818376e66cf843d497486ea8fed8700b340f308f076c6fb1229dff318b6"}, - {file = "isort-5.12.0.tar.gz", hash = "sha256:8bef7dde241278824a6d83f44a544709b065191b95b6e50894bdc722fcba0504"}, + {file = "isort-5.13.2-py3-none-any.whl", hash = "sha256:8ca5e72a8d85860d5a3fa69b8745237f2939afe12dbf656afbcb47fe72d947a6"}, + {file = "isort-5.13.2.tar.gz", hash = "sha256:48fdfcb9face5d58a4f6dde2e72a1fb8dcaf8ab26f95ab49fab84c2ddefb0109"}, +] + +[package.extras] +colors = ["colorama (>=0.4.6)"] + +[[package]] +name = "linkify-it-py" +version = "2.0.3" +description = "Links recognition library with FULL unicode support." +category = "main" +optional = false +python-versions = ">=3.7" +files = [ + {file = "linkify-it-py-2.0.3.tar.gz", hash = "sha256:68cda27e162e9215c17d786649d1da0021a451bdc436ef9e0fa0ba5234b9b048"}, + {file = "linkify_it_py-2.0.3-py3-none-any.whl", hash = "sha256:6bcbc417b0ac14323382aef5c5192c0075bf8a9d6b41820a2b66371eac6b6d79"}, ] +[package.dependencies] +uc-micro-py = "*" + [package.extras] -colors = ["colorama (>=0.4.3)"] -pipfile-deprecated-finder = ["pip-shims (>=0.5.2)", "pipreqs", "requirementslib"] -plugins = ["setuptools"] -requirements-deprecated-finder = ["pip-api", "pipreqs"] +benchmark = ["pytest", "pytest-benchmark"] +dev = ["black", "flake8", "isort", "pre-commit", "pyproject-flake8"] +doc = ["myst-parser", "sphinx", "sphinx-book-theme"] +test = ["coverage", "pytest", "pytest-cov"] [[package]] name = "markdown-it-py" @@ -453,6 +473,8 @@ files = [ ] [package.dependencies] +linkify-it-py = {version = ">=1,<3", optional = true, markers = "extra == \"linkify\""} +mdit-py-plugins = {version = "*", optional = true, markers = "extra == \"plugins\""} mdurl = ">=0.1,<1.0" [package.extras] @@ -477,6 +499,26 @@ files = [ {file = "mccabe-0.7.0.tar.gz", hash = "sha256:348e0240c33b60bbdf4e523192ef919f28cb2c3d7d5c7794f74009290f236325"}, ] +[[package]] +name = "mdit-py-plugins" +version = "0.4.0" +description = "Collection of plugins for markdown-it-py" +category = "main" +optional = false +python-versions = ">=3.8" +files = [ + {file = "mdit_py_plugins-0.4.0-py3-none-any.whl", hash = "sha256:b51b3bb70691f57f974e257e367107857a93b36f322a9e6d44ca5bf28ec2def9"}, + {file = "mdit_py_plugins-0.4.0.tar.gz", hash = "sha256:d8ab27e9aed6c38aa716819fedfde15ca275715955f8a185a8e1cf90fb1d2c1b"}, +] + +[package.dependencies] +markdown-it-py = ">=1.0.0,<4.0.0" + +[package.extras] +code-style = ["pre-commit"] +rtd = ["myst-parser", "sphinx-book-theme"] +testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] + [[package]] name = "mdurl" version = "0.1.2" @@ -491,49 +533,50 @@ files = [ [[package]] name = "mypy" -version = "1.2.0" +version = "1.8.0" description = "Optional static typing for Python" category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "mypy-1.2.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:701189408b460a2ff42b984e6bd45c3f41f0ac9f5f58b8873bbedc511900086d"}, - {file = "mypy-1.2.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:fe91be1c51c90e2afe6827601ca14353bbf3953f343c2129fa1e247d55fd95ba"}, - {file = "mypy-1.2.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8d26b513225ffd3eacece727f4387bdce6469192ef029ca9dd469940158bc89e"}, - {file = "mypy-1.2.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:3a2d219775a120581a0ae8ca392b31f238d452729adbcb6892fa89688cb8306a"}, - {file = "mypy-1.2.0-cp310-cp310-win_amd64.whl", hash = "sha256:2e93a8a553e0394b26c4ca683923b85a69f7ccdc0139e6acd1354cc884fe0128"}, - {file = "mypy-1.2.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:3efde4af6f2d3ccf58ae825495dbb8d74abd6d176ee686ce2ab19bd025273f41"}, - {file = "mypy-1.2.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:695c45cea7e8abb6f088a34a6034b1d273122e5530aeebb9c09626cea6dca4cb"}, - {file = "mypy-1.2.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d0e9464a0af6715852267bf29c9553e4555b61f5904a4fc538547a4d67617937"}, - {file = "mypy-1.2.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:8293a216e902ac12779eb7a08f2bc39ec6c878d7c6025aa59464e0c4c16f7eb9"}, - {file = "mypy-1.2.0-cp311-cp311-win_amd64.whl", hash = "sha256:f46af8d162f3d470d8ffc997aaf7a269996d205f9d746124a179d3abe05ac602"}, - {file = "mypy-1.2.0-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:031fc69c9a7e12bcc5660b74122ed84b3f1c505e762cc4296884096c6d8ee140"}, - {file = "mypy-1.2.0-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:390bc685ec209ada4e9d35068ac6988c60160b2b703072d2850457b62499e336"}, - {file = "mypy-1.2.0-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:4b41412df69ec06ab141808d12e0bf2823717b1c363bd77b4c0820feaa37249e"}, - {file = "mypy-1.2.0-cp37-cp37m-win_amd64.whl", hash = "sha256:4e4a682b3f2489d218751981639cffc4e281d548f9d517addfd5a2917ac78119"}, - {file = "mypy-1.2.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:a197ad3a774f8e74f21e428f0de7f60ad26a8d23437b69638aac2764d1e06a6a"}, - {file = "mypy-1.2.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:c9a084bce1061e55cdc0493a2ad890375af359c766b8ac311ac8120d3a472950"}, - {file = "mypy-1.2.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:eaeaa0888b7f3ccb7bcd40b50497ca30923dba14f385bde4af78fac713d6d6f6"}, - {file = "mypy-1.2.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:bea55fc25b96c53affab852ad94bf111a3083bc1d8b0c76a61dd101d8a388cf5"}, - {file = "mypy-1.2.0-cp38-cp38-win_amd64.whl", hash = "sha256:4c8d8c6b80aa4a1689f2a179d31d86ae1367ea4a12855cc13aa3ba24bb36b2d8"}, - {file = "mypy-1.2.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:70894c5345bea98321a2fe84df35f43ee7bb0feec117a71420c60459fc3e1eed"}, - {file = "mypy-1.2.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4a99fe1768925e4a139aace8f3fb66db3576ee1c30b9c0f70f744ead7e329c9f"}, - {file = "mypy-1.2.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:023fe9e618182ca6317ae89833ba422c411469156b690fde6a315ad10695a521"}, - {file = "mypy-1.2.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:4d19f1a239d59f10fdc31263d48b7937c585810288376671eaf75380b074f238"}, - {file = "mypy-1.2.0-cp39-cp39-win_amd64.whl", hash = "sha256:2de7babe398cb7a85ac7f1fd5c42f396c215ab3eff731b4d761d68d0f6a80f48"}, - {file = "mypy-1.2.0-py3-none-any.whl", hash = "sha256:d8e9187bfcd5ffedbe87403195e1fc340189a68463903c39e2b63307c9fa0394"}, - {file = "mypy-1.2.0.tar.gz", hash = "sha256:f70a40410d774ae23fcb4afbbeca652905a04de7948eaf0b1789c8d1426b72d1"}, + {file = "mypy-1.8.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:485a8942f671120f76afffff70f259e1cd0f0cfe08f81c05d8816d958d4577d3"}, + {file = "mypy-1.8.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:df9824ac11deaf007443e7ed2a4a26bebff98d2bc43c6da21b2b64185da011c4"}, + {file = "mypy-1.8.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2afecd6354bbfb6e0160f4e4ad9ba6e4e003b767dd80d85516e71f2e955ab50d"}, + {file = "mypy-1.8.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:8963b83d53ee733a6e4196954502b33567ad07dfd74851f32be18eb932fb1cb9"}, + {file = "mypy-1.8.0-cp310-cp310-win_amd64.whl", hash = "sha256:e46f44b54ebddbeedbd3d5b289a893219065ef805d95094d16a0af6630f5d410"}, + {file = "mypy-1.8.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:855fe27b80375e5c5878492f0729540db47b186509c98dae341254c8f45f42ae"}, + {file = "mypy-1.8.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:4c886c6cce2d070bd7df4ec4a05a13ee20c0aa60cb587e8d1265b6c03cf91da3"}, + {file = "mypy-1.8.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d19c413b3c07cbecf1f991e2221746b0d2a9410b59cb3f4fb9557f0365a1a817"}, + {file = "mypy-1.8.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9261ed810972061388918c83c3f5cd46079d875026ba97380f3e3978a72f503d"}, + {file = "mypy-1.8.0-cp311-cp311-win_amd64.whl", hash = "sha256:51720c776d148bad2372ca21ca29256ed483aa9a4cdefefcef49006dff2a6835"}, + {file = "mypy-1.8.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:52825b01f5c4c1c4eb0db253ec09c7aa17e1a7304d247c48b6f3599ef40db8bd"}, + {file = "mypy-1.8.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f5ac9a4eeb1ec0f1ccdc6f326bcdb464de5f80eb07fb38b5ddd7b0de6bc61e55"}, + {file = "mypy-1.8.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:afe3fe972c645b4632c563d3f3eff1cdca2fa058f730df2b93a35e3b0c538218"}, + {file = "mypy-1.8.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:42c6680d256ab35637ef88891c6bd02514ccb7e1122133ac96055ff458f93fc3"}, + {file = "mypy-1.8.0-cp312-cp312-win_amd64.whl", hash = "sha256:720a5ca70e136b675af3af63db533c1c8c9181314d207568bbe79051f122669e"}, + {file = "mypy-1.8.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:028cf9f2cae89e202d7b6593cd98db6759379f17a319b5faf4f9978d7084cdc6"}, + {file = "mypy-1.8.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:4e6d97288757e1ddba10dd9549ac27982e3e74a49d8d0179fc14d4365c7add66"}, + {file = "mypy-1.8.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7f1478736fcebb90f97e40aff11a5f253af890c845ee0c850fe80aa060a267c6"}, + {file = "mypy-1.8.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:42419861b43e6962a649068a61f4a4839205a3ef525b858377a960b9e2de6e0d"}, + {file = "mypy-1.8.0-cp38-cp38-win_amd64.whl", hash = "sha256:2b5b6c721bd4aabaadead3a5e6fa85c11c6c795e0c81a7215776ef8afc66de02"}, + {file = "mypy-1.8.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:5c1538c38584029352878a0466f03a8ee7547d7bd9f641f57a0f3017a7c905b8"}, + {file = "mypy-1.8.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4ef4be7baf08a203170f29e89d79064463b7fc7a0908b9d0d5114e8009c3a259"}, + {file = "mypy-1.8.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7178def594014aa6c35a8ff411cf37d682f428b3b5617ca79029d8ae72f5402b"}, + {file = "mypy-1.8.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:ab3c84fa13c04aeeeabb2a7f67a25ef5d77ac9d6486ff33ded762ef353aa5592"}, + {file = "mypy-1.8.0-cp39-cp39-win_amd64.whl", hash = "sha256:99b00bc72855812a60d253420d8a2eae839b0afa4938f09f4d2aa9bb4654263a"}, + {file = "mypy-1.8.0-py3-none-any.whl", hash = "sha256:538fd81bb5e430cc1381a443971c0475582ff9f434c16cd46d2c66763ce85d9d"}, + {file = "mypy-1.8.0.tar.gz", hash = "sha256:6ff8b244d7085a0b425b56d327b480c3b29cafbd2eff27316a004f9a7391ae07"}, ] [package.dependencies] mypy-extensions = ">=1.0.0" tomli = {version = ">=1.1.0", markers = "python_version < \"3.11\""} -typing-extensions = ">=3.10" +typing-extensions = ">=4.1.0" [package.extras] dmypy = ["psutil (>=4.0)"] install-types = ["pip"] -python2 = ["typed-ast (>=1.4.0,<2)"] +mypyc = ["setuptools (>=50)"] reports = ["lxml"] [[package]] @@ -548,40 +591,28 @@ files = [ {file = "mypy_extensions-1.0.0.tar.gz", hash = "sha256:75dbf8955dc00442a438fc4d0666508a9a97b6bd41aa2f0ffe9d2f2725af0782"}, ] -[[package]] -name = "nanoid" -version = "2.0.0" -description = "A tiny, secure, URL-friendly, unique string ID generator for Python" -category = "main" -optional = false -python-versions = "*" -files = [ - {file = "nanoid-2.0.0-py3-none-any.whl", hash = "sha256:90aefa650e328cffb0893bbd4c236cfd44c48bc1f2d0b525ecc53c3187b653bb"}, - {file = "nanoid-2.0.0.tar.gz", hash = "sha256:5a80cad5e9c6e9ae3a41fa2fb34ae189f7cb420b2a5d8f82bd9d23466e4efa68"}, -] - [[package]] name = "packaging" -version = "23.1" +version = "23.2" description = "Core utilities for Python packages" category = "dev" optional = false python-versions = ">=3.7" files = [ - {file = "packaging-23.1-py3-none-any.whl", hash = "sha256:994793af429502c4ea2ebf6bf664629d07c1a9fe974af92966e4b8d2df7edc61"}, - {file = "packaging-23.1.tar.gz", hash = "sha256:a392980d2b6cffa644431898be54b0045151319d1e7ec34f0cfed48767dd334f"}, + {file = "packaging-23.2-py3-none-any.whl", hash = "sha256:8c491190033a9af7e1d931d0b5dacc2ef47509b34dd0de67ed209b5203fc88c7"}, + {file = "packaging-23.2.tar.gz", hash = "sha256:048fb0e9405036518eaaf48a55953c750c11e1a1b68e0dd1a9d62ed0c092cfc5"}, ] [[package]] name = "pathspec" -version = "0.11.1" +version = "0.12.1" description = "Utility library for gitignore style pattern matching of file paths." category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "pathspec-0.11.1-py3-none-any.whl", hash = "sha256:d8af70af76652554bd134c22b3e8a1cc46ed7d91edcdd721ef1a0c51a84a5293"}, - {file = "pathspec-0.11.1.tar.gz", hash = "sha256:2798de800fa92780e33acca925945e9a19a133b715067cf165b8866c15a31687"}, + {file = "pathspec-0.12.1-py3-none-any.whl", hash = "sha256:a0d503e138a4c123b27490a4f7beda6a01c6f288df0e4a8b79c7eb0dc7b4cc08"}, + {file = "pathspec-0.12.1.tar.gz", hash = "sha256:a482d51503a1ab33b1c67a6c3813a26953dbdc71c31dacaef9a838c4e29f5712"}, ] [[package]] @@ -601,30 +632,30 @@ flake8 = ">=5.0.0" [[package]] name = "platformdirs" -version = "3.5.0" +version = "4.2.0" description = "A small Python package for determining appropriate platform-specific dirs, e.g. a \"user data dir\"." category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "platformdirs-3.5.0-py3-none-any.whl", hash = "sha256:47692bc24c1958e8b0f13dd727307cff1db103fca36399f457da8e05f222fdc4"}, - {file = "platformdirs-3.5.0.tar.gz", hash = "sha256:7954a68d0ba23558d753f73437c55f89027cf8f5108c19844d4b82e5af396335"}, + {file = "platformdirs-4.2.0-py3-none-any.whl", hash = "sha256:0614df2a2f37e1a662acbd8e2b25b92ccf8632929bc6d43467e17fe89c75e068"}, + {file = "platformdirs-4.2.0.tar.gz", hash = "sha256:ef0cc731df711022c174543cb70a9b5bd22e5a9337c8624ef2c2ceb8ddad8768"}, ] [package.extras] -docs = ["furo (>=2023.3.27)", "proselint (>=0.13)", "sphinx (>=6.1.3)", "sphinx-autodoc-typehints (>=1.23,!=1.23.4)"] -test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.3.1)", "pytest-cov (>=4)", "pytest-mock (>=3.10)"] +docs = ["furo (>=2023.9.10)", "proselint (>=0.13)", "sphinx (>=7.2.6)", "sphinx-autodoc-typehints (>=1.25.2)"] +test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4.3)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)"] [[package]] name = "pluggy" -version = "1.0.0" +version = "1.4.0" description = "plugin and hook calling mechanisms for python" category = "dev" optional = false -python-versions = ">=3.6" +python-versions = ">=3.8" files = [ - {file = "pluggy-1.0.0-py2.py3-none-any.whl", hash = "sha256:74134bbf457f031a36d68416e1509f34bd5ccc019f0bcc952c7b909d06b37bd3"}, - {file = "pluggy-1.0.0.tar.gz", hash = "sha256:4224373bacce55f955a878bf9cfa763c1e360858e330072059e10bad68531159"}, + {file = "pluggy-1.4.0-py3-none-any.whl", hash = "sha256:7db9f7b503d67d1c5b95f59773ebb58a8c1c288129a88665838012cfb07b8981"}, + {file = "pluggy-1.4.0.tar.gz", hash = "sha256:8c85c2876142a764e5b7548e7d9a0e0ddb46f5185161049a79b7e974454223be"}, ] [package.extras] @@ -660,61 +691,62 @@ test = ["enum34", "ipaddress", "mock", "pywin32", "wmi"] [[package]] name = "pybind11" -version = "2.10.4" +version = "2.11.1" description = "Seamless operability between C++11 and Python" category = "main" optional = false python-versions = ">=3.6" files = [ - {file = "pybind11-2.10.4-py3-none-any.whl", hash = "sha256:ec9be0c45061c829648d7e8c98a7d041768b768c934acd15196e0f1943d9a818"}, - {file = "pybind11-2.10.4.tar.gz", hash = "sha256:0bb621d3c45a049aa5923debb87c5c0e2668227905c55ebe8af722608d8ed927"}, + {file = "pybind11-2.11.1-py3-none-any.whl", hash = "sha256:33cdd02a6453380dd71cc70357ce388ad1ee8d32bd0e38fc22b273d050aa29b3"}, + {file = "pybind11-2.11.1.tar.gz", hash = "sha256:00cd59116a6e8155aecd9174f37ba299d1d397ed4a6b86ac1dfe01b3e40f2cc4"}, ] [package.extras] -global = ["pybind11-global (==2.10.4)"] +global = ["pybind11-global (==2.11.1)"] [[package]] name = "pycodestyle" -version = "2.10.0" +version = "2.11.1" description = "Python style guide checker" category = "dev" optional = false -python-versions = ">=3.6" +python-versions = ">=3.8" files = [ - {file = "pycodestyle-2.10.0-py2.py3-none-any.whl", hash = "sha256:8a4eaf0d0495c7395bdab3589ac2db602797d76207242c17d470186815706610"}, - {file = "pycodestyle-2.10.0.tar.gz", hash = "sha256:347187bdb476329d98f695c213d7295a846d1152ff4fe9bacb8a9590b8ee7053"}, + {file = "pycodestyle-2.11.1-py2.py3-none-any.whl", hash = "sha256:44fe31000b2d866f2e41841b18528a505fbd7fef9017b04eff4e2648a0fadc67"}, + {file = "pycodestyle-2.11.1.tar.gz", hash = "sha256:41ba0e7afc9752dfb53ced5489e89f8186be00e599e712660695b7a75ff2663f"}, ] [[package]] name = "pyflakes" -version = "3.0.1" +version = "3.2.0" description = "passive checker of Python programs" category = "dev" optional = false -python-versions = ">=3.6" +python-versions = ">=3.8" files = [ - {file = "pyflakes-3.0.1-py2.py3-none-any.whl", hash = "sha256:ec55bf7fe21fff7f1ad2f7da62363d749e2a470500eab1b555334b67aa1ef8cf"}, - {file = "pyflakes-3.0.1.tar.gz", hash = "sha256:ec8b276a6b60bd80defed25add7e439881c19e64850afd9b346283d4165fd0fd"}, + {file = "pyflakes-3.2.0-py2.py3-none-any.whl", hash = "sha256:84b5be138a2dfbb40689ca07e2152deb896a65c3a3e24c251c5c62489568074a"}, + {file = "pyflakes-3.2.0.tar.gz", hash = "sha256:1c61603ff154621fb2a9172037d84dca3500def8c8b630657d1701f026f8af3f"}, ] [[package]] name = "pygments" -version = "2.15.1" +version = "2.17.2" description = "Pygments is a syntax highlighting package written in Python." category = "main" optional = false python-versions = ">=3.7" files = [ - {file = "Pygments-2.15.1-py3-none-any.whl", hash = "sha256:db2db3deb4b4179f399a09054b023b6a586b76499d36965813c71aa8ed7b5fd1"}, - {file = "Pygments-2.15.1.tar.gz", hash = "sha256:8ace4d3c1dd481894b2005f560ead0f9f19ee64fe983366be1a21e171d12775c"}, + {file = "pygments-2.17.2-py3-none-any.whl", hash = "sha256:b27c2826c47d0f3219f29554824c30c5e8945175d888647acd804ddd04af846c"}, + {file = "pygments-2.17.2.tar.gz", hash = "sha256:da46cec9fd2de5be3a8a784f434e4c4ab670b4ff54d605c4c2717e9d49c4c367"}, ] [package.extras] plugins = ["importlib-metadata"] +windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.272" +version = "0.1.679" description = "" category = "main" optional = false @@ -727,16 +759,17 @@ cmd2 = "^2.4.2" coloredlogs = "^15.0.1" filelock = "^3.9.0" graphviz = "^0.20.1" -psutil = "^5.9.4" +psutil = "5.9.5" pybind11 = "^2.10.3" -textual = "^0.10.1" +textual = "^0.27.0" tomli = "^2.0.1" +xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "subproofs" -resolved_reference = "3b602b2bde5111ad6382e8873d9297763cf6a761" +reference = "v0.1.679" +resolved_reference = "66c283fc5533f02d9eb504ff9fc0c292995ad9cc" [[package]] name = "pyperclip" @@ -763,14 +796,14 @@ files = [ [[package]] name = "pytest" -version = "7.3.1" +version = "8.0.2" description = "pytest: simple powerful testing with Python" category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "pytest-7.3.1-py3-none-any.whl", hash = "sha256:3799fa815351fea3a5e96ac7e503a96fa51cc9942c3753cda7651b93c1cfa362"}, - {file = "pytest-7.3.1.tar.gz", hash = "sha256:434afafd78b1d78ed0addf160ad2b77a30d35d4bdf8af234fe621919d9ed15e3"}, + {file = "pytest-8.0.2-py3-none-any.whl", hash = "sha256:edfaaef32ce5172d5466b5127b42e0d6d35ebbe4453f0e3505d96afd93f6b096"}, + {file = "pytest-8.0.2.tar.gz", hash = "sha256:d4051d623a2e0b7e51960ba963193b09ce6daeb9759a451844a21e4ddedfc1bd"}, ] [package.dependencies] @@ -778,22 +811,22 @@ colorama = {version = "*", markers = "sys_platform == \"win32\""} exceptiongroup = {version = ">=1.0.0rc8", markers = "python_version < \"3.11\""} iniconfig = "*" packaging = "*" -pluggy = ">=0.12,<2.0" +pluggy = ">=1.3.0,<2.0" tomli = {version = ">=1.0.0", markers = "python_version < \"3.11\""} [package.extras] -testing = ["argcomplete", "attrs (>=19.2.0)", "hypothesis (>=3.56)", "mock", "nose", "pygments (>=2.7.2)", "requests", "xmlschema"] +testing = ["argcomplete", "attrs (>=19.2.0)", "hypothesis (>=3.56)", "mock", "nose", "pygments (>=2.7.2)", "requests", "setuptools", "xmlschema"] [[package]] name = "pytest-cov" -version = "4.0.0" +version = "4.1.0" description = "Pytest plugin for measuring coverage." category = "dev" optional = false -python-versions = ">=3.6" +python-versions = ">=3.7" files = [ - {file = "pytest-cov-4.0.0.tar.gz", hash = "sha256:996b79efde6433cdbd0088872dbc5fb3ed7fe1578b68cdbba634f14bb8dd0470"}, - {file = "pytest_cov-4.0.0-py3-none-any.whl", hash = "sha256:2feb1b751d66a8bd934e5edfa2e961d11309dc37b73b0eabe73b5945fee20f6b"}, + {file = "pytest-cov-4.1.0.tar.gz", hash = "sha256:3904b13dfbfec47f003b8e77fd5b589cd11904a21ddf1ab38a64f204d6a10ef6"}, + {file = "pytest_cov-4.1.0-py3-none-any.whl", hash = "sha256:6ba70b9e97e69fcc3fb45bfeab2d0a138fb65c4d0d6a41ef33983ad114be8c3a"}, ] [package.dependencies] @@ -805,14 +838,14 @@ testing = ["fields", "hunter", "process-tests", "pytest-xdist", "six", "virtuale [[package]] name = "pytest-mock" -version = "3.10.0" +version = "3.12.0" description = "Thin-wrapper around the mock package for easier use with pytest" category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "pytest-mock-3.10.0.tar.gz", hash = "sha256:fbbdb085ef7c252a326fd8cdcac0aa3b1333d8811f131bdcc701002e1be7ed4f"}, - {file = "pytest_mock-3.10.0-py3-none-any.whl", hash = "sha256:f4c973eeae0282963eb293eb173ce91b091a79c1334455acfac9ddee8a1c784b"}, + {file = "pytest-mock-3.12.0.tar.gz", hash = "sha256:31a40f038c22cad32287bb43932054451ff5583ff094bca6f675df2f8bc1a6e9"}, + {file = "pytest_mock-3.12.0-py3-none-any.whl", hash = "sha256:0972719a7263072da3a21c7f4773069bcc7486027d7e8e1f81d98a47e701bc4f"}, ] [package.dependencies] @@ -823,14 +856,14 @@ dev = ["pre-commit", "pytest-asyncio", "tox"] [[package]] name = "pytest-xdist" -version = "3.2.1" +version = "3.5.0" description = "pytest xdist plugin for distributed testing, most importantly across multiple CPUs" category = "dev" optional = false python-versions = ">=3.7" files = [ - {file = "pytest-xdist-3.2.1.tar.gz", hash = "sha256:1849bd98d8b242b948e472db7478e090bf3361912a8fed87992ed94085f54727"}, - {file = "pytest_xdist-3.2.1-py3-none-any.whl", hash = "sha256:37290d161638a20b672401deef1cba812d110ac27e35d213f091d15b8beb40c9"}, + {file = "pytest-xdist-3.5.0.tar.gz", hash = "sha256:cbb36f3d67e0c478baa57fa4edc8843887e0f6cfc42d677530a36d7472b32d8a"}, + {file = "pytest_xdist-3.5.0-py3-none-any.whl", hash = "sha256:d075629c7e00b611df89f490a5063944bee7a4362a5ff11c7cc7824a03dfce24"}, ] [package.dependencies] @@ -844,68 +877,86 @@ testing = ["filelock"] [[package]] name = "pyupgrade" -version = "3.3.2" +version = "3.15.1" description = "A tool to automatically upgrade syntax for newer versions." category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8.1" files = [ - {file = "pyupgrade-3.3.2-py2.py3-none-any.whl", hash = "sha256:c05b82c911934b3a638b29f48f48dc6e0ef6c57c55ec36f2b41ae9dbf6711b4b"}, - {file = "pyupgrade-3.3.2.tar.gz", hash = "sha256:bcfed63d38811809f179fd269dec246680b0aaa5bbe662b535826e5fa2275219"}, + {file = "pyupgrade-3.15.1-py2.py3-none-any.whl", hash = "sha256:c5e005de2805edcd333d1deb04553200ec69da85e4bc9db37b16345ed9e27ed9"}, + {file = "pyupgrade-3.15.1.tar.gz", hash = "sha256:7690857cae0f6253f39241dcd2e57118c333c438b78609fc3c17a5aa61227b7d"}, ] [package.dependencies] -tokenize-rt = ">=3.2.0" +tokenize-rt = ">=5.2.0" [[package]] name = "rich" -version = "13.3.5" +version = "13.7.1" description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" category = "main" optional = false python-versions = ">=3.7.0" files = [ - {file = "rich-13.3.5-py3-none-any.whl", hash = "sha256:69cdf53799e63f38b95b9bf9c875f8c90e78dd62b2f00c13a911c7a3b9fa4704"}, - {file = "rich-13.3.5.tar.gz", hash = "sha256:2d11b9b8dd03868f09b4fffadc84a6a8cda574e40dc90821bd845720ebb8e89c"}, + {file = "rich-13.7.1-py3-none-any.whl", hash = "sha256:4edbae314f59eb482f54e9e30bf00d33350aaa94f4bfcd4e9e3110e64d0d7222"}, + {file = "rich-13.7.1.tar.gz", hash = "sha256:9be308cb1fe2f1f57d67ce99e95af38a1e2bc71ad9813b0e247cf7ffbcc3a432"}, ] [package.dependencies] -markdown-it-py = ">=2.2.0,<3.0.0" +markdown-it-py = ">=2.2.0" pygments = ">=2.13.0,<3.0.0" [package.extras] jupyter = ["ipywidgets (>=7.5.1,<9)"] +[[package]] +name = "setuptools" +version = "69.1.1" +description = "Easily download, build, install, upgrade, and uninstall Python packages" +category = "dev" +optional = false +python-versions = ">=3.8" +files = [ + {file = "setuptools-69.1.1-py3-none-any.whl", hash = "sha256:02fa291a0471b3a18b2b2481ed902af520c69e8ae0919c13da936542754b4c56"}, + {file = "setuptools-69.1.1.tar.gz", hash = "sha256:5c0806c7d9af348e6dd3777b4f4dbb42c7ad85b190104837488eab9a7c945cf8"}, +] + +[package.extras] +docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "rst.linker (>=1.9)", "sphinx (<7.2.5)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier"] +testing = ["build[virtualenv]", "filelock (>=3.4.0)", "flake8-2020", "ini2toml[lite] (>=0.9)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "packaging (>=23.2)", "pip (>=19.1)", "pytest (>=6)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy (>=0.9.1)", "pytest-perf", "pytest-ruff (>=0.2.1)", "pytest-timeout", "pytest-xdist", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] +testing-integration = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "packaging (>=23.2)", "pytest", "pytest-enabler", "pytest-xdist", "tomli", "virtualenv (>=13.0.0)", "wheel"] + [[package]] name = "textual" -version = "0.10.1" +version = "0.27.0" description = "Modern Text User Interface framework" category = "main" optional = false python-versions = ">=3.7,<4.0" files = [ - {file = "textual-0.10.1-py3-none-any.whl", hash = "sha256:dd9a5b38a74cf42364a0f247e8f57e3ded7d69d44a63ee664af333f986c48e81"}, - {file = "textual-0.10.1.tar.gz", hash = "sha256:928cfeec37c60b212963f484e806b25380afdddb5a2aecd888ce8c9b46f93553"}, + {file = "textual-0.27.0-py3-none-any.whl", hash = "sha256:dc45eaf7da330686c56d6f76f59d05fd216ce6aad90fa44ee269881efc622151"}, + {file = "textual-0.27.0.tar.gz", hash = "sha256:8bdcb09dc35a706ef939b1276ccfdec10eaaee6147b41cb7587cf33298a8dd33"}, ] [package.dependencies] -importlib-metadata = ">=4.11.3,<5.0.0" -nanoid = ">=2.0.0" -rich = ">12.6.0" +importlib-metadata = ">=4.11.3" +markdown-it-py = {version = ">=2.1.0,<3.0.0", extras = ["linkify", "plugins"]} +rich = ">=13.3.3" +typing-extensions = ">=4.4.0,<5.0.0" [package.extras] dev = ["aiohttp (>=3.8.1)", "click (>=8.1.2)", "msgpack (>=1.0.3)"] [[package]] name = "tokenize-rt" -version = "5.0.0" +version = "5.2.0" description = "A wrapper around the stdlib `tokenize` which roundtrips." category = "dev" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "tokenize_rt-5.0.0-py2.py3-none-any.whl", hash = "sha256:c67772c662c6b3dc65edf66808577968fb10badfc2042e3027196bed4daf9e5a"}, - {file = "tokenize_rt-5.0.0.tar.gz", hash = "sha256:3160bc0c3e8491312d0485171dea861fc160a240f5f5766b72a1165408d10740"}, + {file = "tokenize_rt-5.2.0-py2.py3-none-any.whl", hash = "sha256:b79d41a65cfec71285433511b50271b05da3584a1da144a0752e9c621a285289"}, + {file = "tokenize_rt-5.2.0.tar.gz", hash = "sha256:9fe80f8a5c1edad2d3ede0f37481cc0cc1538a2f442c9c2f9e4feacd2792d054"}, ] [[package]] @@ -922,45 +973,72 @@ files = [ [[package]] name = "typing-extensions" -version = "4.5.0" -description = "Backported and Experimental Type Hints for Python 3.7+" -category = "dev" +version = "4.10.0" +description = "Backported and Experimental Type Hints for Python 3.8+" +category = "main" +optional = false +python-versions = ">=3.8" +files = [ + {file = "typing_extensions-4.10.0-py3-none-any.whl", hash = "sha256:69b1a937c3a517342112fb4c6df7e72fc39a38e7891a5730ed4985b5214b5475"}, + {file = "typing_extensions-4.10.0.tar.gz", hash = "sha256:b0abd7c89e8fb96f98db18d86106ff1d90ab692004eb746cf6eda2682f91b3cb"}, +] + +[[package]] +name = "uc-micro-py" +version = "1.0.3" +description = "Micro subset of unicode data files for linkify-it-py projects." +category = "main" optional = false python-versions = ">=3.7" files = [ - {file = "typing_extensions-4.5.0-py3-none-any.whl", hash = "sha256:fb33085c39dd998ac16d1431ebc293a8b3eedd00fd4a32de0ff79002c19511b4"}, - {file = "typing_extensions-4.5.0.tar.gz", hash = "sha256:5cb5f4a79139d699607b3ef622a1dedafa84e115ab0024e0d9c044a9479ca7cb"}, + {file = "uc-micro-py-1.0.3.tar.gz", hash = "sha256:d321b92cff673ec58027c04015fcaa8bb1e005478643ff4a500882eaab88c48a"}, + {file = "uc_micro_py-1.0.3-py3-none-any.whl", hash = "sha256:db1dffff340817673d7b466ec86114a9dc0e9d4d9b5ba229d9d60e5c12600cd5"}, ] +[package.extras] +test = ["coverage", "pytest", "pytest-cov"] + [[package]] name = "wcwidth" -version = "0.2.6" +version = "0.2.13" description = "Measures the displayed width of unicode strings in a terminal" category = "main" optional = false python-versions = "*" files = [ - {file = "wcwidth-0.2.6-py2.py3-none-any.whl", hash = "sha256:795b138f6875577cd91bba52baf9e445cd5118fd32723b460e30a0af30ea230e"}, - {file = "wcwidth-0.2.6.tar.gz", hash = "sha256:a5220780a404dbe3353789870978e472cfe477761f06ee55077256e509b156d0"}, + {file = "wcwidth-0.2.13-py2.py3-none-any.whl", hash = "sha256:3da69048e4540d84af32131829ff948f1e022c1c6bdb8d6102117aac784f6859"}, + {file = "wcwidth-0.2.13.tar.gz", hash = "sha256:72ea0c06399eb286d978fdedb6923a9eb47e1c486ce63e9b4e64fc18303972b5"}, +] + +[[package]] +name = "xdg-base-dirs" +version = "6.0.1" +description = "Variables defined by the XDG Base Directory Specification" +category = "main" +optional = false +python-versions = ">=3.10,<4.0" +files = [ + {file = "xdg_base_dirs-6.0.1-py3-none-any.whl", hash = "sha256:63f6ebc1721ced2e86c340856e004ef829501a30a37e17079c52cfaf0e1741b9"}, + {file = "xdg_base_dirs-6.0.1.tar.gz", hash = "sha256:b4c8f4ba72d1286018b25eea374ec6fbf4fddda3d4137edf50de95de53e195a6"}, ] [[package]] name = "zipp" -version = "3.15.0" +version = "3.17.0" description = "Backport of pathlib-compatible object wrapper for zip files" category = "main" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "zipp-3.15.0-py3-none-any.whl", hash = "sha256:48904fc76a60e542af151aded95726c1a5c34ed43ab4134b597665c86d7ad556"}, - {file = "zipp-3.15.0.tar.gz", hash = "sha256:112929ad649da941c23de50f356a2b5570c954b65150642bccdd66bf194d224b"}, + {file = "zipp-3.17.0-py3-none-any.whl", hash = "sha256:0e923e726174922dce09c53c59ad483ff7bbb8e572e00c7f7c46b88556409f31"}, + {file = "zipp-3.17.0.tar.gz", hash = "sha256:84e64a1c28cf7e91ed2078bb8cc8c259cb19b76942096c8d7b84947690cabaf0"}, ] [package.extras] -docs = ["furo", "jaraco.packaging (>=9)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"] -testing = ["big-O", "flake8 (<5)", "jaraco.functools", "jaraco.itertools", "more-itertools", "pytest (>=6)", "pytest-black (>=0.3.7)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=1.3)", "pytest-flake8", "pytest-mypy (>=0.9.1)"] +docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (<7.2.5)", "sphinx (>=3.5)", "sphinx-lint"] +testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "pytest (>=6)", "pytest-black (>=0.3.7)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-ignore-flaky", "pytest-mypy (>=0.9.1)", "pytest-ruff"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "d63b0037812993bef8238cb3dec1c4a4f3c2abd5ffc969011dc5683ab0dd6130" +content-hash = "4ff46f51015a867e71ffe21053a21daa92bf560011d2f874c9d3e872c9fe601b" diff --git a/kimp/pyproject.toml b/kimp/pyproject.toml index a0035f0..7e5f719 100644 --- a/kimp/pyproject.toml +++ b/kimp/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="subproofs" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.679" } [tool.poetry.scripts] kimp = "kimp.__main__:main" diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index cec8cfb..1033bb9 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -6,8 +6,8 @@ from pathlib import Path from typing import TYPE_CHECKING, Any, Final -from pyk.cli_utils import dir_path, file_path -from pyk.ktool.kprint import KAstInput, KAstOutput +from pyk.cli.utils import dir_path, file_path +from pyk.ktool.kprint import KAstOutput from pyk.ktool.krun import KRunOutput from .kimp import KIMP @@ -46,23 +46,6 @@ def main() -> None: execute(**vars(args)) -def exec_parse( - input_file: str, - definition_dir: str, - input: str = 'program', - output: str = 'kore', - **kwargs: Any, -) -> None: - kast_input = KAstInput[input.upper()] - kast_output = KAstOutput[output.upper()] - - kimp = KIMP(definition_dir, definition_dir) - proc_res = kimp.parse_program_raw(input_file, input=kast_input, output=kast_output) - - if output != KAstOutput.NONE: - print(proc_res.stdout) - - def exec_run( input_file: str, definition_dir: str, @@ -72,6 +55,8 @@ def exec_run( ) -> None: krun_output = KRunOutput[output.upper()] + definition_dir = str(kbuild_definition_dir('llvm')) + kimp = KIMP(definition_dir, definition_dir) try: @@ -93,14 +78,13 @@ def exec_prove( spec_file: str, spec_module: str, claim_id: str, - # output: str = 'none', max_iterations: int, max_depth: int, - reinit: bool, ignore_return_code: bool = False, - # output: str = 'none', **kwargs: Any, ) -> None: + definition_dir = str(kbuild_definition_dir('haskell')) + kimp = KIMP(definition_dir, definition_dir) try: @@ -110,38 +94,12 @@ def exec_prove( claim_id=claim_id, max_iterations=max_iterations, max_depth=max_depth, - reinit=reinit, + includes=['k-src'], # TODO this needs to be more rubust ) except ValueError as err: _LOGGER.critical(err.args) - exit(1) - except RuntimeError as err: - if ignore_return_code: - msg, stdout, stderr = err.args - print(stdout) - print(stderr) - print(msg) - else: - raise - - -def exec_summarize( - definition_dir: str, - spec_file: str, - spec_module: str, - claim_id: str, - max_iterations: int = 20, - ignore_return_code: bool = False, - # output: str = 'none', - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - - try: - kimp.summarize(spec_file=spec_file, spec_module=spec_module, claim_id=claim_id, max_iterations=max_iterations) - except ValueError as err: - _LOGGER.critical(err.args) - exit(1) + # exit(1) + raise except RuntimeError as err: if ignore_return_code: msg, stdout, stderr = err.args @@ -152,129 +110,26 @@ def exec_summarize( raise -def exec_bmc_prove( - definition_dir: str, - spec_file: str, - spec_module: str, - claim_id: str, - max_iterations: int, - max_depth: int, - reinit: bool, - bmc_depth: int, - # output: str = 'none', - ignore_return_code: bool = False, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - - try: - kimp.bmc_prove( - spec_file=spec_file, - spec_module=spec_module, - claim_id=claim_id, - max_iterations=max_iterations, - max_depth=max_depth, - reinit=reinit, - bmc_depth=bmc_depth, - ) - except ValueError as err: - _LOGGER.critical(err.args) - exit(1) - except RuntimeError as err: - if ignore_return_code: - msg, stdout, stderr = err.args - print(stdout) - print(stderr) - print(msg) - else: - raise +# def exec_show_kcfg( +# definition_dir: str, +# spec_module: str, +# claim_id: str, +# to_module: bool = False, +# inline_nodes: bool = False, +# **kwargs: Any, +# ) -> None: +# kimp = KIMP(definition_dir, definition_dir) +# kimp.show_kcfg(spec_module, claim_id, to_module=to_module, inline_nodes=inline_nodes) -def exec_eq_prove( - definition_dir: str, - proof_id: str, - # output: str = 'none', - ignore_return_code: bool = False, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - - try: - kimp.eq_prove(proof_id) - except RuntimeError as err: - if ignore_return_code: - msg, stdout, stderr = err.args - print(stdout) - print(stderr) - print(msg) - else: - raise - - -def exec_refute_node( - definition_dir: str, - spec_module: str, - claim_id: str, - node: str, - # output: str = 'none', - ignore_return_code: bool = False, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - - try: - kimp.kcfg_refute_node(spec_module=spec_module, claim_id=claim_id, node_short_hash=node) - except RuntimeError as err: - if ignore_return_code: - msg, stdout, stderr = err.args - print(stdout) - print(stderr) - print(msg) - else: - raise - - -def exec_show_kcfg( - definition_dir: str, - spec_module: str, - claim_id: str, - to_module: bool = False, - inline_nodes: bool = False, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - kimp.show_kcfg(spec_module, claim_id, to_module=to_module, inline_nodes=inline_nodes) - - -def exec_view_kcfg( - definition_dir: str, - spec_module: str, - claim_id: str, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - kimp.view_kcfg(spec_module, claim_id) - - -def exec_show_refutation( - definition_dir: str, - spec_module: str, - claim_id: str, - node: str, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - kimp.show_refutation(spec_module, claim_id, node=node) - - -def exec_kcfg_to_dot( - definition_dir: str, - spec_module: str, - claim_id: str, - **kwargs: Any, -) -> None: - kimp = KIMP(definition_dir, definition_dir) - kimp.kcfg_to_dot(spec_module, claim_id) +# def exec_view_kcfg( +# definition_dir: str, +# spec_module: str, +# claim_id: str, +# **kwargs: Any, +# ) -> None: +# kimp = KIMP(definition_dir, definition_dir) +# kimp.view_kcfg(spec_module, claim_id) def create_argument_parser() -> ArgumentParser: @@ -286,7 +141,6 @@ def create_argument_parser() -> ArgumentParser: '--definition-dir', dest='definition_dir', nargs='?', - default=kbuild_definition_dir('haskell'), type=dir_path, help='Path to compiled K definition to use.', ) @@ -373,7 +227,7 @@ def create_argument_parser() -> ArgumentParser: '--output', dest='output', type=str, - default='kast', + default='pretty', help='Output mode', choices=['pretty', 'program', 'json', 'kore', 'kast', 'none'], required=False, diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index e0228a4..c240453 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -2,44 +2,89 @@ __all__ = ['KIMP'] -import json import logging -import subprocess +from contextlib import contextmanager from dataclasses import dataclass from functools import cached_property from pathlib import Path -from subprocess import CalledProcessError from tempfile import NamedTemporaryFile -from typing import TYPE_CHECKING, Any, Iterable, Optional, Union, final +from typing import TYPE_CHECKING, Iterable, Iterator, Optional, Union, final -from pyk.cli_utils import check_dir_path, check_file_path -from pyk.cterm import CTerm -from pyk.kast.inner import KApply, KInner, KSequence, KVariable -from pyk.kast.manip import anti_unify_with_constraints +from pyk.cli.utils import check_dir_path, check_file_path +from pyk.cterm.symbolic import CTermSymbolic +from pyk.kast.inner import KApply, KSequence, KVariable from pyk.kcfg.explore import KCFGExplore -from pyk.kcfg.kcfg import KCFG -from pyk.kcfg.show import KCFGShow -from pyk.kcfg.tui import KCFGViewer -from pyk.ktool.kprint import KAstInput, KAstOutput, _kast, gen_glr_parser, paren +from pyk.kcfg.semantics import KCFGSemantics +from pyk.kore.kompiled import KompiledKore +from pyk.kore.rpc import KoreClient, kore_server +from pyk.ktool.kprint import gen_glr_parser from pyk.ktool.kprove import KProve from pyk.ktool.krun import KRun, KRunOutput, _krun from pyk.prelude.kbool import BOOL, notBool from pyk.prelude.ml import mlEqualsTrue -from pyk.proof.equality import EqualityProof, EqualityProver -from pyk.proof.proof import Proof -from pyk.proof.reachability import APRBMCProof, APRBMCProver, APRProof, APRProver -from pyk.proof.utils import read_proof -from pyk.utils import shorten_hashes +from pyk.proof.reachability import APRProof, APRProver +from pyk.proof.show import APRProofShow +from pyk.utils import single if TYPE_CHECKING: from subprocess import CompletedProcess from typing import Final - from pyk.ktool.kprint import SymbolTable + from pyk.cterm.cterm import CTerm + from pyk.kast.inner import KInner + from pyk.kast.outer import KDefinition + from pyk.kore.rpc import FallbackReason + from pyk.ktool.kprint import KPrint + from pyk.utils import BugReport + _LOGGER: Final = logging.getLogger(__name__) +class ImpSemantics(KCFGSemantics): + definition: KDefinition | None + + def __init__(self, definition: KDefinition | None = None): + super().__init__() + self.definition = definition + + def is_terminal(self, c: CTerm) -> bool: + k_cell = c.cell('K_CELL') + if type(k_cell) is KSequence: + if len(k_cell) == 0: + return True + if len(k_cell) == 1 and type(k_cell[0]) is KVariable: + return True + if type(k_cell) is KVariable: + return True + return False + + def extract_branches(self, c: CTerm) -> list[KInner]: + if self.definition is None: + raise ValueError('IMP branch extraction requires a non-None definition') + + k_cell = c.cell('K_CELL') + if type(k_cell) is KSequence and len(k_cell) > 0: + k_cell = k_cell[0] + if type(k_cell) is KApply and k_cell.label.name == 'if(_)_else_': + condition = k_cell.args[0] + if (type(condition) is KVariable and condition.sort == BOOL) or ( + type(condition) is KApply and self.definition.return_sort(condition.label) == BOOL + ): + return [mlEqualsTrue(condition), mlEqualsTrue(notBool(condition))] + return [] + + def abstract_node(self, c: CTerm) -> CTerm: + return c + + def same_loop(self, c1: CTerm, c2: CTerm) -> bool: + k_cell_1 = c1.cell('K_CELL') + k_cell_2 = c2.cell('K_CELL') + if k_cell_1 == k_cell_2 and type(k_cell_1) is KSequence and type(k_cell_1[0]) is KApply: + return k_cell_1[0].label.name == 'while(_)_' # type: ignore + return False + + @final @dataclass(frozen=True) class KIMP: @@ -52,9 +97,9 @@ def __init__(self, llvm_dir: Union[str, Path], haskell_dir: Union[str, Path]): llvm_dir = Path(llvm_dir) check_dir_path(llvm_dir) - imp_parser = llvm_dir / 'parser_Pgm_IMP-SYNTAX' + imp_parser = llvm_dir / 'parser_Stmt_STATEMENTS-SYNTAX' if not imp_parser.is_file(): - imp_parser = gen_glr_parser(imp_parser, definition_dir=llvm_dir, module='IMP-SYNTAX', sort='Pgm') + imp_parser = gen_glr_parser(imp_parser, definition_dir=llvm_dir, module='STATEMENTS-SYNTAX', sort='Stmt') haskell_dir = Path(haskell_dir) check_dir_path(haskell_dir) @@ -67,134 +112,16 @@ def __init__(self, llvm_dir: Union[str, Path], haskell_dir: Union[str, Path]): object.__setattr__(self, 'imp_parser', imp_parser) object.__setattr__(self, 'proof_dir', proof_dir) - @classmethod - def _patch_symbol_table(cls, symbol_table: SymbolTable) -> None: - # fmt: off - symbol_table['while(_)_'] = lambda cond, body: f'\n while({cond})' + '\n' + body - symbol_table['if(_)_else_'] = lambda cond, t, e: f'\n if ({cond})' + '\n' + t + '\n' f'else {e}' - symbol_table['_Map_'] = paren(lambda m1, m2: m1 + '\n' + m2) - paren_symbols = [ - '_|->_', - '#And', - '_andBool_', - '#Implies', - '_impliesBool_', - '_&Int_', - '_*Int_', - '_+Int_', - '_-Int_', - '_/Int_', - '_|Int_', - '_modInt_', - 'notBool_', - '#Or', - '_orBool_', - '_Set_', - ] - for symb in paren_symbols: - if symb in symbol_table: - symbol_table[symb] = paren(symbol_table[symb]) - # fmt: on - @cached_property def kprove(self) -> KProve: kprove = KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir) - KIMP._patch_symbol_table(kprove.symbol_table) return kprove @cached_property def krun(self) -> KRun: - krun = KRun(definition_dir=self.haskell_dir, use_directory=self.proof_dir) - KIMP._patch_symbol_table(krun.symbol_table) + krun = KRun(definition_dir=self.llvm_dir) return krun - @staticmethod - def _is_terminal(cterm1: CTerm) -> bool: - k_cell = cterm1.cell('K_CELL') - if type(k_cell) is KSequence: - if len(k_cell) == 0: - return True - if len(k_cell) == 1 and type(k_cell[0]) is KVariable: - return True - if type(k_cell) is KVariable: - return True - return False - - def _extract_branches(self, cterm: CTerm) -> Iterable[KInner]: - k_cell = cterm.cell('K_CELL') - if type(k_cell) is KSequence and len(k_cell) > 0: - k_cell = k_cell[0] - if type(k_cell) is KApply and k_cell.label.name == 'if(_)_else_': - condition = k_cell.args[0] - if (type(condition) is KVariable and condition.sort == BOOL) or ( - type(condition) is KApply and self.kprove.definition.return_sort(condition.label) == BOOL - ): - return [mlEqualsTrue(condition), mlEqualsTrue(notBool(condition))] - return [] - - @staticmethod - def _same_loop(cterm1: CTerm, cterm2: CTerm) -> bool: - k_cell_1 = cterm1.cell('K_CELL') - k_cell_2 = cterm2.cell('K_CELL') - if k_cell_1 == k_cell_2 and type(k_cell_1) is KSequence and type(k_cell_1[0]) is KApply: - return k_cell_1[0].label.name == 'while(_)_' - return False - - def parse_program_raw( - self, - program_file: Union[str, Path], - *, - input: KAstInput, - output: KAstOutput, - temp_file: Optional[Union[str, Path]] = None, - ) -> CompletedProcess: - def parse(program_file: Path) -> CompletedProcess: - try: - if output == KAstOutput.KORE: - command = [str(self.imp_parser)] + [str(program_file)] - proc_res = subprocess.run(command, stdout=subprocess.PIPE, check=True, text=True) - else: - proc_res = _kast( - definition_dir=self.llvm_dir, - file=program_file, - input=input, - output=output, - sort='Pgm', - ) - except CalledProcessError as err: - raise ValueError("Couldn't parse program") from err - return proc_res - - def preprocess_and_parse(program_file: Path, temp_file: Path) -> CompletedProcess: - temp_file.write_text(program_file.read_text()) - return parse(temp_file) - - program_file = Path(program_file) - check_file_path(program_file) - - if temp_file is None: - with NamedTemporaryFile(mode='w') as f: - temp_file = Path(f.name) - return preprocess_and_parse(program_file, temp_file) - - temp_file = Path(temp_file) - return preprocess_and_parse(program_file, temp_file) - - def parse_program( - self, - program_file: Union[str, Path], - *, - temp_file: Optional[Union[str, Path]] = None, - ) -> KInner: - proc_res = self.parse_program_raw( - program_file=program_file, - input=KAstInput.PROGRAM, - output=KAstOutput.JSON, - temp_file=temp_file, - ) - - return KInner.from_dict(json.loads(proc_res.stdout)['term']) - def run_program( self, program_file: Union[str, Path], @@ -229,256 +156,116 @@ def preprocess_and_run(program_file: Path, temp_file: Path) -> CompletedProcess: return preprocess_and_run(program_file, temp_file) def prove( - self, spec_file: str, spec_module: str, claim_id: str, max_iterations: int, max_depth: int, reinit: bool - ) -> None: - proof_id = f'{spec_module}.{claim_id}' - if Proof.proof_exists(proof_id, proof_dir=self.proof_dir) and not reinit: - proof = read_proof(proof_id, proof_dir=self.proof_dir) - if type(proof) is not APRProof: - raise ValueError(f'Proof {proof_id} exists and is of type {type(proof)}, while APRProof was expected') - else: - claims = self.kprove.get_claims( - Path(spec_file), - spec_module_name=spec_module, - claim_labels=[f'{spec_module}.{claim_id}'], - include_dirs=[self.haskell_dir.parent.parent.parent / 'include' / 'imp-semantics'], - ) - assert len(claims) == 1 - kcfg = KCFG.from_claim(self.kprove.definition, claims[0]) - proof = APRProof(f'{spec_module}.{claim_id}', kcfg, proof_dir=self.proof_dir) - prover = APRProver(proof, is_terminal=KIMP._is_terminal, extract_branches=self._extract_branches) - with KCFGExplore( - self.kprove, - id=f'{spec_module}.{claim_id}', - ) as kcfg_explore: - kcfg = prover.advance_proof( - kcfg_explore, - max_iterations=max_iterations, - execute_depth=max_depth, - cut_point_rules=['IMP.while'], - ) - - proof.write_proof() - print('\n'.join(proof.summary)) - - def summarize( - self, - spec_file: str, - spec_module: str, - claim_id: str, - max_iterations: int, - ) -> None: - claims = self.kprove.get_claims( - Path(spec_file), - spec_module_name=spec_module, - claim_labels=[f'{spec_module}.{claim_id}'], - include_dirs=[self.haskell_dir.parent.parent.parent / 'include' / 'imp-semantics'], - ) - assert len(claims) == 1 - - kcfg = KCFG.from_claim(self.kprove.definition, claims[0]) - proof = APRProof(f'{spec_module}.{claim_id}', kcfg, proof_dir=self.proof_dir) - prover = APRProver(proof, is_terminal=KIMP._is_terminal, extract_branches=self._extract_branches) - with KCFGExplore( - self.kprove, - id=f'{spec_module}.{claim_id}', - ) as kcfg_explore: - iterations = 0 - checked_nodes = [] - while iterations < max_iterations and kcfg.frontier: - iterations += 1 - next_node = kcfg.frontier[0] - if next_node not in checked_nodes: - _LOGGER.info(f'Checking for loops: {shorten_hashes(next_node.id)}') - checked_nodes.append(next_node) - prior_loops_on_path = [ - node - for node in proof.kcfg.reachable_nodes(next_node.id, reverse=True, traverse_covers=True) - if node != next_node - and self._same_loop(next_node.cterm, node.cterm) - and not next_node.cterm.match_with_constraint(node.cterm) - ] - if len(prior_loops_on_path) > 0: - _LOGGER.info( - f'Loops found: {shorten_hashes(next_node.id)} -> {shorten_hashes([nd.id for nd in prior_loops_on_path])}' - ) - generalized_term = next_node.cterm.kast - for node in prior_loops_on_path: - generalized_term = anti_unify_with_constraints(generalized_term, node.cterm.kast) - cover_node = proof.kcfg.create_node(CTerm.from_kast(generalized_term)) - proof.kcfg.create_cover(next_node.id, cover_node.id) - continue - else: - kcfg = prover.advance_proof( - kcfg_explore, - max_iterations=1, - cut_point_rules=['IMP.while'], - ) - - proof.write_proof() - print(proof.status) - - def bmc_prove( self, spec_file: str, spec_module: str, + includes: Iterable[str], claim_id: str, max_iterations: int, max_depth: int, - bmc_depth: int, - reinit: bool, ) -> None: - proof_id = f'{spec_module}.{claim_id}' - if Proof.proof_exists(proof_id, proof_dir=self.proof_dir) and not reinit: - proof = read_proof(proof_id, proof_dir=self.proof_dir) - if type(proof) is not APRBMCProof: - raise ValueError( - f'Proof {proof_id} exists and is of type {type(proof)}, while APRBMCProof was expected' - ) - else: - claims = self.kprove.get_claims( - Path(spec_file), - spec_module_name=spec_module, - claim_labels=[f'{spec_module}.{claim_id}'], - include_dirs=[self.haskell_dir.parent.parent.parent / 'include' / 'imp-semantics'], - ) - assert len(claims) == 1 - - kcfg = KCFG.from_claim(self.kprove.definition, claims[0]) - proof = APRBMCProof(f'{spec_module}.{claim_id}', kcfg, proof_dir=self.proof_dir, bmc_depth=bmc_depth) - prover = APRBMCProver(proof, is_terminal=KIMP._is_terminal, same_loop=KIMP._same_loop) - with KCFGExplore( - self.kprove, - id=f'{spec_module}.{claim_id}', - ) as kcfg_explore: - kcfg = prover.advance_proof( - kcfg_explore, - max_iterations=max_iterations, - execute_depth=max_depth, - cut_point_rules=['IMP.while'], - ) - - proof.write_proof() - print('\n'.join(proof.summary)) - - def eq_prove(self, proof_id: str) -> None: - proof = read_proof(proof_id, self.proof_dir) - assert type(proof) == EqualityProof - prover = EqualityProver(proof) - with KCFGExplore( - self.kprove, - id=proof_id, - ) as kcfg_explore: - prover.advance_proof( - kcfg_explore, - ) + include_dirs = [Path(include) for include in includes] - proof.write_proof() - print(proof.status) - - def show_kcfg( - self, - spec_module: str, - claim_id: str, - to_module: bool = False, - inline_nodes: bool = False, - **kwargs: Any, - ) -> None: - def _node_printer(cterm: CTerm) -> Iterable[str]: - return self.kprove.pretty_print(cterm.kast).split('\n') - - node_printer = _node_printer if inline_nodes else None - - proof = read_proof(f'{spec_module}.{claim_id}', proof_dir=self.proof_dir) - if type(proof) == EqualityProof: - raise ValueError(f'Cannot show KCFG of EqualityProof {proof.id}') - assert type(proof) == APRProof or type(proof) == APRBMCProof - kcfg_show = KCFGShow(self.kprove) - res_lines = kcfg_show.show( - proof.id, - proof.kcfg, - to_module=to_module, - node_printer=node_printer, + spec_modules = self.kprove.get_claim_modules( + Path(spec_file), spec_module_name=spec_module, include_dirs=include_dirs ) - print('\n'.join(res_lines)) - - print('Proof summary:') - print('\n'.join(proof.summary)) + spec_label = f'{spec_module}.{claim_id}' + + proofs = APRProof.from_spec_modules( + self.kprove.definition, + spec_modules, + spec_labels=[spec_label], + logs={}, + proof_dir=self.proof_dir, + ) + proof = single([p for p in proofs if p.id == spec_label]) - def kcfg_refute_node( - self, - spec_module: str, - claim_id: str, - node_short_hash: str, - assuming: KInner | None = None, - ) -> None: - proof = read_proof(f'{spec_module}.{claim_id}', proof_dir=self.proof_dir) - assert proof.proof_dir - assert type(proof) == APRProof - - node_id = proof.kcfg._resolve(node_short_hash) - node_to_refute = proof.kcfg.get_node(node_id) - if node_to_refute is None: - raise ValueError(f'No such node {node_short_hash}') - refutation_id = proof.refute_node(node_to_refute, assuming=assuming) - if refutation_id is None: - return None - proof = read_proof(refutation_id, proof_dir=proof.proof_dir) - if type(proof) is not EqualityProof: - raise ValueError(f'Refutation proof {proof.id} must be EqualityProof, but {type(proof)} was found.') - prover = EqualityProver(proof) - with KCFGExplore( + with legacy_explore( self.kprove, - id=refutation_id, + kcfg_semantics=ImpSemantics(self.kprove.definition), + id=spec_label, ) as kcfg_explore: - prover.advance_proof(kcfg_explore) + prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=['IMP.while']) + prover.advance_proof(max_iterations=max_iterations) - for s in prover.proof.pretty(self.kprove): - print(s) - - def kcfg_to_dot( - self, - spec_module: str, - claim_id: str, - **kwargs: Any, - ) -> None: - def node_printer(cterm: CTerm) -> Iterable[str]: - k_cell = cterm.cells['K_CELL'] - if type(k_cell) is KSequence: - return [self.kprove.pretty_print(k_cell.items[0])] - else: - return [self.kprove.pretty_print(k_cell)] - - proof = APRProof.read_proof(f'{spec_module}.{claim_id}', proof_dir=self.proof_dir) - kcfg_show = KCFGShow(self.kprove) - dump_dir = self.proof_dir / 'dump' - kcfg_show.dump( - f'{spec_module}.{claim_id}', - proof.kcfg, - dump_dir, - dot=True, - node_printer=node_printer, - ) - - def view_kcfg( - self, - spec_module: str, - claim_id: str, - **kwargs: Any, - ) -> None: - proof = read_proof(f'{spec_module}.{claim_id}', proof_dir=self.proof_dir) - if type(proof) == APRProof or type(proof) == APRBMCProof: - kcfg_viewer = KCFGViewer(proof.kcfg, self.kprove) - kcfg_viewer.run() - - def show_refutation( - self, - spec_module: str, - claim_id: str, - node: str, - **kwargs: Any, - ) -> None: - proof = read_proof(f'{spec_module}.{claim_id}.node-infeasible-{node}', proof_dir=self.proof_dir) - - assert type(proof) == EqualityProof - print('\n'.join(proof.pretty(self.kprove))) + proof_show = APRProofShow(self.kprove) + res_lines = proof_show.show( + proof, + ) + print(proof.status) + print('\n'.join(res_lines)) + + +# def view_kcfg( +# self, +# spec_module: str, +# claim_id: str, +# **kwargs: Any, +# ) -> None: +# proof = read_proof(f'{spec_module}.{claim_id}', proof_dir=self.proof_dir) +# if type(proof) is APRProof: +# kcfg_viewer = KCFGViewer(proof.kcfg, self.kprove) +# kcfg_viewer.run() + + +@contextmanager +def legacy_explore( + kprint: KPrint, + *, + kcfg_semantics: KCFGSemantics | None = None, + id: str | None = None, + port: int | None = None, + kore_rpc_command: str | Iterable[str] | None = None, + llvm_definition_dir: Path | None = None, + smt_timeout: int | None = None, + smt_retry_limit: int | None = None, + smt_tactic: str | None = None, + bug_report: BugReport | None = None, + log_axioms_file: Path | None = None, + start_server: bool = True, + fallback_on: Iterable[FallbackReason] | None = None, + interim_simplification: int | None = None, + no_post_exec_simplify: bool = False, +) -> Iterator[KCFGExplore]: + if start_server: + with kore_server( + definition_dir=kprint.definition_dir, + llvm_definition_dir=llvm_definition_dir, + module_name=kprint.main_module, + port=port, + command=kore_rpc_command, + bug_report=bug_report, + smt_timeout=smt_timeout, + smt_retry_limit=smt_retry_limit, + smt_tactic=smt_tactic, + log_axioms_file=log_axioms_file, + fallback_on=fallback_on, + interim_simplification=interim_simplification, + no_post_exec_simplify=no_post_exec_simplify, + ) as server: + with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client: + cterm_symbolic = cterm_symbolic = CTermSymbolic( + kore_client=client, + definition=kprint.definition, + kompiled_kore=KompiledKore.load(kprint.definition_dir), + ) + yield KCFGExplore( + # kore_client=client, + kcfg_semantics=kcfg_semantics, + id=id, + cterm_symbolic=cterm_symbolic, + ) + else: + if port is None: + raise ValueError('Missing port with start_server=False') + with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id) as client: + cterm_symbolic = cterm_symbolic = CTermSymbolic( + kore_client=client, + definition=kprint.definition, + kompiled_kore=KompiledKore.load(kprint.definition_dir), + ) + yield KCFGExplore( + kcfg_semantics=kcfg_semantics, + id=id, + cterm_symbolic=cterm_symbolic, + ) diff --git a/kimp/tests/specs/imp-simple-spec.k b/kimp/tests/specs/imp-simple-spec.k index dff6d94..3230175 100644 --- a/kimp/tests/specs/imp-simple-spec.k +++ b/kimp/tests/specs/imp-simple-spec.k @@ -12,11 +12,11 @@ module IMP-SIMPLE-SPEC claim [pre-branch-proved]: $n = 7 ; if (B:Bool) { $n = 6 ; } else { $n = 5 ; } => if (B:Bool) { $n = 6 ; } else { $n = 5 ; } $n |-> (0 => 7) - claim [branching]: $n = 7 ; if (_B:Bool) { $n = 6 ; } else { $n = 5 ; } => . ... + claim [branching]: $n = 7 ; if (_B:Bool) { $n = 6 ; } else { $n = 5 ; } => .K ... $n |-> (0 => ?N) ensures ?N ==Int 5 orBool ?N ==Int 6 - claim [branching-program]: $n = 7 ; if (_B:Bool) { $n = 6 ; } else { $n = 5 ; } => . ... + claim [branching-program]: $n = 7 ; if (_B:Bool) { $n = 6 ; } else { $n = 5 ; } => .K ... _ => ?_ claim [branching-deadcode]: $n = 7 ; if (B:Bool) { $n = 6 ; } else { if (! B:Bool) { $n = 5 ; } else { $n = 4 ; } } => . ... @@ -29,20 +29,20 @@ module IMP-SIMPLE-SPEC $n |-> (_ => ?_) claim [sum-loop]: - while (0 < $n) { $s = $s + $n ; $n = $n - 1 ; } => . ... + while (0 < $n) { $s = $s + $n ; $n = $n - 1 ; } => .K ... $s |-> S $n |-> N => $s |-> S +Int (N *Int (N +Int 1)) /Int 2 $n |-> 0 requires 0 <=Int N // Try without this! claim [sum-N]: - $s = 0; $n = N; while (0 < $n) { $s = $s + $n ; $n = $n - 1 ; } => . ... + $s = 0; $n = N; while (0 < $n) { $s = $s + $n ; $n = $n - 1 ; } => .K ... .Map => $s |-> (N *Int (N +Int 1)) /Int 2 $n |-> 0 requires 0 <=Int N - claim [bmc-loop-concrete]: while (0 <= $n) { $n = $n + -1 ; } => . ... + claim [bmc-loop-concrete]: while (0 <= $n) { $n = $n + -1 ; } => .K ... $n |-> (1 => ?N) ensures 0 while ($s <= $n) { $n = $n + -1 ; } => . ... + claim [bmc-loop-symbolic]: while ($s <= $n) { $n = $n + -1 ; } => .K ... ($n |-> (1 => ?N)) ($s |-> S) requires 0 <=Int S ensures 0 - + $n |-> (N:Int => 0) $s |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2)) - + requires N >=Int 0 claim [two-sum-spec]: @@ -33,12 +33,12 @@ module IMP-SUM-SPEC .K ... - + $n |-> (N:Int => 0) $m |-> (M:Int => 0) $s1 |-> (S1:Int => S1 +Int ((N +Int 1) *Int N /Int 2)) $s2 |-> (S2:Int => S2 +Int ((M +Int 1) *Int M /Int 2)) - + requires N >=Int 0 andBool M >=Int 0