pyspec: add --reject-approximations CLI flag

Strata/Languages/Python/Approximation.lean

@@ -0,0 +1,50 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+/-!
+# Approximation diagnostics
+
+Single source of truth for the wording and `[approximation]` prefix used by
+both the Python→Laurel translator and the PySpec parser when an unsupported
+Python construct is approximated (or silently dropped) under lax mode and
+would be rejected as an error under `--reject-approximations`. Keeping the
+prefix in one place lets downstream tooling filter on it reliably.
+-/
+
+public section
+
+namespace Strata.Python.Approximation
+
+/-- Kind of approximation site. -/
+inductive Kind where
+  /-- The translator emits a havoc'd `Hole` instead of a faithful translation. -/
+  | hole
+  /-- The translator silently drops the construct from the lowered program. -/
+  | drop
+  /-- The PySpec parser fell back to `.placeholder` and emitted a warning;
+      strict mode promotes that warning to an error. -/
+  | warningPromotion
+  deriving DecidableEq, Repr
+
+/-- The `[approximation] ` prefix that downstream tooling filters on. Must
+    not change without coordinating with consumers. -/
+def prefixTag : String := "[approximation] "
+
+/-- Render a strict-mode approximation diagnostic. The `construct` argument
+    names the surface form (e.g. `"BinOp Div"`) for `.hole` and `.drop`; for
+    `.warningPromotion`, it carries the original warning message verbatim. -/
+def render : Kind → (construct : String) → String
+  | .hole, c =>
+    s!"{prefixTag}{c} is approximated as Hole; not in the sound subset"
+  | .drop, c =>
+    s!"{prefixTag}{c} is silently dropped by current translation; not in the sound subset"
+  | .warningPromotion, msg =>
+    s!"{prefixTag}{msg}"
+
+end Strata.Python.Approximation
+
+end

Strata/Languages/Python/PySpecPipeline.lean

@@ -134,7 +134,8 @@ private def mergeOverloads (old new : OverloadTable) : OverloadTable :=
     to namespace all generated Laurel names (e.g., `"servicelib_Storage"` for
     module `servicelib.Storage`). -/
 private def buildPySpecLaurelM (pyspecEntries : Array (Python.ModuleName × String))
-    (overloads : OverloadTable) : Pipeline.PipelineM PySpecLaurelResult := do
+    (overloads : OverloadTable) (rejectApproximations : Bool := false)
+    : Pipeline.PipelineM PySpecLaurelResult := do
   let mut combinedProcedures : Array (Laurel.Procedure × String) := #[]
   let mut combinedTypes : Array (Laurel.TypeDefinition × String) := #[]
   let mut allOverloads := overloads
@@ -150,6 +151,7 @@ private def buildPySpecLaurelM (pyspecEntries : Array (Python.ModuleName × Stri
         emitMessageAndAbort .pySpecReadError msg (file := ionFile)
     let { program, errors, overloads, typeAliases, exhaustiveClasses } :=
       Python.Specs.ToLaurel.signaturesToLaurel ionPath sigs moduleName
+        (rejectApproximations := rejectApproximations)
     for msg in errors do
       Pipeline.addMessage msg
       if msg.kind.impact.isFatal then throw ()
@@ -207,8 +209,9 @@ private def buildPySpecLaurelM (pyspecEntries : Array (Python.ModuleName × Stri
 public def buildPySpecLaurel
     (ctx : Pipeline.PipelineContext)
     (pyspecEntries : Array (Python.ModuleName × String))
-    (overloads : OverloadTable) : EIO Unit PySpecLaurelResult :=
-  buildPySpecLaurelM pyspecEntries overloads |>.run ctx
+    (overloads : OverloadTable) (rejectApproximations : Bool := false)
+    : EIO Unit PySpecLaurelResult :=
+  buildPySpecLaurelM pyspecEntries overloads (rejectApproximations := rejectApproximations) |>.run ctx
 
 /-- Read dispatch Ion files and merge their overload tables. -/
 private def readDispatchOverloadsM
@@ -278,6 +281,7 @@ public def resolveAndBuildLaurelPrelude
     (pyspecModules : Array String)
     (stmts : Array (Python.stmt SourceRange))
     (specDir : System.FilePath := ".")
+    (rejectApproximations : Bool := false)
     : Pipeline.PipelineM PySpecLaurelResult := do
   -- Dispatch modules (fatal on invalid name or missing file)
   let dispatchEntries ← resolveModules dispatchModules specDir
@@ -296,6 +300,7 @@ public def resolveAndBuildLaurelPrelude
   -- Explicit pyspec modules (fatal on invalid name or missing file)
   let explicitEntries ← resolveModules pyspecModules specDir
   buildPySpecLaurelM (autoSpecEntries ++ explicitEntries) dispatchOverloads
+    (rejectApproximations := rejectApproximations)
 
 /-! ### Pipeline Steps -/
 
@@ -427,6 +432,7 @@ public def pythonAndSpecToLaurel
     (pyspecModules : Array String := #[])
     (sourcePath : Option String := none)
     (specDir : System.FilePath := ".")
+    (rejectApproximations : Bool := false)
     : Pipeline.PipelineM Laurel.Program := do
   let stmts ← Pipeline.withPhase "readPythonIon" do
     match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with
@@ -436,12 +442,14 @@ public def pythonAndSpecToLaurel
 
   let result ← Pipeline.withPhase "resolveAndBuildPrelude" do
     resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir
+      (rejectApproximations := rejectApproximations)
 
   let preludeInfo := buildPreludeInfo result
   let metadataPath := sourcePath.getD pythonIonPath
 
   let (laurelProgram, _ctx) ←
-    match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with
+    match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads
+            (rejectApproximations := rejectApproximations) with
     | .error (.userPythonError range msg) =>
       emitMessageAndAbort (file := sourcePath.getD pythonIonPath) (loc := range)
         .laurelLoweringUserError msg