Remove MetaData from Laurel Identifier and AstNode

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -41,21 +41,21 @@ partial def resolveBaseType (ptMap : ConstrainedTypeMap) (ty : HighType) : HighT
   | .UserDefined name => match ptMap.get? name.text with
     | some ct => resolveBaseType ptMap ct.base.val | none => ty
   | .Applied ctor args =>
-    .Applied ctor (args.map fun a => ⟨resolveBaseType ptMap a.val, a.source, a.md⟩)
+    .Applied ctor (args.map fun a => ⟨resolveBaseType ptMap a.val, a.source⟩)
   | _ => ty
 
 def resolveType (ptMap : ConstrainedTypeMap) (ty : HighTypeMd) : HighTypeMd :=
-  ⟨resolveBaseType ptMap ty.val, ty.source, ty.md⟩
+  ⟨resolveBaseType ptMap ty.val, ty.source⟩
 
 def isConstrainedType (ptMap : ConstrainedTypeMap) (ty : HighType) : Bool :=
   match ty with | .UserDefined name => ptMap.contains name.text | _ => false
 
 /-- Build a call to the constraint function for a constrained type, or `none` if not constrained -/
 def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
-    (varName : Identifier) (md : Imperative.MetaData Core.Expression) (src : Option FileRange := none) : Option StmtExprMd :=
+    (varName : Identifier) (src : Option FileRange := none) : Option StmtExprMd :=
   match ty with
   | .UserDefined name => if ptMap.contains name.text then
-      some ⟨.StaticCall (mkId s!"{name.text}$constraint") [⟨.Identifier varName, src, md⟩], src, md⟩
+      some ⟨.StaticCall (mkId s!"{name.text}$constraint") [⟨.Identifier varName, src⟩], src⟩
     else none
   | _ => none
 
