Mutable fields

Strata/DDM/Elab.lean

@@ -394,7 +394,6 @@ def elabDialect
     elabDialectRest fm dialects #[] inputContext loc dialect startPos stopPos
 
 def parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (input : InputContext) : IO Strata.Program := do
-
   let leanEnv ← Lean.mkEmptyEnvironment 0
 
   let isTrue mem := inferInstanceAs (Decidable (dialect ∈ dialects.dialects))

Strata/Languages/Boogie/Verifier.lean

@@ -485,18 +485,19 @@ structure Diagnostic where
   message : String
   deriving Repr, BEq
 
-def toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Boogie.VCResult) : Option Diagnostic := do
+def DiagnosticModel.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (dm: DiagnosticModel): Diagnostic :=
+  let fileMap := (files.find? dm.fileRange.file).get!
+  let startPos := fileMap.toPosition dm.fileRange.range.start
+  let endPos := fileMap.toPosition dm.fileRange.range.stop
+  {
+    start := { line := startPos.line, column := startPos.column }
+    ending := { line := endPos.line, column := endPos.column }
+    message := dm.message
+  }
+
+def Boogie.VCResult.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Boogie.VCResult) : Option Diagnostic := do
   let modelOption := toDiagnosticModel vcr
-  modelOption.map (fun dm =>
-      let fileMap := (files.find? dm.fileRange.file).get!
-      let startPos := fileMap.toPosition dm.fileRange.range.start
-      let endPos := fileMap.toPosition dm.fileRange.range.stop
-      {
-        start := { line := startPos.line, column := startPos.column }
-        ending := { line := endPos.line, column := endPos.column }
-        message := dm.message
-      }
-    )
+  modelOption.map (fun dm => dm.toDiagnostic files)
 
 end Strata
 

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -10,6 +10,7 @@ import Strata.Languages.Laurel.Laurel
 import Strata.DL.Imperative.MetaData
 import Strata.Languages.Boogie.Expressions
 
+namespace Strata
 namespace Laurel
 
 open Std (ToFormat Format format)
@@ -79,10 +80,13 @@ instance : Inhabited Parameter where
 def translateHighType (arg : Arg) : TransM HighType := do
   match arg with
   | .op op =>
-    match op.name with
-    | q`Laurel.intType => return .TInt
-    | q`Laurel.boolType => return .TBool
-    | _ => TransM.error s!"translateHighType expects intType or boolType, got {repr op.name}"
+    match op.name, op.args with
+    | q`Laurel.intType, _ => return .TInt
+    | q`Laurel.boolType, _ => return .TBool
+    | q`Laurel.compositeType, #[nameArg] =>
+      let name ← translateIdent nameArg
+      return .UserDefined name
+    | _, _ => TransM.error s!"translateHighType expects intType, boolType or compositeType, got {repr op.name}"
   | _ => TransM.error s!"translateHighType expects operation"
 
 def translateNat (arg : Arg) : TransM Nat := do
@@ -116,8 +120,6 @@ instance : Inhabited Procedure where
     outputs := []
     precondition := .LiteralBool true
     decreases := none
-    determinism := Determinism.deterministic none
-    modifies := none
     body := .Transparent (.LiteralBool true)
   }
 
@@ -157,8 +159,8 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
       let varType ← match typeArg with
         | .option _ (some (.op typeOp)) => match typeOp.name, typeOp.args with
           | q`Laurel.optionalType, #[typeArg0] => translateHighType typeArg0
-          | _, _ => pure .TInt
-        | _ => pure .TInt
+          | _, _ => TransM.error s!"Variable {name} requires explicit type"
+        | _ => TransM.error s!"Variable {name} requires explicit type"
       let value ← match assignArg with
         | .option _ (some (.op assignOp)) => match assignOp.args with
           | #[assignArg0] => translateStmtExpr assignArg0 >>= (pure ∘ some)
@@ -173,7 +175,8 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
       let value ← translateStmtExpr arg1
