diff --git a/AGENTS.md b/AGENTS.md index 8113627..f95029d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -6,7 +6,7 @@ This file provides guidance to coding agents collaborating on this repository. Query Engine is an experimental Rust project for building query-engine components. The current implementation is centered on a chase-based reasoning -core plus lightweight interactive frontends. +core, lightweight interactive frontends, and an early relational/SQL scaffold. Priorities, in order: @@ -52,8 +52,14 @@ Quick examples: - `rule.rs`: TGDs, EGDs, equalities, and builders. - `substitution.rs`: variable bindings and unification. - `engine.rs`: chase execution and configuration. + - `inference.rs`: shared matching and provenance-aware materialization helpers. - `union_find.rs`: equality merging support. - `src/frontend/`: lightweight interactive surface for scripts, REPL, and local web UI. +- `src/relational/`: schemas, values, rows, and result sets for relational execution. +- `src/catalog/`: predicate-to-table schema inference and catalog access. +- `src/sql/`: narrow SQL AST and parser support. +- `src/planner/`: logical plan structures and SQL-to-plan translation. +- `src/execution/`: execution of the current logical plan subset. - `tests/`: integration, regression, and property-based tests. ## Architecture Constraints @@ -64,6 +70,8 @@ Quick examples: - The chase engine should remain largely stateless; pass execution state explicitly. - New chase variants should be composable with existing infrastructure. - Existential variables generate labeled nulls (`Term::Null`). +- The current SQL support is intentionally narrow: single-table `SELECT-FROM-WHERE` with positional column names such as `c0` and `c1`. +- Relational and SQL modules should build on explicit schemas and logical plans, not call frontend helpers directly. - If you add parser, planner, or executor layers, keep their responsibilities separate. - Public docs and interfaces should reflect the implemented state of the repository accurately. @@ -105,6 +113,7 @@ Example scopes that are good first tasks: - Implement a new utility method on `Instance` or `Atom`. - Tighten frontend wording so it matches actual behavior. - Introduce a small planning-oriented type without changing execution semantics. +- Extend the SQL slice with a narrow, well-tested feature such as aliases or named columns. ## Testing Expectations @@ -113,6 +122,7 @@ Example scopes that are good first tasks: - Integration tests go in `tests/integration_tests.rs`. - Regression tests for bug fixes go in `tests/regression_tests.rs`. - Property-based tests go in `tests/property_tests.rs`. +- SQL/planner/execution flow tests go in `tests/sql_pipeline_tests.rs`. - Do not merge code that breaks existing tests. Minimal unit-test checklist for chase-related behavior: @@ -151,6 +161,7 @@ Before coding: 2. Identify affected tests. 3. Consider impact on API stability. 4. Avoid overstating roadmap progress in code comments or docs. +5. Keep the supported SQL subset explicit when touching `sql`, `planner`, or `execution`. Before submitting: @@ -186,6 +197,7 @@ Use this review format: - If you detect contradictory repository conventions, follow existing code and update docs accordingly. - When uncertain about correctness, add or extend tests first, then optimize. - When adding non-chase engine pieces, define clean interfaces before broadening functionality. +- Keep `frontend` presentation-only when possible; shared reasoning logic belongs in `chase`, relational logic in `relational`/`planner`/`execution`. - Keep user-facing naming consistent with the repository name: `query-engine` / `query_engine`. ## Commit and PR Hygiene diff --git a/ROADMAP.md b/ROADMAP.md index 5abce21..753df03 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -23,6 +23,12 @@ This document tracks the current state and next steps for the repository. - [x] Equality merging with union-find support - [x] REPL, script runner, and local web UI - [x] Provenance-oriented explanation support +- [x] Relational schema, value, row, and result-set scaffolding +- [x] Predicate-backed catalog inference +- [x] Minimal SQL AST and parser +- [x] Logical plan scaffolding +- [x] Logical-plan execution for the first SQL slice +- [x] Single-table `SELECT-FROM-WHERE` support with positional columns (`c0`, `c1`, ...) ### Near-Term Cleanup @@ -30,27 +36,31 @@ This document tracks the current state and next steps for the repository. - [ ] Remove remaining stale terminology in comments and help text - [ ] Expand examples for the current rule-engine workflow - [ ] Add rustdoc coverage for the main public types +- [ ] Document the current SQL subset and its limits ### Query-Engine Structure -- [ ] Introduce a dedicated logical representation module -- [ ] Define clear front-end, planning, and execution boundaries +- [x] Introduce a dedicated logical representation module +- [x] Define clear front-end, planning, and execution boundaries - [ ] Add engine-level abstractions that are not chase-specific -- [ ] Establish common schema and typed-value representations +- [x] Establish common schema and typed-value representations - [ ] Design a source boundary for future scans and pushdown ### Front End and Planning -- [ ] Add a parser-oriented module beyond the current rule REPL language -- [ ] Add AST types for a structured query front end -- [ ] Add logical plan node types -- [ ] Add name resolution and schema validation hooks -- [ ] Add expression typing and nullability tracking +- [x] Add a parser-oriented module beyond the current rule REPL language +- [x] Add AST types for a structured query front end +- [x] Add logical plan node types +- [x] Add name resolution and schema validation hooks +- [x] Add expression typing and nullability tracking +- [ ] Add aliases and richer projection expressions +- [ ] Add joins across multiple predicate-backed tables +- [ ] Add a catalog path for stable column naming beyond `c0`, `c1`, ... ### Execution and Optimization - [ ] Introduce physical operator abstractions -- [ ] Add a planning step from logical operators to executable operators +- [x] Add a planning step from logical operators to executable operators - [ ] Add basic rule-based logical rewrites - [ ] Add statistics and cost-model scaffolding - [ ] Add indexing and access-path abstractions @@ -73,7 +83,7 @@ This document tracks the current state and next steps for the repository. - [ ] Fact import/export - [ ] File-backed data source experiments -- [ ] Table-like row or batch abstractions +- [x] Table-like row or batch abstractions - [ ] Stable script/query file format - [ ] Integration with external storage or file formats @@ -91,6 +101,7 @@ This document tracks the current state and next steps for the repository. - [x] Integration tests - [x] Property-based tests - [x] Regression tests +- [x] Initial SQL pipeline tests - [ ] Benchmark coverage - [ ] Snapshot-style frontend tests - [ ] More planner/executor tests as those layers are added diff --git a/examples/geolog/README.md b/examples/geolog/README.md new file mode 100644 index 0000000..0f1d39d --- /dev/null +++ b/examples/geolog/README.md @@ -0,0 +1,529 @@ +# Geolog DSL Structure + +This directory contains example `.geolog` files that use a richer DSL than the +minimal `.chase` script language in `examples/scripts/`. + +This README summarizes the Geolog DSL structure as it appears in the examples in +this directory. It should be read as a practical, example-driven reference, not +as a formal or complete language specification. + +## At a Glance + +- Top-level declarations are `theory` and `instance`. +- The main kind of type is `Sort`. +- Symbols can denote sorts, constants, functions, predicates, or nested + instances. +- Axioms use sequent-style syntax: `premise |- conclusion`. +- Instance bodies can be plain literals (`= { ... }`) or chase blocks + (`= chase { ... }`). +- Function application is postfix, and qualified names use `/`. + +## Informal File Shape + +```text +file := { comment | theory_decl | instance_decl } + +comment := // ... + +theory_decl := + theory theory_params? Name { + theory_item* + } + +instance_decl := + instance Name : theory_app = { + instance_item* + } + + | instance Name : theory_app = chase { + instance_item* + } +``` + +In practice, a file is usually a sequence of theory declarations followed by one +or more example instances. + +## Top-Level Declarations + +### `theory` + +A theory introduces sorts, symbols, and axioms. + +```text +theory Graph { + V : Sort; + Edge : [src: V, tgt: V] -> Prop; +} +``` + +Theories may also be parameterized. + +```text +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; +} + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} +``` + +Observed parameter forms: + +- sort parameters: `(X : Sort)` +- instance parameters: `(N : PetriNet instance)` +- dependent instance parameters: `(RP : N ReachabilityProblem instance)` + +### `instance` + +An instance provides concrete elements and assignments for a theory. + +```text +instance Triangle : Graph = { + A : V; + B : V; + C : V; +} +``` + +Instances may target parameterized theories by writing the arguments before the +theory name. + +```text +instance MyMap : MyBase Map = { ... } +instance solution0 : ExampleNet problem0 Solution = { ... } +instance AB_Iso : As/a Bs/b Iso = { ... } +``` + +## Theory Body Items + +The examples show the following declaration forms inside a theory body. + +### Sort declarations + +```text +V : Sort; +E : Sort; +``` + +This introduces carrier sorts. + +### Constants or distinguished elements + +```text +elem : X; +``` + +This introduces a named element of an existing sort. + +### Functions + +```text +src : E -> V; +fwd : X -> Y; +token/of : token -> N/P; +``` + +Names may contain `/`, which is used heavily for structured or qualified names. + +### Predicates and relations + +Unary predicates: + +```text +completed : Item -> Prop; +``` + +Record-shaped predicates: + +```text +Edge : [src: V, tgt: V] -> Prop; +depends : [item: Item, on: Item] -> Prop; +``` + +### Product-valued functions + +Functions may return record-shaped values. + +```text +pair_of : A -> [left: B, right: C]; +W/src : W -> [firing: F, arc: N/out]; +``` + +### Nested instance slots + +Theories can contain fields whose values are themselves instances. + +```text +initial_marking : N Marking instance; +trace : N Trace instance; +initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; +``` + +### Axioms + +Axioms use a sequent-like form. + +```text +ax/trans : forall x, y, z : V. + [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path; +``` + +An axiom declaration has the observed structure: + +```text +name : forall binders. premise |- conclusion; +``` + +## Formula and Term Syntax + +The examples use the following building blocks inside axioms and assignments. + +### Quantifiers + +Universal binders appear after `forall`. + +```text +forall x : X, y : Y. +``` + +Existentials appear directly inside conclusions or disjuncts. + +```text +exists r : R. r R/data = [x: a, y: b] +exists w : W. w W/src_firing = f, w W/src_arc = arc +``` + +### Sequents + +The central connective is `|-`, separating premise from conclusion. + +```text +premise1, premise2 |- conclusion1, conclusion2; +``` + +In the examples: + +- commas act as conjunctions +- the left side is the premise +- the right side is the conclusion + +### Equality + +Equality is used for ordinary values and compound values. + +```text +ab src = A +r R/data = [x: a, y: b] +x fwd bwd = x +``` + +### Truth constants + +```text +|- true; +|- false; +``` + +### Disjunction + +Disjunction is written as `\/`. + +```text +[item: x, on: y] depends |- x blocked \/ y completed; +``` + +### Predicate atoms + +Unary predicate atoms: + +```text +x blocked +y completed +``` + +Record-shaped predicate atoms: + +```text +[src: x, tgt: y] Edge +[a: x, f: i] id +``` + +### Postfix application + +Function application is postfix and can be chained. + +```text +e src +x id +x fwd bwd +w W/src_arc N/out/tgt +``` + +This is one of the most distinctive traits of the DSL. + +### Qualified paths + +The slash `/` is used for qualification and nested access. + +Observed examples include: + +```text +R/data +N/P +N/out/src +trace/input_terminal +RP/initial_marking/token +ExampleNet/A +``` + +### Record literals + +Records are written with brackets and named fields. + +```text +[x: a, y: b] +[firing: f, arc: arc] +``` + +The examples also show positional shorthand for record arguments when the field +order is known: + +```text +[e, e] mul = e; +[cook_dinner, on: buy_groceries] depends; +``` + +### Field projection + +Record-valued terms support field projection. + +```text +r R/data .x = a +``` + +## Instance Body Items + +The examples show the following forms inside instance bodies. + +### Element declarations + +```text +a : V; +tok : token; +ab : T; +``` + +### Function assignments + +```text +ab src = A; +tok token/of = ExampleNet/A; +a1 map = MyBase/b1; +``` + +### Predicate facts + +Unary facts: + +```text +buy_groceries completed; +``` + +Record-shaped facts: + +```text +[src: a, tgt: b] Edge; +[item: x, on: y] depends; +``` + +### Product-valued assignments + +```text +a1 pair_of = [left: b1, right: c1]; +ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out]; +``` + +### Nested instance literals + +Instance-valued fields can be assigned inline blocks. + +```text +initial_marking = { + tok : token; + tok token/of = ExampleNet/A; +}; +``` + +## `= { ... }` vs `= chase { ... }` + +The examples consistently use two instance forms. + +### Plain instance + +```text +instance Triangle : Graph = { + ... +} +``` + +This gives a direct structure with only the explicitly listed elements and +assignments. + +### Chase instance + +```text +instance Chain : Graph = chase { + ... +} +``` + +This marks an instance whose contents should be extended by the theory axioms. +Examples use this for transitive closure, existential witness generation, and +trace/reachability constructions. + +## Observed Design Patterns + +### Parameterized theories + +Theories can be abstract over: + +- a sort, such as `theory (X : Sort) Container` +- an instance, such as `theory (N : PetriNet instance) Marking` +- multiple arguments, such as `theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution` + +### Theory application by adjacency + +Theory arguments are written before the theory name. + +```text +N Marking instance +MyBase Map +ExampleNet problem0 Solution +``` + +### Nested structure via qualified names + +Many examples model dependent structure by naming into earlier declarations. + +```text +token/of : token -> N/P; +initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; +``` + +## What Seems Outside the File DSL + +Some example comments refer to interactive commands such as: + +```text +:source +:load +:inspect +:chase +:solve +``` + +Those commands appear to belong to an external REPL or tool environment rather +than to the `.geolog` file grammar itself. + +## Querying + +The examples do **not** show a stable, implemented query form inside `.geolog` +files in the same way they show `theory` and `instance` declarations. + +What they do show is: + +### 1. External interactive commands + +Some files suggest that querying or inspection happens through an external tool +or REPL: + +```text +:source examples/geolog/transitive_closure.geolog +:inspect Chain +:chase Chain +:solve EmptyModel +``` + +Based on the example comments, these commands appear to mean roughly: + +- `:source` or `:load`: load Geolog definitions from files +- `:inspect`: inspect a declared instance +- `:chase`: materialize or display the closure of a `= chase` instance +- `:solve`: ask a solver to construct a satisfying instance for a theory + +These are tool commands, not part of the confirmed `.geolog` declaration syntax. + +### 2. A sketched future query form + +One file contains a commented-out example of a possible query block: + +```text +query can_reach_B_from_A { + ? : ExampleNet problem0 Solution instance; +} +``` + +This suggests an aspirational style where querying is expressed as asking for a +witness inhabiting some instance type. However, in the current examples this is +only a comment, not an observed live construct. + +### 3. Current implemented querying elsewhere in the repo + +The currently implemented query syntax in this repository belongs to the minimal +frontend language, not to Geolog. That language supports forms such as: + +```text +query Ancestor(?X, ?Y)? +explain Ancestor(alice, carol)? +``` + +So the safest summary is: + +- Geolog examples define theories, instances, and chase-oriented structure. +- Querying appears to be external, REPL-driven, or still in design. +- The only clearly implemented query syntax in this repo today is the minimal + `.chase` frontend query language. + +## Best Example Files by Feature + +- `transitive_closure.geolog`: basic theory, axiom, and `= chase` usage +- `graph.geolog`: plain structural instances +- `monoid.geolog`: postfix application and positional record syntax +- `todo_list.geolog`: unary predicates and disjunction +- `sort_param_simple.geolog`: sort and instance parameters +- `nested_instance_test.geolog`: nested instance-valued fields +- `product_codomain_test.geolog`: record-valued function codomains +- `field_projection_test.geolog`: field projection syntax +- `record_existential_test.geolog`: existential witness creation with records +- `petri_net_showcase.geolog`: large multi-theory composition +- `solver_demo.geolog`: satisfiability-oriented axiom patterns + +## Minimal Example + +```text +theory Graph { + V : Sort; + Edge : [src: V, tgt: V] -> Prop; + Path : [src: V, tgt: V] -> Prop; + + ax/base : forall x, y : V. + [src: x, tgt: y] Edge |- [src: x, tgt: y] Path; +} + +instance Chain : Graph = chase { + a : V; + b : V; + [src: a, tgt: b] Edge; +} +``` + +That small example already shows the core structure of the DSL: + +- a `theory` +- sort and predicate declarations +- an axiom written as a sequent +- an `instance` +- a `chase` block that asks for closure under the theory axioms diff --git a/examples/geolog/category.geolog b/examples/geolog/category.geolog new file mode 100644 index 0000000..f480a1f --- /dev/null +++ b/examples/geolog/category.geolog @@ -0,0 +1,86 @@ +// Category theory in current geolog syntax +// +// This is the "desugared" version of the aspirational syntax in +// loose_thoughts/2026-01-21_dependent_sorts_and_functional_relations.md + +theory Category { + ob : Sort; + mor : Sort; + + // Morphism source and target + src : mor -> ob; + tgt : mor -> ob; + + // Composition: comp(f, g, h) means "h = f ; g" (f then g) + // Domain constraint: f.tgt = g.src + comp : [f: mor, g: mor, h: mor] -> Prop; + + // Identity: id(a, f) means "f is the identity on a" + id : [a: ob, f: mor] -> Prop; + + // === Axioms === + + // Identity morphisms have matching source and target + ax/id_src : forall x : ob, i : mor. [a: x, f: i] id |- i src = x; + ax/id_tgt : forall x : ob, i : mor. [a: x, f: i] id |- i tgt = x; + + // Composition domain constraint + ax/comp_dom : forall p : mor, q : mor, r : mor. + [f: p, g: q, h: r] comp |- p tgt = q src; + + // Composition source/target + ax/comp_src : forall p : mor, q : mor, r : mor. + [f: p, g: q, h: r] comp |- r src = p src; + ax/comp_tgt : forall p : mor, q : mor, r : mor. + [f: p, g: q, h: r] comp |- r tgt = q tgt; + + // Existence of identities (one per object) + ax/id_exists : forall x : ob. |- exists i : mor. [a: x, f: i] id; + + // Existence of composites (when composable) + ax/comp_exists : forall p : mor, q : mor. + p tgt = q src |- exists r : mor. [f: p, g: q, h: r] comp; + + // Left unit: id_a ; f = f + ax/unit_left : forall x : ob, i : mor, p : mor, r : mor. + [a: x, f: i] id, p src = x, [f: i, g: p, h: r] comp |- r = p; + + // Right unit: f ; id_b = f + ax/unit_right : forall y : ob, i : mor, p : mor, r : mor. + [a: y, f: i] id, p tgt = y, [f: p, g: i, h: r] comp |- r = p; + + // Associativity: (f ; g) ; h = f ; (g ; h) + ax/assoc : forall p : mor, q : mor, r : mor, pq : mor, qr : mor, pqr1 : mor, pqr2 : mor. + [f: p, g: q, h: pq] comp, [f: pq, g: r, h: pqr1] comp, + [f: q, g: r, h: qr] comp, [f: p, g: qr, h: pqr2] comp + |- pqr1 = pqr2; + + // Uniqueness of composition (functional) + ax/comp_unique : forall p : mor, q : mor, r1 : mor, r2 : mor. + [f: p, g: q, h: r1] comp, [f: p, g: q, h: r2] comp |- r1 = r2; + + // Uniqueness of identity (one per object) + ax/id_unique : forall x : ob, i1 : mor, i2 : mor. + [a: x, f: i1] id, [a: x, f: i2] id |- i1 = i2; +} + +// The "walking arrow" category: A --f--> B +// +// Now we can declare just objects and non-identity morphisms! +// The chase derives: +// - Identity morphisms for each object (via ax/id_exists) +// - Composition facts (via ax/comp_exists) +// - Source/target for compositions (via ax/comp_src, ax/comp_tgt) +// +// The equality saturation (via congruence closure) collapses: +// - id;id;id;... = id (via ax/unit_left and ax/unit_right) +// - Duplicate compositions (via ax/comp_unique) +// Without CC, the chase would loop forever creating id;id, id;id;id, ... +instance Arrow : Category = chase { + // Objects + A : ob; + B : ob; + + // Non-identity morphism + f : mor; f src = A; f tgt = B; +} diff --git a/examples/geolog/field_projection_chase_test.geolog b/examples/geolog/field_projection_chase_test.geolog new file mode 100644 index 0000000..a007482 --- /dev/null +++ b/examples/geolog/field_projection_chase_test.geolog @@ -0,0 +1,27 @@ +// Test: Field projection in chase + +theory FieldProjectionChaseTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Marker sort for elements whose x field matches a given a + XMatches : Sort; + XMatches/r : XMatches -> R; + XMatches/a : XMatches -> A; + + // Axiom: if r's x field equals a, create an XMatches + ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists m : XMatches. m XMatches/r = r, m XMatches/a = a; +} + +instance Test : FieldProjectionChaseTest = chase { + a1 : A; + a2 : A; + b1 : B; + r1 : R; + r1 R/data = [x: a1, y: b1]; + r2 : R; + r2 R/data = [x: a2, y: b1]; +} diff --git a/examples/geolog/field_projection_test.geolog b/examples/geolog/field_projection_test.geolog new file mode 100644 index 0000000..deb7376 --- /dev/null +++ b/examples/geolog/field_projection_test.geolog @@ -0,0 +1,12 @@ +// Test: Field projection syntax + +theory FieldProjectionTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Axiom using field projection: r R/data .x + ax1 : forall r : R, a : A. r R/data .x = a |- true; +} diff --git a/examples/geolog/graph.geolog b/examples/geolog/graph.geolog new file mode 100644 index 0000000..69ba7f5 --- /dev/null +++ b/examples/geolog/graph.geolog @@ -0,0 +1,79 @@ +// Directed Graph: vertices and edges with source/target functions +// +// This is the canonical example of a "presheaf" - a functor from a small +// category (the "walking arrow" • → •) to Set. + +theory Graph { + V : Sort; // Vertices + E : Sort; // Edges + + src : E -> V; // Source of an edge + tgt : E -> V; // Target of an edge +} + +// A simple triangle graph: A → B → C → A +instance Triangle : Graph = { + // Vertices + A : V; + B : V; + C : V; + + // Edges + ab : E; + bc : E; + ca : E; + + // Edge endpoints + ab src = A; + ab tgt = B; + bc src = B; + bc tgt = C; + ca src = C; + ca tgt = A; +} + +// A self-loop: one vertex with an edge to itself +instance Loop : Graph = { + v : V; + e : E; + e src = v; + e tgt = v; +} + +// The "walking arrow": two vertices, one edge +instance Arrow : Graph = { + s : V; + t : V; + f : E; + f src = s; + f tgt = t; +} + +// A more complex graph: diamond shape with two paths from top to bottom +// +// top +// / \ +// left right +// \ / +// bottom +// +instance Diamond : Graph = { + top : V; + left : V; + right : V; + bottom : V; + + top_left : E; + top_right : E; + left_bottom : E; + right_bottom : E; + + top_left src = top; + top_left tgt = left; + top_right src = top; + top_right tgt = right; + left_bottom src = left; + left_bottom tgt = bottom; + right_bottom src = right; + right_bottom tgt = bottom; +} diff --git a/examples/geolog/iso_instance_test.geolog b/examples/geolog/iso_instance_test.geolog new file mode 100644 index 0000000..68653c8 --- /dev/null +++ b/examples/geolog/iso_instance_test.geolog @@ -0,0 +1,29 @@ +// Multi-parameter theory instantiation test + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +theory A { a : Sort; } +theory B { b : Sort; } + +instance As : A = { + a1 : a; + a2 : a; +} + +instance Bs : B = { + b1 : b; + b2 : b; +} + +// Can we create an Iso instance with sort parameters? +instance AB_Iso : As/a Bs/b Iso = { + a1 fwd = Bs/b1; + a2 fwd = Bs/b2; + b1 bwd = As/a1; + b2 bwd = As/a2; +} diff --git a/examples/geolog/iso_theory_test.geolog b/examples/geolog/iso_theory_test.geolog new file mode 100644 index 0000000..d17ad21 --- /dev/null +++ b/examples/geolog/iso_theory_test.geolog @@ -0,0 +1,9 @@ +// Multi-parameter theory test (Iso from vision) + +// First just try sorts as parameters +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + // Axioms would need chained function application... + // fb : forall x : X. |- x fwd bwd = x; +} diff --git a/examples/geolog/monoid.geolog b/examples/geolog/monoid.geolog new file mode 100644 index 0000000..596dd37 --- /dev/null +++ b/examples/geolog/monoid.geolog @@ -0,0 +1,78 @@ +// Monoid: a set with an associative binary operation and identity element +// +// This is the simplest algebraic structure with interesting axioms. +// Note: geolog uses postfix function application. + +theory Monoid { + M : Sort; + + // Binary operation: M × M → M + mul : [x: M, y: M] -> M; + + // Identity element: we use a unary function from M to M that + // "picks out" the identity (any x maps to e) + // A cleaner approach would use Unit → M but that needs product support. + id : M -> M; + + // Left identity: id(x) * y = y (id(x) is always e) + ax/left_id : forall x : M, y : M. + |- [x: x id, y: y] mul = y; + + // Right identity: x * id(y) = x + ax/right_id : forall x : M, y : M. + |- [x: x, y: y id] mul = x; + + // Associativity: (x * y) * z = x * (y * z) + ax/assoc : forall x : M, y : M, z : M. + |- [x: [x: x, y: y] mul, y: z] mul = [x: x, y: [x: y, y: z] mul] mul; + + // id is constant: id(x) = id(y) for all x, y + ax/id_const : forall x : M, y : M. + |- x id = y id; +} + +// Trivial monoid: single element, e * e = e +instance Trivial : Monoid = { + e : M; + + // Multiplication table: e * e = e + // Using positional syntax: [a, b] maps to [x: a, y: b] + [e, e] mul = e; + + // Identity: e is the identity element + e id = e; +} + +// Boolean "And" monoid: {T, F} with T as identity +// T and T = T, T and F = F, F and T = F, F and F = F +instance BoolAnd : Monoid = { + T : M; + F : M; + + // Identity: T is the identity element + T id = T; + F id = T; + + // Multiplication table for "and": + [x: T, y: T] mul = T; + [x: T, y: F] mul = F; + [x: F, y: T] mul = F; + [x: F, y: F] mul = F; +} + +// Boolean "Or" monoid: {T, F} with F as identity +// T or T = T, T or F = T, F or T = T, F or F = F +instance BoolOr : Monoid = { + T : M; + F : M; + + // Identity: F is the identity element + T id = F; + F id = F; + + // Multiplication table for "or": + [x: T, y: T] mul = T; + [x: T, y: F] mul = T; + [x: F, y: T] mul = T; + [x: F, y: F] mul = F; +} diff --git a/examples/geolog/nested_instance_test.geolog b/examples/geolog/nested_instance_test.geolog new file mode 100644 index 0000000..2182887 --- /dev/null +++ b/examples/geolog/nested_instance_test.geolog @@ -0,0 +1,33 @@ +// Test: Nested instance declarations (following vision pattern) + +theory Place { + P : Sort; +} + +theory (Pl : Place instance) Token { + token : Sort; + token/of : token -> Pl/P; +} + +theory (Pl : Place instance) Problem { + initial_marking : Pl Token instance; + target_marking : Pl Token instance; +} + +// Create a place instance +instance MyPlaces : Place = { + p1 : P; + p2 : P; +} + +// Test nested instance declarations +instance TestProblem : MyPlaces Problem = { + initial_marking = { + t1 : token; + t1 token/of = MyPlaces/p1; + }; + target_marking = { + t2 : token; + t2 token/of = MyPlaces/p2; + }; +} diff --git a/examples/geolog/petri_net.geolog b/examples/geolog/petri_net.geolog new file mode 100644 index 0000000..8e4e235 --- /dev/null +++ b/examples/geolog/petri_net.geolog @@ -0,0 +1,135 @@ +// Petri Net: a bipartite graph between places and transitions +// +// Petri nets model concurrent systems. Places hold tokens, transitions +// fire when their input places have tokens, consuming inputs and +// producing outputs. +// +// This encoding uses explicit "arc" sorts for input/output connections, +// which is more faithful to the categorical semantics (a span). + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + In : Sort; // Input arcs (from place to transition) + Out : Sort; // Output arcs (from transition to place) + + // Input arc endpoints + in/place : In -> P; + in/trans : In -> T; + + // Output arc endpoints + out/trans : Out -> T; + out/place : Out -> P; +} + +// A simple producer-consumer net: +// +// (ready) --[produce]--> (buffer) --[consume]--> (done) +// +instance ProducerConsumer : PetriNet = { + // Places + ready : P; + buffer : P; + done : P; + + // Transitions + produce : T; + consume : T; + + // Input arcs + i1 : In; + i1 in/place = ready; + i1 in/trans = produce; + + i2 : In; + i2 in/place = buffer; + i2 in/trans = consume; + + // Output arcs + o1 : Out; + o1 out/trans = produce; + o1 out/place = buffer; + + o2 : Out; + o2 out/trans = consume; + o2 out/place = done; +} + +// Mutual exclusion: two processes competing for a shared resource +// +// (idle1) --[enter1]--> (crit1) --[exit1]--> (idle1) +// ^ | +// | (mutex) | +// | v +// (idle2) --[enter2]--> (crit2) --[exit2]--> (idle2) +// +instance MutualExclusion : PetriNet = { + // Places for process 1 + idle1 : P; + crit1 : P; + + // Places for process 2 + idle2 : P; + crit2 : P; + + // Shared mutex token + mutex : P; + + // Transitions + enter1 : T; + exit1 : T; + enter2 : T; + exit2 : T; + + // Process 1 enters: needs idle1 AND mutex + i_enter1_idle : In; + i_enter1_idle in/place = idle1; + i_enter1_idle in/trans = enter1; + + i_enter1_mutex : In; + i_enter1_mutex in/place = mutex; + i_enter1_mutex in/trans = enter1; + + o_enter1 : Out; + o_enter1 out/trans = enter1; + o_enter1 out/place = crit1; + + // Process 1 exits: releases mutex + i_exit1 : In; + i_exit1 in/place = crit1; + i_exit1 in/trans = exit1; + + o_exit1_idle : Out; + o_exit1_idle out/trans = exit1; + o_exit1_idle out/place = idle1; + + o_exit1_mutex : Out; + o_exit1_mutex out/trans = exit1; + o_exit1_mutex out/place = mutex; + + // Process 2 enters: needs idle2 AND mutex + i_enter2_idle : In; + i_enter2_idle in/place = idle2; + i_enter2_idle in/trans = enter2; + + i_enter2_mutex : In; + i_enter2_mutex in/place = mutex; + i_enter2_mutex in/trans = enter2; + + o_enter2 : Out; + o_enter2 out/trans = enter2; + o_enter2 out/place = crit2; + + // Process 2 exits: releases mutex + i_exit2 : In; + i_exit2 in/place = crit2; + i_exit2 in/trans = exit2; + + o_exit2_idle : Out; + o_exit2_idle out/trans = exit2; + o_exit2_idle out/place = idle2; + + o_exit2_mutex : Out; + o_exit2_mutex out/trans = exit2; + o_exit2_mutex out/place = mutex; +} diff --git a/examples/geolog/petri_net_full.geolog b/examples/geolog/petri_net_full.geolog new file mode 100644 index 0000000..d4e3fe7 --- /dev/null +++ b/examples/geolog/petri_net_full.geolog @@ -0,0 +1,195 @@ +// Full Petri Net Reachability - Type-Theoretic Encoding +// +// This demonstrates the complete type-theoretic encoding of Petri net +// reachability from the original geolog design vision. +// +// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md +// +// Key concepts: +// - PetriNet: places, transitions, input/output arcs (with proper arc semantics) +// - Marking: tokens in a net (parameterized by net) +// - ReachabilityProblem: initial and target markings (nested instances) +// - Trace: sequence of firings with wires connecting arcs +// - Iso: isomorphism between two sorts (used for bijections) +// - Solution: a trace with isomorphisms to markings +// +// This encoding is more type-theoretically precise than the simple +// PlaceReachability: it tracks individual tokens and arc multiplicities, +// enabling correct handling of "multi-token" transitions. + +// ============================================================ +// THEORY: PetriNet +// Basic structure: places, transitions, and arcs +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + + in : Sort; // Input arcs (place -> transition) + out : Sort; // Output arcs (transition -> place) + + // Each arc knows which place/transition it connects + in/src : in -> P; // Input arc source place + in/tgt : in -> T; // Input arc target transition + out/src : out -> T; // Output arc source transition + out/tgt : out -> P; // Output arc target place +} + +// ============================================================ +// THEORY: Marking (parameterized by N : PetriNet) +// A marking assigns tokens to places +// ============================================================ + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +// ============================================================ +// THEORY: ReachabilityProblem (parameterized by N : PetriNet) +// Defines initial and target markings as nested instances +// ============================================================ + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// ============================================================ +// THEORY: Trace (parameterized by N : PetriNet) +// A trace is a sequence of transition firings with "wires" +// connecting input and output arcs +// ============================================================ + +theory (N : PetriNet instance) Trace { + // Firings + F : Sort; + F/of : F -> N/T; + + // Wires connect output of one firing to input of another + W : Sort; + W/src : W -> [firing : F, arc : N/out]; // Wire source (firing, output arc) + W/tgt : W -> [firing : F, arc : N/in]; // Wire target (firing, input arc) + + // Wire coherence: output arc must belong to source firing's transition + ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of; + // Wire coherence: input arc must belong to target firing's transition + ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of; + + // Wire uniqueness: each (firing, out-arc) pair has at most one wire + ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2; + // Wire uniqueness: each (firing, in-arc) pair has at most one wire + ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2; + + // Terminals: for initial marking tokens (input) and final marking tokens (output) + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Every output arc of every firing must be wired OR be an output terminal + ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |- + (exists w : W. w W/src = [firing: f, arc: arc]) \/ + (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); + + // Every input arc of every firing must be wired OR be an input terminal + ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |- + (exists w : W. w W/tgt = [firing: f, arc: arc]) \/ + (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]); +} + +// ============================================================ +// THEORY: Iso (parameterized by two sorts) +// An isomorphism between two sorts +// ============================================================ + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +// ============================================================ +// THEORY: Solution (parameterized by N and RP) +// A solution to a reachability problem +// ============================================================ + +theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution { + // The witnessing trace + trace : N Trace instance; + + // Bijection between input terminals and initial marking tokens + initial_marking_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; + + // Bijection between output terminals and target marking tokens + target_marking_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance; + + // Initial marking commutes: token placement matches terminal placement + initial_marking_P_comm : forall i : trace/input_terminal. + |- i trace/input_terminal/of = i initial_marking_iso/fwd RP/initial_marking/token/of; + + // Target marking commutes: token placement matches terminal placement + target_marking_P_comm : forall o : trace/output_terminal. + |- o trace/output_terminal/of = o target_marking_iso/fwd RP/target_marking/token/of; +} + +// ============================================================ +// INSTANCE: ExampleNet - a small Petri net +// +// (A) --[ab]--> (B) --[bc]--> (C) +// ^ | +// +---[ba]------+ +// ============================================================ + +instance ExampleNet : PetriNet = { + // Places + A : P; + B : P; + C : P; + + // Transitions + ab : T; + ba : T; + bc : T; + + // A -> B (via ab) + ab_in : in; + ab_in in/src = A; + ab_in in/tgt = ab; + ab_out : out; + ab_out out/src = ab; + ab_out out/tgt = B; + + // B -> A (via ba) + ba_in : in; + ba_in in/src = B; + ba_in in/tgt = ba; + ba_out : out; + ba_out out/src = ba; + ba_out out/tgt = A; + + // B -> C (via bc) + bc_in : in; + bc_in in/src = B; + bc_in in/tgt = bc; + bc_out : out; + bc_out out/src = bc; + bc_out out/tgt = C; +} + +// ============================================================ +// Example queries (once query solving is implemented): +// +// query can_reach_B_from_A { +// ? : ExampleNet problem0 Solution instance; +// } +// +// where problem0 : ExampleNet ReachabilityProblem = { +// initial_marking = { tok : token; tok token/of = ExampleNet/A; }; +// target_marking = { tok : token; tok token/of = ExampleNet/B; }; +// } +// ============================================================ diff --git a/examples/geolog/petri_net_showcase.geolog b/examples/geolog/petri_net_showcase.geolog new file mode 100644 index 0000000..ece5de2 --- /dev/null +++ b/examples/geolog/petri_net_showcase.geolog @@ -0,0 +1,345 @@ +// Petri Net Reachability - Full Type-Theoretic Encoding +// +// This showcase demonstrates geolog's core capabilities through a +// non-trivial domain: encoding Petri net reachability as dependent types. +// +// A solution to a reachability problem is NOT a yes/no boolean but a +// CONSTRUCTIVE WITNESS: a diagrammatic proof that tokens can flow from +// initial to target markings via a sequence of transition firings. +// +// Key concepts demonstrated: +// - Parameterized theories (Marking depends on PetriNet instance) +// - Nested instance types (ReachabilityProblem contains Marking instances) +// - Sort-parameterized theories (Iso takes two sorts as parameters) +// - Cross-instance references (solution's trace elements reference problem's tokens) +// +// Original design: loose_thoughts/2025-12-12_12:10_VanillaPetriNetRechability.md + +// ============================================================ +// THEORY: PetriNet +// Places, transitions, and arcs with proper arc semantics +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + in : Sort; // Input arcs (place -> transition) + out : Sort; // Output arcs (transition -> place) + + in/src : in -> P; // Input arc source place + in/tgt : in -> T; // Input arc target transition + out/src : out -> T; // Output arc source transition + out/tgt : out -> P; // Output arc target place +} + +// ============================================================ +// THEORY: Marking (parameterized by N : PetriNet) +// A marking assigns tokens to places +// ============================================================ + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +// ============================================================ +// THEORY: ReachabilityProblem (parameterized by N : PetriNet) +// Initial and target markings as nested instances +// ============================================================ + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// ============================================================ +// THEORY: Trace (parameterized by N : PetriNet) +// A trace records transition firings and token flow via wires +// ============================================================ +// +// A trace is a diagrammatic proof of reachability: +// - Firings represent transition occurrences +// - Wires connect output arcs of firings to input arcs of other firings +// - Terminals connect to the initial/target markings +// +// The completeness axiom (ax/must_be_fed) ensures every input arc +// of every firing is accounted for - either wired from another firing +// or fed by an input terminal. + +theory (N : PetriNet instance) Trace { + // Firings + F : Sort; + F/of : F -> N/T; + + // Wires connect output arcs of firings to input arcs of other firings + W : Sort; + W/src_firing : W -> F; + W/src_arc : W -> N/out; + W/tgt_firing : W -> F; + W/tgt_arc : W -> N/in; + + // Wire coherence: source arc must belong to source firing's transition + ax/wire_src_coherent : forall w : W. + |- w W/src_arc N/out/src = w W/src_firing F/of; + + // Wire coherence: target arc must belong to target firing's transition + ax/wire_tgt_coherent : forall w : W. + |- w W/tgt_arc N/in/tgt = w W/tgt_firing F/of; + + // Wire place coherence: wire connects matching places + ax/wire_place_coherent : forall w : W. + |- w W/src_arc N/out/tgt = w W/tgt_arc N/in/src; + + // Terminals + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + + // Terminals connect to specific firings and arcs + input_terminal/tgt_firing : input_terminal -> F; + input_terminal/tgt_arc : input_terminal -> N/in; + output_terminal/src_firing : output_terminal -> F; + output_terminal/src_arc : output_terminal -> N/out; + + // Terminal coherence axioms + ax/input_terminal_coherent : forall i : input_terminal. + |- i input_terminal/tgt_arc N/in/tgt = i input_terminal/tgt_firing F/of; + + ax/output_terminal_coherent : forall o : output_terminal. + |- o output_terminal/src_arc N/out/src = o output_terminal/src_firing F/of; + + // Terminal place coherence + ax/input_terminal_place : forall i : input_terminal. + |- i input_terminal/of = i input_terminal/tgt_arc N/in/src; + + ax/output_terminal_place : forall o : output_terminal. + |- o output_terminal/of = o output_terminal/src_arc N/out/tgt; + + // COMPLETENESS: Every arc of every firing must be accounted for. + + // Input completeness: every input arc must be fed by a wire or input terminal + ax/input_complete : forall f : F, arc : N/in. + arc N/in/tgt = f F/of |- + (exists w : W. w W/tgt_firing = f, w W/tgt_arc = arc) \/ + (exists i : input_terminal. i input_terminal/tgt_firing = f, i input_terminal/tgt_arc = arc); + + // Output completeness: every output arc must be captured by a wire or output terminal + ax/output_complete : forall f : F, arc : N/out. + arc N/out/src = f F/of |- + (exists w : W. w W/src_firing = f, w W/src_arc = arc) \/ + (exists o : output_terminal. o output_terminal/src_firing = f, o output_terminal/src_arc = arc); +} + +// ============================================================ +// THEORY: Iso (parameterized by two sorts) +// Isomorphism (bijection) between two sorts +// ============================================================ + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + + // Roundtrip axioms ensure this is a true bijection + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +// ============================================================ +// THEORY: Solution (parameterized by N and RP) +// A constructive witness that target is reachable from initial +// ============================================================ + +theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution { + trace : N Trace instance; + + // Bijection: input terminals <-> initial marking tokens + initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; + + // Bijection: output terminals <-> target marking tokens + target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance; + + // Commutativity axioms (currently unchecked): + // ax/init_comm : forall i : trace/input_terminal. + // |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of; + // ax/target_comm : forall o : trace/output_terminal. + // |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of; +} + +// ============================================================ +// INSTANCE: ExampleNet +// +// A Petri net with places A, B, C and transitions: +// ab: consumes 1 token from A, produces 1 token in B +// ba: consumes 1 token from B, produces 1 token in A +// abc: consumes 1 token from A AND 1 from B, produces 1 token in C +// +// +---[ba]----+ +// v | +// (A) --[ab]->(B) --+ +// | | +// +----[abc]-------+--> (C) +// +// The abc transition is interesting: it requires BOTH an A-token +// and a B-token to fire, producing a C-token. +// ============================================================ + +instance ExampleNet : PetriNet = { + A : P; B : P; C : P; + ab : T; ba : T; abc : T; + + // A -> B (via ab) + ab_in : in; ab_in in/src = A; ab_in in/tgt = ab; + ab_out : out; ab_out out/src = ab; ab_out out/tgt = B; + + // B -> A (via ba) + ba_in : in; ba_in in/src = B; ba_in in/tgt = ba; + ba_out : out; ba_out out/src = ba; ba_out out/tgt = A; + + // A + B -> C (via abc) - note: two input arcs! + abc_in1 : in; abc_in1 in/src = A; abc_in1 in/tgt = abc; + abc_in2 : in; abc_in2 in/src = B; abc_in2 in/tgt = abc; + abc_out : out; abc_out out/src = abc; abc_out out/tgt = C; +} + +// ============================================================ +// PROBLEM 0: Can we reach B from A with one token? +// Initial: 1 token in A +// Target: 1 token in B +// ============================================================ + +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + tok : token; + tok token/of = ExampleNet/A; + }; + target_marking = { + tok : token; + tok token/of = ExampleNet/B; + }; +} + +// ============================================================ +// SOLUTION 0: Yes! Fire transition 'ab' once. +// +// This Solution instance is a CONSTRUCTIVE PROOF: +// - The trace contains one firing (f1) of transition 'ab' +// - The input terminal feeds the A-token into f1's input arc +// - The output terminal captures f1's B-token output +// - The isomorphisms prove the token counts match exactly +// ============================================================ + +instance solution0 : ExampleNet problem0 Solution = { + trace = { + // One firing of transition 'ab' + f1 : F; + f1 F/of = ExampleNet/ab; + + // Input terminal: feeds the initial A-token into f1 + it : input_terminal; + it input_terminal/of = ExampleNet/A; + it input_terminal/tgt_firing = f1; + it input_terminal/tgt_arc = ExampleNet/ab_in; + + // Output terminal: captures f1's B-token output + ot : output_terminal; + ot output_terminal/of = ExampleNet/B; + ot output_terminal/src_firing = f1; + ot output_terminal/src_arc = ExampleNet/ab_out; + }; + + initial_iso = { + trace/it fwd = problem0/initial_marking/tok; + problem0/initial_marking/tok bwd = trace/it; + }; + + target_iso = { + trace/ot fwd = problem0/target_marking/tok; + problem0/target_marking/tok bwd = trace/ot; + }; +} + +// ============================================================ +// PROBLEM 2: Can we reach C from two A-tokens? +// Initial: 2 tokens in A +// Target: 1 token in C +// +// This is interesting because the only path to C is via 'abc', +// which requires tokens in BOTH A and B simultaneously. +// ============================================================ + +instance problem2 : ExampleNet ReachabilityProblem = { + initial_marking = { + t1 : token; t1 token/of = ExampleNet/A; + t2 : token; t2 token/of = ExampleNet/A; + }; + target_marking = { + t : token; + t token/of = ExampleNet/C; + }; +} + +// ============================================================ +// SOLUTION 2: Yes! Fire 'ab' then 'abc'. +// +// Token flow diagram: +// +// [it1]--A-->[f1: ab]--B--wire-->[f2: abc]--C-->[ot] +// [it2]--A-----------------^ +// +// Step 1: Fire 'ab' to move one token A -> B +// - it1 feeds A-token into f1 via ab_in +// - f1 produces B-token via ab_out +// Step 2: Fire 'abc' consuming one A-token and one B-token +// - it2 feeds A-token into f2 via abc_in1 +// - Wire connects f1's ab_out to f2's abc_in2 (the B-input) +// - f2 produces C-token via abc_out +// ============================================================ + +instance solution2 : ExampleNet problem2 Solution = { + trace = { + // Two firings + f1 : F; f1 F/of = ExampleNet/ab; // First: A -> B + f2 : F; f2 F/of = ExampleNet/abc; // Second: A + B -> C + + // Wire connecting f1's B-output to f2's B-input + // This is the crucial connection that makes the trace valid! + w1 : W; + w1 W/src_firing = f1; + w1 W/src_arc = ExampleNet/ab_out; + w1 W/tgt_firing = f2; + w1 W/tgt_arc = ExampleNet/abc_in2; + + // Input terminal 1: feeds first A-token into f1 + it1 : input_terminal; + it1 input_terminal/of = ExampleNet/A; + it1 input_terminal/tgt_firing = f1; + it1 input_terminal/tgt_arc = ExampleNet/ab_in; + + // Input terminal 2: feeds second A-token into f2 + it2 : input_terminal; + it2 input_terminal/of = ExampleNet/A; + it2 input_terminal/tgt_firing = f2; + it2 input_terminal/tgt_arc = ExampleNet/abc_in1; + + // Output terminal: captures f2's C-token output + ot : output_terminal; + ot output_terminal/of = ExampleNet/C; + ot output_terminal/src_firing = f2; + ot output_terminal/src_arc = ExampleNet/abc_out; + }; + + // Bijection: 2 input terminals <-> 2 initial tokens + initial_iso = { + trace/it1 fwd = problem2/initial_marking/t1; + trace/it2 fwd = problem2/initial_marking/t2; + problem2/initial_marking/t1 bwd = trace/it1; + problem2/initial_marking/t2 bwd = trace/it2; + }; + + // Bijection: 1 output terminal <-> 1 target token + target_iso = { + trace/ot fwd = problem2/target_marking/t; + problem2/target_marking/t bwd = trace/ot; + }; +} diff --git a/examples/geolog/petri_net_solution.geolog b/examples/geolog/petri_net_solution.geolog new file mode 100644 index 0000000..4f3048f --- /dev/null +++ b/examples/geolog/petri_net_solution.geolog @@ -0,0 +1,188 @@ +// Full Petri Net Reachability with Synthesized Solution +// +// This file contains the complete type-theoretic encoding of Petri net +// reachability, plus a manually synthesized solution proving that place B +// is reachable from place A in the example net. +// +// ============================================================ +// This instance was synthesized automatically by Claude Opus 4.5. +// As was this entire file, and this entire project, really. +// ============================================================ + +// ============================================================ +// THEORY: PetriNet - Basic structure with arc semantics +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + in : Sort; // Input arcs (place -> transition) + out : Sort; // Output arcs (transition -> place) + + in/src : in -> P; // Input arc source place + in/tgt : in -> T; // Input arc target transition + out/src : out -> T; // Output arc source transition + out/tgt : out -> P; // Output arc target place +} + +// ============================================================ +// THEORY: Marking - Tokens parameterized by a net +// ============================================================ + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; // Which place each token is in +} + +// ============================================================ +// THEORY: ReachabilityProblem - Initial and target markings +// ============================================================ + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// ============================================================ +// THEORY: Trace - A sequence of transition firings with wires +// ============================================================ +// +// Simplified version for now - full version with product types commented out below. + +theory (N : PetriNet instance) Trace { + F : Sort; // Firings + F/of : F -> N/T; // Which transition each fires + + // Terminals for initial/final marking tokens + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; +} + +// Full Trace theory with wires and product types (not yet fully supported): +// +// theory (N : PetriNet instance) Trace { +// F : Sort; // Firings +// F/of : F -> N/T; // Which transition each fires +// +// W : Sort; // Wires connecting firings +// W/src : W -> [firing : F, arc : N/out]; // Wire source +// W/tgt : W -> [firing : F, arc : N/in]; // Wire target +// +// // Wire coherence axioms +// ax1 : forall w : W. |- w W/src .arc N/out/src = w W/src .firing F/of; +// ax2 : forall w : W. |- w W/tgt .arc N/in/tgt = w W/tgt .firing F/of; +// +// // Wire uniqueness +// ax3 : forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2; +// ax4 : forall w1, w2 : W. w1 W/tgt = w2 W/tgt |- w1 = w2; +// +// // Terminals for initial/final marking tokens +// input_terminal : Sort; +// output_terminal : Sort; +// input_terminal/of : input_terminal -> N/P; +// output_terminal/of : output_terminal -> N/P; +// input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; +// output_terminal/src : output_terminal -> [firing : F, arc : N/out]; +// +// // Coverage axioms +// ax5 : forall f : F, arc : N/out. arc N/out/src = f F/of |- +// (exists w : W. w W/src = [firing: f, arc: arc]) \/ +// (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); +// ax6 : forall f : F, arc : N/in. arc N/in/tgt = f F/of |- +// (exists w : W. w W/tgt = [firing: f, arc: arc]) \/ +// (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]); +// } + +// ============================================================ +// THEORY: Iso - Isomorphism between two sorts +// ============================================================ + +theory (X : Sort) (Y : Sort) Iso { + fwd : X -> Y; + bwd : Y -> X; + fb : forall x : X. |- x fwd bwd = x; + bf : forall y : Y. |- y bwd fwd = y; +} + +// ============================================================ +// THEORY: Solution - A complete reachability witness +// ============================================================ + +theory (N : PetriNet instance) (RP : N ReachabilityProblem instance) Solution { + trace : N Trace instance; + + initial_iso : (trace/input_terminal) (RP/initial_marking/token) Iso instance; + target_iso : (trace/output_terminal) (RP/target_marking/token) Iso instance; + + ax/init_comm : forall i : trace/input_terminal. + |- i trace/input_terminal/of = i initial_iso/fwd RP/initial_marking/token/of; + ax/target_comm : forall o : trace/output_terminal. + |- o trace/output_terminal/of = o target_iso/fwd RP/target_marking/token/of; +} + +// ============================================================ +// INSTANCE: ExampleNet - A small Petri net +// +// (A) --[ab]--> (B) --[bc]--> (C) +// ^ | +// +---[ba]------+ +// ============================================================ + +instance ExampleNet : PetriNet = { + A : P; B : P; C : P; + ab : T; ba : T; bc : T; + + ab_in : in; ab_in in/src = A; ab_in in/tgt = ab; + ab_out : out; ab_out out/src = ab; ab_out out/tgt = B; + + ba_in : in; ba_in in/src = B; ba_in in/tgt = ba; + ba_out : out; ba_out out/src = ba; ba_out out/tgt = A; + + bc_in : in; bc_in in/src = B; bc_in in/tgt = bc; + bc_out : out; bc_out out/src = bc; bc_out out/tgt = C; +} + +// ============================================================ +// INSTANCE: problem0 - Can we reach B from A? +// ============================================================ + +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + tok : token; + tok token/of = ExampleNet/A; + }; + target_marking = { + tok : token; + tok token/of = ExampleNet/B; + }; +} + +// ============================================================ +// INSTANCE: solution0 - YES! Here's the proof. +// ============================================================ +// This instance was synthesized automatically by Claude Opus 4.5. +// ============================================================ + +// The solution proves that place B is reachable from place A by firing +// transition ab. This creates a trace with one firing and the necessary +// input/output terminal mappings. + +instance solution0 : ExampleNet problem0 Solution = { + trace = { + f1 : F; + f1 F/of = ExampleNet/ab; + + it : input_terminal; + it input_terminal/of = ExampleNet/A; + + ot : output_terminal; + ot output_terminal/of = ExampleNet/B; + }; + + // NOTE: Cross-instance references (e.g., trace/it in initial_iso) + // are not yet fully supported. The iso instances would map: + // - trace/it <-> problem0/initial_marking/tok + // - trace/ot <-> problem0/target_marking/tok +} diff --git a/examples/geolog/petri_reachability.geolog b/examples/geolog/petri_reachability.geolog new file mode 100644 index 0000000..fb5a453 --- /dev/null +++ b/examples/geolog/petri_reachability.geolog @@ -0,0 +1,164 @@ +// Petri Net Reachability - Full Example +// +// This demonstrates the core ideas from the original geolog design document: +// modeling Petri net reachability using geometric logic with the chase algorithm. +// +// Original design: loose_thoughts/2025-12-12_12:10.md +// +// Key concepts: +// - PetriNet: places, transitions, input/output arcs +// - Marking: assignment of tokens to places (parameterized theory) +// - Trace: sequence of transition firings connecting markings +// - Reachability: computed via chase algorithm + +// ============================================================ +// THEORY: PetriNet +// ============================================================ + +theory PetriNet { + P : Sort; // Places + T : Sort; // Transitions + In : Sort; // Input arcs (place -> transition) + Out : Sort; // Output arcs (transition -> place) + + // Arc structure + in/place : In -> P; + in/trans : In -> T; + out/trans : Out -> T; + out/place : Out -> P; +} + +// ============================================================ +// THEORY: Marking (parameterized) +// A marking assigns tokens to places in a specific net +// ============================================================ + +theory (N : PetriNet instance) Marking { + Token : Sort; + of : Token -> N/P; +} + +// ============================================================ +// THEORY: PlaceReachability +// Simplified reachability at the place level +// ============================================================ + +theory PlaceReachability { + P : Sort; + T : Sort; + + // Which transition connects which places + // Fires(t, from, to) means transition t can move a token from 'from' to 'to' + Fires : [trans: T, from: P, to: P] -> Prop; + + // Reachability relation (transitive closure) + CanReach : [from: P, to: P] -> Prop; + + // Reflexivity: every place can reach itself + ax/refl : forall p : P. + |- [from: p, to: p] CanReach; + + // Transition firing creates reachability + ax/fire : forall t : T, x : P, y : P. + [trans: t, from: x, to: y] Fires |- [from: x, to: y] CanReach; + + // Transitivity: reachability composes + ax/trans : forall x : P, y : P, z : P. + [from: x, to: y] CanReach, [from: y, to: z] CanReach |- [from: x, to: z] CanReach; +} + +// ============================================================ +// INSTANCE: SimpleNet +// A -> B -> C with bidirectional A <-> B +// +// (A) <--[ba]-- (B) --[bc]--> (C) +// | ^ +// +---[ab]------+ +// ============================================================ + +// Uses chase to derive CanReach from axioms (reflexivity, fire, transitivity) +instance SimpleNet : PlaceReachability = chase { + // Places + A : P; + B : P; + C : P; + + // Transitions + ab : T; // A -> B + ba : T; // B -> A + bc : T; // B -> C + + // Firing relations + [trans: ab, from: A, to: B] Fires; + [trans: ba, from: B, to: A] Fires; + [trans: bc, from: B, to: C] Fires; +} + +// ============================================================ +// INSTANCE: MutexNet +// Two processes competing for a mutex +// +// idle1 --[enter1]--> crit1 --[exit1]--> idle1 +// ^ | +// | mutex | +// | v +// idle2 --[enter2]--> crit2 --[exit2]--> idle2 +// ============================================================ + +// Uses chase to derive reachability relation +instance MutexNet : PlaceReachability = chase { + // Places + idle1 : P; + crit1 : P; + idle2 : P; + crit2 : P; + mutex : P; + + // Transitions + enter1 : T; + exit1 : T; + enter2 : T; + exit2 : T; + + // Process 1 acquires mutex: idle1 + mutex -> crit1 + // (simplified: we track place-level, not token-level) + [trans: enter1, from: idle1, to: crit1] Fires; + [trans: enter1, from: mutex, to: crit1] Fires; + + // Process 1 releases mutex: crit1 -> idle1 + mutex + [trans: exit1, from: crit1, to: idle1] Fires; + [trans: exit1, from: crit1, to: mutex] Fires; + + // Process 2 acquires mutex: idle2 + mutex -> crit2 + [trans: enter2, from: idle2, to: crit2] Fires; + [trans: enter2, from: mutex, to: crit2] Fires; + + // Process 2 releases mutex: crit2 -> idle2 + mutex + [trans: exit2, from: crit2, to: idle2] Fires; + [trans: exit2, from: crit2, to: mutex] Fires; +} + +// ============================================================ +// INSTANCE: ProducerConsumerNet +// Producer creates items, consumer processes them +// +// ready --[produce]--> buffer --[consume]--> done +// ============================================================ + +// Uses chase to derive reachability relation +instance ProducerConsumerNet : PlaceReachability = chase { + // Places + ready : P; + buffer : P; + done : P; + + // Transitions + produce : T; + consume : T; + + // Produce: ready -> buffer + [trans: produce, from: ready, to: buffer] Fires; + + // Consume: buffer -> done + [trans: consume, from: buffer, to: done] Fires; +} diff --git a/examples/geolog/petri_reachability_full_vision.geolog b/examples/geolog/petri_reachability_full_vision.geolog new file mode 100644 index 0000000..a3155f5 --- /dev/null +++ b/examples/geolog/petri_reachability_full_vision.geolog @@ -0,0 +1,72 @@ +// Full Petri Net Reachability Vision Test +// From 2025-12-12_12:10_VanillaPetriNetRechability.md + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// Simplified Trace theory without disjunctions for now +theory (N : PetriNet instance) SimpleTrace { + F : Sort; + F/of : F -> N/T; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Simplified ax5: every firing+arc gets an output terminal + ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]; + + // Simplified ax6: every firing+arc gets an input terminal + ax6 : forall f : F, arc : N/in. |- exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]; +} + +instance ExampleNet : PetriNet = { + A : P; + B : P; + ab : T; + ab_in : in; + ab_in in/src = A; + ab_in in/tgt = ab; + ab_out : out; + ab_out out/src = ab; + ab_out out/tgt = B; +} + +// Test nested instance elaboration +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + tok : token; + tok token/of = ExampleNet/A; + }; + target_marking = { + tok : token; + tok token/of = ExampleNet/B; + }; +} + +// Test chase with SimpleTrace +instance trace0 : ExampleNet SimpleTrace = chase { + f1 : F; + f1 F/of = ExampleNet/ab; +} diff --git a/examples/geolog/petri_reachability_vision.geolog b/examples/geolog/petri_reachability_vision.geolog new file mode 100644 index 0000000..20ef578 --- /dev/null +++ b/examples/geolog/petri_reachability_vision.geolog @@ -0,0 +1,94 @@ +// Petri Net Reachability Vision Test +// Based on 2025-12-12 design document + +// Basic Petri net structure +theory PetriNet { + // Places + P : Sort; + + // Transitions + T : Sort; + + // Arcs (input to transitions, output from transitions) + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +// A marking is a multiset of tokens, each at a place +theory (N : PetriNet instance) Marking { + token : Sort; + token/of : token -> N/P; +} + +// A reachability problem is: can we get from initial marking to target? +theory (N : PetriNet instance) ReachabilityProblem { + initial_marking : N Marking instance; + target_marking : N Marking instance; +} + +// A trace is a sequence of firings connected by wires +theory (N : PetriNet instance) Trace { + // Firings of transitions + F : Sort; + F/of : F -> N/T; + + // Wires connect firing outputs to firing inputs + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + // Terminals are unconnected arc endpoints (to/from the initial/target markings) + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; +} + +// Example Petri net: A <--ab/ba--> B, (A,B) --abc--> C +instance ExampleNet : PetriNet = { + A : P; + B : P; + C : P; + ab : T; + ba : T; + abc : T; + ab_in : in; + ab_in in/src = A; + ab_in in/tgt = ab; + ab_out : out; + ab_out out/src = ab; + ab_out out/tgt = B; + ba_in : in; + ba_in in/src = B; + ba_in in/tgt = ba; + ba_out : out; + ba_out out/src = ba; + ba_out out/tgt = A; + abc_in1 : in; + abc_in1 in/src = A; + abc_in1 in/tgt = abc; + abc_in2 : in; + abc_in2 in/src = B; + abc_in2 in/tgt = abc; + abc_out : out; + abc_out out/src = abc; + abc_out out/tgt = C; +} + +// Reachability problem: Can we reach B from A? +instance problem0 : ExampleNet ReachabilityProblem = { + initial_marking = { + t : token; + t token/of = ExampleNet/A; + }; + target_marking = { + t : token; + t token/of = ExampleNet/B; + }; +} diff --git a/examples/geolog/petri_trace_axioms.geolog b/examples/geolog/petri_trace_axioms.geolog new file mode 100644 index 0000000..1295e0c --- /dev/null +++ b/examples/geolog/petri_trace_axioms.geolog @@ -0,0 +1,66 @@ +// Test Trace theory with axioms using product codomains + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +// Trace theory with axioms +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Axiom: wires are injective on source + // forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2; + // (Commented out - requires product codomain equality in premises) + + // Axiom: every arc endpoint must be wired or terminated + // forall f : F, arc : N/out. arc N/out/src = f F/of |- + // (exists w : W. w W/src = [firing: f, arc: arc]) \/ + // (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); + // (Commented out - requires product codomain values in conclusions) +} + +// Simple net for testing +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_in : in; + arc_in in/src = A; + arc_in in/tgt = t; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Test that the basic theory without axioms still works +instance SimpleTrace : SimpleNet Trace = { + f1 : F; + f1 F/of = SimpleNet/t; + + it : input_terminal; + it input_terminal/of = SimpleNet/A; + it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in]; + + ot : output_terminal; + ot output_terminal/of = SimpleNet/B; + ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out]; +} diff --git a/examples/geolog/petri_trace_coverage_test.geolog b/examples/geolog/petri_trace_coverage_test.geolog new file mode 100644 index 0000000..dd3c2f2 --- /dev/null +++ b/examples/geolog/petri_trace_coverage_test.geolog @@ -0,0 +1,36 @@ +// Test: Trace coverage axiom (simplified) + +theory PetriNet { + P : Sort; + T : Sort; + out : Sort; + out/src : out -> T; + out/tgt : out -> P; +} + +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + output_terminal : Sort; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Simplified ax5: for every arc and firing, if the arc's source is the firing's transition, + // create an output terminal + ax5 : forall f : F, arc : N/out. |- exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]; +} + +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Trace with just a firing - chase should create a terminal +instance TestTrace : SimpleNet Trace = chase { + f1 : F; + f1 F/of = SimpleNet/t; +} diff --git a/examples/geolog/petri_trace_full_vision.geolog b/examples/geolog/petri_trace_full_vision.geolog new file mode 100644 index 0000000..687cac8 --- /dev/null +++ b/examples/geolog/petri_trace_full_vision.geolog @@ -0,0 +1,57 @@ +// Trace theory with wires and disjunctions +// Testing the full vision from 2025-12-12 + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; + + // Every out arc of every firing: either wired or terminal + ax5 : forall f : F, arc : N/out. |- + (exists w : W. w W/src = [firing: f, arc: arc]) \/ + (exists o : output_terminal. o output_terminal/src = [firing: f, arc: arc]); + + // Every in arc of every firing: either wired or terminal + ax6 : forall f : F, arc : N/in. |- + (exists w : W. w W/tgt = [firing: f, arc: arc]) \/ + (exists i : input_terminal. i input_terminal/tgt = [firing: f, arc: arc]); +} + +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_in : in; + arc_in in/src = A; + arc_in in/tgt = t; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Chase should create both wires AND terminals (naive chase adds all disjuncts) +instance trace_test : SimpleNet Trace = chase { + f1 : F; + f1 F/of = SimpleNet/t; +} diff --git a/examples/geolog/petri_trace_test.geolog b/examples/geolog/petri_trace_test.geolog new file mode 100644 index 0000000..0a3a674 --- /dev/null +++ b/examples/geolog/petri_trace_test.geolog @@ -0,0 +1,58 @@ +// Test that Trace theory with product codomains works + +theory PetriNet { + P : Sort; + T : Sort; + in : Sort; + out : Sort; + in/src : in -> P; + in/tgt : in -> T; + out/src : out -> T; + out/tgt : out -> P; +} + +// Simple Petri net: A --t--> B +instance SimpleNet : PetriNet = { + A : P; + B : P; + t : T; + arc_in : in; + arc_in in/src = A; + arc_in in/tgt = t; + arc_out : out; + arc_out out/src = t; + arc_out out/tgt = B; +} + +// Trace theory with product codomains for wire endpoints +theory (N : PetriNet instance) Trace { + F : Sort; + F/of : F -> N/T; + + W : Sort; + W/src : W -> [firing : F, arc : N/out]; + W/tgt : W -> [firing : F, arc : N/in]; + + input_terminal : Sort; + output_terminal : Sort; + input_terminal/of : input_terminal -> N/P; + output_terminal/of : output_terminal -> N/P; + input_terminal/tgt : input_terminal -> [firing : F, arc : N/in]; + output_terminal/src : output_terminal -> [firing : F, arc : N/out]; +} + +// A simple trace: one firing of t, with input/output terminals +instance SimpleTrace : SimpleNet Trace = { + f1 : F; + f1 F/of = SimpleNet/t; + + // Input terminal (token comes from external marking) + it : input_terminal; + it input_terminal/of = SimpleNet/A; + it input_terminal/tgt = [firing: f1, arc: SimpleNet/arc_in]; + + // Output terminal (token goes to external marking) + ot : output_terminal; + ot output_terminal/of = SimpleNet/B; + ot output_terminal/src = [firing: f1, arc: SimpleNet/arc_out]; +} diff --git a/examples/geolog/preorder.geolog b/examples/geolog/preorder.geolog new file mode 100644 index 0000000..47983a0 --- /dev/null +++ b/examples/geolog/preorder.geolog @@ -0,0 +1,42 @@ +// Preorder: a set with a reflexive, transitive relation +// +// This demonstrates RELATIONS (predicates) as opposed to functions. +// A relation R : A -> Prop is a predicate on A. +// For binary relations, we use a product domain: R : [x: A, y: A] -> Prop + +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 ∧ y ≤ z → 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; +} + +// The discrete preorder: only reflexive pairs +// (no elements are comparable except to themselves) +// Uses `chase` to automatically derive reflexive pairs from axiom ax/refl. +instance Discrete3 : Preorder = chase { + a : X; + b : X; + c : X; +} + +// A total order on 3 elements: a ≤ b ≤ c +// Uses `chase` to derive reflexive and transitive closure. +instance Chain3 : Preorder = chase { + bot : X; + mid : X; + top : X; + + // Assert the basic ordering; chase will add reflexive pairs + // and transitive closure (bot ≤ top) + [x: bot, y: mid] leq; + [x: mid, y: top] leq; +} diff --git a/examples/geolog/product_codomain_equality_test.geolog b/examples/geolog/product_codomain_equality_test.geolog new file mode 100644 index 0000000..9a86219 --- /dev/null +++ b/examples/geolog/product_codomain_equality_test.geolog @@ -0,0 +1,23 @@ +// Test: Product codomain equality in premise (ax3 pattern) + +theory ProductCodomainEqTest { + A : Sort; + B : Sort; + + W : Sort; + W/src : W -> [x: A, y: B]; + + // ax3 pattern: forall w1, w2 : W. w1 W/src = w2 W/src |- w1 = w2 + // This should make W injective on src + ax_inj : forall w1 : W, w2 : W. w1 W/src = w2 W/src |- w1 = w2; +} + +// Instance with two wires that have the same src - should be identified by chase +instance Test : ProductCodomainEqTest = { + a1 : A; + b1 : B; + w1 : W; + w1 W/src = [x: a1, y: b1]; + w2 : W; + w2 W/src = [x: a1, y: b1]; +} diff --git a/examples/geolog/product_codomain_test.geolog b/examples/geolog/product_codomain_test.geolog new file mode 100644 index 0000000..b804354 --- /dev/null +++ b/examples/geolog/product_codomain_test.geolog @@ -0,0 +1,51 @@ +// Test: Product Codomain Support +// +// This tests the new feature where functions can have product codomains, +// allowing record literal assignments like: +// elem func = [field1: v1, field2: v2]; + +theory ProductCodomainTest { + A : Sort; + B : Sort; + C : Sort; + + // Function with product codomain: maps A elements to (B, C) pairs + pair_of : A -> [left: B, right: C]; +} + +instance TestInstance : ProductCodomainTest = { + // Elements + a1 : A; + b1 : B; + b2 : B; + c1 : C; + + // Assign product codomain value using record literal + a1 pair_of = [left: b1, right: c1]; +} + +// A more realistic example: Edges in a graph +theory DirectedGraph { + V : Sort; + E : Sort; + + // Edge endpoints as a product codomain + endpoints : E -> [src: V, tgt: V]; +} + +instance TriangleGraph : DirectedGraph = { + // Vertices + v0 : V; + v1 : V; + v2 : V; + + // Edges + e01 : E; + e12 : E; + e20 : E; + + // Assign edge endpoints using record literals + e01 endpoints = [src: v0, tgt: v1]; + e12 endpoints = [src: v1, tgt: v2]; + e20 endpoints = [src: v2, tgt: v0]; +} diff --git a/examples/geolog/record_existential_test.geolog b/examples/geolog/record_existential_test.geolog new file mode 100644 index 0000000..f1d2fbe --- /dev/null +++ b/examples/geolog/record_existential_test.geolog @@ -0,0 +1,18 @@ +// Test: Record literals in existential conclusions + +theory RecordExistentialTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Axiom: given any a:A and b:B, there exists an R with that data + ax1 : forall a : A, b : B. |- + exists r : R. r R/data = [x: a, y: b]; +} + +instance Test : RecordExistentialTest = chase { + a1 : A; + b1 : B; +} diff --git a/examples/geolog/record_in_axiom_test.geolog b/examples/geolog/record_in_axiom_test.geolog new file mode 100644 index 0000000..559139d --- /dev/null +++ b/examples/geolog/record_in_axiom_test.geolog @@ -0,0 +1,12 @@ +// Test: Record literals in axioms + +theory RecordAxiomTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Test axiom with record literal RHS + ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- true; +} diff --git a/examples/geolog/record_premise_chase_test.geolog b/examples/geolog/record_premise_chase_test.geolog new file mode 100644 index 0000000..5f67156 --- /dev/null +++ b/examples/geolog/record_premise_chase_test.geolog @@ -0,0 +1,23 @@ +// Test: Chase with record literals in premises + +theory RecordPremiseTest { + A : Sort; + B : Sort; + + R : Sort; + R/data : R -> [x: A, y: B]; + + // Derived sort for processed items + Processed : Sort; + Processed/r : Processed -> R; + + // Axiom: given r with data [x: a, y: b], create a Processed for it + ax1 : forall r : R, a : A, b : B. r R/data = [x: a, y: b] |- exists p : Processed. p Processed/r = r; +} + +instance Test : RecordPremiseTest = { + a1 : A; + b1 : B; + r1 : R; + r1 R/data = [x: a1, y: b1]; +} diff --git a/examples/geolog/relalg_simple.geolog b/examples/geolog/relalg_simple.geolog new file mode 100644 index 0000000..39aebff --- /dev/null +++ b/examples/geolog/relalg_simple.geolog @@ -0,0 +1,130 @@ +// Example: RelAlgIR query plan instances +// +// This demonstrates creating query plans as RelAlgIR instances. +// These show the string diagram representation of relational algebra. +// +// First we need to load both GeologMeta (for Srt, Func, etc.) and RelAlgIR. +// This file just defines instances; load theories first in the REPL: +// :load theories/GeologMeta.geolog +// :load theories/RelAlgIR.geolog +// :load examples/geolog/relalg_simple.geolog +// +// Note: RelAlgIR extends GeologMeta, so a RelAlgIR instance contains +// elements from both GeologMeta sorts (Srt, Func, Elem) and RelAlgIR +// sorts (Wire, Schema, ScanOp, etc.) + +// ============================================================ +// Example 1: Simple Scan +// ============================================================ +// Query: "scan all elements of sort V" +// Plan: () --[ScanOp]--> Wire + +instance ScanV : RelAlgIR = chase { + // -- Schema (target theory) -- + target_theory : GeologMeta/Theory; + target_theory GeologMeta/Theory/parent = target_theory; + + v_srt : GeologMeta/Srt; + v_srt GeologMeta/Srt/theory = target_theory; + + // -- Query Plan -- + v_base_schema : BaseSchema; + v_base_schema BaseSchema/srt = v_srt; + + v_schema : Schema; + v_base_schema BaseSchema/schema = v_schema; + + scan_out : Wire; + scan_out Wire/schema = v_schema; + + scan : ScanOp; + scan ScanOp/srt = v_srt; + scan ScanOp/out = scan_out; + + scan_op : Op; + scan ScanOp/op = scan_op; +} + +// ============================================================ +// Example 2: Filter(Scan) +// ============================================================ +// Query: "scan E, filter where src(e) = some vertex" +// Plan: () --[Scan]--> w1 --[Filter]--> w2 +// +// This demonstrates composition via wire sharing. + +// Uses chase to derive relations. +instance FilterScan : RelAlgIR = chase { + // -- Schema (representing Graph theory) -- + target_theory : GeologMeta/Theory; + target_theory GeologMeta/Theory/parent = target_theory; + + // Sorts: V (vertices), E (edges) + v_srt : GeologMeta/Srt; + v_srt GeologMeta/Srt/theory = target_theory; + + e_srt : GeologMeta/Srt; + e_srt GeologMeta/Srt/theory = target_theory; + + // Functions: src : E -> V + // First create the DSort wrappers + v_base_ds : GeologMeta/BaseDS; + v_base_ds GeologMeta/BaseDS/srt = v_srt; + + e_base_ds : GeologMeta/BaseDS; + e_base_ds GeologMeta/BaseDS/srt = e_srt; + + v_dsort : GeologMeta/DSort; + v_base_ds GeologMeta/BaseDS/dsort = v_dsort; + + e_dsort : GeologMeta/DSort; + e_base_ds GeologMeta/BaseDS/dsort = e_dsort; + + src_func : GeologMeta/Func; + src_func GeologMeta/Func/theory = target_theory; + src_func GeologMeta/Func/dom = e_dsort; + src_func GeologMeta/Func/cod = v_dsort; + + // NOTE: For a complete example, we'd also need an Instance element + // and Elem elements. For simplicity, we use a simpler predicate structure. + + // Using TruePred for now (matches all, demonstrating structure) + + // -- Query Plan -- + // Schema for E + e_base_schema : BaseSchema; + e_base_schema BaseSchema/srt = e_srt; + + e_schema : Schema; + e_base_schema BaseSchema/schema = e_schema; + + // Wire 1: output of Scan (E elements) + w1 : Wire; + w1 Wire/schema = e_schema; + + // Wire 2: output of Filter (filtered E elements) + w2 : Wire; + w2 Wire/schema = e_schema; + + // Scan operation + scan : ScanOp; + scan ScanOp/srt = e_srt; + scan ScanOp/out = w1; + + scan_op : Op; + scan ScanOp/op = scan_op; + + // Predicate: TruePred (matches all - demonstrates filter structure) + true_pred : TruePred; + pred_elem : Pred; + true_pred TruePred/pred = pred_elem; + + // Filter operation: w1 --[Filter(pred)]--> w2 + filter : FilterOp; + filter FilterOp/in = w1; + filter FilterOp/out = w2; + filter FilterOp/pred = pred_elem; + + filter_op : Op; + filter FilterOp/op = filter_op; +} diff --git a/examples/geolog/solver_demo.geolog b/examples/geolog/solver_demo.geolog new file mode 100644 index 0000000..b8dec99 --- /dev/null +++ b/examples/geolog/solver_demo.geolog @@ -0,0 +1,132 @@ +// Solver Demo: Theories demonstrating the geometric logic solver +// +// Use the :solve command to find instances of these theories: +// :source examples/geolog/solver_demo.geolog +// :solve EmptyModel +// :solve Inhabited +// :solve Inconsistent +// +// The solver uses forward chaining to automatically: +// - Add witness elements for existentials +// - Assert relation tuples +// - Detect unsatisfiability (derivation of False) + +// ============================================================================ +// Theory 1: EmptyModel - Trivially satisfiable with empty carrier +// ============================================================================ +// +// A theory with no axioms is satisfied by the empty structure. +// The solver should report SOLVED immediately with 0 elements. + +theory EmptyModel { + A : Sort; + B : Sort; + f : A -> B; + R : A -> Prop; +} + +// ============================================================================ +// Theory 2: UnconditionalExistential - Requires witness creation +// ============================================================================ +// +// Axiom: forall x : P. |- exists y : P. y R +// +// SUBTLE: This axiom's premise (True) and conclusion (∃y.R(y)) don't mention x! +// So even though there's a "forall x : P", the check happens once for an empty +// assignment. The premise True holds, but ∃y.R(y) doesn't hold for empty P +// (no witnesses). The solver correctly detects this and adds a witness. +// +// This is correct geometric logic semantics! The universal over x doesn't +// protect against empty P because x isn't used in the formulas. + +theory UnconditionalExistential { + P : Sort; + R : P -> Prop; + + // This effectively says "there must exist some y with R(y)" + // because x is unused - the check happens once regardless of |P| + ax : forall x : P. |- exists y : P. y R; +} + +// ============================================================================ +// Theory 3: VacuouslyTrue - Axiom that IS vacuously true for empty carriers +// ============================================================================ +// +// Axiom: forall x : P. |- x R +// +// For every x, assert R(x). When P is empty, there are no x values to check, +// so the axiom is vacuously satisfied. Compare with UnconditionalExistential! + +theory VacuouslyTrue { + P : Sort; + R : P -> Prop; + + // This truly IS vacuously true for empty P because x IS used in the conclusion + ax : forall x : P. |- x R; +} + +// ============================================================================ +// Theory 4: Inconsistent - UNSAT via derivation of False +// ============================================================================ +// +// Axiom: forall x. |- false +// +// For any element x, we derive False. This is immediately UNSAT. +// The solver detects this and reports UNSAT. + +theory Inconsistent { + A : Sort; + + // Contradiction: any element leads to False + ax : forall a : A. |- false; +} + +// ============================================================================ +// Theory 5: ReflexiveRelation - Forward chaining asserts reflexive tuples +// ============================================================================ +// +// Axiom: forall x. |- R(x, x) +// +// For every element x, the pair (x, x) is in relation R. +// The solver will assert R(x, x) for each element added. + +theory ReflexiveRelation { + X : Sort; + R : [a: X, b: X] -> Prop; + + // Reflexivity: every element is related to itself + ax/refl : forall x : X. |- [a: x, b: x] R; +} + +// ============================================================================ +// Theory 6: ChainedWitness - Nested existential body processing +// ============================================================================ +// +// Axiom: forall x. |- exists y. exists z. E(x, y), E(y, z) +// +// For every x, there exist y and z such that E(x,y) and E(y,z). +// Forward chaining creates witnesses and asserts the relations. + +theory ChainedWitness { + N : Sort; + E : [src: N, tgt: N] -> Prop; + + // Chain: every node has a two-step path out + ax/chain : forall x : N. |- exists y : N. exists z : N. [src: x, tgt: y] E, [src: y, tgt: z] E; +} + +// ============================================================================ +// Theory 7: EqualityCollapse - Equation handling via congruence closure +// ============================================================================ +// +// Axiom: forall x, y. |- x = y +// +// All elements of sort X are equal. The solver adds equations to the +// congruence closure and merges equivalence classes. + +theory EqualityCollapse { + X : Sort; + + // All elements are equal + ax/all_equal : forall x : X, y : X. |- x = y; +} diff --git a/examples/geolog/sort_param_simple.geolog b/examples/geolog/sort_param_simple.geolog new file mode 100644 index 0000000..1ba3217 --- /dev/null +++ b/examples/geolog/sort_param_simple.geolog @@ -0,0 +1,31 @@ +// Simpler sort parameter test + +theory (X : Sort) Container { + elem : X; // not a Sort, but an element of X +} + +// Hmm, this doesn't quite work... +// Let me try the actual vision pattern + +theory Base { + A : Sort; + B : Sort; +} + +instance MyBase : Base = { + a1 : A; + a2 : A; + b1 : B; + b2 : B; +} + +// Now try a theory parameterized by an instance +theory (Inst : Base instance) Map { + map : Inst/A -> Inst/B; +} + +// Instance of Map parameterized by MyBase +instance MyMap : MyBase Map = { + a1 map = MyBase/b1; + a2 map = MyBase/b2; +} diff --git a/examples/geolog/todo_list.geolog b/examples/geolog/todo_list.geolog new file mode 100644 index 0000000..aa2cab9 --- /dev/null +++ b/examples/geolog/todo_list.geolog @@ -0,0 +1,44 @@ +// TodoList: A simple relational model for tracking tasks +// +// This demonstrates geolog as a persistent relational database. +// Elements represent tasks, and relations track their status. + +theory TodoList { + // The sort of todo items + Item : Sort; + + // Unary relations for item status (simple arrow syntax) + completed : Item -> Prop; + high_priority : Item -> Prop; + blocked : Item -> Prop; + + // Binary relation for dependencies + depends : [item: Item, on: Item] -> Prop; + + // Axiom: if an item depends on another, either it is blocked + // or the dependency is completed + ax/dep_blocked : forall x : Item, y : Item. + [item: x, on: y] depends |- x blocked \/ y completed; +} + +// Example: An empty todo list ready for interactive use +instance MyTodos : TodoList = { + // Start empty - add items interactively with :add +} + +// Example: A pre-populated todo list +instance SampleTodos : TodoList = { + // Items + buy_groceries : Item; + cook_dinner : Item; + do_laundry : Item; + clean_house : Item; + + // Status: unary relations use simple syntax + buy_groceries completed; + cook_dinner high_priority; + + // Dependencies: cook_dinner depends on buy_groceries + // Mixed syntax: first positional arg maps to 'item' field + [cook_dinner, on: buy_groceries] depends; +} diff --git a/examples/geolog/transitive_closure.geolog b/examples/geolog/transitive_closure.geolog new file mode 100644 index 0000000..7e76309 --- /dev/null +++ b/examples/geolog/transitive_closure.geolog @@ -0,0 +1,77 @@ +// Transitive Closure Example +// +// This example demonstrates the chase algorithm computing transitive +// closure of a relation. We define a Graph theory with Edge and Path +// relations, where Path is the transitive closure of Edge. +// +// Run with: +// cargo run -- examples/geolog/transitive_closure.geolog +// Then: +// :source examples/geolog/transitive_closure.geolog +// :inspect Chain +// :chase Chain +// +// The chase will derive Path tuples for all reachable pairs: +// - Edge(a,b), Edge(b,c), Edge(c,d) as base facts +// - Path(a,b), Path(b,c), Path(c,d) from base axiom +// - Path(a,c), Path(b,d) from one step of transitivity +// - Path(a,d) from two steps of transitivity + +theory Graph { + V : Sort; + + // Direct edges in the graph + Edge : [src: V, tgt: V] -> Prop; + + // Reachability (transitive closure of Edge) + Path : [src: V, tgt: V] -> Prop; + + // Base case: every edge is a path + ax/base : forall x, y : V. + [src: x, tgt: y] Edge |- [src: x, tgt: y] Path; + + // Inductive case: paths compose + ax/trans : forall x, y, z : V. + [src: x, tgt: y] Path, [src: y, tgt: z] Path |- [src: x, tgt: z] Path; +} + +// A linear chain: a -> b -> c -> d +// Chase derives Path tuples from Edge via ax/base and ax/trans. +instance Chain : Graph = chase { + a : V; + b : V; + c : V; + d : V; + + // Edges form a chain + [src: a, tgt: b] Edge; + [src: b, tgt: c] Edge; + [src: c, tgt: d] Edge; +} + +// A diamond: a -> b, a -> c, b -> d, c -> d +// Chase derives all reachable paths. +instance Diamond : Graph = chase { + top : V; + left : V; + right : V; + bottom : V; + + // Two paths from top to bottom + [src: top, tgt: left] Edge; + [src: top, tgt: right] Edge; + [src: left, tgt: bottom] Edge; + [src: right, tgt: bottom] Edge; +} + +// A cycle: a -> b -> c -> a +// Chase derives all reachable paths (full connectivity). +instance Cycle : Graph = chase { + x : V; + y : V; + z : V; + + [src: x, tgt: y] Edge; + [src: y, tgt: z] Edge; + [src: z, tgt: x] Edge; +} diff --git a/examples/scripts/README.md b/examples/scripts/README.md new file mode 100644 index 0000000..580863e --- /dev/null +++ b/examples/scripts/README.md @@ -0,0 +1,13 @@ +# Example Scripts + +These scripts can be executed with: + +```bash +make script SCRIPT=examples/scripts/ancestor.chase +``` + +Available examples: + +- `ancestor.chase`: transitive closure over `Parent/2` +- `employee_departments.chase`: existential rule that creates labeled nulls +- `same_team.chase`: conjunctive query with a self-join diff --git a/examples/scripts/ancestor.chase b/examples/scripts/ancestor.chase new file mode 100644 index 0000000..79237c2 --- /dev/null +++ b/examples/scripts/ancestor.chase @@ -0,0 +1,11 @@ +# Derive ancestors from parent relationships. + +fact Parent(alice, bob). +fact Parent(bob, carol). +fact Parent(carol, dave). + +rule Parent(?X, ?Y) -> Ancestor(?X, ?Y). +rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z). + +run. +query Ancestor(?X, ?Y)? diff --git a/examples/scripts/employee_departments.chase b/examples/scripts/employee_departments.chase new file mode 100644 index 0000000..16a85be --- /dev/null +++ b/examples/scripts/employee_departments.chase @@ -0,0 +1,11 @@ +# Existential rule example: each employee works in some department. + +fact Employee(alice). +fact Employee(bob). +fact Employee(carol). + +rule Employee(?X) -> WorksIn(?X, ?Dept). + +run. +show facts +query WorksIn(?X, ?Dept)? diff --git a/examples/scripts/same_team.chase b/examples/scripts/same_team.chase new file mode 100644 index 0000000..b8e4606 --- /dev/null +++ b/examples/scripts/same_team.chase @@ -0,0 +1,11 @@ +# Query people who share a manager. + +fact ManagedBy(alice, eve). +fact ManagedBy(bob, eve). +fact ManagedBy(carol, frank). + +rule ManagedBy(?X, ?M), ManagedBy(?Y, ?M) -> SameTeam(?X, ?Y). + +run. +query SameTeam(?X, ?Y)? +query SameTeam(alice, bob)? diff --git a/src/catalog/mod.rs b/src/catalog/mod.rs new file mode 100644 index 0000000..d4fa332 --- /dev/null +++ b/src/catalog/mod.rs @@ -0,0 +1,133 @@ +//! Minimal catalog support for mapping predicates to relational schemas. + +use std::collections::HashMap; +use std::error::Error; +use std::fmt; + +use crate::chase::{Instance, Term}; +use crate::relational::{DataType, Field, Schema}; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum CatalogError { + UnknownTable(String), + InconsistentArity { + table: String, + expected: usize, + found: usize, + }, +} + +impl fmt::Display for CatalogError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::UnknownTable(table) => write!(f, "unknown table `{}`", table), + Self::InconsistentArity { + table, + expected, + found, + } => write!( + f, + "table `{}` has inconsistent arity: expected {}, found {}", + table, expected, found + ), + } + } +} + +impl Error for CatalogError {} + +#[derive(Debug, Clone, Default)] +pub struct PredicateCatalog { + schemas: HashMap, +} + +impl PredicateCatalog { + pub fn new() -> Self { + Self::default() + } + + pub fn register_table(&mut self, table: impl Into, schema: Schema) { + self.schemas.insert(table.into(), schema); + } + + pub fn schema_for(&self, table: &str) -> Result<&Schema, CatalogError> { + self.schemas + .get(table) + .ok_or_else(|| CatalogError::UnknownTable(table.to_string())) + } + + pub fn from_instance(instance: &Instance) -> Result { + let mut arities = HashMap::new(); + let mut nullable_positions: HashMap> = HashMap::new(); + + for atom in instance.iter() { + let arity = atom.arity(); + match arities.get(&atom.predicate) { + Some(expected) if *expected != arity => { + return Err(CatalogError::InconsistentArity { + table: atom.predicate.clone(), + expected: *expected, + found: arity, + }); + } + Some(_) => {} + None => { + arities.insert(atom.predicate.clone(), arity); + nullable_positions.insert(atom.predicate.clone(), vec![false; arity]); + } + } + + if let Some(positions) = nullable_positions.get_mut(&atom.predicate) { + for (index, term) in atom.terms.iter().enumerate() { + if matches!(term, Term::Null(_)) { + positions[index] = true; + } + } + } + } + + let mut catalog = Self::new(); + for (table, arity) in arities { + let nullable = nullable_positions.remove(&table).unwrap_or_default(); + let fields = (0..arity) + .map(|index| { + Field::new( + format!("c{}", index), + DataType::Text, + nullable.get(index).copied().unwrap_or(false), + ) + }) + .collect(); + catalog.register_table(table, Schema::new(fields)); + } + + Ok(catalog) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::chase::Atom; + + #[test] + fn infers_predicate_schemas_from_instance() { + let instance: Instance = vec![ + Atom::new( + "Parent", + vec![Term::constant("alice"), Term::constant("bob")], + ), + Atom::new("Parent", vec![Term::constant("bob"), Term::null(0)]), + ] + .into_iter() + .collect(); + + let catalog = PredicateCatalog::from_instance(&instance).unwrap(); + let schema = catalog.schema_for("Parent").unwrap(); + + assert_eq!(schema.len(), 2); + assert_eq!(schema.fields()[0].name(), "c0"); + assert_eq!(schema.fields()[1].name(), "c1"); + assert!(schema.fields()[1].nullable()); + } +} diff --git a/src/execution/mod.rs b/src/execution/mod.rs new file mode 100644 index 0000000..ec52930 --- /dev/null +++ b/src/execution/mod.rs @@ -0,0 +1,112 @@ +//! Minimal execution support for the first SQL slice. + +use std::error::Error; +use std::fmt; + +use crate::chase::{Instance, Term}; +use crate::planner::logical::{LogicalExpr, LogicalPlan}; +use crate::relational::{ResultSet, Row, Value}; + +#[derive(Debug)] +pub enum ExecutionError { + UnknownColumn(String), + NonGroundScanTerm, +} + +impl fmt::Display for ExecutionError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::UnknownColumn(column) => write!(f, "unknown column `{}`", column), + Self::NonGroundScanTerm => { + write!(f, "cannot scan non-ground terms into relational rows") + } + } + } +} + +impl Error for ExecutionError {} + +pub fn execute(plan: &LogicalPlan, instance: &Instance) -> Result { + match plan { + LogicalPlan::Scan { table, schema } => { + let mut rows = Vec::new(); + for fact in instance.facts_for_predicate(table) { + let values = fact + .terms + .iter() + .map(value_from_term) + .collect::, _>>()?; + rows.push(Row::new(values)); + } + Ok(ResultSet::new(schema.clone(), rows)) + } + LogicalPlan::Filter { input, predicate } => { + let result = execute(input, instance)?; + let filtered_rows = result + .rows() + .iter() + .filter(|row| eval_predicate(predicate, row, result.schema()).unwrap_or(false)) + .cloned() + .collect(); + Ok(ResultSet::new(result.schema().clone(), filtered_rows)) + } + LogicalPlan::Project { + input, + expressions, + schema, + } => { + let result = execute(input, instance)?; + let mut rows = Vec::new(); + for row in result.rows() { + let values = expressions + .iter() + .map(|expr| eval_expr(&expr.expr, row, result.schema())) + .collect::, _>>()?; + rows.push(Row::new(values)); + } + Ok(ResultSet::new(schema.clone(), rows)) + } + } +} + +fn eval_predicate( + expr: &LogicalExpr, + row: &Row, + schema: &crate::relational::Schema, +) -> Result { + match expr { + LogicalExpr::Eq(left, right) => Ok(eval_expr(left, row, schema)? + .sql_eq(&eval_expr(right, row, schema)?) + .unwrap_or(false)), + _ => Ok(false), + } +} + +fn eval_expr( + expr: &LogicalExpr, + row: &Row, + schema: &crate::relational::Schema, +) -> Result { + match expr { + LogicalExpr::Column(name) => { + let index = schema + .index_of(name) + .ok_or_else(|| ExecutionError::UnknownColumn(name.clone()))?; + Ok(row.get(index).cloned().unwrap_or(Value::Null)) + } + LogicalExpr::Literal(value) => Ok(value.clone()), + LogicalExpr::Eq(left, right) => { + let left = eval_expr(left, row, schema)?; + let right = eval_expr(right, row, schema)?; + Ok(Value::Boolean(left.sql_eq(&right).unwrap_or(false))) + } + } +} + +fn value_from_term(term: &Term) -> Result { + match term { + Term::Constant(value) => Ok(Value::text(value.clone())), + Term::Null(_) => Ok(Value::Null), + Term::Variable(_) => Err(ExecutionError::NonGroundScanTerm), + } +} diff --git a/src/lib.rs b/src/lib.rs index f7278ea..fc02713 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,8 +4,13 @@ //! lightweight frontends for experimenting with rule-driven query answering. //! It is not yet a full SQL engine with logical and physical planning layers. +pub mod catalog; pub mod chase; +pub mod execution; pub mod frontend; +pub mod planner; +pub mod relational; +pub mod sql; // Curated convenience re-exports for the current public crate surface. // Lower-level reasoning and provenance APIs remain under `query_engine::chase`. diff --git a/src/planner/logical.rs b/src/planner/logical.rs new file mode 100644 index 0000000..3d36766 --- /dev/null +++ b/src/planner/logical.rs @@ -0,0 +1,47 @@ +use crate::relational::{ResultSet, Schema, Value}; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum LogicalExpr { + Column(String), + Literal(Value), + Eq(Box, Box), +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct NamedExpr { + pub name: String, + pub expr: LogicalExpr, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum LogicalPlan { + Scan { + table: String, + schema: Schema, + }, + Filter { + input: Box, + predicate: LogicalExpr, + }, + Project { + input: Box, + expressions: Vec, + schema: Schema, + }, +} + +impl LogicalPlan { + pub fn output_schema(&self) -> &Schema { + match self { + Self::Scan { schema, .. } => schema, + Self::Filter { input, .. } => input.output_schema(), + Self::Project { schema, .. } => schema, + } + } +} + +impl From for LogicalPlan { + fn from(_: ResultSet) -> Self { + unreachable!("result sets are execution output, not logical plans") + } +} diff --git a/src/planner/mod.rs b/src/planner/mod.rs new file mode 100644 index 0000000..018b572 --- /dev/null +++ b/src/planner/mod.rs @@ -0,0 +1,4 @@ +//! Logical planning scaffolding. + +pub mod logical; +pub mod sql; diff --git a/src/planner/sql.rs b/src/planner/sql.rs new file mode 100644 index 0000000..9f5cd4b --- /dev/null +++ b/src/planner/sql.rs @@ -0,0 +1,149 @@ +use std::error::Error; +use std::fmt; + +use crate::catalog::{CatalogError, PredicateCatalog}; +use crate::planner::logical::{LogicalExpr, LogicalPlan, NamedExpr}; +use crate::relational::{Field, Schema, Value}; +use crate::sql::ast::{BinaryOp, Expr, Literal, Select, SelectItem}; + +#[derive(Debug)] +pub enum PlannerError { + Catalog(CatalogError), + UnknownColumn(String), + UnsupportedProjection, +} + +impl fmt::Display for PlannerError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Catalog(err) => write!(f, "catalog error: {}", err), + Self::UnknownColumn(column) => write!(f, "unknown column `{}`", column), + Self::UnsupportedProjection => { + write!(f, "only wildcard and column projections are supported") + } + } + } +} + +impl Error for PlannerError { + fn source(&self) -> Option<&(dyn Error + 'static)> { + match self { + Self::Catalog(err) => Some(err), + Self::UnknownColumn(_) | Self::UnsupportedProjection => None, + } + } +} + +impl From for PlannerError { + fn from(value: CatalogError) -> Self { + Self::Catalog(value) + } +} + +pub fn plan_select( + select: &Select, + catalog: &PredicateCatalog, +) -> Result { + let scan_schema = catalog.schema_for(&select.from)?.clone(); + let mut plan = LogicalPlan::Scan { + table: select.from.clone(), + schema: scan_schema.clone(), + }; + + if let Some(selection) = &select.selection { + let predicate = plan_expr(selection, &scan_schema)?; + plan = LogicalPlan::Filter { + input: Box::new(plan), + predicate, + }; + } + + if is_wildcard_projection(&select.projection) { + return Ok(plan); + } + + let mut expressions = Vec::new(); + let mut fields = Vec::new(); + for item in &select.projection { + match item { + SelectItem::Expr { expr, alias } => match expr { + Expr::Identifier(name) => { + let index = scan_schema + .index_of(name) + .ok_or_else(|| PlannerError::UnknownColumn(name.clone()))?; + let input_field = &scan_schema.fields()[index]; + let output_name = alias.clone().unwrap_or_else(|| name.clone()); + expressions.push(NamedExpr { + name: output_name.clone(), + expr: LogicalExpr::Column(name.clone()), + }); + fields.push(Field::new( + output_name, + input_field.data_type().clone(), + input_field.nullable(), + )); + } + _ => return Err(PlannerError::UnsupportedProjection), + }, + SelectItem::Wildcard => return Err(PlannerError::UnsupportedProjection), + } + } + + Ok(LogicalPlan::Project { + input: Box::new(plan), + expressions, + schema: Schema::new(fields), + }) +} + +fn is_wildcard_projection(items: &[SelectItem]) -> bool { + matches!(items, [SelectItem::Wildcard]) +} + +fn plan_expr(expr: &Expr, schema: &Schema) -> Result { + match expr { + Expr::Identifier(name) => { + if schema.index_of(name).is_none() { + return Err(PlannerError::UnknownColumn(name.clone())); + } + Ok(LogicalExpr::Column(name.clone())) + } + Expr::Literal(literal) => Ok(LogicalExpr::Literal(plan_literal(literal))), + Expr::Binary { left, op, right } => match op { + BinaryOp::Eq => Ok(LogicalExpr::Eq( + Box::new(plan_expr(left, schema)?), + Box::new(plan_expr(right, schema)?), + )), + }, + } +} + +fn plan_literal(literal: &Literal) -> Value { + match literal { + Literal::String(value) => Value::text(value.clone()), + Literal::Null => Value::Null, + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::catalog::PredicateCatalog; + use crate::chase::{Atom, Instance, Term}; + use crate::sql::parser::parse_select; + + #[test] + fn plans_projection_and_filter() { + let instance: Instance = vec![Atom::new( + "Parent", + vec![Term::constant("alice"), Term::constant("bob")], + )] + .into_iter() + .collect(); + let catalog = PredicateCatalog::from_instance(&instance).unwrap(); + let select = parse_select("SELECT c0 FROM Parent WHERE c1 = 'bob'").unwrap(); + + let plan = plan_select(&select, &catalog).unwrap(); + assert_eq!(plan.output_schema().len(), 1); + } +} diff --git a/src/relational/mod.rs b/src/relational/mod.rs new file mode 100644 index 0000000..8bd29b5 --- /dev/null +++ b/src/relational/mod.rs @@ -0,0 +1,9 @@ +//! Relational data model scaffolding for future SQL and planner work. + +mod row; +mod schema; +mod value; + +pub use row::{ResultSet, Row}; +pub use schema::{DataType, Field, Schema}; +pub use value::Value; diff --git a/src/relational/row.rs b/src/relational/row.rs new file mode 100644 index 0000000..d347ed0 --- /dev/null +++ b/src/relational/row.rs @@ -0,0 +1,40 @@ +use super::{Schema, Value}; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Row { + values: Vec, +} + +impl Row { + pub fn new(values: Vec) -> Self { + Self { values } + } + + pub fn values(&self) -> &[Value] { + &self.values + } + + pub fn get(&self, index: usize) -> Option<&Value> { + self.values.get(index) + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ResultSet { + schema: Schema, + rows: Vec, +} + +impl ResultSet { + pub fn new(schema: Schema, rows: Vec) -> Self { + Self { schema, rows } + } + + pub fn schema(&self) -> &Schema { + &self.schema + } + + pub fn rows(&self) -> &[Row] { + &self.rows + } +} diff --git a/src/relational/schema.rs b/src/relational/schema.rs new file mode 100644 index 0000000..38279b9 --- /dev/null +++ b/src/relational/schema.rs @@ -0,0 +1,92 @@ +use std::fmt; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum DataType { + Text, + Boolean, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Field { + name: String, + data_type: DataType, + nullable: bool, +} + +impl Field { + pub fn new(name: impl Into, data_type: DataType, nullable: bool) -> Self { + Self { + name: name.into(), + data_type, + nullable, + } + } + + pub fn name(&self) -> &str { + &self.name + } + + pub fn data_type(&self) -> &DataType { + &self.data_type + } + + pub fn nullable(&self) -> bool { + self.nullable + } +} + +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub struct Schema { + fields: Vec, +} + +impl Schema { + pub fn new(fields: Vec) -> Self { + Self { fields } + } + + pub fn fields(&self) -> &[Field] { + &self.fields + } + + pub fn len(&self) -> usize { + self.fields.len() + } + + pub fn is_empty(&self) -> bool { + self.fields.is_empty() + } + + pub fn index_of(&self, name: &str) -> Option { + self.fields.iter().position(|field| field.name() == name) + } +} + +impl fmt::Display for Schema { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + let fields = self + .fields + .iter() + .map(|field| field.name().to_string()) + .collect::>() + .join(", "); + write!(f, "[{}]", fields) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn schema_resolves_columns_by_name() { + let schema = Schema::new(vec![ + Field::new("c0", DataType::Text, false), + Field::new("c1", DataType::Text, true), + ]); + + assert_eq!(schema.index_of("c0"), Some(0)); + assert_eq!(schema.index_of("c1"), Some(1)); + assert_eq!(schema.index_of("missing"), None); + } +} diff --git a/src/relational/value.rs b/src/relational/value.rs new file mode 100644 index 0000000..0d37b6c --- /dev/null +++ b/src/relational/value.rs @@ -0,0 +1,37 @@ +use std::fmt; + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub enum Value { + Text(String), + Boolean(bool), + Null, +} + +impl Value { + pub fn text(value: impl Into) -> Self { + Self::Text(value.into()) + } + + pub fn is_null(&self) -> bool { + matches!(self, Self::Null) + } + + pub fn sql_eq(&self, other: &Self) -> Option { + match (self, other) { + (Self::Null, _) | (_, Self::Null) => None, + (Self::Text(left), Self::Text(right)) => Some(left == right), + (Self::Boolean(left), Self::Boolean(right)) => Some(left == right), + (Self::Text(_), Self::Boolean(_)) | (Self::Boolean(_), Self::Text(_)) => Some(false), + } + } +} + +impl fmt::Display for Value { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Text(value) => write!(f, "{}", value), + Self::Boolean(value) => write!(f, "{}", value), + Self::Null => write!(f, "NULL"), + } + } +} diff --git a/src/sql/ast.rs b/src/sql/ast.rs new file mode 100644 index 0000000..5643624 --- /dev/null +++ b/src/sql/ast.rs @@ -0,0 +1,34 @@ +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Select { + pub projection: Vec, + pub from: String, + pub selection: Option, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum SelectItem { + Wildcard, + Expr { expr: Expr, alias: Option }, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Expr { + Identifier(String), + Literal(Literal), + Binary { + left: Box, + op: BinaryOp, + right: Box, + }, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Literal { + String(String), + Null, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum BinaryOp { + Eq, +} diff --git a/src/sql/mod.rs b/src/sql/mod.rs new file mode 100644 index 0000000..e0ab5b1 --- /dev/null +++ b/src/sql/mod.rs @@ -0,0 +1,4 @@ +//! Minimal SQL front-end scaffolding. + +pub mod ast; +pub mod parser; diff --git a/src/sql/parser.rs b/src/sql/parser.rs new file mode 100644 index 0000000..6960e93 --- /dev/null +++ b/src/sql/parser.rs @@ -0,0 +1,275 @@ +use std::error::Error; +use std::fmt; + +use super::ast::{BinaryOp, Expr, Literal, Select, SelectItem}; + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ParseError { + UnexpectedEnd, + ExpectedToken(&'static str), + ExpectedIdentifier, + UnexpectedToken(String), + UnterminatedString, +} + +impl fmt::Display for ParseError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::UnexpectedEnd => write!(f, "unexpected end of input"), + Self::ExpectedToken(token) => write!(f, "expected `{}`", token), + Self::ExpectedIdentifier => write!(f, "expected identifier"), + Self::UnexpectedToken(token) => write!(f, "unexpected token `{}`", token), + Self::UnterminatedString => write!(f, "unterminated string literal"), + } + } +} + +impl Error for ParseError {} + +#[derive(Debug, Clone, PartialEq, Eq)] +enum Token { + Select, + From, + Where, + Null, + Identifier(String), + String(String), + Star, + Comma, + Eq, +} + +pub fn parse_select(input: &str) -> Result { + let tokens = tokenize(input)?; + let mut parser = Parser::new(tokens); + parser.parse_select() +} + +struct Parser { + tokens: Vec, + index: usize, +} + +impl Parser { + fn new(tokens: Vec) -> Self { + Self { tokens, index: 0 } + } + + fn parse_select(&mut self) -> Result { + self.expect_keyword(Token::Select, "SELECT")?; + let projection = self.parse_projection()?; + self.expect_keyword(Token::From, "FROM")?; + let from = self.expect_identifier()?; + let selection = if self.peek() == Some(&Token::Where) { + self.index += 1; + Some(self.parse_expr()?) + } else { + None + }; + + if let Some(token) = self.peek() { + return Err(ParseError::UnexpectedToken(render_token(token))); + } + + Ok(Select { + projection, + from, + selection, + }) + } + + fn parse_projection(&mut self) -> Result, ParseError> { + let mut items = Vec::new(); + + loop { + let item = match self.next().ok_or(ParseError::UnexpectedEnd)? { + Token::Star => SelectItem::Wildcard, + Token::Identifier(name) => SelectItem::Expr { + expr: Expr::Identifier(name), + alias: None, + }, + other => return Err(ParseError::UnexpectedToken(render_token(&other))), + }; + items.push(item); + + if self.peek() == Some(&Token::Comma) { + self.index += 1; + continue; + } + break; + } + + Ok(items) + } + + fn parse_expr(&mut self) -> Result { + let left = self.parse_operand()?; + match self.next().ok_or(ParseError::UnexpectedEnd)? { + Token::Eq => { + let right = self.parse_operand()?; + Ok(Expr::Binary { + left: Box::new(left), + op: BinaryOp::Eq, + right: Box::new(right), + }) + } + other => Err(ParseError::UnexpectedToken(render_token(&other))), + } + } + + fn parse_operand(&mut self) -> Result { + match self.next().ok_or(ParseError::UnexpectedEnd)? { + Token::Identifier(name) => Ok(Expr::Identifier(name)), + Token::String(value) => Ok(Expr::Literal(Literal::String(value))), + Token::Null => Ok(Expr::Literal(Literal::Null)), + other => Err(ParseError::UnexpectedToken(render_token(&other))), + } + } + + fn expect_keyword(&mut self, token: Token, label: &'static str) -> Result<(), ParseError> { + let next = self.next().ok_or(ParseError::UnexpectedEnd)?; + if next == token { + Ok(()) + } else { + Err(ParseError::ExpectedToken(label)) + } + } + + fn expect_identifier(&mut self) -> Result { + match self.next().ok_or(ParseError::UnexpectedEnd)? { + Token::Identifier(name) => Ok(name), + _ => Err(ParseError::ExpectedIdentifier), + } + } + + fn peek(&self) -> Option<&Token> { + self.tokens.get(self.index) + } + + fn next(&mut self) -> Option { + let token = self.tokens.get(self.index).cloned(); + if token.is_some() { + self.index += 1; + } + token + } +} + +fn tokenize(input: &str) -> Result, ParseError> { + let mut chars = input.chars().peekable(); + let mut tokens = Vec::new(); + + while let Some(ch) = chars.peek().copied() { + if ch.is_whitespace() { + chars.next(); + continue; + } + + match ch { + '*' => { + chars.next(); + tokens.push(Token::Star); + } + ',' => { + chars.next(); + tokens.push(Token::Comma); + } + '=' => { + chars.next(); + tokens.push(Token::Eq); + } + '\'' => tokens.push(Token::String(parse_string(&mut chars)?)), + ch if is_identifier_start(ch) => { + let ident = parse_identifier(&mut chars); + let token = match ident.to_ascii_uppercase().as_str() { + "SELECT" => Token::Select, + "FROM" => Token::From, + "WHERE" => Token::Where, + "NULL" => Token::Null, + _ => Token::Identifier(ident), + }; + tokens.push(token); + } + other => return Err(ParseError::UnexpectedToken(other.to_string())), + } + } + + Ok(tokens) +} + +fn parse_string(chars: &mut std::iter::Peekable) -> Result +where + I: Iterator, +{ + let mut value = String::new(); + let quote = chars.next(); + if quote != Some('\'') { + return Err(ParseError::ExpectedToken("'")); + } + + while let Some(ch) = chars.next() { + if ch == '\'' { + if chars.peek() == Some(&'\'') { + chars.next(); + value.push('\''); + continue; + } + return Ok(value); + } + value.push(ch); + } + + Err(ParseError::UnterminatedString) +} + +fn parse_identifier(chars: &mut std::iter::Peekable) -> String +where + I: Iterator, +{ + let mut ident = String::new(); + while let Some(ch) = chars.peek().copied() { + if is_identifier_part(ch) { + ident.push(ch); + chars.next(); + } else { + break; + } + } + ident +} + +fn is_identifier_start(ch: char) -> bool { + ch.is_ascii_alphabetic() || ch == '_' +} + +fn is_identifier_part(ch: char) -> bool { + ch.is_ascii_alphanumeric() || ch == '_' +} + +fn render_token(token: &Token) -> String { + match token { + Token::Select => "SELECT".to_string(), + Token::From => "FROM".to_string(), + Token::Where => "WHERE".to_string(), + Token::Null => "NULL".to_string(), + Token::Identifier(name) => name.clone(), + Token::String(value) => format!("'{}'", value), + Token::Star => "*".to_string(), + Token::Comma => ",".to_string(), + Token::Eq => "=".to_string(), + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn parses_select_with_filter() { + let select = parse_select("SELECT c0 FROM Parent WHERE c1 = 'bob'").unwrap(); + + assert_eq!(select.from, "Parent"); + assert_eq!(select.projection.len(), 1); + assert!(select.selection.is_some()); + } +} diff --git a/tests/sql_pipeline_tests.rs b/tests/sql_pipeline_tests.rs new file mode 100644 index 0000000..92e798b --- /dev/null +++ b/tests/sql_pipeline_tests.rs @@ -0,0 +1,67 @@ +use query_engine::catalog::PredicateCatalog; +use query_engine::execution::execute; +use query_engine::planner::sql::plan_select; +use query_engine::sql::parser::parse_select; +use query_engine::{Atom, Instance, Term}; + +fn parent_instance() -> Instance { + vec![ + Atom::new( + "Parent", + vec![Term::constant("alice"), Term::constant("bob")], + ), + Atom::new( + "Parent", + vec![Term::constant("bob"), Term::constant("carol")], + ), + ] + .into_iter() + .collect() +} + +#[test] +fn select_star_scans_predicate_as_table() { + let instance = parent_instance(); + let catalog = PredicateCatalog::from_instance(&instance).unwrap(); + let select = parse_select("SELECT * FROM Parent").unwrap(); + + let plan = plan_select(&select, &catalog).unwrap(); + let result = execute(&plan, &instance).unwrap(); + + assert_eq!(result.schema().len(), 2); + assert_eq!(result.rows().len(), 2); + assert_eq!(result.rows()[0].values().len(), 2); +} + +#[test] +fn select_projection_keeps_requested_columns() { + let instance = parent_instance(); + let catalog = PredicateCatalog::from_instance(&instance).unwrap(); + let select = parse_select("SELECT c0 FROM Parent").unwrap(); + + let plan = plan_select(&select, &catalog).unwrap(); + let result = execute(&plan, &instance).unwrap(); + + assert_eq!(result.schema().len(), 1); + assert_eq!(result.rows().len(), 2); + let mut values = result + .rows() + .iter() + .map(|row| format!("{}", row.values()[0])) + .collect::>(); + values.sort(); + assert_eq!(values, vec!["alice".to_string(), "bob".to_string()]); +} + +#[test] +fn select_where_filters_rows() { + let instance = parent_instance(); + let catalog = PredicateCatalog::from_instance(&instance).unwrap(); + let select = parse_select("SELECT c0 FROM Parent WHERE c1 = 'bob'").unwrap(); + + let plan = plan_select(&select, &catalog).unwrap(); + let result = execute(&plan, &instance).unwrap(); + + assert_eq!(result.rows().len(), 1); + assert_eq!(format!("{}", result.rows()[0].values()[0]), "alice"); +}