Unify pyAnalyzeLaurel error classification

Strata.lean

@@ -17,6 +17,7 @@ import Strata.DL.Lambda.Lambda
 import Strata.DL.Imperative.Imperative
 
 /- Utilities -/
+import Strata.Util.DiagnosticClassifier
 import Strata.Util.NameProofs
 import Strata.Util.Sarif
 

Strata/Languages/Python/PySpecPipeline.lean

@@ -390,20 +390,16 @@ public def translateCombinedLaurel (combined : Laurel.Program)
   let (coreOption, errors, _, _) ← translateCombinedLaurelWithLowered combined (profile := profile)
   return (coreOption, errors)
 
-/-- Errors from the pyAnalyzeLaurel pipeline. -/
-public inductive PipelineError where
-  /-- The Python source contains invalid code (bad method name, wrong arguments, etc.). -/
-  | userCode (range : SourceRange := .none) (msg : String)
-  /-- The pipeline encountered a Python construct it intentionally does not yet support. -/
-  | knownLimitation (msg : String)
-  /-- An unexpected failure — likely a bug in the tool itself. -/
-  | internal (msg : String)
-
-public instance : ToString PipelineError where
-  toString
-    | .userCode _ msg => s!"User code error: {msg}"
-    | .knownLimitation msg => s!"Known limitation: {msg}"
-    | .internal msg => msg
+/-- A batch of diagnostics emitted by the pyAnalyzeLaurel pipeline. Routing
+to an exit category is driven by each entry's `DiagnosticType` via
+`classifyDiagnostics`. -/
+public abbrev PipelineError := List DiagnosticModel
+
+public def mkUserCodeDiagnostic (filePath : String) (range : SourceRange) (msg : String)
+    : DiagnosticModel :=
+  { fileRange := { file := .file filePath, range := range }
+    message := msg
+    type := .UserError }
 
 /-- Run the pyAnalyzeLaurel pipeline: read a Python Ion program,
     resolve overloads from dispatch files, load PySpec declarations,
@@ -430,17 +426,19 @@ public def pythonAndSpecToLaurel
     (quiet : Bool := false)
     (warningSummaryFile : Option String := none)
     : EIO PipelineError Laurel.Program := do
+  let metadataPath := sourcePath.getD pythonIonPath
+  let internalErr (msg : String) : PipelineError :=
+    [DiagnosticModel.fromMessage msg (type := .StrataBug)]
   let stmts ← profileStep profile "Read Python Ion" do
     match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with
     | .ok r => pure r
-    | .error msg => throw (.internal msg)
+    | .error msg => throw (internalErr msg)
 
   let result ← profileStep profile "Resolve and build Laurel prelude" do
     match ← resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir (quiet := quiet) |>.toBaseIO with
     | .ok r => pure r
-    | .error msg => throw (.internal msg)
+    | .error msg => throw (internalErr msg)
 
-  -- Print and write PySpec warnings before later stages can fail
   let pyspecWarnings := result.pyspecWarnings
   if pyspecWarnings.size > 0 && !quiet then
     let _ ← IO.eprintln
@@ -468,19 +466,20 @@ public def pythonAndSpecToLaurel
 
   let preludeInfo := buildPreludeInfo result
 
-  let metadataPath := sourcePath.getD pythonIonPath
   let (laurelProgram, _ctx) ← profileStep profile "Translate Python to Laurel" do
     match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with
-    | .error (.userPythonError range msg) => throw (.userCode range msg)
+    | .error (.userPythonError range msg) =>
+        throw [mkUserCodeDiagnostic metadataPath range msg]
     | .error (.unsupportedConstruct msg ast) =>
-        throw (.knownLimitation s!"Unsupported construct: {msg}\nAST: {ast}")
-    | .error e => throw (.internal s!"Python to Laurel translation failed: {e}")
+        throw [DiagnosticModel.fromMessage s!"Unsupported construct: {msg}\nAST: {ast}"
+                 (type := .NotYetImplemented)]
+    | .error e => throw (internalErr s!"Python to Laurel translation failed: {e}")
     | .ok result => pure result
 
   let filteredPrelude ← profileStep profile "Filter prelude" do
     match Laurel.filterPrelude result.laurelProgram laurelProgram with
     | .ok prog => pure prog
-    | .error msg => throw (.internal msg)
+    | .error msg => throw (internalErr msg)
 
   profileStep profile "Combine PySpec and user Laurel" do
     return combinePySpecLaurel filteredPrelude laurelProgram

