Always use 1d locations in metadata

Examples/expected/ProcedureTypeError.core.expected

@@ -1,3 +1,3 @@
 Successfully parsed.
-❌ Type checking error.
-ProcedureTypeError.core.st(21, (4-32)) [SumPositive:precond2]: Cannot find this fvar in the context! c
+ProcedureTypeError.core.st(21,(4-32)) ❌ Type checking error.
+[SumPositive:precond2]: Cannot find this fvar in the context! c

Examples/expected/TypeError.core.expected

@@ -1,4 +1,4 @@
 Successfully parsed.
-❌ Type checking error.
-TypeError.core.st(25, 2) Impossible to unify (Map int (Map bool bool)) with (Map int int).
+TypeError.core.st(25,(2-18)) ❌ Type checking error.
+Impossible to unify (Map int (Map bool bool)) with (Map int int).
 First mismatch: (Map bool bool) with int.

Strata/DDM/AST.lean

@@ -306,17 +306,78 @@ structure FileRange where
 instance : ToFormat FileRange where
  format fr := f!"{fr.file}:{fr.range}"
 
-structure File2dRange where
-  file: Uri
-  start: Lean.Position
-  ending: Lean.Position
-  deriving DecidableEq, Repr
-
-instance : ToFormat File2dRange where
- format fr :=
-    let baseName := match fr.file with
-                    | .file path => (path.splitToList (· == '/')).getLast!
-    f!"{baseName}({fr.start.line}, {fr.start.column})-({fr.ending.line}, {fr.ending.column})"
+/-- A default file range for errors without source location.
+This should only be used for generated nodes that are guaranteed to be correct. -/
+def FileRange.unknown : FileRange :=
+  { file := .file "<unknown>", range := SourceRange.none }
+
+/-- A diagnostic model that holds a file range and a message.
+    This can be converted to a formatted string using a FileMap. -/
+structure DiagnosticModel where
+  fileRange : FileRange
+  message : String
+  deriving Repr, BEq, Inhabited
+
+instance : Inhabited DiagnosticModel where
+  default := { fileRange := FileRange.unknown, message := "" }
+
+/-- Create a DiagnosticModel from just a message (using default location).
+This should not be called, it only exists temporarily to enabling incrementally migrating code without error locations -/
+def DiagnosticModel.fromMessage (msg : String) : DiagnosticModel :=
+  { fileRange := FileRange.unknown, message := msg }
+
+/-- Create a DiagnosticModel from a Format (using default location).
+This should not be called, it only exists temporarily to enabling incrementally migrating code without error locations -/
+def DiagnosticModel.fromFormat (fmt : Std.Format) : DiagnosticModel :=
+  { fileRange := FileRange.unknown, message := toString fmt }
+
+/-- Create a DiagnosticModel with source location. -/
+def DiagnosticModel.withRange (fr : FileRange) (msg : Format) : DiagnosticModel :=
+  { fileRange := fr, message := toString msg }
+
+/-- Format a file range using a FileMap to convert byte offsets to line/column positions. -/
+def FileRange.format (fr : FileRange) (fileMap : Option Lean.FileMap) (includeEnd? : Bool := true) : Std.Format :=
+  let baseName := match fr.file with
+                  | .file path => (path.splitToList (· == '/')).getLast!
+  match fileMap with
+  | some fm =>
+    let startPos := fm.toPosition fr.range.start
+    let endPos := fm.toPosition fr.range.stop
+    if includeEnd? then
+      if startPos.line == endPos.line then
+        f!"{baseName}({startPos.line},({startPos.column}-{endPos.column}))"
+      else
+        f!"{baseName}(({startPos.line},{startPos.column})-({endPos.line},{endPos.column}))"
+    else
+      f!"{baseName}({startPos.line}, {startPos.column})"
+  | none =>
+    if fr.range.isNone then
+      f!""
+    else
+      f!"{baseName}({fr.range.start}-{fr.range.stop})"
+
+/-- Format a DiagnosticModel using a FileMap to convert byte offsets to line/column positions. -/
+def DiagnosticModel.format (dm : DiagnosticModel) (fileMap : Option Lean.FileMap) (includeEnd? : Bool := true) : Std.Format :=
+  let rangeStr := dm.fileRange.format fileMap includeEnd?
+  if dm.fileRange.range.isNone then
+    f!"{dm.message}"
+  else
+    f!"{rangeStr} {dm.message}"
+
+/-- Format just the file range portion of a DiagnosticModel. -/
+def DiagnosticModel.formatRange (dm : DiagnosticModel) (fileMap : Option Lean.FileMap) (includeEnd? : Bool := true) : Std.Format :=
+  dm.fileRange.format fileMap includeEnd?
+
+/-- Update the file range of a DiagnosticModel if it's currently unknown.
+This should not be called, it only exists temporarily to enabling incrementally migrating code without error locations -/
+def DiagnosticModel.withRangeIfUnknown (dm : DiagnosticModel) (fr : FileRange) : DiagnosticModel :=
+  if dm.fileRange.range.isNone then
+    { dm with fileRange := fr }
+  else
+    dm
+
+instance : ToString DiagnosticModel where
+  toString dm := dm.format none |> toString
 
 abbrev Arg := ArgF SourceRange
 abbrev Expr := ExprF SourceRange

