# AGENTS.md

This file provides guidance to coding agents collaborating on this repository.

## Mission

Geolog is a Rust codebase for geometric logic:

- a parser and pretty-printer for the Geolog language,
- an elaboration layer that turns syntax into core structures,
- a REPL and workspace/persistence layer,
- a chase/query/solver runtime,
- and an optional egui GUI behind the `gui` Cargo feature.

Priorities, in order:

1. Semantic correctness of theories, instances, queries, and chase behavior.
2. Clear boundaries between parsing, elaboration, core structures, REPL/workspace, and GUI code.
3. Focused, maintainable changes with good regression coverage.
4. Performance only after correctness and testability are preserved.

## Core Rules

- Use English for code, comments, docs, tests, and commit-facing text.
- Prefer small, targeted changes over broad rewrites.
- Fix root causes rather than layering on ad hoc workarounds.
- Keep modules decoupled: parsing in parser/lexer, semantics in `core`/`elaborate`, runtime behavior in `repl`/`query`/`solver`, presentation in `gui`.
- Do not introduce unnecessary global mutable state.
- Preserve feature gating: GUI code must remain behind the `gui` feature.
- Avoid adding dependencies unless clearly justified.
- Add comments only when they clarify non-obvious invariants, algorithms, or semantic constraints.

Quick examples:

- Good: add a targeted regression test for a chase bug in an existing GUI or unit test module.
- Good: fix a REPL/workspace bug in `src/repl.rs` or `src/store/` without refactoring unrelated parser code.
- Bad: rewrite the AST/core boundary during a small GUI task.
- Bad: mix GUI presentation logic into core semantic modules.

## Repository Layout

- `src/lib.rs`: crate entrypoint and module exports.
- `src/ast.rs`, `src/lexer.rs`, `src/parser.rs`, `src/pretty.rs`: syntax pipeline and round-tripping.
- `src/core.rs`: core semantic data structures such as signatures, theories, and structures.
- `src/elaborate/`: elaboration from AST into core representations.
- `src/repl.rs`: REPL state, command handling, and top-level execution flow.
- `src/store/`: persistence/workspace and storage-related logic.
- `src/query/`: chase, query compilation, optimization, backend execution.
- `src/solver/`: solver and tactic logic.
- `src/tensor/`: tensor-based checking/evaluation support.
- `src/gui/`: egui GUI state, panels, and visualizations.
- `src/bin/geolog.rs`: CLI/REPL binary.
- `src/bin/geolog-gui.rs`: GUI binary (requires `--features gui`).
- `examples/geolog/`: sample Geolog programs.
- `tests/`: integration, regression, unit-style cross-module, and property tests.
- `docs/`: architecture and syntax documentation.
- `proofs/`: Lean proofs and formal artifacts.
- `fuzz/`: fuzzing targets.

## Architecture Constraints

- Keep the syntax pipeline clean: text → lexer → parser → AST.
- Keep elaboration separate from parsing and separate from UI code.
- `core` types should remain usable without the GUI.
- GUI code should orchestrate and present existing behavior, not reimplement semantic logic.
- Workspace/persistence behavior belongs in `repl`/`store`, not inside GUI widgets.
- Query/chase behavior changes must preserve observable semantics and existing tests.
- If a change affects persistence or serialization, consider compatibility with existing workspace behavior.

## GUI Rules

- The GUI is optional and must compile cleanly only when the `gui` feature is enabled.
- Prefer fixing GUI bugs in `src/gui/state.rs`, `src/gui/panels/`, or `src/gui/visualizations/` before touching core logic.
- Keep GUI state transitions explicit and centralized when possible.
- Avoid hard-coding theme assumptions; UI should remain readable in the intended visual style.
- File dialog, editor, browser, inspector, console, and visualization behavior should stay consistent with REPL/workspace state.

## Testing Layout Rules

- Prefer unit tests near the code they exercise when there is already a local test module.
- Put broader cross-module coverage in `tests/`.
- Keep regression tests close to the bug they reproduce when that is the clearest fit.
- Do not add a new testing framework if existing `cargo test`, property tests, or fuzz targets are sufficient.
- If you move behavior across modules, move or rewrite the relevant tests with it.

## Workflow

Before coding:

1. Identify whether the task is parser, elaboration, runtime, persistence, solver/query, or GUI work.
2. Read the touched module and nearby tests first.
3. Check whether the change should live in `core`/`repl`/`store` rather than the GUI.

Implement and validate:

1. Make the smallest change that solves the problem.
2. Add or update tests when behavior changes or a bug is fixed.
3. Run the narrowest relevant command while iterating.
4. Run broader validation once the change is stable.
5. Update docs if user-facing behavior or workflow changed.

## Validation Commands

Use the narrowest relevant command first:

- General compile check: `cargo check`
- Full test suite: `cargo test`
- GUI compile check: `cargo check --features gui --bin geolog-gui`
- GUI-related tests: `cargo test --features gui`
- Single test/module during iteration: `cargo test <name>`

Formatting:

- Prefer formatting only touched Rust files when the repository is not already fully formatted.
- Avoid reformatting unrelated files as part of a focused bugfix.

## Testing Expectations

- No semantic bugfix is complete without appropriate validation.
- Parser/elaboration changes should preserve round-trip and error-reporting behavior where relevant.
- Query/chase/solver changes need explicit coverage because regressions can be subtle.
- GUI bugfixes should get a focused test when practical, especially for state transitions or regressions.
- Keep tests deterministic and focused on observable behavior.

## Documentation Expectations

- Update `README.md` when user workflow, CLI behavior, or GUI usage changes.
- Update `docs/ARCHITECTURE.md` or `docs/SYNTAX.md` when architectural or language behavior changes materially.
- If you find stale docs directly related to your change, fix them in the same patch.

## Review Guidelines

Review output should be concise and focus on real defects.

- `P0`: broken build, broken tests, data loss, or incorrect core semantics.
- `P1`: likely semantic regression, unsafe state transition, missing validation on risky changes.

Use this review format:

1. `Severity` (`P0`/`P1`)
2. `File:line`
3. `Issue`
4. `Why it matters`
5. `Minimal fix direction`

Do not include style-only feedback or broad praise.