habedi-work/storage-engine-playground
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add the scafolding for Geomerge-demo

Browse Source
This commit is contained in:
Hassan Abedi 2026-05-21 16:16:14 +02:00
parent 0e5572d1c8
commit c59a40e93f
14 changed files with 404 additions and 133 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.editorconfig
View File

@ -15,7 +15,7 @@ max_line_length = 100
max_line_length = 150 max_line_length = 150
trim_trailing_whitespace = false trim_trailing_whitespace = false
[*.{sh,nix,flake}] [*.sh]
indent_size = 2 indent_size = 2
[*.{yaml,yml,json}] [*.{yaml,yml,json}]

4
.gitattributes vendored
View File

@ -1,8 +1,6 @@
* text=auto eol=lf * text=auto eol=lf
*.go text *.rs text
*.mod text
*.sum text
*.md text *.md text
*.rst text *.rst text
*.json text *.json text

3
.gitignore vendored
View File

@ -73,9 +73,6 @@ poetry.lock
cobertura.xml cobertura.xml
tarpaulin-report.html tarpaulin-report.html
# Comment out the next line if you want to checkin your lock file for Cargo
Cargo.lock
# Misc # Misc
*.proptest-regressions *.proptest-regressions
.DS_Store .DS_Store

20
.pre-commit-config.yaml
View File

@ -19,26 +19,26 @@ repos:
- repo: local - repo: local
hooks: hooks:
- id: nix-fmt-check - id: cargo-fmt-check
name: Check Nix Formatting name: Check Rust Formatting
entry: make fmt-check entry: make fmt-check
language: system language: system
pass_filenames: false pass_filenames: false
files: \.nix$ files: \.rs$
stages: [ pre-commit ] stages: [ pre-commit ]
- id: nix-lint - id: cargo-clippy
name: Lint Nix Files name: Run Clippy
entry: make lint entry: make clippy
language: system language: system
pass_filenames: false pass_filenames: false
files: \.nix$ files: \.rs$
stages: [ pre-commit ] stages: [ pre-commit ]
- id: nix-flake-check - id: cargo-test
name: Run Nix Flake Checks name: Run Rust Tests
entry: make check entry: make check
language: system language: system
pass_filenames: false pass_filenames: false
files: \.(nix|lock)$ files: \.(rs|toml|lock)$
stages: [ pre-push ] stages: [ pre-push ]

21
AGENTS.md
View File

@ -227,16 +227,17 @@ Tests should prefer small facts with readable expected outputs. Avoid large benc
## Required Validation ## Required Validation
Use the repository's actual tooling. At the time this file was written, the copied `Makefile` is still Nix-playground-oriented and may not match this Use the repository's actual tooling.
project. Do not assume `make check` is meaningful until the Makefile is updated for this repository. The `Makefile` wraps the standard Rust commands and skips Rust checks with a clear message if no `Cargo.toml` exists yet.
For Rust changes, prefer: For Rust changes, prefer:
1. `cargo fmt` 1. `make fmt-check`
2. `cargo clippy --all-targets --all-features` 2. `make clippy`
3. `cargo test --all-targets --all-features` 3. `make test`
If the project does not yet have a `Cargo.toml`, record that validation was not available. These map to `cargo fmt --all --check`, `cargo clippy --all-targets --all-features -- -D warnings`, and `cargo test --all-targets --all-features`.
If the project does not yet have a `Cargo.toml`, `make check` should still pass by skipping Rust-specific checks.
For Markdown-only changes, run a manual read-through and check that headings follow the writing style. For Markdown-only changes, run a manual read-through and check that headings follow the writing style.
@ -283,7 +284,7 @@ Use this review format:
- Prefer textual plan explanations in early tests. They make the planner easier to debug. - Prefer textual plan explanations in early tests. They make the planner easier to debug.
- Keep backend comparison fair: same rule, same input facts, same expected output. - Keep backend comparison fair: same rule, same input facts, same expected output.
- Keep transaction and rollback behavior explicit for validation experiments. - Keep transaction and rollback behavior explicit for validation experiments.
- When the Makefile becomes project-specific, update this file's validation section. - Keep project tooling aligned with this file when new commands or checks are added.
## Commit and PR Hygiene ## Commit and PR Hygiene
@ -298,8 +299,8 @@ Use this review format:
Suggested PR checklist: Suggested PR checklist:
- [ ] `cargo fmt` passes, if applicable - [ ] `make fmt-check` passes, if applicable
- [ ] `cargo clippy --all-targets --all-features` passes, if applicable - [ ] `make clippy` passes, if applicable
- [ ] `cargo test --all-targets --all-features` passes, if applicable - [ ] `make test` passes, if applicable
- [ ] Snapshot oracle or expected output included for planner behavior - [ ] Snapshot oracle or expected output included for planner behavior
- [ ] Unsupported cases documented - [ ] Unsupported cases documented