@@ -75,38 +75,38 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
       else ct.constraint
     | _ => ct.constraint
   { name := mkId s!"{ct.name.text}$constraint"
-    inputs := [{ name := ct.valueName, type := { baseType with md := #[] } }]
+    inputs := [{ name := ct.valueName, type := baseType }]
     outputs := [{ name := mkId "result", type := { val := .TBool, source := none } }]
     body := .Transparent { val := .Block [bodyExpr] none, source := none }
     isFunctional := true
     decreases := none
     preconditions := [] }
 
-private def wrap (stmts : List StmtExprMd) (src : Option FileRange) (md : Imperative.MetaData Core.Expression := .empty)
+private def wrap (stmts : List StmtExprMd) (src : Option FileRange)
     : StmtExprMd :=
-  match stmts with | [s] => s | ss => ⟨.Block ss none, src, md⟩
+  match stmts with | [s] => s | ss => ⟨.Block ss none, src⟩
 
 /-- Resolve constrained types in type positions and inject constraint calls into quantifier bodies.
     Recursion into StmtExprMd children is handled by `mapStmtExpr`. -/
 def resolveExprNode (ptMap : ConstrainedTypeMap) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
-  let md := expr.md
+
   match expr.val with
   | .LocalVariable n ty init =>
-    ⟨.LocalVariable n (resolveType ptMap ty) init, source, md⟩
+    ⟨.LocalVariable n (resolveType ptMap ty) init, source⟩
   | .Quantifier mode param trigger body =>
     let param' := { param with type := resolveType ptMap param.type }
     -- With bottom-up traversal, `body` is already recursed into. The newly
     -- created `PrimitiveOp` won't be visited again, which is safe because
     -- `c` (from `constraintCallFor`) is a StaticCall with Identifier leaves
     -- that don't need further resolution.
     let combiner := match mode with | .Forall => Operation.Implies | .Exists => Operation.And
-    let injected := match constraintCallFor ptMap param.type.val param.name md (src := source) with
-      | some c => ⟨.PrimitiveOp combiner [c, body], source, md⟩
+    let injected := match constraintCallFor ptMap param.type.val param.name (src := source) with
+      | some c => ⟨.PrimitiveOp combiner [c, body], source⟩
       | none => body
-    ⟨.Quantifier mode param' trigger injected, source, md⟩
-  | .AsType t ty => ⟨.AsType t (resolveType ptMap ty), source, md⟩
-  | .IsType t ty => ⟨.IsType t (resolveType ptMap ty), source, md⟩
+    ⟨.Quantifier mode param' trigger injected, source⟩
+  | .AsType t ty => ⟨.AsType t (resolveType ptMap ty), source⟩
+  | .IsType t ty => ⟨.IsType t (resolveType ptMap ty), source⟩
   | _ => expr
 
 abbrev ElimM := StateM PredVarMap
@@ -120,43 +120,43 @@ private def inScope (action : ElimM α) : ElimM α := do
 def elimStmt (ptMap : ConstrainedTypeMap)
     (stmt : StmtExprMd) : ElimM (List StmtExprMd) := do
   let source := stmt.source
-  let md := stmt.md
+
   match _h : stmt.val with
   | .LocalVariable name ty init =>
-    let callOpt := constraintCallFor ptMap ty.val name md (src := source)
+    let callOpt := constraintCallFor ptMap ty.val name (src := source)
     if callOpt.isSome then modify fun pv => pv.insert name.text ty.val
     let (init', check) : Option StmtExprMd × List StmtExprMd := match init with
       | none => match callOpt with
-        | some c => (none, [⟨.Assume c, source, md⟩])
+        | some c => (none, [⟨.Assume c, source⟩])
         | none => (none, [])
-      | some _ => (init, callOpt.toList.map fun c => ⟨.Assert { condition := c }, source, md⟩)
-    pure ([⟨.LocalVariable name ty init', source, md⟩] ++ check)
+      | some _ => (init, callOpt.toList.map fun c => ⟨.Assert { condition := c }, source⟩)
+    pure ([⟨.LocalVariable name ty init', source⟩] ++ check)
 
   | .Assign [target] _ => match target.val with
     | .Identifier name => do
       match (← get).get? name.text with
       | some ty =>
-        let assert := (constraintCallFor ptMap ty name md (src := source)).toList.map
-          fun c => ⟨.Assert { condition := c }, source, md⟩
+        let assert := (constraintCallFor ptMap ty name (src := source)).toList.map
+          fun c => ⟨.Assert { condition := c }, source⟩
         pure ([stmt] ++ assert)
       | none => pure [stmt]
     | _ => pure [stmt]
 
   | .Block stmts sep =>
     let stmtss ← inScope (stmts.mapM (elimStmt ptMap))
-    pure [⟨.Block stmtss.flatten sep, source, md⟩]
+    pure [⟨.Block stmtss.flatten sep, source⟩]
 
   | .IfThenElse cond thenBr (some elseBr) =>
     let thenSs ← inScope (elimStmt ptMap thenBr)
     let elseSs ← inScope (elimStmt ptMap elseBr)
-    pure [⟨.IfThenElse cond (wrap thenSs source md) (some (wrap elseSs source md)), source, md⟩]
+    pure [⟨.IfThenElse cond (wrap thenSs source) (some (wrap elseSs source)), source⟩]
   | .IfThenElse cond thenBr none =>
     let thenSs ← inScope (elimStmt ptMap thenBr)
-    pure [⟨.IfThenElse cond (wrap thenSs source md) none, source, md⟩]
+    pure [⟨.IfThenElse cond (wrap thenSs source) none, source⟩]
 
   | .While cond inv dec body =>
     let bodySs ← inScope (elimStmt ptMap body)
-    pure [⟨.While cond inv dec (wrap bodySs source md), source, md⟩]
+    pure [⟨.While cond inv dec (wrap bodySs source), source⟩]
 
   | _ => pure [stmt]
 termination_by sizeOf stmt
@@ -168,23 +168,23 @@ decreasing_by
 
 def elimProc (ptMap : ConstrainedTypeMap) (proc : Procedure) : Procedure :=
   let inputRequires : List Condition := proc.inputs.filterMap fun p =>
-    (constraintCallFor ptMap p.type.val p.name p.type.md (src := p.type.source)).map
+    (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := c }
   let outputEnsures : List Condition := if proc.isFunctional then [] else proc.outputs.filterMap fun p =>
-    (constraintCallFor ptMap p.type.val p.name p.type.md (src := p.type.source)).map
-      fun c => { condition := ⟨c.val, p.type.source, p.type.md⟩ }
+    (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
+      fun c => { condition := ⟨c.val, p.type.source⟩ }
   let initVars : PredVarMap := proc.inputs.foldl (init := {}) fun s p =>
     if isConstrainedType ptMap p.type.val then s.insert p.name.text p.type.val else s
   let body' := match proc.body with
   | .Transparent bodyExpr =>
     let (stmts, _) := (elimStmt ptMap bodyExpr).run initVars
-    let body := wrap stmts bodyExpr.source bodyExpr.md
+    let body := wrap stmts bodyExpr.source
     if outputEnsures.isEmpty then .Transparent body
     else
-      let retBody := if proc.isFunctional then ⟨.Return (some body), bodyExpr.source, bodyExpr.md⟩ else body
+      let retBody := if proc.isFunctional then ⟨.Return (some body), bodyExpr.source⟩ else body
       .Opaque outputEnsures (some retBody) []
   | .Opaque postconds impl modif =>
-    let impl' := impl.map fun b => wrap ((elimStmt ptMap b).run initVars).1 b.source b.md
+    let impl' := impl.map fun b => wrap ((elimStmt ptMap b).run initVars).1 b.source
     .Opaque (postconds ++ outputEnsures) impl' modif
   | .Abstract postconds => .Abstract (postconds ++ outputEnsures)
   | .External => .External
@@ -202,16 +202,16 @@ def elimProc (ptMap : ConstrainedTypeMap) (proc : Procedure) : Procedure :=
 
 private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
   let src := ct.witness.source
-  let md := ct.witness.md
+
   let witnessId : Identifier := mkId "$witness"
   let witnessInit : StmtExprMd :=
-    ⟨.LocalVariable witnessId (resolveType ptMap ct.base) (some ct.witness), src, md⟩
+    ⟨.LocalVariable witnessId (resolveType ptMap ct.base) (some ct.witness), src⟩
   let assert : StmtExprMd :=
-    ⟨.Assert { condition := (constraintCallFor ptMap (.UserDefined ct.name) witnessId md (src := src)).get! }, src, md⟩
+    ⟨.Assert { condition := (constraintCallFor ptMap (.UserDefined ct.name) witnessId (src := src)).get! }, src⟩
   { name := mkId s!"$witness_{ct.name.text}"
     inputs := []
     outputs := []
-    body := .Transparent ⟨.Block [witnessInit, assert] none, src, md⟩
+    body := .Transparent ⟨.Block [witnessInit, assert] none, src⟩
     preconditions := []
     isFunctional := false
     decreases := none }
@@ -226,7 +226,7 @@ public def constrainedTypeElim (_model : SemanticModel) (program : Program)
     | .Constrained ct => some (mkWitnessProc ptMap ct) | _ => none
   let funcDiags := program.staticProcedures.foldl (init := []) fun acc proc =>
     if proc.isFunctional && proc.outputs.any (fun p => isConstrainedType ptMap p.type.val) then
-      acc.cons (proc.name.md.toDiagnostic "constrained return types on functions are not yet supported")
+      acc.cons (diagnosticFromSource proc.name.source "constrained return types on functions are not yet supported")
     else acc
   ({ program with
     staticProcedures := constraintFuncs ++ program.staticProcedures.map (elimProc ptMap)

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -29,15 +29,15 @@ open Lambda (LMonoTy LExpr)
 
 /-- Collect all `UserDefined` type names referenced in a `HighType`, including nested ones. -/
 def collectTypeRefs : HighTypeMd → List String
-  | ⟨.UserDefined name, _, _⟩ => [name.text]
-  | ⟨.TSet elem, _, _⟩ => collectTypeRefs elem
-  | ⟨.TMap k v, _, _⟩ => collectTypeRefs k ++ collectTypeRefs v
-  | ⟨.TTypedField vt, _, _⟩ => collectTypeRefs vt
-  | ⟨.Applied base args, _, _⟩ =>
+  | ⟨.UserDefined name, _⟩ => [name.text]
+  | ⟨.TSet elem, _⟩ => collectTypeRefs elem
+  | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
+  | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt
+  | ⟨.Applied base args, _⟩ =>
       collectTypeRefs base ++ args.flatMap collectTypeRefs
-  | ⟨.Pure base, _, _⟩ => collectTypeRefs base
-  | ⟨.Intersection ts, _, _⟩ => ts.flatMap collectTypeRefs
-  | ⟨.TCore name, _, _⟩ => [name]
+  | ⟨.Pure base, _⟩ => collectTypeRefs base
+  | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs
+  | ⟨.TCore name, _⟩ => [name]
   | _ => []
 
 /-- Get all datatype names that a `DatatypeDefinition` references in its constructor args. -/
@@ -50,7 +50,7 @@ Used to build the call graph for SCC-based procedure ordering.
 -/
 def collectStaticCallNames (expr : StmtExprMd) : List String :=
   match expr with
-  | AstNode.mk val _ _ =>
+  | AstNode.mk val _ =>
   match val with
   | .StaticCall callee args =>
       callee.text :: args.flatMap (fun a => collectStaticCallNames a)

Strata/Languages/Laurel/DesugarShortCircuit.lean

@@ -23,12 +23,11 @@ namespace Strata.Laurel
 
 public section
 
-private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none, default⟩
+private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none⟩
 
 /-- Local rewrite of a single short-circuit node. Recursion is handled by `mapStmtExpr`. -/
 private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
-  let md := expr.md
   match expr.val with
   | .PrimitiveOp op args =>
     match op, args with
@@ -38,11 +37,11 @@ private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd)
     | .AndThen, [a, b] | .Implies, [a, b] =>
       if containsAssignmentOrImperativeCall model b then
         let elseVal := match op with | .AndThen => false | _ => true
-        ⟨.IfThenElse a b (some (bare (.LiteralBool elseVal))), source, md⟩
+        ⟨.IfThenElse a b (some (bare (.LiteralBool elseVal))), source⟩
       else expr
     | .OrElse, [a, b] =>
       if containsAssignmentOrImperativeCall model b then
-        ⟨.IfThenElse a (bare (.LiteralBool true)) (some b), source, md⟩
+        ⟨.IfThenElse a (bare (.LiteralBool true)) (some b), source⟩
       else expr
     | _, _ => expr
   | _ => expr

Strata/Languages/Laurel/EliminateHoles.lean

@@ -26,8 +26,7 @@ namespace Laurel
 
 public section
 
-private def emptyMd : Imperative.MetaData Core.Expression := #[]
-private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none, emptyMd⟩
+private def bare (v : StmtExpr) : StmtExprMd := { val := v, source := none }
 
 structure ElimHoleState where
   counter : Nat := 0
@@ -60,7 +59,7 @@ private def mkHoleCall (holeType : HighTypeMd) : ElimHoleM StmtExprMd := do
 private def elimHoleNode (expr : StmtExprMd) : ElimHoleM StmtExprMd := do
   match expr.val with
   | .Hole true (some ty) => mkHoleCall ty
-  | .Hole true none => mkHoleCall ⟨.Unknown, expr.source, expr.md⟩
+  | .Hole true none => mkHoleCall { val := .Unknown, source := expr.source }
   | .Hole false _ => return expr -- Non-deterministic holes are preserved
   | _ => return expr
 

Strata/Languages/Laurel/EliminateReturnsInExpression.lean

@@ -51,17 +51,17 @@ expression. Each `if-then` (no else) guard wraps as
 `if cond then lastStmtToExpr(body) else acc`; other statements produce
 `Block [stmt, acc]`.
 -/
-def stmtsToExpr (stmts : List StmtExprMd) (acc : StmtExprMd) (blockMd : MetaData)
+def stmtsToExpr (stmts : List StmtExprMd) (acc : StmtExprMd)
     : StmtExprMd :=
   match stmts with
   | [] => acc
   | s :: rest =>
-    let acc' := stmtsToExpr rest acc blockMd
+    let acc' := stmtsToExpr rest acc
     match s with
-    | ⟨.IfThenElse cond thenBr none, ssrc, smd⟩ =>
-      ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some acc'), ssrc, smd⟩
+    | ⟨.IfThenElse cond thenBr none, ssrc⟩ =>
+      ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some acc'), ssrc⟩
     | _ =>
-      ⟨.Block [s, acc'] none, none, blockMd⟩
+      { val := .Block [s, acc'] none, source := none }
   termination_by (sizeOf stmts, 1)
 
 /--
@@ -73,19 +73,19 @@ Convert the last statement of a block into an expression.
 -/
 def lastStmtToExpr (stmt : StmtExprMd) : StmtExprMd :=
   match stmt with
-  | ⟨.Return (some val), _, _⟩ => val
-  | ⟨.Block stmts _, source, md⟩ =>
+  | ⟨.Return (some val), _⟩ => val
+  | ⟨.Block stmts _, _⟩ =>
     match h_last : stmts.getLast? with
     | some last =>
       have := List.mem_of_getLast? h_last
       let lastExpr := lastStmtToExpr last
       let dropped := stmts.dropLast
       have h : sizeOf stmts.dropLast < sizeOf stmts :=
         List.sizeOf_dropLast_lt (by intro h; simp [h] at h_last)
-      stmtsToExpr dropped lastExpr md
+      stmtsToExpr dropped lastExpr
     | none => stmt
-  | ⟨.IfThenElse cond thenBr (some elseBr), source, md⟩ =>
-    ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some (lastStmtToExpr elseBr)), source, md⟩
+  | ⟨.IfThenElse cond thenBr (some elseBr), source⟩ =>
+    ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some (lastStmtToExpr elseBr)), source⟩
   | _ => stmt
   termination_by (sizeOf stmt, 0)
   decreasing_by

Strata/Languages/Laurel/EliminateValueReturns.lean

@@ -27,10 +27,10 @@ private def eliminateValueReturnNode (outParam : Identifier) (stmt : StmtExprMd)
   match stmt.val with
   | .Return (some value) =>
     -- Synthesized nodes use default metadata since no diagnostics should be reported on them
-    let target : StmtExprMd := ⟨.Identifier outParam, none, .empty⟩
-    let assign : StmtExprMd := ⟨.Assign [target] value, none, .empty⟩
-    let ret : StmtExprMd := ⟨.Return none, stmt.source, stmt.md⟩
-    ⟨.Block [assign, ret] none, none, .empty⟩
+    let target : StmtExprMd := { val := .Identifier outParam, source := none }
+    let assign : StmtExprMd := { val := .Assign [target] value, source := none }
+    let ret : StmtExprMd := { val := .Return none, source := stmt.source }
+    { val := .Block [assign, ret] none, source := none }
   | _ => stmt
 
 /-- Check whether a statement tree contains any `Return (some _)`. -/
@@ -74,7 +74,7 @@ def eliminateValueReturnsInProc (proc : Procedure) : Procedure × Array Diagnost
         "Valued return is not supported for procedures with no output parameters"
       else
         "Valued return is not supported for procedures with multiple output parameters"
-      (proc, #[proc.name.md.toDiagnostic msg DiagnosticType.UserError])
+      (proc, #[diagnosticFromSource proc.name.source msg DiagnosticType.UserError])
     else (proc, #[])
 
 public section

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -77,7 +77,8 @@ private def operationName : Operation → String
   | .Gt => "gt" | .Geq => "ge" | .StrConcat => "strConcat"
 
 -- Internal-only: public because `partial` prevents `private` in this section
-partial def stmtExprToArg (s : StmtExprMd) : Arg := stmtExprValToArg s.val
+partial def stmtExprToArg (s : StmtExprMd) : Arg :=
+  stmtExprValToArg s.val
 where
   stmtExprValToArg : StmtExpr → Arg
     | .LiteralBool b => laurelOp "literalBool" #[boolToArg b]
@@ -339,7 +340,7 @@ private def formatOp (o : Strata.Operation) : Format :=
 def formatHighType (t : HighTypeMd) : Format := formatArg (highTypeToArg t)
 def formatHighTypeVal (t : HighType) : Format := formatArg (highTypeValToArg t)
 def formatStmtExpr (s : StmtExprMd) : Format := formatArg (stmtExprToArg s)
-def formatStmtExprVal (s : StmtExpr) : Format := formatArg (stmtExprToArg ⟨s, none, {}⟩)
+def formatStmtExprVal (s : StmtExpr) : Format := formatArg (stmtExprToArg { val := s, source := none })
 def formatParameter (p : Parameter) : Format := formatArg (parameterToArg p)
 def formatField (f : Field) : Format := formatArg (fieldToArg f)
 def formatDatatypeConstructor (c : DatatypeConstructor) : Format := formatArg (datatypeConstructorToArg c)

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -64,8 +64,8 @@ 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"
-  let md ← getArgMetaData arg
-  return { text := id, md := md }
+  let source ← getArgFileRange arg
+  return { text := id, source := source }
 
 def translateBool (arg : Arg) : TransM Bool := do
   match arg with
@@ -154,7 +154,7 @@ instance : Inhabited Procedure where
     decreases := none
     isFunctional := false
     invokeOn := none
-    body := .Transparent ⟨.LiteralBool true, none, #[]⟩
+    body := .Transparent { val := .LiteralBool true, source := none }
   }
 
 def getBinaryOp? (name : QualifiedIdent) : Option Operation :=