Merge branch 'master' into smt_cconstraint_binders

.github/workflows/python-app.yml

@@ -15,43 +15,48 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        python-version: ["3.10", "3.11", "3.12"]
+        python-version: [ "3.10", "3.11", "3.12" ]
 
     steps:
-    - uses: actions/[email protected]
-    - name: Set up Python ${{ matrix.python-version }}
-      uses: actions/setup-python@v5
-      with:
-        python-version: ${{ matrix.python-version }}
-    - name: Install dependencies
-      run: |
-        python -m pip install --upgrade pip
-        pip install flake8 pytest mypy
-        if [ -f requirements.pip ]; then pip install -r requirements.pip; fi
-    - name: Lint with mypy
-      run: |
-        mypy aeon
-    - name: Lint with flake8
-      run: |
-        # stop the build if there are Python syntax errors or undefined names
-        flake8 . --count --select=E9,F63,F7,F82 --show-source --statistics
-        # exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
-        flake8 . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
-    - name: Check install
-      run: |
-        pip install -e .
-    - name: Test with pytest
-      run: |
-        pytest
-    - name: Run Aeon Core Files
-      run: |
-        files=$(find examples/core -type f -name '*_main.ae')
-        for file in $files; do
-          python aeon $file --core --log INFO ERROR TYPECHECKER CONSTRAINT
-        done
-    - name: Run Aeon Sugar Files
-      run: |
-        files=$(find examples/sugar -type f -name '*_main.ae')
-        for file in $files; do
-          python aeon $file --log INFO ERROR TYPECHECKER CONSTRAINT
-        done
+      - uses: actions/[email protected]
+      - name: Set up Python ${{ matrix.python-version }}
+        uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python-version }}
+      - name: Set env
+        run: echo "VIRTUAL_ENV=$(python -c 'import sys; print(sys.prefix)')">> $GITHUB_ENV
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade uv
+          uv pip install flake8 pytest mypy pre-commit
+          if [ -f requirements.pip ]; then uv pip install -r requirements.pip; fi
+      #- name: Lint with pre-commit
+      #  run: |
+      #    pre-commit run --all-files
+      - name: Lint with mypy
+        run: |
+          mypy aeon --no-strict-optional --ignore-missing-imports
+      - name: Lint with flake8
+        run: |
+          # stop the build if there are Python syntax errors or undefined names
+          flake8 --extend-exclude .venv . --count --select=E9,F63,F7,F82 --show-source --statistics
+          # exit-zero treats all errors as warnings. The GitHub editor is 127 chars wide
+          flake8 --extend-exclude .venv . --count --exit-zero --max-complexity=10 --max-line-length=127 --statistics
+      - name: Check install
+        run: |
+          pip install -e .
+      - name: Test with pytest
+        run: |
+          pytest
+      - name: Run Aeon Core Files
+        run: |
+          files=$(find examples/core -type f -name '*_main.ae')
+          for file in $files; do
+            python aeon $file --core --log INFO ERROR TYPECHECKER CONSTRAINT
+          done
+      - name: Run Aeon Sugar Files
+        run: |
+          files=$(find examples/sugar -type f -name '*_main.ae')
+          for file in $files; do
+            python aeon $file --log INFO ERROR TYPECHECKER CONSTRAINT
+          done

.github/workflows/python-publish.yml

@@ -10,27 +10,29 @@ name: Upload Python Package
 
 on:
   release:
