feat(laurel): Adding surface syntax for calling instance procedures & lowering to Core

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -303,13 +303,20 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       return mkStmtExprMd (.AsType target (mkHighTypeMd (.UserDefined typeName) src)) src
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
-      let calleeName := match callee.val with
-        | .Var (.Local name) => name
-        | _ => ""
       let argsList ← match argsSeq with
         | .seq _ .comma args => args.toList.mapM translateStmtExpr
         | _ => pure []
-      return mkStmtExprMd (.StaticCall calleeName argsList) src
+      -- `obj#method(args)` parses as `call(fieldAccess(obj, method), args)`.
+      -- Treat such calls as instance-method calls; everything else stays a
+      -- static call by callee text (empty when the callee is a higher-order
+      -- expression — preserved to match prior behavior).
+      match callee.val with
+      | .Var (.Field target fieldName) =>
+        return mkStmtExprMd (.InstanceCall target fieldName argsList) src
+      | .Var (.Local name) =>
+        return mkStmtExprMd (.StaticCall name argsList) src
+      | _ =>
+        return mkStmtExprMd (.StaticCall (mkId "") argsList) src
     | q`Laurel.return, #[arg0] =>
       let value ← match arg0 with
         | .option _ (some valArg) => some <$> translateStmtExpr valArg

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -3,9 +3,12 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+-- Grammar updated: renamed Optional* categories (op names updated)
+-- Grammar updated: `call` callee at prec 89 to accept fieldAccess (prec 90) chains
+-- Grammar updated: `fieldAccess` is leftassoc so `a#b#c` parses as `(a#b)#c`
 -- Grammar updated: added bitvector literal support (bvLiteral)
-module
 
+module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -34,13 +34,14 @@ op initializer(value: StmtExpr): Initializer => " := " value:0;
 op varDecl (name: Ident, varType: Option TypeAnnotation, assignment: Option Initializer): StmtExpr
   => @[prec(0)] "var " name varType assignment;
 
-op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
+op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr =>
+  @[prec(95)] callee:89 "(" args ")";
 
 // Instantiation
 op new(name: Ident): StmtExpr => "new " name;
 
-// Field access
-op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field;
+// Field access. `leftassoc` so chained access (`a#b#c`) parses as `(a#b)#c`.
+op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90), leftassoc] obj "#" field;
 
 // Identifiers/Variables - must come after fieldAccess so c.value parses as fieldAccess not identifier
 op identifier (name: Ident): StmtExpr => name;

Strata/Languages/Laurel/HeapParameterization.lean

@@ -286,7 +286,8 @@ where
           | return [⟨ .Hole, source ⟩]
 
         let valTy := (model.get fieldName).getType
-        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget, mkMd (.StaticCall qualifiedName [])], source ⟩
+        let selectTarget' ← recurseOne selectTarget
+        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget', mkMd (.StaticCall qualifiedName [])], source ⟩
         -- Unwrap Box: apply the appropriate destructor
         recordBoxConstructor model valTy.val
         return [mkMd <| .StaticCall (boxDestructorName model valTy.val) [readExpr]]
@@ -544,16 +545,10 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
     return proc
 
 def heapParameterization (model: SemanticModel) (program : Program) : Program :=
-  let program := { program with
-    types := program.types
-    staticProcedures := program.staticProcedures }
-  let instanceProcs := program.types.foldl (fun acc td =>
-    match td with
-    | .Composite ct => acc ++ ct.instanceProcedures
-    | _ => acc) ([] : List Procedure)
-  let allProcs := program.staticProcedures ++ instanceProcs
-  let heapReaders := computeReadsHeap allProcs
-  let heapWriters := computeWritesHeap allProcs
+  -- Instance procedures are already lifted to `staticProcedures` by an earlier
+  -- pass, so they're covered by the calls below.
+  let heapReaders := computeReadsHeap program.staticProcedures
+  let heapWriters := computeWritesHeap program.staticProcedures
   let initState : TransformState := { heapReaders, heapWriters }
   let (procs', state1) := (program.staticProcedures.mapM (heapTransformProcedure model)).run initState
   -- Collect all qualified field names and generate a Field datatype
@@ -563,18 +558,14 @@ def heapParameterization (model: SemanticModel) (program : Program) : Program :=
     | _ => acc) ([] : List Identifier)
   let fieldDatatype : TypeDefinition :=
     .Datatype { name := "Field", typeArgs := [], constructors := fieldNames.map fun n => { name := n, args := [] } }
