Python FE (Re)architecture

Strata/Languages/FineGrainLaurel/FineGrainLaurel.dialect.st

@@ -0,0 +1,213 @@
+// FineGrainLaurel Dialect: FGCBV (Fine-Grain Call-By-Value) with explicit polarity
+// This dialect extends Laurel with separate Value and Producer categories,
+// making polarity a representation-level invariant rather than a runtime predicate.
+//
+// Changes in this file are not automatically tracked by the build system.
+// Modify FineGrainLaurel.lean (e.g. update its comment) to trigger a rebuild after changing this file.
+
+dialect FineGrainLaurel;
+// Note: Not importing Laurel for now - FineGrainLaurel is self-contained
+
+// Import Laurel types for reuse
+category LaurelType;
+op intType : LaurelType => "int";
+op boolType : LaurelType => "bool";
+op realType : LaurelType => "real";
+op float64Type : LaurelType => "float64";
+op stringType : LaurelType => "string";
+op coreType (name: Ident): LaurelType => "Core " name;
+op mapType (keyType: LaurelType, valueType: LaurelType): LaurelType => "Map " keyType " " valueType;
+op compositeType (name: Ident): LaurelType => name;
+
+// ===========================================================================
+// FGCBV Core: Separate Value and Producer categories
+// ===========================================================================
+
+// Value category: inert terms (no effects, can be duplicated/discarded)
+category Value;
+
+// Producer category: effectful terms (must be sequenced, single-use)
+category Producer;
+
+// ===========================================================================
+// Value Operators (Inert Terms)
+// ===========================================================================
+
+// Literals
+op valLiteralInt (n: Num): Value => n;
+op valLiteralBool (b: Bool): Value => b;
+op valLiteralReal (d: Decimal): Value => d;
+op valLiteralString (s: Str): Value => s;
+
+// Variables
+op valVar (name: Ident): Value => name;
+
+// Pure binary operations (no effects)
+op valAdd (lhs: Value, rhs: Value): Value => @[prec(60), leftassoc] lhs " + " rhs;
+op valSub (lhs: Value, rhs: Value): Value => @[prec(60), leftassoc] lhs " - " rhs;
+op valMul (lhs: Value, rhs: Value): Value => @[prec(70), leftassoc] lhs " * " rhs;
+op valDiv (lhs: Value, rhs: Value): Value => @[prec(70), leftassoc] lhs " / " rhs;
+op valMod (lhs: Value, rhs: Value): Value => @[prec(70), leftassoc] lhs " % " rhs;
+
+// Pure comparison operations
+op valEq (lhs: Value, rhs: Value): Value => @[prec(40)] lhs " == " rhs;
+op valNeq (lhs: Value, rhs: Value): Value => @[prec(40)] lhs " != " rhs;
+op valLt (lhs: Value, rhs: Value): Value => @[prec(40)] lhs " < " rhs;
+op valLe (lhs: Value, rhs: Value): Value => @[prec(40)] lhs " <= " rhs;
+op valGt (lhs: Value, rhs: Value): Value => @[prec(40)] lhs " > " rhs;
+op valGe (lhs: Value, rhs: Value): Value => @[prec(40)] lhs " >= " rhs;
+
+// Pure logical operations
+op valAnd (lhs: Value, rhs: Value): Value => @[prec(30), leftassoc] lhs " & " rhs;
+op valOr (lhs: Value, rhs: Value): Value => @[prec(20), leftassoc] lhs " | " rhs;
+op valNot (inner: Value): Value => @[prec(80)] "!" inner;
+
+// Pure unary operations
+op valNeg (inner: Value): Value => @[prec(80)] "-" inner;
+
+// Field access (pure)
+op valFieldAccess (obj: Value, field: Ident): Value => @[prec(90)] obj "#" field;
+
+// Parenthesis (for grouping)
+op valParens (inner: Value): Value => "(" inner ")";
+
+// ===========================================================================
+// Producer Operators (Effectful Terms)
+// ===========================================================================
+
+// Return a value (terminal producer)
+op prodReturnValue (value: Value): Producer => @[prec(0)] "return " value:0;
+
+// Call a procedure (effectful)
+op prodCall (callee: Ident, args: CommaSepBy Value): Producer => callee "(" args ")";
+
+// Let-binding for producers (sequence effects)
+// let x: ty = prod in body
+op prodLetProd (var: Ident, ty: LaurelType, prod: Producer, body: Producer): Producer =>
+  @[prec(0)] "let " var ": " ty " = " prod:0 " in " body:0;
+
+// Let-binding for values (introduce binding for a value)
+// let x: ty = value in body
+op prodLetValue (var: Ident, ty: LaurelType, value: Value, body: Producer): Producer =>
+  @[prec(0)] "let " var ": " ty " = " value:0 " in " body:0;
+
+// Assignment (mutation)
+op prodAssign (target: Value, value: Value, body: Producer): Producer =>
+  @[prec(0)] target " := " value:0 ";" body:0;
+
+// Variable declaration with initialization
+op prodVarDecl (name: Ident, ty: LaurelType, init: Value, body: Producer): Producer =>
+  @[prec(0)] "var " name ": " ty " := " init:0 ";" body:0;
+
+// Conditional (if-then-else)
+op prodIfThenElse (cond: Value, thenBranch: Producer, elseBranch: Producer): Producer =>
+  @[prec(0)] "if " cond " then " thenBranch:0 " else " elseBranch:0;
+
+// Assert (specification)
+op prodAssert (cond: Value, body: Producer): Producer =>
+  @[prec(0)] "assert " cond:0 ";" body:0;
+
+// Assume (specification)
+op prodAssume (cond: Value, body: Producer): Producer =>
+  @[prec(0)] "assume " cond:0 ";" body:0;
+
+// While loop
+category Invariant;
+op invariant (cond: Value): Invariant => "invariant " cond:0;
+
+op prodWhile (cond: Value, invariants: Seq Invariant, body: Producer, after: Producer): Producer =>
+  @[prec(0)] "while (" cond ")" invariants " " body:0 after:0;
+
+// Instantiation (heap allocation)
+op prodNew (name: Ident, resultVar: Ident, ty: LaurelType, body: Producer): Producer =>
+  @[prec(0)] "let " resultVar ": " ty " = new " name " in " body:0;
+
+// Call with error handling
+op prodCallWithError (callee: Ident, args: CommaSepBy Value,
+                      resultVar: Ident, errorVar: Ident,
+                      resultTy: LaurelType, errorTy: LaurelType,
+                      body: Producer): Producer =>
+  @[prec(0)] "let [" resultVar ": " resultTy ", " errorVar ": " errorTy "] = " callee "(" args ") in " body:0;
+
+// Sequence (statement sequencing)
+op prodSeq (first: Producer, second: Producer): Producer =>
+  @[prec(5)] first:5 ";" second:5;
+
+// Block with multiple producers
+op prodBlock (stmts: SemicolonSepBy Producer): Producer =>
+  @[prec(1000)] "{" stmts "}";
+
+// Exit a labelled block (break/continue control flow)
+op prodExit (label: Str): Producer => "exit " label;
+
+// Labeled block (target of prodExit — models break/continue)
+op prodLabeledBlock (label: Str, body: Producer): Producer =>
+  @[prec(0)] "block " label " {" body:0 "}";
+
+// ===========================================================================
+// Top-level Declarations (reuse Laurel structure)
+// ===========================================================================
+
+category Parameter;
+op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
+
+category ReturnParameters;
+op returnParameters (parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
+
+category ErrorSummary;
+op errorSummary (msg: Str): ErrorSummary => "summary" msg;
+
+category RequiresClause;
+op requiresClause (cond: Value, errorMessage: Option ErrorSummary): RequiresClause => "requires" cond:0 errorMessage;
+
+category EnsuresClause;
+op ensuresClause (cond: Value, errorMessage: Option ErrorSummary): EnsuresClause => "ensures" cond:0 errorMessage;
+
+category ModifiesClause;
+op modifiesClause (refs: CommaSepBy Value): ModifiesClause => "modifies" refs;
+
+category ProcedureBody;
+op procedureBody (body: Producer): ProcedureBody => body:0;
+op externalBody: ProcedureBody => "external";
+
+category Procedure;
+op procedure (name: Ident, parameters: CommaSepBy Parameter,
+  returnParameters: Option ReturnParameters,
+  requires: Seq RequiresClause,
+  ensures: Seq EnsuresClause,
+  modifies: Seq ModifiesClause,
+  body: Option ProcedureBody): Procedure =>
+  "procedure " name "(" parameters ")" returnParameters requires ensures modifies body ";";
+
+category Field;
+op mutableField (name: Ident, fieldType: LaurelType): Field => "var " name ":" fieldType;
+op immutableField (name: Ident, fieldType: LaurelType): Field => name ":" fieldType;
+
+category Extends;
+op extends (parents: CommaSepBy Ident): Extends => "extends " parents;
+
+category Composite;
+op composite (name: Ident, extending: Option Extends, fields: Seq Field, procedures: Seq Procedure): Composite =>
+  "composite " name extending "{" fields procedures "}";
+
+// ===========================================================================
+// Value-Level Coercion Operators (Subtyping: infallible, value→value)
+// ===========================================================================
+
+// Upcasts: inject concrete types into Any (pure injections into the sum type)
+op valFromInt (inner: Value): Value => "from_int(" inner ")";
+op valFromStr (inner: Value): Value => "from_str(" inner ")";
+op valFromBool (inner: Value): Value => "from_bool(" inner ")";
+op valFromFloat (inner: Value): Value => "from_float(" inner ")";
+op valFromComposite (inner: Value): Value => "from_Composite(" inner ")";
+op valFromListAny (inner: Value): Value => "from_ListAny(" inner ")";
+op valFromDictStrAny (inner: Value): Value => "from_DictStrAny(" inner ")";
+op valFromNone: Value => "from_None()";
+
+// ===========================================================================
+// Top-level Declarations
+// ===========================================================================
+
+// Top-level commands
+op compositeCommand (composite: Composite): Command => composite;
+op procedureCommand (procedure: Procedure): Command => procedure;

Strata/Languages/FineGrainLaurel/FineGrainLaurel.lean

@@ -0,0 +1,24 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+-- FineGrainLaurel dialect definition, loaded from FineGrainLaurel.dialect.st
+-- NOTE: Changes to FineGrainLaurel.dialect.st are not automatically tracked by the build system.
+-- Update this file (e.g. this comment) to trigger a recompile after modifying FineGrainLaurel.dialect.st.
+-- Last grammar change: added prodExit for break/continue control flow preservation.
+
+module
+
+public import Strata.DDM.Integration.Lean
+public meta import Strata.DDM.Integration.Lean
+
+namespace Strata.FineGrainLaurel
+
+public section
+
+#load_dialect "./FineGrainLaurel.dialect.st"
+
+#strata_gen FineGrainLaurel
+
+end

Strata/Languages/Laurel/FilterPrelude.lean

@@ -69,7 +69,7 @@ private def addTypeName (name : String) : CollectM Unit :=
 private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   match ty.val with
   | .UserDefined name => addTypeName name.text
-  | .TCore _ => pure ()
+  | .TCore name => addTypeName name
   | .TTypedField vt => collectHighTypeNames vt
   | .TSet et => collectHighTypeNames et
   | .TMap kt vt => collectHighTypeNames kt; collectHighTypeNames vt

Strata/Languages/Laurel/HeapParameterizationConstants.lean

@@ -16,20 +16,40 @@ namespace Strata.Laurel
 public section
 
 /--
-The Laurel Core prelude defines the heap model types and operations
-used by the Laurel-to-Core translator. These declarations are expressed
-in Laurel syntax via the `#strata program Laurel` macro and parsed into
-a `Laurel.Program` at compile time.
-
-The heap model uses:
-- `Composite` - datatype with a reference (int) and a runtime type tag
-- `Field` - abstract type for field names (zero-constructor datatype)
-- `TypeTag` - abstract type for type tags (zero-constructor datatype)
-- `Heap` - datatype with a `data` map and a `nextReference` for allocation
-- `readField` / `updateField` / `increment` - heap access functions
-
-Note: The `Box` datatype is generated dynamically by `heapParameterization`
-based on which field types are actually used in the program.
+The heap model runtime interface. These are the types and functions that
+elaboration relies on when translating field access, field write, and
+heap allocation.
+
+Types:
+```
+datatype Composite { MkComposite(ref: int) }
+datatype Heap { MkHeap(data: Map Composite (Map Field Box), nextReference: int) }
+datatype Field { ... }     (zero-arity constructors generated per class field)
+datatype TypeTag { ... }   (zero-arity constructors generated per class)
+datatype Box { ... }       (generated dynamically: BoxInt(intVal: int), BoxString(stringVal: string), etc.)
+```
+
+Functions (all pure, grade = pure):
+```
+readField     : (Heap, Composite, Field) → Box
+updateField   : (Heap, Composite, Field, Box) → Heap
+increment     : (Heap) → Heap
+MkComposite   : (int) → Composite
+MkHeap        : (Map …, int) → Heap
+Heap..data!   : (Heap) → Map Composite (Map Field Box)
+Heap..nextReference! : (Heap) → int
+```
+
+Datatype accessors/testers follow the DDM pattern:
+```
+$field.C.f       : () → Field      (zero-arity, one per class field)
+C_TypeTag        : () → TypeTag    (zero-arity, one per class)
+box_T            : (T) → Box       (e.g. BoxInt, BoxString, BoxComposite)
+unbox_T          : (Box) → T       (e.g. Box..intVal!, Box..stringVal!)
+```
+
+Note: `Box` and `Field` constructors are generated dynamically by the
+elaborator based on which field types and classes are actually used.
 -/
 
 private def laurelPreludeDDM :=
@@ -66,7 +86,20 @@ function increment(heap: Heap): Heap {
 
 #end
 
-/-- The Laurel Core prelude as a Laurel Program. -/
+/-- The heap model runtime as a Laurel Program. Elaboration looks up
+    these functions when translating field access, field write, and allocation.
+```
+readField     : (Heap, Composite, Field) → Box & pure
+updateField   : (Heap, Composite, Field, Box) → Heap & pure
+increment     : (Heap) → Heap & pure
+MkComposite   : (int, TypeTag) → Composite & pure
+Heap..nextReference! : (Heap) → int & pure
+$field.C.f    : () → Field & pure   (generated per class field)
+C_TypeTag     : () → TypeTag & pure (generated per class)
+box_T         : (T) → Box & pure    (generated per field type used)
+unbox_T       : (Box) → T & pure    (generated per field type used)
+```
+-/
 def heapConstants : Program :=
   match Laurel.TransM.run none (Laurel.parseProgram laurelPreludeDDM) with
   | .ok program => program