From 6ba970e55c3f51ca20ef93eed048024884531a94 Mon Sep 17 00:00:00 2001 From: Hassan Abedi Date: Mon, 30 Mar 2026 10:34:26 +0200 Subject: [PATCH] Add a glossary section the IR note file --- .../011-geolog-intermediate-representation.md | 31 +++++++++++++++---- 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/hassan/011-geolog-intermediate-representation.md b/hassan/011-geolog-intermediate-representation.md index 3e25f8e..2c705fe 100644 --- a/hassan/011-geolog-intermediate-representation.md +++ b/hassan/011-geolog-intermediate-representation.md @@ -16,9 +16,28 @@ The current pipeline is: The lowering entry point is `geolog-lang/src/Geolog/Lower.hs`, via `lowerTop`, which calls `lower`, then `lowerEntry`, then `finishTheory`. +## Glossary + +- `IR`: Intermediate representation. A simpler form used between elaboration and later evaluation. +- `lowering`: The step that converts elaborated Geolog code into the IR. +- `Path`: A qualified name like `M.mul`. +- `ColType`: The type of one table column. +- `Table`: A lowered relational object with columns and maybe a primary key. +- `RelTable`: A table used for a relation or predicate. +- `FunTable`: A table used for something function-like, where input columns determine an output. +- `Term`: A small IR expression, such as a variable, literal, or projection. +- `Atom`: One table occurrence with concrete arguments. +- `Prop`: A logical formula built from atoms and connectives like equality and conjunction. +- `Law`: A quantified rule over IR propositions. +- `FlatTheory`: The final lowered result: a set of tables plus laws. +- `foreignKeys`: Generated laws saying a row depends on other rows existing. +- `total`: Generated laws saying a function row must exist when its inputs exist. +- `PiColumn`: A column introduced as part of a table's explicit shape. +- `JoinColumn`: A column introduced while following a reference or join. + ## Core IR data types -The IR is intentionally relational. +The IR is intentionally relational. It turns theory structure into tables and rules. - `Path = [QName]`: a hierarchical name like `["M","mul"]`, pretty-printed as `M.mul`. - `ColType` is the type of a column. `EntityType Path` means the column refers to rows from another entity/table, `PrimType PrimInt | PrimString` covers builtin scalars, and `Tuple [(QName, ColType)]` supports structured values. @@ -32,7 +51,7 @@ See `geolog-lang/src/Geolog/IR.hs` for the concrete definitions. ## What lowering does -Lowering walks an elaborated theory and converts type-theoretic structure into tables plus integrity laws. +Lowering walks the elaborated theory and turns it into tables plus rules. ### 1. Records become path prefixes @@ -54,7 +73,7 @@ See `lowerTheoryTy` in `geolog-lang/src/Geolog/Lower.hs`. ### 3. Functions/entities become `FunTable` -When lowering encounters an abstract decoded type that does not reduce to a more concrete theory shape, it emits a `FunTable`. +When lowering finds something function-like that does not reduce to a simpler theory shape, it emits a `FunTable`. At the end of lowering, function tables get a primary key consisting of all columns except the final result column. That matches the examples: @@ -65,7 +84,7 @@ This logic is in `finishTheory` in `geolog-lang/src/Geolog/Lower.hs`. ### 4. Dependent structure becomes extra columns -The interesting part is that lowering is not just flattening syntax. It also lambda-lifts shared context into explicit columns. +Lowering is not just flattening syntax. It also turns shared context into explicit columns. `liftOnShared` copies shared outer variables into the current row shape so that dependencies become relationally explicit. This is why tables like `D.mul` contain both `M.car` arguments and displayed-car columns. @@ -90,7 +109,7 @@ Each lowered table may carry generated laws. `makeFkeys` says: if a row exists in table `p`, then the rows it depends on must also exist. -Operationally, this is how dependent references are reified as relational constraints. A row in `D.mul` implies the existence of corresponding rows in `D.car` and `M.mul`. +This is how dependent references become relational constraints. A row in `D.mul` implies the existence of corresponding rows in `D.car` and `M.mul`. See `makeFkeys` in `geolog-lang/src/Geolog/Lower.hs`. @@ -139,7 +158,7 @@ The implemented IR is best understood as a relationalized, flattened theory: - references become foreign-key-style laws - total functions become tables plus totality laws -So the IR is not just an AST for queries. It is the bridge from elaborated dependent syntax to a database-shaped semantics that downstream query/evaluation machinery can consume. +So the IR is not just an AST for queries. It is the bridge from elaborated dependent syntax to a database-shaped form that later evaluation code can consume. ## Note