pyspec: decorator-recognition framework + diagnostics module

StrataPython/StrataPython/Specs.lean

@@ -9,6 +9,8 @@ import all    StrataDDM.Util.Fin
 import        StrataPython.ReadPython
 import        StrataPython.Specs.DDM
 public import StrataPython.Specs.Decls
+public import StrataPython.Specs.Diagnostics
+public import StrataPython.Specs.Decorators
 import StrataPython.Specs.MessageKind
 import        Strata.Util.DecideProp
 
@@ -79,17 +81,6 @@ open StrataDDM (SourceRange eformat Ann)
 
 namespace StrataPython.Specs
 
-/-- Type class for monads that support PySpec error and warning reporting. -/
-public class PySpecMClass (m : Type → Type) where
-  /-- Report an error at a specific source location. -/
-  specError (loc : SourceRange) (message : String) : m Unit
-  /-- Report a warning at a specific source location. -/
-  specWarning (loc : SourceRange) (message : String) : m Unit
-  /-- Run an action and check if any new errors were reported. -/
-  runChecked {α} (act : m α) : m (Bool × α)
-  /-- Run an action and return `true` if no new errors or warnings were reported. -/
-  runNoWarn {α} (act : m α) : m (Bool × α)
-
 open PySpecMClass (specError specWarning runChecked runNoWarn)
 
 

StrataPython/StrataPython/Specs/Decorators.lean