-      return .Assign target value
+      let md ← getArgMetaData (.op op)
+      return .Assign target value md
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
       let calleeName := match callee with
@@ -195,6 +198,10 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
           | _, _ => pure none
         | _ => pure none
       return .IfThenElse cond thenBranch elseBranch
+    | q`Laurel.fieldAccess, #[objArg, fieldArg] =>
+      let obj ← translateStmtExpr objArg
+      let field ← translateIdent fieldArg
+      return .FieldSelect obj field
     | _, #[arg0, arg1] => match getBinaryOp? op.name with
       | some primOp =>
         let lhs ← translateStmtExpr arg0
@@ -223,32 +230,73 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     | TransM.error s!"parseProcedure expects operation"
 
   match op.name, op.args with
-  | q`Laurel.procedure, #[arg0, arg1, returnParamsArg, arg3] =>
-    let name ← translateIdent arg0
-    let parameters ← translateParameters arg1
-    -- returnParamsArg is ReturnParameters category, need to unwrap returnParameters operation
-    let returnParameters ← match returnParamsArg with
-      | .option _ (some (.op returnOp)) => match returnOp.name, returnOp.args with
-        | q`Laurel.returnParameters, #[returnArg0] => translateParameters returnArg0
-        | _, _ => TransM.error s!"Expected returnParameters operation, got {repr returnOp.name}"
-      | .option _ none => pure []
-      | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}"
-    let body ← translateCommand arg3
+  | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
+      requiresArg, ensuresArg, bodyArg] =>
+    let name ← translateIdent nameArg
+    let parameters ← translateParameters paramArg
+    -- Either returnTypeArg or returnParamsArg may have a value, not both
+    -- If returnTypeArg is set, create a single "result" parameter
+    let returnParameters ← match returnTypeArg with
+      | .option _ (some (.op returnTypeOp)) => match returnTypeOp.name, returnTypeOp.args with
+        | q`Laurel.optionalReturnType, #[typeArg] =>
+          let retType ← translateHighType typeArg
+          pure [{ name := "result", type := retType : Parameter }]
+        | _, _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeOp.name}"
+      | .option _ none =>
+        -- No return type, check returnParamsArg instead
+        match returnParamsArg with
+        | .option _ (some (.op returnOp)) => match returnOp.name, returnOp.args with
+          | q`Laurel.returnParameters, #[returnArg0] => translateParameters returnArg0
+          | _, _ => TransM.error s!"Expected returnParameters operation, got {repr returnOp.name}"
+        | .option _ none => pure []
+        | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}"
+      | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}"
+    -- Parse precondition (requires clause)
+    let precondition ← match requiresArg with
+      | .option _ (some (.op requiresOp)) => match requiresOp.name, requiresOp.args with
+        | q`Laurel.optionalRequires, #[exprArg] => translateStmtExpr exprArg
+        | _, _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresOp.name}"
+      | .option _ none => pure (.LiteralBool true)
+      | _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresArg}"
+    -- Parse postcondition (ensures clause)
+    let postcondition ← match ensuresArg with
+      | .option _ (some (.op ensuresOp)) => match ensuresOp.name, ensuresOp.args with
+        | q`Laurel.optionalEnsures, #[exprArg] => translateStmtExpr exprArg >>= (pure ∘ some)
+        | _, _ => TransM.error s!"Expected optionalEnsures operation, got {repr ensuresOp.name}"
+      | .option _ none => pure none
+      | _ => TransM.error s!"Expected optionalEnsures operation, got {repr ensuresArg}"
+    let body ← translateCommand bodyArg
+    -- If there's a postcondition, use Opaque body; otherwise use Transparent
+    let procBody := match postcondition with
+      | some post => Body.Opaque post (some body) .nondeterministic none
+      | none => Body.Transparent body
     return {
       name := name
       inputs := parameters
       outputs := returnParameters
-      precondition := .LiteralBool true
+      precondition := precondition
       decreases := none
-      determinism := Determinism.deterministic none
-      modifies := none
-      body := .Transparent body
+      body := procBody
     }
   | q`Laurel.procedure, args =>
