# Architecture

## What Geolog Is

Geolog is a command-line tool for defining rules and automatically deriving facts from them. Think of it like a spreadsheet that can figure out new cells based on formulas you define, except the "formulas" are logical rules and the "cells" are facts about things.

**Example:** You tell Geolog "if A is friends with B, and B is friends with C, then A knows C." Then you say "Alice is friends with Bob" and "Bob is friends with Charlie." Geolog automatically figures out "Alice knows Charlie."

---

## Tech Stack

**Language:** Rust (2021 edition)

### Key Dependencies

| Crate               | What It Does                                                    |
|---------------------|-----------------------------------------------------------------|
| `chumsky`           | Reads `.geolog` files and understands their structure           |
| `ariadne`           | Shows helpful error messages with line numbers                  |
| `rkyv`              | Saves data to disk efficiently                                  |
| `rustyline`         | Makes the interactive prompt work (arrow keys, history, etc.)   |
| `egglog-union-find` | Tracks when two things are actually the same thing              |
| `roaring`           | Stores large sets of numbers efficiently                        |
| `indexmap`          | Hash maps that remember insertion order                         |
| `memmap2`           | Reads files by mapping them directly into memory                |

### Testing Tools

| Tool | Purpose |
|------|---------|
| `insta` | Compares output against saved "snapshots" to catch regressions |
| `proptest` | Generates random inputs to find edge cases |
| `tempfile` | Creates temporary directories for tests |

---

## How Data Flows Through the System

```
┌─────────────────────────────────────────────────────┐
│                    USER INTERFACE                    │
│  You type commands or load .geolog files here        │
├─────────────────────────────────────────────────────┤
│                   PARSING LAYER                      │
│  Turns text into a structured tree (like HTML DOM)   │
│  Example: "P : Sort;" becomes {name: "P", kind: Sort}│
├─────────────────────────────────────────────────────┤
│                 ELABORATION LAYER                    │
│  Checks types and resolves names                     │
│  Example: Verifies "src : E -> V" refers to real     │
│           sorts E and V that were declared           │
├─────────────────────────────────────────────────────┤
│                    CORE LAYER                        │
│  The verified, type-checked representation           │
│  Everything here is guaranteed to be well-formed     │
├─────────────────────────────────────────────────────┤
│                  STORAGE LAYER                       │
│  Saves everything to disk, tracks history            │
│  Like git for your data                              │
├─────────────────────────────────────────────────────┤
│               QUERY & SOLVER LAYER                   │
│  Runs the chase algorithm to derive new facts        │
│  Searches for models that satisfy your rules         │
├─────────────────────────────────────────────────────┤
│                  TENSOR ALGEBRA                      │
│  Efficiently checks which rules need to fire         │
│  Uses sparse matrices for performance                │
└─────────────────────────────────────────────────────┘
```

---

## Directory Structure

| Path                | What's There |
|---------------------|--------------|
| `src/bin/geolog.rs` | The main program entry point — run `cargo run` and this executes |
| `src/lib.rs`        | Library code that other Rust programs could use |
| `src/repl.rs`       | The interactive prompt (handles `:chase`, `:inspect`, etc.) |
| `src/lexer.rs`      | Breaks text into tokens like `theory`, `{`, `Sort`, `;` |
| `src/parser.rs`     | Builds a tree structure from tokens |
| `src/ast.rs`        | Defines what the tree structure looks like |
| `src/core.rs`       | The "verified" internal representation |
| `src/elaborate/`    | Type checking and name resolution |
| `src/store/`        | Saving/loading data, version control |
| `src/query/`        | The chase algorithm lives here |
| `src/solver/`       | Model search (finding valid instances) |
| `src/tensor/`       | Efficient rule checking with sparse matrices |
| `src/cc.rs`         | Congruence closure — tracks equalities |
| `examples/geolog/`  | 30+ example files you can learn from |
| `tests/`            | Automated tests |
| `docs/`             | Documentation (ARCHITECTURE.md, SYNTAX.md) |

---

## Key Entry Points

If you're reading the code, start here:

| What You Want | Where To Look |
|---------------|---------------|
| How the CLI starts | `src/bin/geolog.rs` |
| How files are parsed | `src/lib.rs::parse()` |
| How REPL commands work | `src/repl.rs::ReplState::process_line()` |
| How theories are checked | `src/elaborate/theory.rs::elaborate_theory()` |
| How instances are built | `src/elaborate/instance.rs::elaborate_instance_ctx()` |
| How facts are derived | `src/query/chase.rs::chase_fixpoint_with_cc()` |
| How models are searched | `src/solver/mod.rs::enumerate_models()` |

---

## REPL Commands

When you run `geolog` interactively, these commands are available:

```
:list                  - Show all theories and instances
:inspect Triangle      - Show details of "Triangle" instance

:add Triangle v : V;   - Add element v to Triangle
:assert [x:a, y:b] R;  - Assert a relation holds
:retract [x:a, y:b] R; - Remove a relation

:chase Triangle        - Derive all consequences from axioms
:solve MyInstance      - Search for a valid model

:commit "message"      - Save current state (like git commit)
:history               - Show past commits

:source file.geolog    - Load and run a file
:help                  - Show help
```

### Example Session

```
$ cargo run -- examples/geolog/graph.geolog
> :list
Theories: Graph
Instances: Triangle

> :inspect Triangle
Instance Triangle : Graph
  Carriers:
    V: {A, B, C}
    E: {ab, bc, ca}
  Functions:
    src: {ab -> A, bc -> B, ca -> C}
    tgt: {ab -> B, bc -> C, ca -> A}
```