Add a resolution phase to Laurel

Strata/DDM/Elab/Core.lean

@@ -250,7 +250,6 @@ def translateQualifiedIdent (t : Tree) : MaybeQualifiedIdent :=
   | q`Init.qualifiedIdentImplicit, 1 => Id.run do
     let .ident _ name := args[0]
       | return panic! "Expected ident"
-    let name := name.dropPrefix "«" |>.dropSuffix "»" |>.toString
     match name.splitOn "." with
     | [dialect, rest] => .qid { dialect, name := rest }
     | _ => .name name
@@ -1448,7 +1447,7 @@ partial def catElaborator (c : SyntaxCat) : TypingContext → Syntax → ElabM T
     fun tctx stx => do
       let some loc := mkSourceRange? stx
         | panic! "ident missing source location"
-      let info : IdentInfo := { inputCtx := tctx, loc := loc, val := stx.getId.toString }
+      let info : IdentInfo := { inputCtx := tctx, loc := loc, val := stx.getId.toString (escape := false) }
       pure <| .node (.ofIdentInfo info) #[]
   | q`Init.Num =>
     fun tctx stx => do

Strata/DDM/Format.lean

@@ -61,11 +61,6 @@ Strips Lean's «» notation if present.
 Follows SMT-LIB 2.6 specification for quoted symbols.
 -/
 private def formatIdent (s : String) : Format :=
-  -- Strip Lean's «» notation if present
-  let s := if s.startsWith "«" && s.endsWith "»" then
-             s.drop 1 |>.dropEnd 1 |>.toString
-           else
-             s
   if needsPipeDelimiters s then
     Format.text ("|" ++ escapePipeIdent s ++ "|")
   else

Strata/Languages/Core/Verifier.lean

@@ -522,7 +522,8 @@ structure Diagnostic where
   deriving Repr, BEq
 
 def DiagnosticModel.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (dm: DiagnosticModel): Diagnostic :=