-    TransM.error s!"parseProcedure expects 4 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 7 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure, got {repr op.name}"
 
+def parseTopLevel (arg : Arg) : TransM (Option Procedure) := do
+  let .op op := arg
+    | TransM.error s!"parseTopLevel expects operation"
+
+  match op.name, op.args with
+  | q`Laurel.topLevelProcedure, #[procArg] =>
+    let proc ← parseProcedure procArg
+    return some proc
+  | q`Laurel.topLevelComposite, #[_compositeArg] =>
+    -- TODO: handle composite types
+    return none
+  | _, _ =>
+    TransM.error s!"parseTopLevel expects topLevelProcedure or topLevelComposite, got {repr op.name}"
+
 /--
 Translate concrete Laurel syntax into abstract Laurel syntax
 -/
@@ -270,11 +318,10 @@ def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do
 
   let mut procedures : List Procedure := []
   for op in commands do
-    if op.name == q`Laurel.procedure then
-      let proc ← parseProcedure (.op op)
-      procedures := procedures ++ [proc]
-    else
-      TransM.error s!"Unknown top-level declaration: {op.name}"
+    let result ← parseTopLevel (.op op)
+    match result with
+    | some proc => procedures := procedures ++ [proc]
+    | none => pure () -- composite types are skipped for now
   return {
     staticProcedures := procedures
     staticFields := []

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -4,6 +4,7 @@ dialect Laurel;
 category LaurelType;
 op intType : LaurelType => "int";
 op boolType : LaurelType => "bool";
+op compositeType (name: Ident): LaurelType => name;
 
 category StmtExpr;
 op literalBool (b: Bool): StmtExpr => b;
@@ -19,12 +20,17 @@ op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0;
 op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr
   => @[prec(0)] "var " name varType assignment ";";
 
-// Identifiers/Variables
+op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
+
+// Field access
+op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field;
+
+// Identifiers/Variables - must come after fieldAccess so c.value parses as fieldAccess not identifier
 op identifier (name: Ident): StmtExpr => name;
 op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
 
 // Assignment
-op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
+op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target ":=" value ";";
 
 // Binary operators
 op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
@@ -35,8 +41,6 @@ op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<" rhs;
 op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<=" rhs;
 op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">=" rhs;
 
-op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
-
 // If-else
 category OptionalElse;
 op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts;
@@ -52,13 +56,38 @@ op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
 category Parameter;
 op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
 
+// Composite types
+category Field;
+op mutableField (name: Ident, fieldType: LaurelType): Field => "var " name ":" fieldType;
+op immutableField (name: Ident, fieldType: LaurelType): Field => name ":" fieldType;
+
+category Composite;
+op composite (name: Ident, fields: Seq Field): Composite => "composite " name "{" fields "}";
+
+// Procedures
+category OptionalReturnType;
+op optionalReturnType(returnType: LaurelType): OptionalReturnType => ":" returnType;
+
+category OptionalRequires;
+op optionalRequires(cond: StmtExpr): OptionalRequires => "requires" cond:0;
+
+category OptionalEnsures;
+op optionalEnsures(cond: StmtExpr): OptionalEnsures => "ensures" cond:0;
+
 category ReturnParameters;
 op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
 
 category Procedure;
 op procedure (name : Ident, parameters: CommaSepBy Parameter,
+  returnType: Option OptionalReturnType,
   returnParameters: Option ReturnParameters,
+  requires: Option OptionalRequires,
+  ensures: Option OptionalEnsures,
   body : StmtExpr) : Procedure =>
-  "procedure " name "(" parameters ")" returnParameters body:0;
+  "procedure " name "(" parameters ")" returnType returnParameters requires ensures body:0;
+
+category TopLevel;
+op topLevelComposite(composite: Composite): TopLevel => composite;
+op topLevelProcedure(procedure: Procedure): TopLevel => procedure;
 
-op program (staticProcedures: Seq Procedure): Command => staticProcedures;
+op program (items: Seq TopLevel): Command => items;