7
Cargo.lock generated Normal file
View File

@ -0,0 +1,7 @@
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
version = 4
[[package]]
name = "geormerge-demo"
version = "0.1.0"

13
Cargo.toml Normal file
View File

@ -0,0 +1,13 @@
[workspace]
members = ["crates/*"]
resolver = "3"
[workspace.package]
edition = "2024"
license = "MIT OR Apache-2.0"
[workspace.lints.rust]
unsafe_code = "forbid"
[workspace.lints.clippy]
pedantic = "warn"

142
Makefile
View File

@ -1,18 +1,7 @@
# Variables # Storage engine playground helpers.
# Every numbered directory at the repository root is treated as a self-contained flake example.
EXAMPLES := $(sort $(wildcard [0-9][0-9]-*))
# Tools are invoked via `nix run` so nothing needs to be pre-installed beyond Nix itself. HAS_CARGO := $(wildcard Cargo.toml)
# Override any of these if you have the tools on $PATH and want faster startup.
NIX ?= nix
NIXFMT ?= $(NIX) run nixpkgs\#nixfmt --
STATIX ?= $(NIX) run nixpkgs\#statix --
DEADNIX ?= $(NIX) run nixpkgs\#deadnix --
# Selector for single-example targets (dev, show, update-one).
EXAMPLE ?=
# Default target
.DEFAULT_GOAL := help .DEFAULT_GOAL := help
.PHONY: help .PHONY: help
@ -20,114 +9,55 @@ help: ## Show help messages for all available targets
@grep -E '^[a-zA-Z_-]+:.*## .*$$' Makefile | \ @grep -E '^[a-zA-Z_-]+:.*## .*$$' Makefile | \
awk 'BEGIN {FS = ":.*## "}; {printf "\033[36m%-20s\033[0m %s\n", $$1, $$2}' awk 'BEGIN {FS = ":.*## "}; {printf "\033[36m%-20s\033[0m %s\n", $$1, $$2}'
.PHONY: examples
examples: ## List discovered example directories
@echo "Examples:"
@for e in $(EXAMPLES); do echo " - $$e"; done
.PHONY: fmt .PHONY: fmt
fmt: ## Format every .nix file with nixfmt (RFC 166 style) fmt: ## Format Rust code
@echo "Formatting .nix files..." @if [ -z "$(HAS_CARGO)" ]; then \
@find . -type f -name '*.nix' -not -path './.git/*' -print0 | xargs -0 -r $(NIXFMT) echo "No Cargo.toml found. Skipping Rust formatting."; \
else \
cargo fmt --all; \
fi
.PHONY: fmt-check .PHONY: fmt-check
fmt-check: ## Check formatting of every .nix file (non-zero exit on drift) fmt-check: ## Check Rust formatting
@echo "Checking .nix formatting..." @if [ -z "$(HAS_CARGO)" ]; then \
@find . -type f -name '*.nix' -not -path './.git/*' -print0 | xargs -0 -r $(NIXFMT) --check echo "No Cargo.toml found. Skipping Rust format check."; \
else \
cargo fmt --all --check; \
fi
.PHONY: lint .PHONY: clippy
lint: ## Run statix and deadnix against every example clippy: ## Run Clippy for all targets and features
@echo "Running statix..." @if [ -z "$(HAS_CARGO)" ]; then \
@$(STATIX) check . echo "No Cargo.toml found. Skipping Clippy."; \
@echo "Running deadnix..." else \
@$(DEADNIX) --fail . cargo clippy --all-targets --all-features -- -D warnings; \
fi
.PHONY: fix-lint .PHONY: test
fix-lint: ## Apply statix and deadnix autofixes where possible test: ## Run Rust tests for all targets and features
@echo "Applying statix fixes..." @if [ -z "$(HAS_CARGO)" ]; then \
@$(STATIX) fix . echo "No Cargo.toml found. Skipping Rust tests."; \
@echo "Applying deadnix fixes..." else \
@$(DEADNIX) --edit . cargo test --all-targets --all-features; \
fi
.PHONY: check .PHONY: check
check: ## Run `nix flake check` in every example directory check: fmt-check clippy test ## Run all Rust checks
@if [ -z "$(EXAMPLES)" ]; then echo "No examples found."; exit 0; fi
@set -e; for e in $(EXAMPLES); do \
echo ">>> nix flake check $$e"; \
(cd "$$e" && $(NIX) flake check); \
done
.PHONY: build
build: ## Run `nix build` on the default package of every example (skips those without one)
@if [ -z "$(EXAMPLES)" ]; then echo "No examples found."; exit 0; fi
@set -e; for e in $(EXAMPLES); do \
if $(NIX) eval --no-warn-dirty "$$e#packages.$$($(NIX) eval --impure --raw --expr 'builtins.currentSystem').default" --apply 'x: true' >/dev/null 2>&1; then \
echo ">>> nix build $$e"; \
(cd "$$e" && $(NIX) build --no-link); \
else \
echo "--- $$e has no default package, skipping"; \
fi; \
done
.PHONY: show
show: ## Print `nix flake show` for every example
@if [ -z "$(EXAMPLES)" ]; then echo "No examples found."; exit 0; fi
@for e in $(EXAMPLES); do \
echo ">>> nix flake show $$e"; \
(cd "$$e" && $(NIX) flake show) || true; \
done
.PHONY: update
update: ## Run `nix flake update` in every example (updates all flake.lock files)
@if [ -z "$(EXAMPLES)" ]; then echo "No examples found."; exit 0; fi
@set -e; for e in $(EXAMPLES); do \
echo ">>> nix flake update $$e"; \
(cd "$$e" && $(NIX) flake update); \
done
.PHONY: update-one
update-one: ## Run `nix flake update` in EXAMPLE=<dir>
@if [ -z "$(EXAMPLE)" ]; then echo "Usage: make update-one EXAMPLE=<dir>"; exit 1; fi
@(cd "$(EXAMPLE)" && $(NIX) flake update)
.PHONY: dev
dev: ## Enter `nix develop` in EXAMPLE=<dir>
@if [ -z "$(EXAMPLE)" ]; then echo "Usage: make dev EXAMPLE=<dir>"; exit 1; fi
@(cd "$(EXAMPLE)" && $(NIX) develop)
.PHONY: metadata
metadata: ## Print `nix flake metadata` for every example
@for e in $(EXAMPLES); do \
echo ">>> nix flake metadata $$e"; \
(cd "$$e" && $(NIX) flake metadata) || true; \
done
.PHONY: clean .PHONY: clean
clean: ## Remove `result` symlinks produced by `nix build` clean: ## Remove build output
@echo "Removing result symlinks..." @if [ -z "$(HAS_CARGO)" ]; then \
@find . -maxdepth 3 -type l \( -name 'result' -o -name 'result-*' \) -print -delete echo "No Cargo.toml found. Nothing to clean."; \
else \
.PHONY: gc cargo clean; \
gc: ## Run `nix store gc` to garbage collect unreferenced store paths fi
@echo "Running nix store gc..."
@$(NIX) store gc
.PHONY: setup-hooks .PHONY: setup-hooks
setup-hooks: ## Install Git hooks (pre-commit) setup-hooks: ## Install Git hooks with pre-commit
@echo "Setting up Git hooks..."
@if ! command -v pre-commit >/dev/null 2>&1; then \
echo "pre-commit not found. Install it via 'pip install pre-commit' or enter a shell that provides it."; \
exit 1; \
fi
@pre-commit install --hook-type pre-commit @pre-commit install --hook-type pre-commit
@pre-commit install --hook-type pre-push @pre-commit install --hook-type pre-push
@pre-commit install-hooks @pre-commit install-hooks
.PHONY: test-hooks .PHONY: test-hooks
test-hooks: ## Run pre-commit hooks across all files test-hooks: ## Run pre-commit hooks across all files
@echo "Running pre-commit hooks on all files..."
@pre-commit run --all-files --show-diff-on-failure @pre-commit run --all-files --show-diff-on-failure
.PHONY: all
all: fmt-check lint check ## Run format check, lint, and flake checks
@echo "All checks passed."

