250 lines
8.3 KiB
Markdown
250 lines
8.3 KiB
Markdown
|
# Geolog Development Notes
|
||
|
|
|
||
|
|
This document describes the features and components added to the geolog project (by me, Hassan).
|
||
|
|
|
||
|
|
## Overview
|
||
|
|
|
||
|
|
Geolog is a language for geometric logic - a type theory with semantics in topoi and geometric morphisms, designed as a unified language for database schemas, queries, and migrations.
|
||
|
|
|
||
|
|
## Components
|
||
|
|
|
||
|
|
### Core Components (Pre-existing)
|
||
|
|
|
||
|
|
- **Parser & Lexer** (`src/lexer.rs`, `src/parser.rs`) - Chumsky-based parser for geolog syntax
|
||
|
|
- **AST** (`src/ast.rs`) - Abstract syntax tree representation
|
||
|
|
- **Core Types** (`src/core.rs`) - Signatures, structures, theories, axioms
|
||
|
|
- **Elaboration** (`src/elaborate.rs`) - Type checking and elaboration
|
||
|
|
- **Store** (`src/store.rs`) - Append-only persistent storage with version control
|
||
|
|
- **REPL** (`src/repl.rs`) - Interactive command-line environment
|
||
|
|
- **Solver** (`src/solver.rs`) - Model enumeration for geometric theories
|
||
|
|
- **Query Engine** (`src/query/`) - Relational algebra backend for queries
|
||
|
|
- **Chase Algorithm** (`src/query/chase.rs`) - Fixpoint computation for axiom closure
|
||
|
|
|
||
|
|
### Debugger (`src/debugger.rs`)
|
||
|
|
|
||
|
|
Interactive debugger for the chase algorithm providing:
|
||
|
|
- Step-through execution
|
||
|
|
- Breakpoints on axiom name patterns
|
||
|
|
- Variable inspection
|
||
|
|
- Iteration stepping
|
||
|
|
|
||
|
|
Usage in REPL:
|
||
|
|
```
|
||
|
|
:debug-chase <instance> [max_iterations]
|
||
|
|
```
|
||
|
|
|
||
|
|
### GUI Application (`src/gui/`)
|
||
|
|
|
||
|
|
A full-featured graphical interface built with egui.
|
||
|
|
|
||
|
|
#### Building the GUI
|
||
|
|
|
||
|
|
```bash
|
||
|
|
# Build with GUI feature
|
||
|
|
cargo build --features gui
|
||
|
|
|
||
|
|
# Run the GUI
|
||
|
|
cargo run --features gui --bin geolog-gui
|
||
|
|
|
||
|
|
# With workspace persistence
|
||
|
|
cargo run --features gui --bin geolog-gui -- -d ./myproject
|
||
|
|
|
||
|
|
# Load a file on startup
|
||
|
|
cargo run --features gui --bin geolog-gui -- examples/preorder.geolog
|
||
|
|
```
|
||
|
|
|
||
|
|
#### GUI Architecture
|
||
|
|
|
||
|
|
```
|
||
|
|
src/gui/
|
||
|
|
├── mod.rs # Module exports
|
||
|
|
├── app.rs # Main GeologApp (egui::App implementation)
|
||
|
|
├── state.rs # GuiState wrapping ReplState
|
||
|
|
├── panels/
|
||
|
|
│ ├── mod.rs
|
||
|
|
│ ├── browser.rs # Theory/instance tree browser
|
||
|
|
│ ├── editor.rs # Code editor with line numbers
|
||
|
|
│ ├── inspector.rs # Detail view for selected items
|
||
|
|
│ └── console.rs # Output/error messages
|
||
|
|
└── visualizations/
|
||
|
|
├── mod.rs
|
||
|
|
├── chase.rs # Chase step-through visualization
|
||
|
|
└── graph.rs # Relation graph visualization
|
||
|
|
```
|
||
|
|
|
||
|
|
#### GUI Features
|
||
|
|
|
||
|
|
**Browser Panel (Left)**
|
||
|
|
- Tree view of all theories and instances
|
||
|
|
- Filter/search functionality
|
||
|
|
- Click to select, right-click for context menu
|
||
|
|
- Shows counts (sorts, functions, relations, axioms, elements)
|
||
|
|
|
||
|
|
**Editor Panel (Center Top)**
|
||
|
|
- Multi-line code editor
|
||
|
|
- Line numbers
|
||
|
|
- Run button (or Ctrl+Enter) to execute code
|
||
|
|
- Clear button
|
||
|
|
|
||
|
|
**Inspector Panel (Center Bottom)**
|
||
|
|
- Theory details: parameters, sorts, functions, relations, instance fields, axioms
|
||
|
|
- Instance details: elements by sort, function values, relation tuples, nested instances
|
||
|
|
- Collapsible sections
|
||
|
|
- "View Graph" button for instances
|
||
|
|
|
||
|
|
**Console Panel (Bottom)**
|
||
|
|
- Scrollable message log
|
||
|
|
- Color-coded messages: info (gray), success (green), error (red), warning (orange)
|
||
|
|
- Auto-scroll option
|
||
|
|
- Clear button
|
||
|
|
|
||
|
|
**Chase Visualization**
|
||
|
|
- Step/Run All/Stop controls
|
||
|
|
- Events log showing axiom firings with bindings
|
||
|
|
- Breakpoint management
|
||
|
|
- Current structure info (elements, relation tuples)
|
||
|
|
- Mode indicator (Idle/Stepping/Running/Completed)
|
||
|
|
|
||
|
|
**Graph Visualization**
|
||
|
|
- Nodes represent elements (colored by sort)
|
||
|
|
- Edges represent relation tuples
|
||
|
|
- Interactive: drag nodes, zoom (scroll), pan
|
||
|
|
- Relation filter dropdown
|
||
|
|
- Reset Layout / Fit buttons
|
||
|
|
- Hover to see sort name
|
||
|
|
|
||
|
|
#### UI Layout
|
||
|
|
|
||
|
|
```
|
||
|
|
┌─────────────────────────────────────────────────────────────┐
|
||
|
|
│ File Edit View Chase Help │
|
||
|
|
├────────────┬────────────────────────────────────────────────┤
|
||
|
|
│ ▼ Theories │ ┌─────────────────────────────────────────┐ │
|
||
|
|
│ Preorder │ │ Editor │ │
|
||
|
|
│ Graph │ │ theory Foo { │ │
|
||
|
|
│ ▼ Instances│ │ X : Sort; │ │
|
||
|
|
│ Chain3 │ │ } [Run] [Clear] │ │
|
||
|
|
│ │ └─────────────────────────────────────────┘ │
|
||
|
|
│ │ ┌─────────────────────────────────────────┐ │
|
||
|
|
│ │ │ Inspector: Chain3 : Preorder │ │
|
||
|
|
│ │ │ ▼ Elements (3) │ │
|
||
|
|
│ │ │ X: bot, mid, top │ │
|
||
|
|
│ │ │ ▼ Relations │ │
|
||
|
|
│ │ │ leq: 6 tuples [View Graph] │ │
|
||
|
|
│ │ └─────────────────────────────────────────┘ │
|
||
|
|
├────────────┴────────────────────────────────────────────────┤
|
||
|
|
│ Console [Clear]│
|
||
|
|
│ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms) │
|
||
|
|
│ + Defined instance Chain3 : Preorder (3 elements) │
|
||
|
|
└─────────────────────────────────────────────────────────────┘
|
||
|
|
```
|
||
|
|
|
||
|
|
## CLI Commands
|
||
|
|
|
||
|
|
### REPL Commands
|
||
|
|
|
||
|
|
```
|
||
|
|
:help [topic] Show help (topics: syntax, examples)
|
||
|
|
:quit Exit the REPL
|
||
|
|
:list [target] List theories/instances
|
||
|
|
:inspect <name> Show details of a theory or instance
|
||
|
|
:source <file> Load and execute a geolog file
|
||
|
|
:clear Clear the screen
|
||
|
|
:reset Reset all state
|
||
|
|
|
||
|
|
# Version Control
|
||
|
|
:commit [msg] Commit current changes
|
||
|
|
:history Show commit history
|
||
|
|
|
||
|
|
# Instance Mutation
|
||
|
|
:add <inst> <elem> <sort> Add element to instance
|
||
|
|
:assert <inst> <rel> args Assert relation tuple
|
||
|
|
:retract <inst> <elem> Retract element
|
||
|
|
|
||
|
|
# Query
|
||
|
|
:query <inst> <sort> List all elements of a sort
|
||
|
|
:explain <inst> <sort> Show query execution plan
|
||
|
|
:compile <inst> <sort> Show RelAlgIR compilation
|
||
|
|
:chase <inst> [max_iter] Run chase on instance axioms
|
||
|
|
:debug-chase <inst> [max] Run chase with interactive debugger
|
||
|
|
|
||
|
|
# Solver
|
||
|
|
:solve <theory> [budget] Find model of theory from scratch
|
||
|
|
:extend <inst> <theory> Find extension of instance to theory
|
||
|
|
```
|
||
|
|
|
||
|
|
### CLI Usage
|
||
|
|
|
||
|
|
```bash
|
||
|
|
# Start REPL (in-memory)
|
||
|
|
cargo run
|
||
|
|
|
||
|
|
# Start REPL with workspace persistence
|
||
|
|
cargo run -- -d ./myproject
|
||
|
|
|
||
|
|
# Load file on startup
|
||
|
|
cargo run -- examples/preorder.geolog
|
||
|
|
|
||
|
|
# Show help
|
||
|
|
cargo run -- --help
|
||
|
|
```
|
||
|
|
|
||
|
|
## Dependencies
|
||
|
|
|
||
|
|
### Core Dependencies
|
||
|
|
- `chumsky` - Parser combinators
|
||
|
|
- `ariadne` - Error reporting
|
||
|
|
- `uuid` - Unique identifiers
|
||
|
|
- `rkyv` - Zero-copy serialization
|
||
|
|
- `rustyline` - Readline for REPL
|
||
|
|
- `indexmap` - Ordered hash maps
|
||
|
|
|
||
|
|
### GUI Dependencies (feature = "gui")
|
||
|
|
- `eframe` - egui framework with native window
|
||
|
|
- `egui_extras` - Additional egui widgets
|
||
|
|
- `rfd` - Native file dialogs
|
||
|
|
|
||
|
|
## Example
|
||
|
|
|
||
|
|
```geolog
|
||
|
|
// Define a preorder theory
|
||
|
|
theory Preorder {
|
||
|
|
X : Sort;
|
||
|
|
leq : [a: X, b: X] -> Prop;
|
||
|
|
|
||
|
|
// Reflexivity
|
||
|
|
forall x : X. |- [a: x, b: x] leq;
|
||
|
|
|
||
|
|
// Transitivity
|
||
|
|
forall x : X, y : X, z : X.
|
||
|
|
[a: x, b: y] leq, [a: y, b: z] leq |- [a: x, b: z] leq;
|
||
|
|
}
|
||
|
|
|
||
|
|
// Define an instance
|
||
|
|
instance Chain3 : Preorder = {
|
||
|
|
bot : X;
|
||
|
|
mid : X;
|
||
|
|
top : X;
|
||
|
|
[a: bot, b: mid] leq;
|
||
|
|
[a: mid, b: top] leq;
|
||
|
|
}
|
||
|
|
```
|
||
|
|
|
||
|
|
Then run `:chase Chain3` to compute the transitive closure.
|
||
|
|
|
||
|
|
## Development
|
||
|
|
|
||
|
|
```bash
|
||
|
|
# Check without GUI
|
||
|
|
cargo check
|
||
|
|
|
||
|
|
# Check with GUI
|
||
|
|
cargo check --features gui
|
||
|
|
|
||
|
|
# Run tests
|
||
|
|
cargo test
|
||
|
|
|
||
|
|
# Build release
|
||
|
|
cargo build --release --features gui
|
||
|
|
```
|