-    types: [published]
+    types: [ published ]
 
 jobs:
   deploy:
 
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v3
-    - name: Set up Python
-      uses: actions/setup-python@v4
-      with:
-        python-version: '3.x'
-    - name: Install dependencies
-      run: |
-        python -m pip install --upgrade pip
-        pip install build
-    - name: Build package
-      run: python -m build
-    - name: Publish package
-      uses: pypa/gh-action-pypi-publish@27b31702a0e7fc50959f5ad993c78deac1bdfc29
-      with:
-        user: __token__
-        password: ${{ secrets.PYPI_API_TOKEN }}
+      - uses: actions/checkout@v3
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+      - name: Set env
+        run: echo "VIRTUAL_ENV=$(python -c 'import sys; print(sys.prefix)')">> $GITHUB_ENV
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade uv
+          uv pip install build
+      - name: Build package
+        run: python -m build
+      - name: Publish package
+        uses: pypa/gh-action-pypi-publish@27b31702a0e7fc50959f5ad993c78deac1bdfc29
+        with:
+          user: __token__
+          password: ${{ secrets.PYPI_API_TOKEN }}

.pre-commit-config.yaml

@@ -1,45 +1,42 @@
 repos:
--   repo: https://github.com/pre-commit/pre-commit-hooks
+  - repo: https://github.com/pre-commit/pre-commit-hooks
     rev: v4.3.0
     hooks:
-    -   id: check-yaml
-    -   id: check-toml
-    -   id: check-merge-conflict
-    -   id: end-of-file-fixer
-    -   id: trailing-whitespace
-    -   id: check-docstring-first
-    -   id: name-tests-test
-    -   id: requirements-txt-fixer
-    -   id: mixed-line-ending
--   repo: https://github.com/asottile/setup-cfg-fmt
-    rev: v1.20.0
-    hooks:
-    -   id: setup-cfg-fmt
--   repo: https://github.com/asottile/add-trailing-comma
-    rev: v2.2.1
-    hooks:
-    -   id: add-trailing-comma
-        args: [--py36-plus]
--   repo: https://github.com/PyCQA/docformatter
-    rev: v1.5.0
-    hooks:
-      - id: docformatter
--   repo: https://github.com/hadialqattan/pycln
-    rev: v2.1.2
-    hooks:
-    -   id: pycln
+      - id: check-yaml
+      - id: check-toml
+      - id: check-merge-conflict
+      - id: end-of-file-fixer
+      - id: trailing-whitespace
+      - id: check-docstring-first
+      - id: name-tests-test
+      - id: requirements-txt-fixer
+      - id: mixed-line-ending
+  - repo: https://github.com/asottile/setup-cfg-fmt
+    rev: v2.5.0
+    hooks:
+      - id: setup-cfg-fmt
+  - repo: https://github.com/hadialqattan/pycln
+    rev: v2.4.0
+    hooks:
+      - id: pycln
         args: [--config=pyproject.toml]
--   repo: https://github.com/pre-commit/mirrors-mypy
-    rev: v0.991
-    hooks:
-    -   id: mypy
-        args: [--no-strict-optional, --ignore-missing-imports, --explicit-package-bases]
--   repo: https://github.com/charliermarsh/ruff-pre-commit
-    rev: v0.2.2
+  - repo: https://github.com/pre-commit/mirrors-mypy
+    rev: v1.8.0
+    hooks:
+      - id: mypy
+        args:
+          [
+            --no-strict-optional,
+            --ignore-missing-imports,
+            --explicit-package-bases,
+          ]
+  - repo: https://github.com/astral-sh/ruff-pre-commit
+    rev: v0.3.0
     hooks:
       - id: ruff
-        args: [--fix, --exit-non-zero-on-fix]
--   repo: https://github.com/regebro/pyroma
+        args: [--fix, --exit-zero]
+      - id: ruff-format
+  - repo: https://github.com/regebro/pyroma
     rev: "4.2"
     hooks:
-    -   id: pyroma
+      - id: pyroma

aeon/__main__.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 import argparse
+import sys
 
 from aeon.backend.evaluator import eval
 from aeon.backend.evaluator import EvaluationContext
@@ -18,16 +19,35 @@
 
 def parse_arguments():
     parser = argparse.ArgumentParser()
