Laurel Language Enhancements

.gitignore

@@ -5,3 +5,4 @@
 vcs/*.smt2
 
 Strata.code-workspace
+*.conv

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -74,9 +74,11 @@ def translateBool (arg : Arg) : TransM Bool := do
 instance : Inhabited Parameter where
   default := { name := "", type := ⟨.TVoid, #[]⟩ }
 
+/-- Create a HighTypeMd with the given metadata -/
 def mkHighTypeMd (t : HighType) (md : MetaData Core.Expression) : HighTypeMd := ⟨t, md⟩
+
+/-- Create a StmtExprMd with the given metadata -/
 def mkStmtExprMd (e : StmtExpr) (md : MetaData Core.Expression) : StmtExprMd := ⟨e, md⟩
-def mkStmtExprMdEmpty (e : StmtExpr) : StmtExprMd := ⟨e, #[]⟩
 
 partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
   let md ← getArgMetaData arg
@@ -86,10 +88,13 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
     | q`Laurel.intType, _ => return mkHighTypeMd .TInt md
     | q`Laurel.boolType, _ => return mkHighTypeMd .TBool md
     | q`Laurel.stringType, _ => return mkHighTypeMd .TString md
+    | q`Laurel.arrayType, #[elemArg] =>
+      let elemType ← translateHighType elemArg
+      return mkHighTypeMd (.Applied (mkHighTypeMd (.UserDefined "Array") md) [elemType]) md
     | q`Laurel.compositeType, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkHighTypeMd (.UserDefined name) md
-    | _, _ => TransM.error s!"translateHighType expects intType, boolType, arrayType or compositeType, got {repr op.name}"
+    | _, _ => TransM.error s!"translateHighType expects intType, boolType, stringType, arrayType or compositeType, got {repr op.name}"
   | _ => TransM.error s!"translateHighType expects operation"
 
 def translateNat (arg : Arg) : TransM Nat := do
@@ -242,6 +247,10 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let field ← translateIdent fieldArg
       let fieldMd ← getArgMetaData fieldArg
       return mkStmtExprMd (.FieldSelect obj field) fieldMd
+    | q`Laurel.arrayIndex, #[arrArg, idxArg] =>
+      let arr ← translateStmtExpr arrArg
+      let idx ← translateStmtExpr idxArg
+      return mkStmtExprMd (.StaticCall "Array.Get" [arr, idx]) md
     | q`Laurel.while, #[condArg, invSeqArg, bodyArg] =>
       let cond ← translateStmtExpr condArg
       let invariants ← match invSeqArg with
@@ -253,6 +262,11 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
         | _ => pure []
       let body ← translateStmtExpr bodyArg
       return mkStmtExprMd (.While cond invariants none body) md
+    | _, #[arg0] => match getUnaryOp? op.name with
+      | some primOp =>
+        let inner ← translateStmtExpr arg0
+        return mkStmtExprMd (.PrimitiveOp primOp [inner]) md
+      | none => TransM.error s!"Unknown unary operation: {op.name}"
     | q`Laurel.forallExpr, #[nameArg, tyArg, bodyArg] =>
       let name ← translateIdent nameArg
       let ty ← translateHighType tyArg
@@ -263,11 +277,6 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let ty ← translateHighType tyArg
       let body ← translateStmtExpr bodyArg
       return mkStmtExprMd (.Exists name ty body) md
-    | _, #[arg0] => match getUnaryOp? op.name with
-      | some primOp =>
-        let inner ← translateStmtExpr arg0
-        return mkStmtExprMd (.PrimitiveOp primOp [inner]) md
-      | none => TransM.error s!"Unknown unary operation: {op.name}"
     | _, #[arg0, arg1] => match getBinaryOp? op.name with
       | some primOp =>
         let lhs ← translateStmtExpr arg0
@@ -278,8 +287,10 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
   | _ => TransM.error s!"translateStmtExpr expects operation"
 
 partial def translateSeqCommand (arg : Arg) : TransM (List StmtExprMd) := do
-  let .seq _ .none args := arg
-    | TransM.error s!"translateSeqCommand expects seq"
+  let args ← match arg with
+    | .seq _ .none args => pure args
+    | .seq _ .newline args => pure args  -- NewlineSepBy for block statements
+    | _ => TransM.error s!"translateSeqCommand expects seq or newlineSepBy"
   let mut stmts : List StmtExprMd := []
   for arg in args do
     let stmt ← translateStmtExpr arg
@@ -356,15 +367,20 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
         | .option _ none => pure []
         | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}"
       | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}"
-    -- Parse preconditions (requires clause)
+    -- Parse preconditions (requires clauses)
     let preconditions ← match requiresArg with
       | .option _ (some (.op requiresOp)) => match requiresOp.name, requiresOp.args with
         | q`Laurel.optionalRequires, #[exprArg] => do
           let precond ← translateStmtExpr exprArg
           pure [precond]
         | _, _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresOp.name}"
       | .option _ none => pure []
-      | _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresArg}"
+      | .seq _ _ clauses => clauses.toList.mapM fun arg => match arg with
+          | .op reqOp => match reqOp.name, reqOp.args with
+            | q`Laurel.requiresClause, #[exprArg] => translateStmtExpr exprArg
+            | _, _ => TransM.error "Expected requiresClause"
+          | _ => TransM.error "Expected operation"
+      | _ => pure []
     -- Parse postconditions (ensures clauses - zero or more)
     let postconditions ← translateEnsuresClauses ensuresArg
     -- Parse modifies clauses (zero or more)
@@ -398,6 +414,20 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}"
 
+def parseConstrainedType (arg : Arg) : TransM ConstrainedType := do
+  let .op op := arg
+    | TransM.error s!"parseConstrainedType expects operation"
+  match op.name, op.args with
+  | q`Laurel.constrainedType, #[nameArg, valueNameArg, baseArg, constraintArg, witnessArg] =>
+    let name ← translateIdent nameArg
+    let valueName ← translateIdent valueNameArg
+    let base ← translateHighType baseArg
+    let constraint ← translateStmtExpr constraintArg
+    let witness ← translateStmtExpr witnessArg
+    return { name, base, valueName, constraint, witness }
+  | _, _ =>
+    TransM.error s!"parseConstrainedType expects constrainedType, got {repr op.name}"
+
 def parseField (arg : Arg) : TransM Field := do
   let .op op := arg
     | TransM.error s!"parseField expects operation"
@@ -435,19 +465,26 @@ def parseComposite (arg : Arg) : TransM TypeDefinition := do
   | _, _ =>
     TransM.error s!"parseComposite expects composite, got {repr op.name}"
 
-def parseTopLevel (arg : Arg) : TransM (Option Procedure × Option TypeDefinition) := do
+inductive TopLevelItem where
+  | proc (p : Procedure)
+  | typeDef (t : TypeDefinition)
+
+def parseTopLevel (arg : Arg) : TransM (Option TopLevelItem) := 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, none)
+    return some (.proc proc)
   | q`Laurel.topLevelComposite, #[compositeArg] =>
     let typeDef ← parseComposite compositeArg
-    return (none, some typeDef)
+    return some (.typeDef typeDef)
+  | q`Laurel.topLevelConstrainedType, #[ctArg] =>
+    let ct ← parseConstrainedType ctArg
+    return some (.typeDef (.Constrained ct))
   | _, _ =>
-    TransM.error s!"parseTopLevel expects topLevelProcedure or topLevelComposite, got {repr op.name}"
+    TransM.error s!"parseTopLevel expects topLevelProcedure, topLevelComposite, or topLevelConstrainedType, got {repr op.name}"
 
 /--
 Translate concrete Laurel syntax into abstract Laurel syntax
@@ -471,13 +508,11 @@ def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do
   let mut procedures : List Procedure := []
   let mut types : List TypeDefinition := []
   for op in commands do
-    let (procOpt, typeOpt) ← parseTopLevel (.op op)
-    match procOpt with
-    | some proc => procedures := procedures ++ [proc]
-    | none => pure ()
-    match typeOpt with
-    | some typeDef => types := types ++ [typeDef]
-    | none => pure ()
+    let result ← parseTopLevel (.op op)
+    match result with
+    | some (.proc proc) => procedures := procedures ++ [proc]
+    | some (.typeDef td) => types := types ++ [td]
+    | none => pure () -- composite types are skipped for now
   return {
     staticProcedures := procedures
     staticFields := []

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -12,3 +12,5 @@ import Strata.DDM.Integration.Lean
 namespace Strata.Laurel
 
 #load_dialect "./LaurelGrammar.st"
+-- Rebuild trigger: merged grammar
+-- Grammar updated for multiple requires

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -7,6 +7,7 @@ category LaurelType;
 op intType : LaurelType => "int";
 op boolType : LaurelType => "bool";
 op stringType : LaurelType => "string";
+op arrayType (elemType: LaurelType): LaurelType => "Array" "<" elemType ">";
 op compositeType (name: Ident): LaurelType => name;
 
 category StmtExpr;
@@ -32,6 +33,9 @@ op new(name: Ident): StmtExpr => "new " name;
 // Field access
 op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field;
 
+// Array indexing
+op arrayIndex (arr: StmtExpr, idx: StmtExpr): StmtExpr => @[prec(90)] arr "[" idx "]";
+
 // 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 ")";
@@ -110,11 +114,11 @@ op composite (name: Ident, extending: Option OptionalExtends, fields: Seq Field)
 category OptionalReturnType;
 op optionalReturnType(returnType: LaurelType): OptionalReturnType => ":" returnType;
 
-category OptionalRequires;
-op optionalRequires(cond: StmtExpr): OptionalRequires => "requires" cond:0;
+category RequiresClause;
+op requiresClause(cond: StmtExpr): RequiresClause => "requires " cond:0;
 
 category EnsuresClause;
-op ensuresClause(cond: StmtExpr): EnsuresClause => "ensures" cond:0;
+op ensuresClause(cond: StmtExpr): EnsuresClause => "ensures " cond:0;
 
 category ModifiesClause;
 op modifiesClause(refs: CommaSepBy StmtExpr): ModifiesClause => "modifies" refs;
@@ -129,7 +133,7 @@ category Procedure;
 op procedure (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option OptionalReturnType,
   returnParameters: Option ReturnParameters,
-  requires: Option OptionalRequires,
+  requires: NewlineSepBy RequiresClause,
   ensures: Seq EnsuresClause,
   modifies: Seq ModifiesClause,
   body : Option OptionalBody) : Procedure =>
@@ -138,14 +142,21 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
 op function (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option OptionalReturnType,
   returnParameters: Option ReturnParameters,
-  requires: Option OptionalRequires,
+  requires: NewlineSepBy RequiresClause,
   ensures: Seq EnsuresClause,
   modifies: Seq ModifiesClause,
   body : Option OptionalBody) : Procedure =>
   "function " name "(" parameters ")" returnType returnParameters requires ensures modifies body;
 
+// Constrained types
+category ConstrainedType;
+op constrainedType (name: Ident, valueName: Ident, base: LaurelType,
+                    constraint: StmtExpr, witness: StmtExpr): ConstrainedType
+  => "constrained " name " = " valueName ": " base " where " constraint:0 " witness " witness:0;
+
 category TopLevel;
 op topLevelComposite(composite: Composite): TopLevel => composite;
 op topLevelProcedure(procedure: Procedure): TopLevel => procedure;
+op topLevelConstrainedType(ct: ConstrainedType): TopLevel => ct;
 
 op program (items: Seq TopLevel): Command => items;

Strata/Languages/Laurel/LaurelEval.lean

@@ -252,20 +252,20 @@ partial def eval (expr : StmtExpr) : Eval TypedValue :=
     let tv ← eval valExpr
     withResult (EvalResult.Return tv.val)
   | StmtExpr.Return none => fun env => (EvalResult.Success { val := Value.VVoid, ty := env.returnType }, env)
-  | StmtExpr.While _ [] none _  => withResult <| EvalResult.TypeError "While invariant was not derived"
+  | StmtExpr.While _ none _ _  => withResult <| EvalResult.TypeError "While invariant was not derived"
   | StmtExpr.While _ _ none _  => withResult <| EvalResult.TypeError "While decreases was not derived"
-  | StmtExpr.While condExpr invariantExprs (some decreasedExpr) bodyExpr => do
+  | StmtExpr.While condExpr (some invariantExpr) (some decreasedExpr) bodyExpr => do
     let rec loop : Eval TypedValue := do
       let cond ← eval condExpr
       if (cond.ty.isBool) then
         withResult <| EvalResult.TypeError "Condition must be boolean"
       else if cond.val.asBool! then
-        for invariantExpr in invariantExprs do
-          let invariant ← eval invariantExpr
-          if (invariant.ty.isBool) then
-            withResult <| EvalResult.TypeError "Invariant must be boolean"
-          else if (!invariant.val.asBool!) then
-            withResult <| EvalResult.VerficationError VerificationErrorType.InvariantFailed "While invariant does not hold"
+        let invariant ← eval invariantExpr
+        if (invariant.ty.isBool) then
+          withResult <| EvalResult.TypeError "Invariant must be boolean"
+        else if (!invariant.val.asBool!) then
+          withResult <| EvalResult.VerficationError VerificationErrorType.InvariantFailed "While invariant does not hold"
+        else
         -- TODO handle decreases
           fun env => match eval bodyExpr env with
             | (EvalResult.Success _, env') => loop env'