geolog-zeta-fork/README2.md

# 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.

Current design note:
- The GUI uses a rigid docked layout rather than draggable in-window splitters.
- This was done to reduce hover/drag-induced layout jitter and keep the workspace visually stable.

#### 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)
- Fixed-width docked sidebar

**Editor Panel (Center)**
- Multi-line code editor
- Run button (or Ctrl+Enter) to execute code
- Clear button

**Inspector Panel (Right)**
- 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
- Fixed-width docked sidebar in the main workspace view

**Console Panel (Bottom)**
- Scrollable message log
- Color-coded messages: info (gray), success (green), error (red), warning (orange)
- Auto-scroll option
- Clear button
- **Integrated REPL input** with command history (Up/Down arrows)
  - Type `:help` for commands
  - Type `:list` to list theories/instances
  - Type `:inspect <name>` to inspect
  - Type `:chase <instance>` to run chase
  - Or type geolog code directly
- Fixed-height docked footer

**Layout**
- Docked workspace layout for stability
- Browser on the left, editor in the center, inspector on the right
- Console fixed at the bottom
- Chase and graph visualizations replace the central workspace when active

**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                          │
├──────────────┬──────────────────────────────┬───────────────┤
│ Browser      │ Editor                       │ Inspector     │
│ ▼ Theories   │ theory Foo {                 │ Chain3        │
│   Preorder   │   X : Sort;                  │ : Preorder    │
│ ▼ Instances  │ }           [Run] [Clear]    │ ▼ Elements    │
│   Chain3     │                              │ ▼ Relations   │
│              │                              │ [View Graph]  │
├──────────────┴──────────────────────────────┴───────────────┤
│ Console                                              [Clear]│
│ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms)  │
│ + Defined instance Chain3 : Preorder (3 elements)          │
│─────────────────────────────────────────────────────────────│
│ geolog> :list                                         [Run] │
└─────────────────────────────────────────────────────────────┘
```

## 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;

  // The ordering relation: x <= y
  leq : [x: X, y: X] -> Prop;

  // Reflexivity: x <= x
  ax/refl : forall x : X.
    |- [x: x, y: x] leq;

  // Transitivity: x <= y and y <= z implies x <= z
  ax/trans : forall x : X, y : X, z : X.
    [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
}

// Define an instance with automatic chase
// The 'chase' keyword applies axioms to compute the closure
instance Chain3 : Preorder = chase {
  bot : X;
  mid : X;
  top : X;

  // Assert the basic ordering; chase derives reflexive pairs
  // and transitive closure (bot <= top)
  [x: bot, y: mid] leq;
  [x: mid, y: top] leq;
}
```

After loading this file, the chase algorithm automatically computes:
- Reflexive pairs: `bot <= bot`, `mid <= mid`, `top <= top`
- Transitive closure: `bot <= top`

You can also define an instance without `chase` and run `:chase Chain3` manually.

## 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
```