152 lines
7.0 KiB
Markdown
152 lines
7.0 KiB
Markdown
# 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}
|
|
```
|