Remove core frontend parser, --core flag, and examples/core

CLAUDE.md

@@ -0,0 +1,86 @@
+# CLAUDE.md
+
+This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
+
+## Project Overview
+
+Aeon is a statically-typed programming language with native Liquid Types (refinement types), implemented as a Python interpreter with Python FFI. Developed at LASIGE, University of Lisbon.
+
+## Common Commands
+
+```bash
+# Install for development
+uv pip install -e ".[dev]"
+uvx pre-commit install
+
+# Run tests
+uv run pytest
+
+# Run a single test
+uv run pytest tests/end_to_end_test.py::test_name -x
+
+# Run an .ae file
+uv run python -m aeon [file.ae]
+
+# Run with synthesis (genetic programming, 60s default budget)
+uv run python -m aeon --budget 10 -s gp examples/synthesis/example.ae
+
+# Run all examples (used in CI)
+bash run_examples.sh
+
+# Linting/formatting (via pre-commit hooks)
+uvx pre-commit run --all-files
+
+# Type checking
+uv run mypy aeon
+```
+
+**Synthesizer options:** `gp` (genetic programming, default), `synquid`, `random_search`, `enumerative`, `hc` (hill climbing), `1p1` (one plus one)
+
+## Code Style
+
+- Line length: 120 (ruff + black)
+- Ruff rules: E and F codes (ignoring E741, E501)
+- Strict mypy with custom stubs in `/stubs`
+- pytest-beartype enabled for `aeon.core` package
+- Python 3.10+ target
+
+## Architecture
+
+The codebase follows a compiler pipeline:
+
+```
+Source (.ae) → Parse (lark) → Sugar AST → Desugar/Elaborate → Core AST → ANF → Typecheck (z3 SMT) → Synthesize/Evaluate
+```
+
+### Key Packages
+
+| Package | Role |
+|---|---|
+| `aeon/facade` | Entry point: `AeonDriver` orchestrates the full pipeline, `AeonConfig` holds settings |
+| `aeon/sugar` | Surface language: AST (`STypes`/`STerm` in `program.py`), parser (lark grammar in `aeon_sugar.lark`), desugaring |
+| `aeon/core` | Core language: `Types`/`Term` (internal representation, never user-facing), substitutions, liquid constraints, core term/type parser |
+| `aeon/frontend` | ANF conversion |
+| `aeon/elaboration` | Converts sugar AST to core AST with type elaboration |
+| `aeon/typechecking` | Type inference and liquid type constraint verification |
+| `aeon/verification` | SMT-based verification via z3: horn clauses, constraint solving |
+| `aeon/synthesis` | Program synthesis: multiple backends (genetic programming via geneticengine, synquid, enumerative, LLM/ollama) |
+| `aeon/backend` | Runtime evaluation |
+| `aeon/lsp` | Language Server Protocol implementation (pygls v2.1.0) |
+| `aeon/libraries` | Standard library `.ae` files (List, Math, Image, etc.) |
+| `aeon/prelude` | Built-in functions and type definitions |
+
+### Important Distinction
+
+- **`STypes`/`STerm`** (in `aeon/sugar/program.py`): Surface/sugar language types — safe to expose to users and tooling
+- **`Types`/`Term`** (in `aeon/core/types.py`, `aeon/core/terms.py`): Core language types — internal only, never exposed to users
+
+### Grammars
+
+- `aeon/sugar/aeon_sugar.lark` — surface language grammar
+- `aeon/core/aeon_core.lark` — core language grammar (used internally by tests and verification)
+
+### Entry Points
+
+- CLI: `aeon/__main__.py` → `AeonDriver` (modes: parse/run/synth/lsp/format)
+- Synthesis: `aeon/synthesis/entrypoint.py` identifies holes and routes to synthesizer backends

aeon/__main__.py

@@ -40,7 +40,6 @@ def parse_arguments():
 
 
 def _parse_common_arguments(parser: ArgumentParser):