16
crates/README.md Normal file
View File

@ -0,0 +1,16 @@
## Crates
Independent Rust app crates live in this directory.
Each subdirectory should be a normal Cargo package with its own `Cargo.toml`.
The repository root is a virtual workspace, so shared commands such as `make fmt-check`, `make clippy`, and `make test` run across all crates.
Suggested shape:
```text
crates/
app-name/
Cargo.toml
src/
main.rs
```

10
crates/geormerge-demo/Cargo.toml Normal file
View File

@ -0,0 +1,10 @@
[package]
name = "geormerge-demo"
version = "0.1.0"
edition.workspace = true
license.workspace = true
[lints]
workspace = true
[dependencies]

17
crates/geormerge-demo/src/main.rs Normal file
View File

@ -0,0 +1,17 @@
fn main() {
println!("{}", greeting());
}
fn greeting() -> &'static str {
"storage-engine-playground"
}
#[cfg(test)]
mod tests {
use super::greeting;
#[test]
fn greeting_names_the_workspace() {
assert_eq!(greeting(), "storage-engine-playground");
}
}

60
notes/adapter/01-geolog-branches.md Normal file
View File

@ -0,0 +1,60 @@
# Geolog Branch Focus
Generated from the local `tmp/geolog` repository. Focus is inferred from branch names, tip commit messages, commits unique relative to `origin/main`,
and touched files. Branches are sorted by latest tip commit date, newest first. Git does not store branch creator metadata in refs, so
`First Unique Commit Author` is the author of the oldest commit unique to that branch relative to `origin/main`.
| Branch | Latest Update | Last Change Author | First Unique Commit Author | Unique Commits Versus `origin/main` | Focus |
|---------------------------|---------------|--------------------|----------------------------|------------------------------------:|----------------------------------------------------------------------------------------------------------------------------------------------|
| `may-spring-cleaning` | 2026-05-21 | James Deikun | Owen Lynch | 4 | Core cleanup around conversion checking, evaluation parameters, readback, value syntax, and printing. |
| `wasm-diagrams-demo` | 2026-05-21 | George Thomas | Owen Lynch | 136 | Wasm diagrams demo with interactive query-plan diagrams, Graphviz and diagrams vendoring, web layout fixes, and live frontend work. |
| `query-plan-ir-draft-1` | 2026-05-21 | Patrick Aldis | Owen Lynch | 81 | Query plan IR draft with evaluation passing tests, diagram rendering, join orientation visualization, and REPL query diagrams. |
| `main` | 2026-05-21 | Owen Lynch | Unknown, no unique commits | 0 | Current mainline. Tip is a merge of `manual-deploy-fixup`. |
| `reports-2026-05-19` | 2026-05-19 | George Thomas | Owen Lynch | 8 | Team report files through May 19, 2026. |
| `query-plan-ir` | 2026-05-18 | Patrick Aldis | Owen Lynch | 64 | Query planning IR on top of the in-memory and IR integration branch, including register information and plan rendering. |
| `wasm` | 2026-05-15 | George Thomas | Owen Lynch | 69 | Wasm and web frontend work, including JSON output, Geolog Wasm library, Nix/Haskell build updates, and diagrams dependencies. |
| `post-cale-in-memory-ir2` | 2026-05-13 | Patrick Aldis | Owen Lynch | 60 | Integration branch combining in-memory and REPL cleanup with `ir-draft2`. |
| `wasm-dist` | 2026-05-12 | George Thomas | Owen Lynch | 68 | Wasm distribution branch for built assets and frontend output, based on the Wasm and in-memory work. |
| `reports-2026-05-12` | 2026-05-12 | felix | Owen Lynch | 7 | Team report files for late April and May 12, 2026. |
| `felix-db-2` | 2026-05-12 | felix | felix | 8 | Experimental Datalog database backend work, including in-memory and Orville SQL APIs, `applyRule`, and chase tests. |
| `energy` | 2026-05-05 | James Deikun | James Deikun | 3 | Energy or potential semantics in core operations, elaboration, notation, pretty printing, and related golden tests. |
| `ir-draft2-bands` | 2026-05-01 | felix | Owen Lynch | 21 | `ir-draft2` plus a band example and golden output showing lowering behavior. |
| `hexane` | 2026-05-01 | George Thomas | George Thomas | 9 | Hexane integration, Haskell FFI and Rust tooling, Geomerge Haskell wrapper, JSON tests, and IR cherry-picks. |
| `in-memory-devibed` | 2026-04-30 | Patrick Aldis | Owen Lynch | 57 | Cleanup of in-memory and REPL code, structured REPL errors, command and state modules, comments, and property tests. |
| `lowering-via-eval-quote` | 2026-04-29 | Owen Lynch | Owen Lynch | 7 | Alternative lowering approach via eval and quote, with SSA and graded-rig tests. |
| `in-memory` | 2026-04-28 | Patrick Aldis | Owen Lynch | 48 | In-memory database execution, DB plan modules, IR lowering, REPL support, and formatting cleanup. |
| `lower-to-js` | 2026-04-26 | Owen Lynch | Owen Lynch | 8 | TypeScript and JavaScript runtime lowering experiments, including graph-of-graphs compilation and relation validators. |
| `george/wip` | 2026-04-20 | Cale Gibbard | Owen Lynch | 96 | Broad work-in-progress branch covering Nix flakes, Reflex, examples, data partitioning, diagnostics, FNotation, and Geolog language changes. |
| `latex-dates` | 2026-04-20 | George Thomas | George Thomas | 2 | Nix shell and Shake fixes for LaTeX date generation in documentation builds. |
| `config-default` | 2026-04-17 | Shuntian Liu | Unknown, no unique commits | 0 | Configuration default fix, likely already merged or superseded by `main`. |
| `geomerge` | 2026-04-17 | Shuntian Liu | Unknown, no unique commits | 0 | Geomerge import or merge branch, likely already merged or superseded by `main`. |
| `warmup-ci` | 2026-04-17 | Owen Lynch | Owen Lynch | 8 | CI warmup work, including Cabal update steps and a freeze file for Shake. |
| `mcp` | 2026-04-09 | George Thomas | Owen Lynch | 56 | MCP server or tool experiment with REPL-like functionality, LaTeX source-reading tools, transcripts, and in-memory dependencies. |
| `ir-draft2` | 2026-04-09 | James Deikun | Owen Lynch | 20 | Second IR draft with equality-type support and updates across core, elaborator, IR, lowering, diagnostics, and tests. |
| `golden-tests-fix` | 2026-04-09 | Patrick Aldis | Patrick Aldis | 2 | Golden-test path fix so `tasty-golden` looks in the `test` directory for FNotation and Geolog. |
| `in-memory-demo` | 2026-04-07 | Felix Dilke | Owen Lynch | 38 | In-memory demo and REPL workflow, including `:schema`, dotted table names for insert and query, and REPL test scripts. |
| `ir-draft1-clean` | 2026-04-07 | Cale Gibbard | Owen Lynch | 22 | Cleaned and rebased version of `ir-draft1`, including explicit lowering context and local environment handling. |
| `lsp-demo` | 2026-04-02 | Patrick Aldis | Patrick Aldis | 2 | Demo-only LSP behavior change to hide fatal errors. |
| `ir-draft1` | 2026-04-01 | James Deikun | Owen Lynch | 16 | First IR lowering draft, with support for columns, totality-rule cleanup, core lowering, and golden tests. |
| `lsp` | 2026-03-31 | Patrick Aldis | Patrick Aldis | 28 | Geolog LSP development, diagnostics integration, analyzed buffer result types, and `lsp-test` coverage. |
| `benchmarks` | 2026-03-31 | felix | Unknown, no unique commits | 0 | Benchmark work that appears already merged or superseded by `main`. |
| `why-geolog` | 2026-03-31 | Martin Kleppmann | Unknown, no unique commits | 0 | Why-Geolog documentation or positioning notes, likely already merged or superseded by `main`. |
| `fnotation-release` | 2026-03-30 | Owen Lynch | Unknown, no unique commits | 0 | Documentation for an FNotation release, likely already merged or superseded by `main`. |
| `repl` | 2026-03-27 | George Thomas | George Thomas | 18 | REPL usability changes, including command renames, completions, declaration display, and load-to-source naming. |
| `reporting-refactor` | 2026-03-27 | Patrick Aldis | Patrick Aldis | 4 | Reporter abstraction cleanup, including contrafunctor support and lifted `reportIO`. |
| `parser-exceptions` | 2026-03-25 | Patrick Aldis | Patrick Aldis | 8 | Parser, lexer, and elaborator refactor to use `ExceptT` and pure reporting. |
| `fb3-fail` | 2026-03-24 | felix | Patrick Aldis | 6 | Failure-case fixtures and Nix setup around `fb3` parser and elaborator golden tests. |
| `edits-from-london` | 2026-03-24 | Owen Lynch | Owen Lynch | 2 | London meeting edits across core syntax, operations, elaboration, lexer, pretty printing, and linear-order tests. |
| `fix-off-by-one` | 2026-03-20 | Patrick Aldis | Patrick Aldis | 2 | Diagnostic source-position fix for an off-by-one error in `lineOf`. |
| `felix-db-2-cale-edits` | 2026-03-11 | Felix Dilke | Felix Dilke | 2 | Incomplete Cale edits making `InMDB` monadic via state in `felix-db`. |
| `cg/query-planning` | 2026-03-10 | Cale Gibbard | Unknown, no unique commits | 0 | Query planning work that appears already merged or superseded by `main`. |
| `ir-design-2` | 2026-03-06 | James Deikun | Unknown, no unique commits | 0 | Follow-up IR design document cleanup, likely already merged or superseded by `main`. |
| `observational` | 2026-02-24 | Owen Lynch | Owen Lynch | 16 | Observational checking and diagnostics refactor, including lexer, parser, elaborator diagnostics, and related documentation. |
| `ir-design-1` | 2026-02-23 | James Deikun | Unknown, no unique commits | 0 | IR vision-document draft, likely already merged or superseded by `main`. |
| `haddock-ci` | 2026-01-15 | Owen Lynch | Unknown, no unique commits | 0 | Haddock CI experiment, likely already merged or superseded by `main`. |
| `notation-refactor` | 2025-12-24 | Owen Lynch | Unknown, no unique commits | 0 | Notation refactor and output-name updates, likely already merged or superseded by `main`. |
| `tests` | 2025-12-19 | Owen Lynch | Owen Lynch | 2 | Prospectus documentation change clarifying theorem expectations. |
## Change Log
- 2026-05-22: Updated branch table with latest update dates, last-change authors, first unique commit authors, unique commit counts, and inferred focus notes.