Strata/DL/Imperative/CmdType.lean

@@ -11,26 +11,26 @@ import Strata.DL.Imperative.TypeContext
 
 namespace Imperative
 open Std (ToFormat Format format)
+open Strata (DiagnosticModel FileRange)
 
 ---------------------------------------------------------------------
 
 /--
 Type checker for an Imperative Command.
 
-The `TypeError` parameter for the `TypeContext` instance `TC` is a concrete type
-here. We can change this to a more generic type in the future, if needed.
+The `TypeError` parameter for the `TypeContext` instance `TC` is `DiagnosticModel`.
 -/
 def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
-    [DecidableEq P.Ident] [TC : TypeContext P C T Format]
-    (ctx: C) (τ : T) (c : Cmd P) : Except Format (Cmd P × T) := do
+    [DecidableEq P.Ident] [TC : TypeContext P C T DiagnosticModel]
+    (ctx: C) (τ : T) (c : Cmd P) : Except DiagnosticModel (Cmd P × T) := do
 
   try match c with
 
   | .init x xty e md =>
     match TC.lookup τ x with
     | none =>
       if x ∈ TC.freeVars e then
-        .error f!"Variable {x} cannot appear in its own initialization expression!"
+        .error <| md.toDiagnosticF f!"Variable {x} cannot appear in its own initialization expression!"
       else
         let (xty, τ) ← TC.preprocess ctx τ xty
         let (e, ety, τ) ← TC.inferType ctx τ c e
@@ -40,29 +40,29 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
         let c := Cmd.init x xty e md
         .ok (c, τ)
     | some xty =>
-      .error f!"Variable {x} of type {xty} already in context."
+      .error <| md.toDiagnosticF f!"Variable {x} of type {xty} already in context."
 
   | .set x e md =>
     match TC.lookup τ x with
-    | none => .error f!"Cannot set undeclared variable {x}."
+    | none => .error <| md.toDiagnosticF f!"Cannot set undeclared variable {x}."
     | some xty =>
       let (e, ety, τ) ← TC.inferType ctx τ c e
       let τ ← TC.unifyTypes τ [(xty, ety)]
       let c := Cmd.set x e md
       .ok (c, τ)
 
-  | .havoc x _md =>
+  | .havoc x md =>
     match TC.lookup τ x with
     | some _ => .ok (c, τ)
-    | none => .error f!"Cannot havoc undeclared variable {x}."
+    | none => .error <| md.toDiagnosticF f!"Cannot havoc undeclared variable {x}."
 
   | .assert label e md =>
     let (e, ety, τ) ← TC.inferType ctx τ c e
     if TC.isBoolType ety then
        let c := Cmd.assert label e md
        .ok (c, τ)
     else