-    parser.add_argument("--core", action="store_true", help="synthesize a aeon core file")
     parser.add_argument("--budget", type=int, default=60, help="Time for synthesis (in seconds).")
     parser.add_argument(
         "-l",
@@ -146,10 +145,7 @@ def main() -> None:
         aeon_lsp.start(args.tcp)
         sys.exit(0)
 
-    if args.core:
-        errors = driver.parse_core(args.filename)
-    else:
-        errors = driver.parse(args.filename)
+    errors = driver.parse(args.filename)
 
     if errors:
         for err in errors:

aeon/facade/driver.py

@@ -1,7 +1,6 @@
 import sys
 from dataclasses import dataclass
-from functools import reduce
-from typing import Any, Iterable
+from typing import Iterable
 
 from aeon.backend.evaluator import EvaluationContext
 from aeon.backend.evaluator import eval
@@ -13,22 +12,19 @@
 from aeon.elaboration import elaborate
 from aeon.facade.api import AeonError
 from aeon.frontend.anf_converter import ensure_anf
-from aeon.frontend.parser import parse_term
 from aeon.prelude.prelude import evaluation_vars
-from aeon.prelude.prelude import typing_vars
 from aeon.sugar.ast_helpers import st_top
 from aeon.sugar.bind import bind, bind_program
 from aeon.sugar.desugar import DesugaredProgram, desugar
 from aeon.sugar.lifting import lift
-from aeon.sugar.lowering import lower_to_core, lower_to_core_context, type_to_core
+from aeon.sugar.lowering import lower_to_core, lower_to_core_context
 from aeon.sugar.parser import parse_main_program
 from aeon.sugar.program import Program, STerm
 from aeon.synthesis.entrypoint import synthesize_holes
 from aeon.synthesis.identification import incomplete_functions_and_holes
 from aeon.synthesis.modules.synthesizerfactory import make_synthesizer
 from aeon.synthesis.uis.api import SynthesisUI, SynthesisFormat
 from aeon.typechecking.typeinfer import check_type_errors
-from aeon.utils.ctx_helpers import build_context
 from aeon.utils.name import Name
 from aeon.utils.pprint import pretty_print_node
 from aeon.utils.time_utils import RecordTime
@@ -53,20 +49,6 @@ class AeonDriver:
     def __init__(self, cfg: AeonConfig):
         self.cfg = cfg
 
-    def parse_core(self, filename: str):
-        # TODO: deprecate core parsing
-        aeon_code = read_file(filename)
-
-        core_typing_vars: dict[Name, Any] = reduce(
-            lambda acc, el: acc | {el[0]: type_to_core(el[1], available_vars=[e for e in acc.items()])},
-            typing_vars.items(),
-            {},
-        )
-
-        self.typing_ctx = build_context(core_typing_vars)
-        self.core_ast = parse_term(aeon_code)
-        self.metadata: Metadata = {}
-
     def parse(self, filename: str = None, aeon_code: str = None) -> Iterable[AeonError]:
         if aeon_code is None:
             aeon_code = read_file(filename)

aeon/verification/helpers.py

@@ -12,7 +12,7 @@
 from aeon.core.substitutions import substitution_in_liquid
 from aeon.core.types import AbstractionType, TypeConstructor, Top, TypeVar
 from aeon.core.types import t_bool
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 from aeon.verification.smt import base_functions
 from aeon.verification.vcs import Conjunction
 from aeon.verification.vcs import Constraint

docs/index.md

@@ -181,7 +181,6 @@ There are a few libraries available, but unstable as they are under development:
 | -----: | :---------------------------------------------------------------------------- |
 |     -d | Prints debug information                                                      |
 |     -t | Prints timing information about the different steps of the compiler           |
-| --core | Parses the input file as being the Core language, instead of the surface aeon |
 | -l, --log | Sets the log level (TRACE, DEBUG, INFO, WARNINGS, ERROR, CRITICAL, etc.)  |
 | -f, --logfile | Exports the log to a file                                              |
 | -n, --no-main | Disables introducing hole in main                                     |

tests/backend_test.py

@@ -7,7 +7,7 @@
 from aeon.backend.evaluator import EvaluationContext, eval
 from aeon.core.terms import Literal, Term, TypeAbstraction, TypeApplication
 from aeon.core.types import BaseKind, TypeConstructor
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 
 
 def weval(t: Term, ctx: EvaluationContext = EvaluationContext()):

tests/driver.py

@@ -19,7 +19,7 @@
 from aeon.backend.evaluator import eval
 from aeon.decorators import Metadata
 
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 from aeon.core.types import top
 from aeon.utils.name import Name
 

tests/frontend_test.py

@@ -20,8 +20,8 @@
 from aeon.core.types import TypePolymorphism
 from aeon.core.types import TypeVar
 from aeon.frontend.anf_converter import ensure_anf
-from aeon.frontend.parser import parse_term
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_term
+from aeon.core.parser import parse_type
 from aeon.utils.ast_helpers import false
 from aeon.utils.ast_helpers import i0
 from aeon.utils.ast_helpers import i1

tests/instantiation_test.py

@@ -3,7 +3,7 @@
 from aeon.core.instantiation import type_substitution
 from aeon.core.types import t_bool
 from aeon.core.types import t_int
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.utils.name import Name
 
 

tests/optimization_test.py

@@ -1,7 +1,7 @@
 from __future__ import annotations
 
 from aeon.optimization.normal_form import optimize
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 
 
 def eq(source, expected):

tests/polytypes_test.py

@@ -1,5 +1,5 @@
 from aeon.core.types import TypeConstructor
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 
 from aeon.sugar.ast_helpers import st_top
 from tests.driver import check_compile

tests/sub_test.py

@@ -1,5 +1,5 @@
 from aeon.utils.name import Name
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.typechecking.context import TypingContext, VariableBinder
 from aeon.typechecking.entailment import entailment
 from aeon.verification.sub import sub

tests/substitutions_test.py

@@ -2,8 +2,8 @@
 
 from aeon.core.substitutions import substitution
 from aeon.core.substitutions import substitution_in_type
-from aeon.frontend.parser import parse_term
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_term
+from aeon.core.parser import parse_type
 from aeon.utils.name import Name
 
 

tests/typevars_test.py

@@ -2,7 +2,7 @@
 
 from aeon.core.types import get_type_vars
 from aeon.core.types import TypeVar
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.utils.name import Name
 
 

tests/wellformed_test.py

@@ -8,7 +8,7 @@
 from aeon.core.types import t_int
 from aeon.core.types import TypePolymorphism
 from aeon.core.types import TypeVar
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.typechecking.context import TypingContext
 from aeon.typechecking.well_formed import wellformed
 from aeon.utils.ctx_helpers import built_std_context