-    parser.add_argument("filename", help="name of the aeon files to be synthesized")
-    parser.add_argument("--core", action="store_true", help="synthesize a aeon core file")
+    parser.add_argument(
+        "filename",
+        help="name of the aeon files to be synthesized",
+    )
+    parser.add_argument(
+        "--core",
+        action="store_true",
+        help="synthesize a aeon core file",
+    )
     parser.add_argument(
         "-l",
         "--log",
         nargs="+",
         default="",
-        help="set log level: \nTRACE \nDEBUG \nINFO \nTYPECHECKER \nCONSTRAINT " "\nWARNINGS \nERROR \nCRITICAL",
+        help="set log level: \nTRACE \nDEBUG \nINFO \nTYPECHECKER \nCONSTRAINT "
+        "\nWARNINGS \nERROR \nCRITICAL",
+    )
+    parser.add_argument(
+        "-f",
+        "--logfile",
+        action="store_true",
+        help="export log file",
+    )
+    parser.add_argument(
+        "-d",
+        "--debug",
+        action="store_true",
+        help="Show debug information",
     )
-    parser.add_argument("-f", "--logfile", action="store_true", help="export log file")
     return parser.parse_args()
 
 
@@ -50,10 +70,11 @@ def process_code(core: bool, code: str) -> tuple:
     args = parse_arguments()
     logger = setup_logger()
     export_log(args.log, args.logfile, args.filename)
+    if args.debug:
+        logger.add(sys.stderr)
 
     aeon_code = read_file(args.filename)
     p, ctx, ectx = process_code(args.core, aeon_code)
     logger.info(p)
-
-    if not check_and_log_type_errors (ctx, p, top):
+    if not check_and_log_type_errors(ctx, p, top):
         eval(p, ectx)

aeon/sugar/desugar.py

@@ -55,7 +55,8 @@ def desugar(p: Program) -> tuple[Term, TypingContext, EvaluationContext]:
             assert isinstance(d.type, AbstractionType)
             d_type = d.type
             for tyname in type_decls:
-                d_type = substitute_vartype(d_type, BaseType(tyname.name), tyname.name)
+                d_type = substitute_vartype(d_type, BaseType(tyname.name),
+                                            tyname.name)
             ctx = UninterpretedBinder(
                 ctx,
                 d.name,
@@ -64,30 +65,29 @@ def desugar(p: Program) -> tuple[Term, TypingContext, EvaluationContext]:
         else:
             ty = d.type
             body = d.body
-            for a, t in d.args:
+            for a, t in d.args[::-1]:
                 ty = AbstractionType(a, t, ty)
                 body = Abstraction(a, body)
             prog = Rec(d.name, ty, body, prog)
 
     tydeclname: TypeDecl
     for tydeclname in type_decls:
-        prog = substitute_vartype_in_term(prog, BaseType(tydeclname.name), tydeclname.name)
+        prog = substitute_vartype_in_term(prog, BaseType(tydeclname.name),
+                                          tydeclname.name)
     return (prog, ctx, ectx)
 
 
 def handle_import(path: str) -> Program:
     """Imports a given path, following the precedence rules of current folder,
     AEONPATH."""
-    possible_containers = (
-        [Path.cwd()]
-        + [Path.cwd() / "libraries"]
-        + [Path(str) for str in os.environ.get("AEONPATH", ";").split(";") if str]
-    )
+    possible_containers = ([Path.cwd()] + [Path.cwd() / "libraries"] + [
+        Path(str) for str in os.environ.get("AEONPATH", ";").split(";") if str
+    ])
     for container in possible_containers:
         file = container / f"{path}.ae"
         if file.exists():
             contents = open(file).read()
             return mk_parser("program").parse(contents)
     raise Exception(
-        f"Could not import {path} in any of the following paths: " + ";".join([str(p) for p in possible_containers]),
-    )
+        f"Could not import {path} in any of the following paths: " +
+        ";".join([str(p) for p in possible_containers]), )