222
notes/adapter/02-geolog-lang-findings.md Normal file
View File

@ -0,0 +1,222 @@
# Geolog Lang Findings
Source inspected: local reference checkout at `tmp/geolog/geolog-lang`.
## Summary
`geolog-lang` is a Haskell prototype for a Geolog source language. It parses `.glog` theory files, elaborates them into a typed core language, lowers a selected `Main` theory into a flat relational representation, and includes an in-memory relation engine with law checking and a conjunctive-query planner.
For this repository, the useful reference is not the Haskell implementation itself. The useful reference is the shape of the pipeline:
```text
Geolog theory
-> typed core elaboration
-> flat relational theory
-> tables, generated laws, and validation queries
-> in-memory execution and query planning experiments
```
## Package Shape
The package exposes modules for:
- core syntax, values, evaluation, quoting, and equality checking
- notation, lexer, parser configuration, and diagnostics
- elaboration from parsed notation into typed core entries
- lowering from the typed `Main` theory into a flat relational theory
- relational IR for tables, atoms, propositions, and laws
- an in-memory database and a conjunctive-query planner
The test suite combines golden tests for `.glog` elaboration and lowering with unit and property tests for the in-memory database and planner.
## Source Language Shape
The examples use declarations such as:
```text
theory Main := sig
Node : Set
Edge : Node -> Node -> Set
end
```
The notation supports `theory`, `def`, `set`, `let`, `open`, `import`, `Set`, `Prop`, `Int`, `String`, `Inductive`, `pure`, `init`, `->`, `*->`, and `=>`.
The source language is closer to a dependent typed theory language than to ordinary Datalog. Relations, functions, records, equality, and inductive constructions are represented in the source and then selectively lowered.
## Lowered Relational IR
The lowered IR has these main concepts:
- `Path`: dotted table or law names represented as path components
- `Table`: column types and an optional primary key
- `Atom`: table reference, optional row identity term, and positional value terms
- `Prop`: atom, equality, conjunction, or disjunction
- `Law`: universally quantified variables, an antecedent proposition, and a consequent proposition
- `FlatTheory`: maps of tables and laws
For the graph example above, lowering produces a `Node` table, an `Edge` table, and an `Edge.foreignKeys` law. The law says that every edge row implies the existence of both endpoint node rows.
This is directly relevant to Geomerge-style validation experiments. A high-level declaration can compile into maintained violation checks by turning generated laws into queries:
```text
required_consequent(x) :- antecedent(x).
violation(x) :- required_consequent(x), not consequent(x).
```
## Generated Law Patterns
Two generated law shapes matter for this playground:
- foreign-key laws: rows in one table require referenced rows in another table
- totality laws: functional relations require an output for each valid input
Foreign-key laws are generated from dependent arguments that reference prior sets or relations. Totality laws are generated for functional table shapes.
The current lowering appears intentionally narrow. Unsupported shapes are reported or panic in prototype code rather than being treated as complete semantics. That is useful for this repo because early adapters should also make supported and unsupported cases explicit.
## In-Memory Execution
The in-memory database stores:
- ground values: integers, text, and entity identities
- relations: set-valued tuples with secondary indexes by column and value
- bindings: rows of variable assignments
Query evaluation supports atoms and conjunctions. Conjunctions are evaluated with natural join. Law checking evaluates a law antecedent to produce witness bindings, then checks the consequent for each witness. Violations carry the law path and witness values.
This gives a simple snapshot oracle shape for validation experiments:
```text
facts + generated law
-> antecedent witnesses
-> consequent checks
-> violation rows
```
## Storage Engine
`geolog-lang` uses a custom in-memory storage engine, not SQLite, Postgres, or another external database. The storage module is `Geolog.DB.InMemory`.
The core storage structures are:
- `DB`: schema, relations, and next entity IDs
- `Relation`: fixed-arity tuple set plus a secondary index
- `Val`: stored values, including integers, text, and entity identities
- `Bindings`: query result rows as variable-to-value maps
The relation storage shape is:
```text
Relation {
arity: tuple width,
members: set of tuples,
index: map from (column position, value) to matching tuples
}
```
Inserts add a tuple to the `members` set and update the secondary index for every `(column, value)` pair in the tuple. Atom evaluation uses literal terms to probe those secondary indexes, intersects candidate tuple sets when multiple literal constraints are present, and then produces variable bindings.
Conjunction evaluation has two paths:
- naive evaluation: evaluate each atom, then natural-join the resulting bindings
- planned evaluation: use `Geolog.DB.Plan` to build a semijoin-based join plan, then evaluate that plan against the same in-memory relations
The checked insert path inserts into a temporary updated database and checks generated laws such as `foreignKeys`. If the law check finds violations, the updated database is not returned. This gives rollback-like behavior at the API boundary, but it is not a transactional storage engine with durable logs or multi-step rollback.
## Storage API
`geolog-lang` does not define a storage abstraction or backend trait. It directly uses the concrete in-memory API in `Geolog.DB.InMemory`.
The minimal storage API it needs is:
```text
schema registration:
fromTheory :: FlatTheory -> DB
entity allocation:
freshEntity :: Path -> DB -> (Val, DB)
writes:
insertRow :: Path -> [Val] -> DB -> DB
checkedInsertRow :: FlatTheory -> Path -> [Val] -> DB -> Either InsertError DB
reads:
evalAtom :: DB -> QAtom -> Either DBError Bindings
evalConjunction :: DB -> [QAtom] -> Either DBError Bindings
validation:
checkLaw :: DB -> Path -> Law -> Either DBError [LawViolation]
```
The planner also depends on planned conjunction evaluation:
```text
planConjunction :: [QAtom] -> JoinPlan
evalRootedPlan :: DB -> JoinPlan -> Either DBError Bindings
evalConjunctionPlanned :: DB -> [QAtom] -> Either DBError Bindings
```
For this repository, an adapter-facing storage interface should probably provide:
1. flat schema registration from lowered tables,
2. fixed-arity tuple insertion into named relations,
3. stable entity ID allocation per table path,
4. tuple lookup by table and positional constraints,
5. variable binding output for query atoms,
6. natural join and semijoin support, or enough scans and index probes for the planner to implement them,
7. generated-law checking with structured violations, and
8. checked insert behavior that rejects or rolls back invalid writes.
This API is snapshot-oriented. It is not yet a durable transaction API, an incremental DBSP API, or a general SQL-like storage layer.
## Query Planning
The planner targets conjunctive queries over the in-memory database. It:
1. evaluates each atom independently,
2. builds an atom intersection graph weighted by shared variables,
3. computes a maximum spanning forest,
4. performs bottom-up and top-down semijoin reduction, and
5. performs full joins along the forest.
The tests compare planned conjunction evaluation against naive conjunction evaluation on generated graph workloads. This is a useful test pattern for this repository: every planned execution path should have a simple snapshot or naive oracle while the planner is still experimental.
## Adapter Takeaways
The practical adapter direction is:
1. Model a small `FlatTheory`-like IR in Rust before implementing a full Geolog frontend.
2. Start with generated foreign-key and totality laws because they have clear violation semantics.
3. Represent violation outputs with law identity, violation kind, relation or consequent identity, and bound variable values.
4. Keep source elaboration, relational lowering, planning, and execution as separate modules.
5. Add textual plan output early so planner behavior is inspectable.
6. Use a naive snapshot evaluator as the oracle for planned or maintained execution.
## Open Questions
- How much of Geolog source syntax should this repo parse directly versus using hand-built fixtures first?
- Should equality in consequents be supported before disjunction, existential witnesses, or recursive laws?
- Should totality validation use explicit missing-output violations or a generated required-output relation?
- How should entity identities map onto this repo's storage transaction and rollback model?
- Which law subset is enough to test Geomerge-style maintained violation relations without building a full chase engine?
## Next Experiment Shape
A small vertical slice for this repository could be:
```text
input:
table node(id)
table edge(src, dst, id)
law edge_foreign_keys:
edge(src, dst, id) -> node(src) and node(dst)
snapshot output:
violation rows for missing src or dst nodes
planned output:
textual antijoin plan for edge against node(src) and node(dst)
```
That would test catalog construction, generated-law representation, antijoin planning, deterministic violation rows, and a snapshot oracle without requiring the rest of Geolog.

0
notes/flowlog/.gitkeep Normal file
View File