-      .error f!"Assertion {label} expected to be of type boolean, \
+      .error <| md.toDiagnosticF f!"Assertion {label} expected to be of type boolean, \
                 but inferred type is {ety}."
 
   | .assume label e md =>
@@ -71,7 +71,7 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
        let c := Cmd.assume label e md
        .ok (c, τ)
     else
-      .error f!"Assumption {label} expected to be of type boolean, \
+      .error <| md.toDiagnosticF f!"Assumption {label} expected to be of type boolean, \
                 but inferred type is {ety}."
 
   | .cover label e md =>
@@ -80,23 +80,19 @@ def Cmd.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
        let c := Cmd.cover label e md
        .ok (c, τ)
     else
-      .error f!"Cover {label} expected to be of type boolean, \
+      .error <| md.toDiagnosticF f!"Cover {label} expected to be of type boolean, \
                 but inferred type is {ety}."
 
   catch e =>
-    -- Add source location to error messages.
-    let sourceLoc := MetaData.formatFileRangeD c.getMetaData
-    if sourceLoc.isEmpty then
-      .error e
-    else
-      .error f!"{sourceLoc} {e}"
+    -- Add source location to error messages if not already present.
+    .error <| e.withRangeIfUnknown (getFileRange c.getMetaData |>.getD FileRange.unknown)
 
 /--
 Type checker for Imperative's Commands.
 -/
 def Cmds.typeCheck {P C T} [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat (Cmd P)]
-    [DecidableEq P.Ident] [TC : TypeContext P C T Format]
-    (ctx: C) (τ : T) (cs : Cmds P) : Except Format (Cmds P × T) := do
+    [DecidableEq P.Ident] [TC : TypeContext P C T DiagnosticModel]
+    (ctx: C) (τ : T) (cs : Cmds P) : Except DiagnosticModel (Cmds P × T) := do
   match cs with
   | [] => .ok ([], τ)
   | c :: crest =>

Strata/DL/Imperative/MetaData.lean

@@ -10,6 +10,7 @@ import Strata.DDM.AST
 import Lean.Data.Position
 
 namespace Imperative
+open Strata (DiagnosticModel FileRange)
 
 ---------------------------------------------------------------------
 
@@ -73,16 +74,13 @@ inductive MetaDataElem.Value (P : PureExpr) where
   /-- Metadata value in the form of an arbitrary string. -/
   | msg (s : String)
   /-- Metadata value in the form of a fileRange. -/
-  | fileRange (r: Strata.FileRange)
-  /-- Metadata value in the form of a fileRange. -/
-  | file2dRange (r: Strata.File2dRange)
+  | fileRange (r: FileRange)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
   format f := match f with
               | .expr e => f!"{e}"
               | .msg s => f!"{s}"
               | .fileRange r => f!"{r}"
-              | .file2dRange r => f!"{r}"
 
 instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
   reprPrec v prec :=
@@ -91,15 +89,13 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       | .expr e => f!".expr {reprPrec e prec}"
       | .msg s => f!".msg {s}"
       | .fileRange fr => f!".fileRange {fr}"
-      | .file2dRange fr => f!".file2dRange {fr}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
   match v1, v2 with
   | .expr e1, .expr e2 => e1 == e2
   | .msg m1, .msg m2 => m1 == m2
   | .fileRange r1, .fileRange r2 => r1 == r2
-  | .file2dRange r1, .file2dRange r2 => r1 == r2
   | _, _ => false
 
 instance [BEq P.Expr] : BEq (MetaDataElem.Value P) where
@@ -175,34 +171,31 @@ instance [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P) where
 
 def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
-def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Strata.FileRange := do
+def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option FileRange := do
   let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
   match fileRangeElement.value with
     | .fileRange fileRange =>
       some fileRange
     | _ => none
 