Strata/Util/DiagnosticClassifier.lean

@@ -0,0 +1,36 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Util.FileRange
+
+/-! # Diagnostic Classifier
+
+Priority order: StrataBug > UserError > NotYetImplemented.
+Empty or warnings-only batches fall through to `internalError`.
+-/
+
+public section
+namespace Strata
+
+inductive DiagnosticOutcome where
+  | internalError
+  | userError
+  | knownLimitation
+  deriving DecidableEq, Repr, Inhabited
+
+def classifyDiagnostics (diags : List DiagnosticModel) : DiagnosticOutcome :=
+  if diags.any (fun d => d.type == DiagnosticType.StrataBug) then
+    .internalError
+  else if diags.any (fun d => d.type == DiagnosticType.UserError) then
+    .userError
+  else if diags.any (fun d => d.type == DiagnosticType.NotYetImplemented) then
+    .knownLimitation
+  else
+    .internalError
+
+end Strata
+end

StrataMain.lean

@@ -26,6 +26,7 @@ import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Languages.Laurel.Laurel
 import Strata.Languages.Core.EntryPoint
 import Strata.Transform.ProcedureInlining
+import Strata.Util.DiagnosticClassifier
 import Strata.Util.IO
 
 import Strata.SimpleAPI
@@ -506,6 +507,56 @@ private def exitPyAnalyzeKnownLimitation {α} (message : String) : IO α := do
   printPyAnalyzeResult "Known limitation" message
   IO.Process.exit ExitCode.knownLimitation
 
+/-- Render diagnostics through `DiagnosticModel.format` so locations resolve
+    against the user's source. -/
+private def formatDiagnostics (diags : List DiagnosticModel)
+    (fileMap : Option Lean.FileMap) : String :=
+  match fileMap with
+  | none => toString diags
+  | some _ =>
+    String.intercalate "; " (diags.map (fun d => toString (d.format fileMap)))
+
+/-- Render a user-code diagnostic as "`msg` at line N, col M". -/
+private def formatUserErrorMessage (d : DiagnosticModel) (fileMap : Option Lean.FileMap) : String :=
+  let location := if d.fileRange.range.isNone then "" else
+    match fileMap with
+    | some fm =>
+      let pos := fm.toPosition d.fileRange.range.start
+      s!" at line {pos.line}, col {pos.column}"
+    | none => ""
+  s!"{d.message}{location}"
+
+/-- Classify `diags` and exit with the matching `pyAnalyzeLaurel` category.
+    `prefixMsg` is prepended only to internal-error details. -/
+private def classifyDiagnosticsAndExit {α} (prefixMsg : String)
+    (diags : List DiagnosticModel) (fileMap : Option Lean.FileMap) : IO α := do
+  let firstOf (t : DiagnosticType) (fmt : DiagnosticModel → String) : String :=
+    match (diags.filter (·.type == t)).head? with
+    | some d => fmt d
+    | none => formatDiagnostics diags fileMap
+  match classifyDiagnostics diags with
+  | .internalError   =>
+    exitPyAnalyzeInternalError s!"{prefixMsg}: {formatDiagnostics diags fileMap}"
+  | .userError       =>
+    exitPyAnalyzeUserError (firstOf .UserError (formatUserErrorMessage · fileMap))
+  | .knownLimitation =>
+    exitPyAnalyzeKnownLimitation (firstOf .NotYetImplemented (·.message))
+
+/-- Emit SMT `set-info` lines and write `user_errors.txt` for the first
+    user-code diagnostic in the batch. -/
+private def emitUserErrorsFile (diags : List DiagnosticModel) : IO Unit := do
+  let some d := (diags.filter (·.type == DiagnosticType.UserError)).head? | pure ()
+  let .file filePath := d.fileRange.file
+  let range := d.fileRange.range
+  let mut lines := #[s!"(set-info :file {Strata.escapeSMTStringLit filePath})"]
+  unless range.isNone do
+    lines := lines.push s!"(set-info :start {range.start})"
+    lines := lines.push s!"(set-info :stop {range.stop})"
+  lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit d.message})"
+  for line in lines do
+    IO.println line
+  IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n")
+
 /-- Print the final RESULT/DETAIL lines based on solver outcomes.
     Always called on successful pipeline completion (as opposed to the
     exit helpers above, which are called on early pipeline failure).
