import Semantics.RRC.Emit
import Semantics.RRCLogogramProjection

open Semantics.RRC.Emit
open Semantics.RRCLogogramProjection

-- RRC Watchdog -- classifies a proof attempt through the RRC alignment gate.
-- CLI: lake exe rrc-watchdog --pist-label <l> --exact-label <l> --rrc-shape <s>
-- Returns JSON with alignment status + score. Exit 0 if score >= 86 (alignedProxy).

structure AlignmentCheckResult where
  status   : String
  score    : Nat
  warnings : List String

def renderAlignment (s : AlignmentStatus) : String :=
  match s with
  | .alignedExact                   => "alignedExact"
  | .alignedProxy                   => "alignedProxy"
  | .compatibleStructuralProjection => "compatibleStructuralProjection"
  | .alignmentWarning               => "alignmentWarning"
  | .missingPrediction              => "missingPrediction"

def checkAlignment (status : AlignmentStatus) : AlignmentCheckResult :=
  { status   := renderAlignment status
    score    := alignmentScore status
    warnings := alignmentWarnings status }

def warningsToJson (ws : List String) : String :=
  "[" ++ String.intercalate ", " (ws.map fun w => "\"" ++ w ++ "\"") ++ "]"

def resultToJson (r : AlignmentCheckResult) : String :=
  "{\n  \"alignmentStatus\": \"" ++ r.status ++ "\",\n  \"score\": " ++ toString r.score ++ ",\n  \"warnings\": " ++ warningsToJson r.warnings ++ "\n}"

def classifyLabels (pistProxy : Option String) (pistExact : Option String) (shape : RRCShape) : AlignmentCheckResult :=
  let row : FixtureRow := {
    equationId := "rrc_watchdog_proof"
    name := "watchdog_classification"
    shape := shape
    status := .candidate
    rrcKind := "watchdog"
    weakAxesCnt := 0
    pistProxyLabel := pistProxy
    pistExactLabel := pistExact
    operatorTokens := []
    invariantsDeclared := "watchdog"
    boundaryConds := "watchdog"
    templateKey := "receipt"
    templateParams := ""
  }
  checkAlignment (determineAlignment row)

partial def parseArg (args : List String) (flag : String) : Option String :=
  match args with
  | [] => none
  | a :: b :: rest =>
    if a = flag then some b
    else parseArg (b :: rest) flag
  | _ :: rest => parseArg rest flag

def main (args : List String) : IO Unit := do
  if args.isEmpty || args.contains "--help" then
    IO.println "Usage: rrc-watchdog [--pist-label <l>] [--exact-label <l>] --rrc-shape <s>"
    IO.println ""
    IO.println "Shapes: signalShapedRouteCompiler, projectableGeometryTopology,"
    IO.println "        cognitiveLoadField, cadForceProbeReceipt, logogramProjection,"
    IO.println "        holdForUnlawfulOrUnderspecifiedShape"
    return ()

  let pistProxy := parseArg args "--pist-label"
  let pistExact := parseArg args "--exact-label"
  let shapeStr  := parseArg args "--rrc-shape"

  let shape : RRCShape := match shapeStr with
    | some "signalShapedRouteCompiler"         => .signalShapedRouteCompiler
    | some "projectableGeometryTopology"       => .projectableGeometryTopology
    | some "cognitiveLoadField"                => .cognitiveLoadField
    | some "cadForceProbeReceipt"              => .cadForceProbeReceipt
    | some "logogramProjection"                => .logogramProjection
    | some "holdForUnlawfulOrUnderspecifiedShape" => .holdForUnlawfulOrUnderspecifiedShape
    | _                                         => .holdForUnlawfulOrUnderspecifiedShape

  let result := classifyLabels pistProxy pistExact shape
  IO.println (resultToJson result)

  if result.score ≥ 86 then
    IO.Process.exit 0
  else
    IO.Process.exit 1