@@ -0,0 +1,159 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import StrataPython.Specs.Diagnostics
+public import StrataPython.ReadPython
+
+/-! # Generic decorator-recognition framework for PySpec
+
+Shared gearing for recognizing PySpec decorator surfaces (`@requires`,
+`@ensures`, `@overload`, …): `DecoratorForm` normalizes a decorator expression,
+the lambda/keyword helpers parse predicate-bearing calls, and `DecoratorScheme`
+is a composable recognizer. Depends only on `PySpecMClass` and the Python AST,
+not the spec pipeline. -/
+
+namespace StrataPython.Specs.Decorators
+
+open StrataDDM (SourceRange)
+open PySpecMClass (specError specWarning)
+
+/-- A decorator expression normalized across the four surface shapes
+    (`@name`, `@mod.name`, `@name(...)`, `@mod.name(...)`). -/
+public structure DecoratorForm where
+  /-- Qualifier of `@qualifier.name`; `none` for a bare `@name`. -/
+  qualifier : Option String
+  name : String
+  /-- Whether applied as a call (`@name(...)`) or bare (`@name`). -/
+  isCall : Bool
+  /-- Positional/keyword call args (empty unless `isCall`). -/
+  args : Array (expr SourceRange) := #[]
+  kwargs : Array (keyword SourceRange) := #[]
+  loc : SourceRange
+deriving Inhabited
+
+/-- Normalize a decorator expression into a `DecoratorForm`, or `none` if it is
+    not a recognized surface shape. -/
+public def DecoratorForm.ofExpr? (pyd : expr SourceRange) : Option DecoratorForm :=
+  match pyd with
+  | .Name loc ⟨_, name⟩ (.Load _) =>
+    some { qualifier := none, name, isCall := false, loc }
+  | .Attribute loc (.Name _ ⟨_, qual⟩ (.Load _)) ⟨_, attr⟩ (.Load _) =>
+    some { qualifier := some qual, name := attr, isCall := false, loc }
+  | .Call loc (.Name _ ⟨_, name⟩ (.Load _)) ⟨_, args⟩ ⟨_, kwargs⟩ =>
+    some { qualifier := none, name, isCall := true, args, kwargs, loc }
+  | .Call loc (.Attribute _ (.Name _ ⟨_, qual⟩ (.Load _)) ⟨_, attr⟩ (.Load _))
+      ⟨_, args⟩ ⟨_, kwargs⟩ =>
+    some { qualifier := some qual, name := attr, isCall := true, args, kwargs, loc }
+  | _ => none
+
+/-- True when this form is `@qualifier.name` (qualified, either call or bare). -/
+public def DecoratorForm.isQualified (f : DecoratorForm) (qualifier : String) : Bool :=
+  f.qualifier == some qualifier
+
+/-- The positional-only + positional + keyword-only binder names of a lambda's
+    argument list. -/
+public def lambdaBinderNames (lamArgs : arguments SourceRange) : Array String :=
+  let .mk_arguments _ ⟨_, posonly⟩ ⟨_, pos⟩ _ ⟨_, kwonly⟩ _ _ _ := lamArgs
+  (posonly ++ pos ++ kwonly).map fun a => let .mk_arg _ ⟨_, n⟩ _ _ := a; n
+
+/-- Pull the lambda body and its binder names from `args[0]` of a decorator
+    call. Reports a failure (severity chosen by the caller via `report`) and
+    returns `none` when the argument is missing or is not a lambda. -/
+public def expectLambda? {m : Type → Type} [Monad m]
+    (report : SourceRange → String → m Unit)
+    (what : String) (loc : SourceRange) (args : Array (expr SourceRange))
+    : m (Option (expr SourceRange × Array String)) := do
+  if h : args.size ≥ 1 then
+    match args[0] with
+    | .Lambda _ lamArgs lamBody => return some (lamBody, lambdaBinderNames lamArgs)
+    | _ => report loc s!"{what} expects a lambda as its first argument"; return none
+  else
+    report loc s!"{what} requires at least one argument"
+    return none
+
+/-- Warn about each lambda binder not present in `allowed`; such binders make the
+    predicate vacuous because nothing binds them at the use site. -/
+public def warnUnknownBinders {m : Type → Type} [Monad m] [PySpecMClass m]
+    (loc : SourceRange) (binders allowed : Array String)
+    (describe : String → String) : m Unit := do
+  for n in binders do
+    unless allowed.contains n do specWarning loc (describe n)
+
+/-- Read a required string-literal keyword `name=...` from a decorator call's
+    keyword arguments. Reports (via `what`-prefixed errors) a duplicate, a
+    non-string-literal value, and returns `none` if absent. -/
+public def stringKeyword? {m : Type → Type} [Monad m] [PySpecMClass m]
+    (what : String) (key : String) (kwargs : Array (keyword SourceRange))
+    : m (Option String) := do
+  let mut value : Option String := none
+  for kw in kwargs do
+    match kw.arg with
+    | ⟨_, some ⟨_, k⟩⟩ =>
+      if k == key then
+        if value.isSome then
+          specError kw.value.ann s!"{what}: duplicate {key}= keyword"
+        match kw.value with
+        | .Constant _ (.ConString _ ⟨_, s⟩) _ => value := some s
+        | _ => specError kw.value.ann s!"{what}: {key}= must be a string literal"
+    | _ => pure ()
+  return value
+
+/-- Report each keyword argument whose name is not in `allowed`, at a severity
+    chosen by the caller via `report`. -/
+public def reportUnexpectedKeywords {m : Type → Type} [Monad m]
+    (report : SourceRange → String → m Unit)
+    (what : String) (allowed : Array String) (kwargs : Array (keyword SourceRange))
+    : m Unit := do
+  for kw in kwargs do
+    match kw.arg with
+    | ⟨_, some ⟨_, k⟩⟩ =>
+      unless allowed.contains k do
+        report kw.value.ann s!"{what}: unexpected keyword '{k}'"
+    | _ => pure ()
+
+/-- A first-class decorator recognizer over an accumulator `σ`: an `init` value
+    plus an `absorb` step returning `(absorbed, σ')`. Contract: a decline
+    (`absorbed = false`) must be a no-op (accumulator unchanged, no diagnostics)
+    since `prod`/`run` may offer the form to another scheme; a successful absorb
+    owns the form. -/
+public structure DecoratorScheme (m : Type → Type) (σ : Type) where
+  /-- The empty accumulator before any decorator is seen. -/
+  init : σ
+  /-- Try to absorb one normalized decorator form (see the type docstring for
+      the decline-is-a-no-op contract). -/
+  absorb : DecoratorForm → σ → m (Bool × σ)
+
+/-- Compose two schemes over the product accumulator: a form is offered to `a`
+    first, and to `b` only if `a` declines. -/
+public def DecoratorScheme.prod {m : Type → Type} [Monad m] {σ₁ σ₂ : Type}
+    (a : DecoratorScheme m σ₁) (b : DecoratorScheme m σ₂)
+    : DecoratorScheme m (σ₁ × σ₂) where
+  init := (a.init, b.init)
+  absorb form := fun (s₁, s₂) => do
+    let (ok₁, s₁') ← a.absorb form s₁
+    if ok₁ then return (true, (s₁', s₂))
+    let (ok₂, s₂') ← b.absorb form s₂
+    return (ok₂, (s₁', s₂'))
+
+/-- Fold a scheme over a decorator list, normalizing each and offering it to the
+    scheme; anything not absorbed (or not a recognized shape) goes to
+    `onUnknown`. Returns the accumulator. -/
+public def DecoratorScheme.run {m : Type → Type} [Monad m] {σ : Type}
+    (scheme : DecoratorScheme m σ)
+    (decorators : Array (expr SourceRange))
+    (onUnknown : expr SourceRange → m Unit) : m σ := do
+  let mut acc := scheme.init
+  for pyd in decorators do
+    match DecoratorForm.ofExpr? pyd with
+    | none => onUnknown pyd
+    | some form =>
+      let (absorbed, acc') ← scheme.absorb form acc
+      acc := acc'
+      unless absorbed do onUnknown pyd
+  return acc
+
+end StrataPython.Specs.Decorators

StrataPython/StrataPython/Specs/Diagnostics.lean

@@ -0,0 +1,36 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import StrataDDM.Util.SourceRange
+
+/-! # Diagnostic interface for the PySpec parser
+
+`PySpecMClass` abstracts the error/warning reporting capability shared by the
+PySpec parsing monads. It lives in its own low-level module (rather than in
+`Specs.lean`) so that focused recognizers such as the native decorator surface
+(`Specs/Decorators.lean`) can be written generically over `[PySpecMClass m]`
+without importing — and creating an import cycle with — the full spec pipeline.
+
+The concrete instances for `PySpecM` and `SpecAssertionM` are defined in
+`Specs.lean`, alongside the state types they manipulate. -/
+
+namespace StrataPython.Specs
+
+open StrataDDM (SourceRange)
+
+/-- Type class for monads that support PySpec error and warning reporting. -/
+public class PySpecMClass (m : Type → Type) where
+  /-- Report an error at a specific source location. -/
+  specError (loc : SourceRange) (message : String) : m Unit
+  /-- Report a warning at a specific source location. -/
+  specWarning (loc : SourceRange) (message : String) : m Unit
+  /-- Run an action and check if any new errors were reported. -/
+  runChecked {α} (act : m α) : m (Bool × α)
+  /-- Run an action and return `true` if no new errors or warnings were reported. -/
+  runNoWarn {α} (act : m α) : m (Bool × α)
+
+end StrataPython.Specs