@@ -615,29 +666,10 @@ def pyAnalyzeLaurelCommand : Command where
                 (quiet := quiet)
                 (warningSummaryFile := warningSummaryFile) |>.toBaseIO with
       | .ok r => pure r
-      | .error (.userCode range msg) =>
-        let location := if range.isNone then "" else
-          match mfm with
-          | some (_, fm) =>
-            let pos := fm.toPosition range.start
-            s!" at line {pos.line}, col {pos.column}"
-          | none => ""
-        let filePath' := sourcePath.getD filePath
-        let mut lines := #[
-          s!"(set-info :file {Strata.escapeSMTStringLit filePath'})"
-        ]
-        unless range.isNone do
-          lines := lines.push s!"(set-info :start {range.start})"
-          lines := lines.push s!"(set-info :stop {range.stop})"
-        lines := lines.push s!"(set-info :error-message {Strata.escapeSMTStringLit msg})"
-        for line in lines do
-          IO.println line
-        IO.FS.writeFile "user_errors.txt" (String.intercalate "\n" lines.toList ++ "\n")
-        exitPyAnalyzeUserError s!"{msg}{location}"
-      | .error (.knownLimitation msg) =>
-        exitPyAnalyzeKnownLimitation msg
-      | .error (.internal msg) =>
-        exitPyAnalyzeInternalError msg
+      | .error diags =>
+        emitUserErrorsFile diags
+        let fileMap := mfm.map (·.2)
+        classifyDiagnosticsAndExit "Python to Laurel translation failed" diags fileMap
 
     if verbose then
       IO.println "\n==== Laurel Program ===="
@@ -656,7 +688,10 @@ def pyAnalyzeLaurelCommand : Command where
     let coreProgram ←
       match coreProgramOption with
       | none =>
-        exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}"
+        emitUserErrorsFile laurelTranslateErrors
+        let fileMap := mfm.map (·.2)
+        classifyDiagnosticsAndExit "Laurel to Core translation failed"
+          laurelTranslateErrors fileMap
       | some core => pure core
 
     if verbose then

StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.expected

@@ -0,0 +1,6 @@
+(set-info :file "StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py")
+(set-info :start 69)
+(set-info :stop 77)
+(set-info :error-message "calls to procedures are not supported in functions or contracts")
+DETAIL: calls to procedures are not supported in functions or contracts at line 5, col 22
+RESULT: User error

StrataTest/Languages/Python/expected_laurel/test_laurel_to_core_user_error.user_errors.expected

@@ -0,0 +1,4 @@
+(set-info :file "StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py")
+(set-info :start 69)
+(set-info :stop 77)
+(set-info :error-message "calls to procedures are not supported in functions or contracts")

StrataTest/Languages/Python/tests/test_laurel_to_core_user_error.py

@@ -0,0 +1,5 @@
+def helper() -> int:
+    return 0
+
+def main():
+    assert helper() < helper() < 10, "chained compare with procedure calls"

StrataTest/Util/DiagnosticClassifier.lean

@@ -0,0 +1,31 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+meta import Strata.Util.DiagnosticClassifier
+import Strata.Util.DiagnosticClassifier
+
+open Strata
+
+def mkDiag (t : DiagnosticType) : DiagnosticModel :=
+  { fileRange := FileRange.unknown, message := "test", type := t }
+
+-- Individual arms
+#guard classifyDiagnostics [mkDiag .StrataBug] = .internalError
+#guard classifyDiagnostics [mkDiag .UserError] = .userError
+#guard classifyDiagnostics [mkDiag .NotYetImplemented] = .knownLimitation
+
+-- Priority: StrataBug > UserError > NotYetImplemented
+#guard classifyDiagnostics [mkDiag .UserError, mkDiag .StrataBug] = .internalError
+#guard classifyDiagnostics [mkDiag .StrataBug, mkDiag .UserError] = .internalError
+#guard classifyDiagnostics [mkDiag .NotYetImplemented, mkDiag .UserError] = .userError
+#guard classifyDiagnostics
+  [mkDiag .NotYetImplemented, mkDiag .UserError, mkDiag .StrataBug] = .internalError
+
+-- Defensive fallthrough
+#guard classifyDiagnostics [] = .internalError
+#guard classifyDiagnostics [mkDiag .Warning] = .internalError
+#guard classifyDiagnostics [mkDiag .Warning, mkDiag .Warning] = .internalError