-  let fileMap := (files.find? dm.fileRange.file).getD (panic s!"Could not find {repr dm.fileRange.file} in {repr files.keys} when converting model '{dm}' to a diagnostic")
+  let fileMap := (files.find? dm.fileRange.file).getD
+    (dbg_trace s!"Could not find {repr dm.fileRange.file} in {repr files.keys} when converting model '{dm}' to a diagnostic"; default)
   let startPos := fileMap.toPosition dm.fileRange.range.start
   let endPos := fileMap.toPosition dm.fileRange.range.stop
   {

Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean

@@ -0,0 +1,46 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.AST
+import Strata.Languages.Laurel.Grammar.LaurelGrammar
+import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
+
+namespace Strata.Laurel
+
+/--
+Core map operations (`select`, `update`, `const`) expressed in Laurel syntax.
+These are polymorphic map primitives used by the Laurel-to-Core translator.
+Since Laurel doesn't have polymorphic types, `int` is used as a placeholder type
+for all parameters — the actual types are inferred during Core translation.
+-/
+def coreDefinitionsForLaurelDDM :=
+#strata
+program Laurel;
+
+// The types for these Map functions are incorrect.
+// We'll fix them when Laurel supports polymorphism
+function select(map: int, key: int) : int
+  external
+
+function update(map: int, key: int, value: int) : int
+  external
+
+function const(value: int) : int
+  external
+
+#end
+
+/--
+The core map operation definitions as a `Laurel.Program`, parsed at compile time.
+-/
+def coreDefinitionsForLaurel : Program :=
+  let uri := Strata.Uri.file "Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean"
+  match TransM.run uri (parseProgram coreDefinitionsForLaurelDDM) with
+  | .ok program => program
+  | .error e => panic! s!"CoreDefinitionsForLaurel parse error: {e}"
+
+end Strata.Laurel

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -19,12 +19,12 @@ open Lean.Parser (InputContext)
 open Imperative (MetaData)
 
 structure TransState where
-  uri : Uri
+  uri : Option Uri
   errors : Array String
 
 abbrev TransM := StateT TransState (Except String)
 
-def TransM.run (uri : Uri) (m : TransM α) : Except String α :=
+def TransM.run (uri : Option Uri) (m : TransM α) : Except String α :=
   match StateT.run m { uri := uri, errors := #[] } with
   | .ok (v, _) => .ok v
   | .error e => .error e
@@ -36,8 +36,10 @@ def SourceRange.toMetaData (uri : Uri) (sr : SourceRange) : Imperative.MetaData
   let fileRangeElt := ⟨ Imperative.MetaDataElem.Field.label "fileRange", .fileRange ⟨ uri, sr.start, sr.stop ⟩ ⟩
   #[fileRangeElt]
 
-def getArgMetaData (arg : Arg) : TransM (Imperative.MetaData Core.Expression) :=
-  return SourceRange.toMetaData (← get).uri arg.ann
+def getArgMetaData (arg : Arg) : TransM (Imperative.MetaData Core.Expression) := do
+  return match (← get).uri with
+  | some uri => SourceRange.toMetaData uri arg.ann
+  | none => default
 
 def checkOp (op : Strata.Operation) (name : QualifiedIdent) (argc : Nat) :
   TransM Unit := do
@@ -55,7 +57,7 @@ def checkOp (op : Strata.Operation) (name : QualifiedIdent) (argc : Nat) :
 def translateIdent (arg : Arg) : TransM Identifier := do
   let .ident _ id := arg
     | TransM.error s!"translateIdent expects ident"
-  return id
+  return { text := id }
 
 def translateBool (arg : Arg) : TransM Bool := do
   match arg with
@@ -72,7 +74,7 @@ def translateBool (arg : Arg) : TransM Bool := do
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
 instance : Inhabited Parameter where
-  default := { name := "", type := ⟨.TVoid, #[]⟩ }
+  default := { name := "" , type := ⟨.TVoid, #[]⟩ }
 
 def mkHighTypeMd (t : HighType) (md : MetaData Core.Expression) : HighTypeMd := ⟨t, md⟩
 def mkStmtExprMd (e : StmtExpr) (md : MetaData Core.Expression) : StmtExprMd := ⟨e, md⟩
@@ -85,7 +87,12 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
     match op.name, op.args with
     | q`Laurel.intType, _ => return mkHighTypeMd .TInt md
     | q`Laurel.boolType, _ => return mkHighTypeMd .TBool md
+    | q`Laurel.float64Type, _ => return mkHighTypeMd .TFloat64 md
     | q`Laurel.stringType, _ => return mkHighTypeMd .TString md
+    | q`Laurel.mapType, #[keyArg, valArg] =>
+      let keyType ← translateHighType keyArg
+      let valType ← translateHighType valArg
+      return mkHighTypeMd (.TMap keyType valType) md
     | q`Laurel.compositeType, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkHighTypeMd (.UserDefined name) md
@@ -257,12 +264,12 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let name ← translateIdent nameArg
       let ty ← translateHighType tyArg
       let body ← translateStmtExpr bodyArg
-      return mkStmtExprMd (.Forall name ty body) md
+      return mkStmtExprMd (.Forall { name := name, type := ty } body) md
     | q`Laurel.existsExpr, #[nameArg, tyArg, bodyArg] =>
       let name ← translateIdent nameArg
       let ty ← translateHighType tyArg
       let body ← translateStmtExpr bodyArg
-      return mkStmtExprMd (.Exists name ty body) md
+      return mkStmtExprMd (.Exists { name := name, type := ty } body) md
     | _, #[arg0] => match getUnaryOp? op.name with
       | some primOp =>
         let inner ← translateStmtExpr arg0
@@ -370,14 +377,22 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     -- Parse modifies clauses (zero or more)
     let modifies ← translateModifiesClauses modifiesArg
     -- Parse optional body
+    let isExternal ← match bodyArg with
+      | .option _ (some (.op bodyOp)) => match bodyOp.name, bodyOp.args with
+        | q`Laurel.externalBody, #[] => pure true
+        | _, _ => pure false
+      | _ => pure false
     let body ← match bodyArg with
       | .option _ (some (.op bodyOp)) => match bodyOp.name, bodyOp.args with
         | q`Laurel.optionalBody, #[exprArg] => translateCommand exprArg >>= (pure ∘ some)
-        | _, _ => TransM.error s!"Expected optionalBody operation, got {repr bodyOp.name}"
+        | q`Laurel.externalBody, #[] => pure none
+        | _, _ => TransM.error s!"Expected optionalBody or externalBody operation, got {repr bodyOp.name}"
       | .option _ none => pure none
       | _ => TransM.error s!"Expected optionalBody, got {repr bodyArg}"
     -- Determine procedure body kind
-    let procBody := match postconditions, body with
+    let procBody :=
+      if isExternal then Body.External
+      else match postconditions, body with
       | _ :: _, bodyOpt => Body.Opaque postconditions bodyOpt modifies
       | [], some b => Body.Transparent b
       | [], none => Body.Opaque [] none modifies
@@ -435,6 +450,51 @@ def parseComposite (arg : Arg) : TransM TypeDefinition := do
   | _, _ =>
     TransM.error s!"parseComposite expects composite, got {repr op.name}"
 
+def parseDatatypeConstructorArg (arg : Arg) : TransM Parameter := do
+  let .op op := arg
+    | TransM.error s!"parseDatatypeConstructorArg expects operation"
+  match op.name, op.args with
+  | q`Laurel.datatypeConstructorArg, #[nameArg, typeArg] =>
+    let name ← translateIdent nameArg
+    let argType ← translateHighType typeArg
+    return { name := name, type := argType }
+  | _, _ =>
+    TransM.error s!"parseDatatypeConstructorArg expects datatypeConstructorArg, got {repr op.name}"
+
+def parseDatatypeConstructor (arg : Arg) : TransM DatatypeConstructor := do
+  let .op op := arg
+    | TransM.error s!"parseDatatypeConstructor expects operation"
+  match op.name, op.args with
+  | q`Laurel.datatypeConstructor, #[nameArg, argsSeq] =>
+    let name ← translateIdent nameArg
+    let args ← match argsSeq with
+      | .seq _ .comma args => args.toList.mapM parseDatatypeConstructorArg
+      | _ => pure []
+    return { name := name, args := args }
+  | q`Laurel.datatypeConstructorNoArgs, #[nameArg] =>
+    let name ← translateIdent nameArg
+    return { name := name, args := [] }
+  | _, _ =>
+    TransM.error s!"parseDatatypeConstructor expects datatypeConstructor, got {repr op.name}"
+
+def parseDatatype (arg : Arg) : TransM TypeDefinition := do
+  let .op op := arg
+    | TransM.error s!"parseDatatype expects operation"
+  match op.name, op.args with
+  | q`Laurel.datatype, #[nameArg, constructorsArg] =>
+    let name ← translateIdent nameArg
+    let constructors ← match constructorsArg with
+      | .op listOp => match listOp.name, listOp.args with
+        | q`Laurel.datatypeConstructorList, #[csArg] =>
+          match csArg with
+          | .seq _ .comma args => args.toList.mapM parseDatatypeConstructor
+          | singleArg => do let c ← parseDatatypeConstructor singleArg; pure [c]
+        | _, _ => TransM.error s!"Expected datatypeConstructorList, got {repr listOp.name}"
+      | _ => TransM.error s!"Expected datatypeConstructorList operation"
+    return .Datatype { name := name, typeArgs := [], constructors := constructors }
+  | _, _ =>
+    TransM.error s!"parseDatatype expects datatype, got {repr op.name}"
+
 def parseTopLevel (arg : Arg) : TransM (Option Procedure × Option TypeDefinition) := do
   let .op op := arg
     | TransM.error s!"parseTopLevel expects operation"
@@ -446,8 +506,11 @@ def parseTopLevel (arg : Arg) : TransM (Option Procedure × Option TypeDefinitio
   | q`Laurel.topLevelComposite, #[compositeArg] =>
     let typeDef ← parseComposite compositeArg
     return (none, some typeDef)
+  | q`Laurel.topLevelDatatype, #[datatypeArg] =>
+    let typeDef ← parseDatatype datatypeArg
+    return (none, some typeDef)
   | _, _ =>
-    TransM.error s!"parseTopLevel expects topLevelProcedure or topLevelComposite, got {repr op.name}"
+    TransM.error s!"parseTopLevel expects topLevelProcedure, topLevelComposite, or topLevelDatatype, got {repr op.name}"
 
 /--
 Translate concrete Laurel syntax into abstract Laurel syntax

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -7,6 +7,7 @@
 -- 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.
+-- Last grammar change: added externalBody op for external procedure/function bodies.
 import Strata.DDM.Integration.Lean
 
 namespace Strata.Laurel

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -6,7 +6,9 @@ dialect Laurel;
 category LaurelType;
 op intType : LaurelType => "int";
 op boolType : LaurelType => "bool";
+op float64Type : LaurelType => "float64";
 op stringType : LaurelType => "string";
+op mapType (keyType: LaurelType, valueType: LaurelType): LaurelType => "Map " keyType " " valueType;
 op compositeType (name: Ident): LaurelType => name;
 
 category StmtExpr;
@@ -106,6 +108,20 @@ op optionalExtends(parents: CommaSepBy Ident): OptionalExtends => "extends " par
 category Composite;
 op composite (name: Ident, extending: Option OptionalExtends, fields: Seq Field): Composite => "composite " name extending "{" fields "}";
 
+// Datatype definitions
+category DatatypeConstructorArg;
+op datatypeConstructorArg (name: Ident, argType: LaurelType): DatatypeConstructorArg => name ":" argType;
+
+category DatatypeConstructor;
+op datatypeConstructor (name: Ident, args: CommaSepBy DatatypeConstructorArg): DatatypeConstructor => name "(" args ")";
+op datatypeConstructorNoArgs (name: Ident): DatatypeConstructor => name;
+
+category DatatypeConstructorList;
+op datatypeConstructorList (constructors: CommaSepBy DatatypeConstructor): DatatypeConstructorList => constructors;
+
+category Datatype;
+op datatype (name: Ident, constructors: DatatypeConstructorList): Datatype => "datatype " name "{" constructors "}";
+
 // Procedures
 category OptionalReturnType;
 op optionalReturnType(returnType: LaurelType): OptionalReturnType => ":" returnType;
@@ -124,6 +140,7 @@ op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "retu
 
 category OptionalBody;
 op optionalBody(body: StmtExpr): OptionalBody => body:0;
+op externalBody: OptionalBody => "external";
 
 category Procedure;
 op procedure (name : Ident, parameters: CommaSepBy Parameter,
@@ -147,5 +164,6 @@ op function (name : Ident, parameters: CommaSepBy Parameter,
 category TopLevel;
 op topLevelComposite(composite: Composite): TopLevel => composite;
 op topLevelProcedure(procedure: Procedure): TopLevel => procedure;
+op topLevelDatatype(datatype: Datatype): TopLevel => datatype;
 
 op program (items: Seq TopLevel): Command => items;