-- PistClassifyTrace.lean
-- SilverSight-ruleset-first proof-trace classifier executable.
--
-- Authority: this executable is the sole classifier. It reads a raw trace
-- JSON, computes spectral features with Q16_16 arithmetic, and emits the
-- predicted RRC shape and tactic family. Python shims may only format I/O
-- and call this executable.

import Semantics.PIST.Spectral
import Semantics.PIST.Classify
import Lean.Data.Json

open Lean
open Semantics.PIST

namespace PistClassifyTrace

/-- Raw input expected from the Python shim. -/
structure Input where
  name : String
  transition_matrix : Array (Array Int)
  deriving FromJson

/-- Shape string used when no higher-energy regime is detected.
    Matches RRC.Emit.shapeStr for HoldForUnlawfulOrUnderspecifiedShape. -/
def holdShape : String := "HoldForUnlawfulOrUnderspecifiedShape"

/-- Map the library tactic family to the Python-facing string. -/
def tacticFamilyString : Spectral.TacticFamily → String
  | .rewrite       => "rewrite"
  | .normalization => "normalization"
  | .arithmetic    => "arithmetic"
  | .induction     => "induction"
  | .algebraic     => "algebraic"
  | .case_analysis => "case_analysis"
  | .discharge      => "discharge"
  | .reflexivity   => "reflexivity"
  | .unknown       => "unknown"

/-- Build a JSON object from a Q16_16 spectral profile. -/
def spectralProfileJson (p : Spectral.SpectralProfile) : Json :=
  Json.mkObj [
    ("matrix_size",              toJson p.matrix_size.toInt),
    ("rank",                     toJson p.rank.toInt),
    ("spectral_gap",             toJson p.spectral_gap.toInt),
    ("density",                  toJson p.density.toInt),
    ("trace_val",                toJson p.trace_val.toInt),
    ("frobenius_norm",           toJson p.frobenius_norm.toInt),
    ("laplacian_zero_count",     toJson p.laplacian_zero_count.toInt),
    ("adjacency_eigenvalue_max", toJson p.adjacency_eigenvalue_max.toInt),
    ("laplacian_eigenvalue_max", toJson p.laplacian_eigenvalue_max.toInt),
    ("singular_value_max",       toJson p.singular_value_max.toInt)
  ]

/-- Build the classifier output JSON. -/
def outputJson (name : String) (profile : Spectral.SpectralProfile)
    (shape : String) (tactic : String) : Json :=
  Json.mkObj [
    ("theorem_name",        toJson name),
    ("spectral_radius",     toJson profile.adjacency_eigenvalue_max.toInt),
    ("spectral_radius_q16", toJson profile.adjacency_eigenvalue_max.toInt),
    ("predicted_rrc_shape", toJson shape),
    ("tactic_family",       toJson tactic),
    ("spectral_profile",    spectralProfileJson profile)
  ]

end PistClassifyTrace

def main (args : List String) : IO Unit := do
  let inputStr ←
    match args with
    | [] =>
        let stdin ← IO.getStdin
        stdin.readToEnd
    | [path] => IO.FS.readFile path
    | _ => throw (IO.userError "Usage: pist-classify-trace [trace.json]")

  match Json.parse inputStr with
  | .error e =>
      IO.println (Json.compress (Json.mkObj [("error", toJson s!"JSON parse error: {e}")]))
  | .ok j =>
      match (fromJson? j : Except String PistClassifyTrace.Input) with
      | .error e =>
          IO.println (Json.compress (Json.mkObj [("error", toJson e)]))
      | .ok input =>
          let profile := Spectral.computeSpectral input.transition_matrix
          let shape := (Classify.classifyExact input.transition_matrix).getD PistClassifyTrace.holdShape
          let tactic := PistClassifyTrace.tacticFamilyString (Spectral.classifyTacticFromName input.name)
          IO.println (Json.compress (PistClassifyTrace.outputJson input.name profile shape tactic))