-def MetaData.formatFileRange? {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : Bool := false) :
-    Option Std.Format := do
-  let fileRangeElem ← md.findElem MetaData.fileRange
-  match fileRangeElem.value with
-  | .file2dRange m =>
-    let baseName := match m.file with
-                    | .file path => (path.splitToList (· == '/')).getLast!
-    if includeEnd? then
-      if m.start.line == m.ending.line then
-        return f!"{baseName}({m.start.line}, ({m.start.column}-{m.ending.column}))"
-      else
-        return f!"{baseName}(({m.start.line}, {m.start.column})-({m.ending.line}, {m.ending.column}))"
-    else -- don't include the end position.
-      return f!"{baseName}({m.start.line}, {m.start.column})"
-  | _ => none
-
-def MetaData.formatFileRangeD {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : Bool := false)
-    : Std.Format :=
-  match formatFileRange? md includeEnd? with
-  | .none => ""
-  | .some f => f
+/-- Create a DiagnosticModel from metadata and a message.
+    Uses the file range from metadata if available, otherwise uses a default location. -/
+def MetaData.toDiagnostic {P : PureExpr} [BEq P.Ident] (md : MetaData P) (msg : String) : DiagnosticModel :=
+  match getFileRange md with
+  | some fr => DiagnosticModel.withRange fr msg
+  | none => DiagnosticModel.fromMessage msg
+
+/-- Create a DiagnosticModel from metadata and a Format message. -/
+def MetaData.toDiagnosticF {P : PureExpr} [BEq P.Ident] (md : MetaData P) (msg : Std.Format) : DiagnosticModel :=
+  MetaData.toDiagnostic md (toString msg)
+
+/-- Get the file range from metadata as a DiagnosticModel (for formatting).
+    This is a compatibility function that formats the file range using byte offsets.
+    For proper line/column display, use toDiagnostic and format with a FileMap at the top level. -/
+def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fileMap : Option Lean.FileMap := none) (includeEnd? : Bool := false) : Format :=
+  match getFileRange md with
+  | some fr => fr.format fileMap includeEnd?
+  | none => f!""
 
 ---------------------------------------------------------------------
 

Strata/DL/Lambda/Factory.lean

@@ -6,6 +6,7 @@
 
 import Strata.DL.Lambda.LExprWF
 import Strata.DL.Lambda.LTy
+import Strata.DDM.AST
 import Strata.DDM.Util.Array
 import Strata.DL.Util.List
 import Strata.DL.Util.ListMap
@@ -25,7 +26,7 @@ Also see `Strata.DL.Lambda.IntBoolFactory` for a concrete example of a factory.
 
 
 namespace Lambda
-
+open Strata
 open Std (ToFormat Format format)
 
 variable {T : LExprParams} [Inhabited T.Metadata] [ToFormat T.IDMeta]
@@ -247,11 +248,11 @@ def Factory.getFactoryLFunc (F : @Factory T) (name : String) : Option (LFunc T)
 /--
 Add a function `func` to the factory `F`. Redefinitions are not allowed.
 -/
-def Factory.addFactoryFunc (F : @Factory T) (func : LFunc T) : Except Format (@Factory T) :=
+def Factory.addFactoryFunc (F : @Factory T) (func : LFunc T) : Except DiagnosticModel (@Factory T) :=
   match F.getFactoryLFunc func.name.name with
   | none => .ok (F.push func)
   | some func' =>
-    .error f!"A function of name {func.name} already exists! \
+    .error <| DiagnosticModel.fromFormat f!"A function of name {func.name} already exists! \
               Redefinitions are not allowed.\n\
               Existing Function: {func'}\n\
               New Function:{func}"
@@ -286,7 +287,7 @@ by
 Append a factory `newF` to an existing factory `F`, checking for redefinitions
 along the way.
 -/
-def Factory.addFactory (F newF : @Factory T) : Except Format (@Factory T) :=
+def Factory.addFactory (F newF : @Factory T) : Except DiagnosticModel (@Factory T) :=
   Array.foldlM (fun factory func => factory.addFactoryFunc func) F newF