-  -- Remove fields from composite types since they are now stored in the heap
-  -- Also transform instance procedures, accumulating used Box constructors
-  let (types', state2) := program.types.foldl (fun (accTypes, accState) td =>
+  -- Remove fields from composite types since they are now stored in the heap.
+  let types' := program.types.map fun td =>
     match td with
-    | .Composite ct =>
-      let (instProcs', s') := (ct.instanceProcedures.mapM (heapTransformProcedure model)).run accState
-      (accTypes ++ [.Composite { ct with fields := [], instanceProcedures := instProcs' }], s')
-    | other => (accTypes ++ [other], accState))
-    ([], state1)
+    | .Composite ct => .Composite { ct with fields := [] }
+    | other => other
   -- Generate Box datatype from all constructors used during transformation
   let boxDatatype : TypeDefinition :=
-    .Datatype { name := "Box", typeArgs := [], constructors := state2.usedBoxConstructors }
+    .Datatype { name := "Box", typeArgs := [], constructors := state1.usedBoxConstructors }
   { program with
     staticProcedures := heapConstants.staticProcedures ++ procs',
     types := fieldDatatype :: boxDatatype :: heapConstants.types ++ types' }

Strata/Languages/Laurel/LaurelCompilationPipeline.lean

@@ -18,7 +18,7 @@ import Strata.Languages.Laurel.EliminateDeterministicHoles
 import Strata.Languages.Laurel.CoreDefinitionsForLaurel
 import Strata.Languages.Laurel.LiftImperativeExpressions
 import Strata.Languages.Laurel.ConstrainedTypeElim
-
+import Strata.Languages.Laurel.LiftInstanceProcedures
 import Strata.Languages.Laurel.TypeAliasElim
 public import Strata.Languages.Laurel.LaurelPass
 public import Strata.Languages.Core
@@ -96,6 +96,7 @@ def laurelPipeline : Array LaurelPass := #[
   typeAliasElimPass,
   filterNonCompositeModifiesPass,
   eliminateValueInReturnsPass,
+  liftInstanceProceduresPass,
   heapParameterizationPass,
   typeHierarchyTransformPass,
   modifiesClausesTransformPass,
@@ -183,6 +184,15 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     | none => Strata.Pipeline.PipelineContext.create (outputMode := .quiet)
   runPipelineM options.keepAllFilesPrefix do
     let (program, model, passDiags, stats) ← runLaurelPasses pctx program
+    -- Sanity check: `LiftInstanceProcedures` should have cleared every
+    -- composite's `instanceProcedures` list.
+    let mut passDiags := passDiags
+    for td in program.types do
+      if let .Composite ct := td then
+        for proc in ct.instanceProcedures do
+          passDiags := passDiags ++ [diagnosticFromSource proc.name.source
+            s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' was not lifted before Core translation (pipeline-ordering bug)"
+            DiagnosticType.StrataBug]
     let unorderedCore := transparencyPass program
     emit "transparencyPass" "core.st" unorderedCore
 

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -722,7 +722,6 @@ abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel)
 
 /--
 Translate a `CoreWithLaurelTypes` program to a `Core.Program`.
-The `program` parameter is the lowered Laurel program, used for type definitions.
 -/
 def translateLaurelToCore (options: LaurelTranslateOptions) (ordered : CoreWithLaurelTypes): TranslateM Core.Program := do
 

Strata/Languages/Laurel/LiftInstanceProcedures.lean

@@ -0,0 +1,132 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.Resolution
+public import Strata.Languages.Laurel.LaurelPass
+
+/-!
+# Lift Instance Procedures
+
+A Laurel-to-Laurel pass that lifts every instance procedure (a procedure
+defined inside a `composite` block) to a top-level static procedure with a
+mangled name `<CompositeName>$<methodName>`, then rewrites every call site
+that resolved to such an instance procedure to use the lifted name.
+
+After this pass:
+- `CompositeType.instanceProcedures` is empty for every composite.
+- `program.staticProcedures` contains the lifted procedures.
+- Every `InstanceCall` (from `obj#method(args)` surface syntax) points
+  at the lifted name. For `InstanceCall`, the receiver is prepended to
+  the argument list to match the lifted procedure's `self : <CompositeName>`
+  parameter.
+-/
+
+namespace Strata.Laurel
+
+/-! ## Lifting + call-site rewriting
+
+Lift instance procedures to static scope (e.g., procedure `proc`
+of composite type `T` will be lifted to `T$proc`).
+Then, rewrite caller-side of `obj#proc` to call the lifted procedure
+
+-/
+
+/-- Top-level name produced for a lifted instance procedure. -/
+def liftedProcName (typeName methodName : Identifier) : Identifier :=
+  mkId s!"{typeName.text}${methodName.text}"
+
+/-- Rewrite a single node so that any callee resolving to an instance procedure
+    is replaced by its lifted name. -/
+private def rewriteCallNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd :=
+  match expr.val with
+  | .StaticCall callee args =>
+    match model.get? callee with
+    | some (.instanceProcedure typeName _) =>
+      let lifted := liftedProcName typeName callee
+      { expr with val := .StaticCall lifted args }
+    | _ => expr
+  | .InstanceCall target callee args =>
+    -- `obj#method(args)` surface syntax parses to InstanceCall. Flatten it to
+    -- a static call against the lifted name, prepending the receiver as the
+    -- first argument to match the lifted procedure's `self` parameter.
+    match model.get? callee with
+    | some (.instanceProcedure typeName _) =>
+      let lifted := liftedProcName typeName callee
+      { expr with val := .StaticCall lifted (target :: args) }
+    | _ => expr
+  | _ => expr
+
+/-- Apply call-site rewriting to every expression in a procedure. -/
+private def rewriteCallsInProc (model : SemanticModel) (proc : Procedure) : Procedure :=
+  let f := mapStmtExpr (rewriteCallNode model)
+  let resolveBody : Body → Body := fun body => match body with
+    | .Transparent b => .Transparent (f b)
+    | .Opaque ps impl modif =>
+      .Opaque (ps.map (·.mapCondition f)) (impl.map f) (modif.map f)
+    | .Abstract ps => .Abstract (ps.map (·.mapCondition f))
+    | .External => .External
+  { proc with
+    body := resolveBody proc.body
+    preconditions := proc.preconditions.map (·.mapCondition f)
+    decreases := proc.decreases.map f
+    invokeOn := proc.invokeOn.map f }
+
+/-- Apply call-site rewriting to a constrained type's constraint and witness. -/
+private def rewriteCallsInType (model : SemanticModel) (td : TypeDefinition) : TypeDefinition :=
+  match td with
+  | .Constrained ct =>
+    let f := mapStmtExpr (rewriteCallNode model)
+    .Constrained { ct with constraint := f ct.constraint, witness := f ct.witness }
+  | _ => td
+
+public section
+
+/--
+Lift every `proc ∈ ct.instanceProcedures` to a top-level static procedure
+named via `liftedProcName`, rewrite call sites that resolved to an instance
+procedure, and clear `instanceProcedures` on every composite.
+-/
+def liftInstanceProcedures (model : SemanticModel) (program : Program) : Program :=
+  -- Step 1: collect lifted clones
+  let liftedProcs : List Procedure :=
+    program.types.foldl (init := []) fun acc td =>
+      match td with
+      | .Composite ct =>
+        acc ++ ct.instanceProcedures.map fun proc =>
+          { proc with name := liftedProcName ct.name proc.name }
+      | _ => acc
+
+  if liftedProcs.isEmpty then program else
+
+  -- Step 2: rewrite call sites in procedure bodies and constrained-type
+  let rewrittenStaticProcs := program.staticProcedures.map (rewriteCallsInProc model)
+  let rewrittenLiftedProcs := liftedProcs.map (rewriteCallsInProc model)
+  let rewrittenTypes := program.types.map (rewriteCallsInType model)
+
+  -- Step 3: clear instanceProcedures on every composite.
+  let cleanedTypes := rewrittenTypes.map fun td =>
+    match td with
+    | .Composite ct => .Composite { ct with instanceProcedures := [] }
+    | _ => td
+
+  -- Step 4: append lifted procs.
+  { program with
+    staticProcedures := rewrittenStaticProcs ++ rewrittenLiftedProcs
+    types := cleanedTypes }
+
+end -- public section
+
+/-- Pipeline pass: lift instance procedures to top-level static procedures
+    and rewrite call sites to use the lifted names. -/
+public def liftInstanceProceduresPass : LaurelPass where
+  name := "LiftInstanceProcedures"
+  documentation := "Lifts every procedure declared inside a `composite` block to a top-level static procedure named `<CompositeName>$<methodName>` and rewrites call sites resolved to an instance procedure (including `obj#method(args)` surface syntax) to point at the lifted name. Clears `instanceProcedures` on every composite. Must run before HeapParameterization."
+  needsResolves := true
+  run := fun p m => (liftInstanceProcedures m p, [], {})
+
+end Strata.Laurel

Strata/Languages/Laurel/Resolution.lean

@@ -158,18 +158,42 @@ def resolveRef (name : Identifier) (source : Option FileRange := none)
     modify fun s => { s with errors := s.errors.push diag }
     return { name with uniqueId := none }
 
+/-- Scope key for a name nested inside a container (composite, datatype),
+    used to disambiguate members in the flat global scope. -/
+private def containerScopedName (containerName memberName : Identifier) : Identifier :=
+  mkId s!"{containerName.text}${memberName.text}"
+
 /-- Extract the UserDefined type name from a resolved target expression by looking up its scope entry. -/
 private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := do
   let s ← get
-  match target.val with
+  match _h : target.val with
   | .Var (.Local ref) =>
     match s.scope.get? ref.text with
     | some (_, node) =>
       match node.getType.val with
       | .UserDefined typRef => pure (some typRef.text)
       | _ => pure none
     | none => pure none
+  | .Var (.Field inner fieldName) => do
+    match (← targetTypeName inner) with
+    | none => pure none
+    | some innerTy =>
+      match s.typeScopes.get? innerTy with
+      | none => pure none
+      | some typeScope =>
+        match typeScope.get? fieldName.text with
+        | some (_, node) =>
+          match node.getType.val with
+          | .UserDefined typRef => pure (some typRef.text)
+          | _ => pure none
+        | none => pure none
   | _ => pure none
+  termination_by sizeOf target
+  decreasing_by
+    have := AstNode.sizeOf_val_lt target
+    have : sizeOf target.val = sizeOf (StmtExpr.Var (Variable.Field inner fieldName)) := congrArg sizeOf _h
+    simp at this
+    omega
 
 /-- Try to resolve a field name via a type scope lookup. Returns `some id` on success. -/
 private def resolveFieldInTypeScope (typeName : String) (fieldName : Identifier) : ResolveM (Option Identifier) := do
@@ -456,8 +480,16 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do
     pure (.IsType target' ty')
   | .InstanceCall target callee args =>
     let target' ← resolveStmtExpr target
-    let callee' ← resolveRef callee source
+    -- Look up under the container-scoped key matching `preRegisterTopLevel`.
+    -- Fall back to the bare name when the target's type can't be determined.
+    let lookupKey ← match (← targetTypeName target') with
+      | some tyName => pure (containerScopedName (mkId tyName) callee)
+      | none => pure callee
+    let resolved ← resolveRef lookupKey source
       (expected := #[.instanceProcedure, .staticProcedure])
+    -- Preserve the user-facing callee text for diagnostics;
+    -- only stamp the resolved `uniqueId` from the lifted lookup.
+    let callee' := { callee with uniqueId := resolved.uniqueId }
     let args' ← args.mapM resolveStmtExpr
     pure (.InstanceCall target' callee' args')
   | .Quantifier mode param trigger body =>
@@ -557,7 +589,9 @@ def resolveField (ownerName : Identifier) (field : Field) : ResolveM Field := do
 
 /-- Resolve an instance procedure on a composite type. -/
 def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : ResolveM Procedure := do
-  let procName' ← resolveRef proc.name
+  let scopedKey := containerScopedName typeName proc.name
+  let resolved ← resolveRef scopedKey
+  let procName' := { proc.name with uniqueId := resolved.uniqueId }
   withScope do
     let savedInstType := (← get).instanceTypeName
     modify fun s => { s with instanceTypeName := some typeName.text }
@@ -955,7 +989,9 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
         let qualifiedName := ct.name.text ++ "." ++ field.name.text
         let _ ← defineNameCheckDup field.name (.field ct.name field) (some qualifiedName)
       for proc in ct.instanceProcedures do
+        let scopedKey := (containerScopedName ct.name proc.name).text
         let _ ← defineNameCheckDup proc.name (.instanceProcedure ct.name proc)
+                                   (some scopedKey)
     | .Constrained ct =>
       let _ ← defineNameCheckDup ct.name (.constrainedType ct)
     | .Datatype dt =>
@@ -989,15 +1025,6 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
 public def resolve (program : Program) (existingModel: Option SemanticModel := none) : ResolutionResult :=
   -- Phase 1: pre-register all top-level names, then assign IDs and resolve references
   let phase1 : ResolveM Program := do
-
-    for td in program.types do
-      if let .Composite ct := td then
-        for proc in ct.instanceProcedures do
-          let diag := diagnosticFromSource proc.name.source
-            s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' is not yet supported"
-            DiagnosticType.NotYetImplemented
-          modify fun s => { s with errors := s.errors.push diag }
-
     preRegisterTopLevel program
     let types' ← program.types.mapM resolveTypeDefinition
     let constants' ← program.constants.mapM resolveConstant

StrataTest/Languages/Laurel/DuplicateNameTests.lean

@@ -61,10 +61,8 @@ procedure foo(x: int, x: bool) opaque { };
 program Laurel;
 composite Foo {
   procedure bar() opaque { };
-//          ^^^ not-yet-implemented: Instance procedure 'bar' on composite type 'Foo' is not yet supported
   procedure bar() opaque { };
-//          ^^^ not-yet-implemented: Instance procedure 'bar' on composite type 'Foo' is not yet supported
-//          ^^^ error: Duplicate definition 'bar' is already defined in this scope
+//          ^^^ error: Duplicate definition 'Foo$bar' is already defined in this scope
 }
 #end