Add a note on current version of Geolog's IR

hassan/011-geolog-intermediate-representation.md

@@ -16,28 +16,9 @@ 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. It turns theory structure into tables and rules.
+The IR is intentionally relational.
 
 - `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.
@@ -51,7 +32,7 @@ See `geolog-lang/src/Geolog/IR.hs` for the concrete definitions.
 
 ## What lowering does
 
-Lowering walks the elaborated theory and turns it into tables plus rules.
+Lowering walks an elaborated theory and converts type-theoretic structure into tables plus integrity laws.
 
 ### 1. Records become path prefixes
 
@@ -73,7 +54,7 @@ See `lowerTheoryTy` in `geolog-lang/src/Geolog/Lower.hs`.
 
 ### 3. Functions/entities become `FunTable`
 
-When lowering finds something function-like that does not reduce to a simpler theory shape, it emits a `FunTable`.
+When lowering encounters an abstract decoded type that does not reduce to a more concrete 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:
 
@@ -84,7 +65,7 @@ This logic is in `finishTheory` in `geolog-lang/src/Geolog/Lower.hs`.
 
 ### 4. Dependent structure becomes extra columns
 
-Lowering is not just flattening syntax. It also turns shared context into explicit columns.
+The interesting part is that lowering is not just flattening syntax. It also lambda-lifts 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.
 
@@ -109,7 +90,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.
 
-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`.
+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`.
 
 See `makeFkeys` in `geolog-lang/src/Geolog/Lower.hs`.
 
@@ -158,7 +139,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 form that later evaluation code can consume.
+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.
 
 ## Note