/-
  Topolei.Cubical.FFITest
  =======================
  Phase C.3 smoke test (2026-04-24).  Exercises the FFI wiring by
  running simple cubical terms through `eval` / `readback` / the
  normalizers.  With `@[implemented_by]` attached, these execute in
  the Rust backend at runtime.

  **Why not `#eval`?**  `#eval` runs at Lean's compile-time in the
  interpreter, which does not link our Rust staticlib.  Calling a
  Rust-backed function under the interpreter raises "Could not find
  native implementation of external declaration ..."  The tests here
  are `def`s + a `runSmokeTests : IO Unit` entry point that exercises
  them inside a compiled binary where Rust IS linked.

  Invoke from a compiled executable.  `Main.lean` can optionally
  route to `CubicalTransportFFITest.runSmokeTests` when passed
  `--cubical-test`.  Or a dedicated test exe target.
-/

import CubicalTransport.Readback
import CubicalTransport.FFI
import CubicalTransport.Inductive

open CubicalTransport.Inductive
open CubicalTransport.Inductive.CTerm

namespace CubicalTransportFFITest

-- ── Summarisers ────────────────────────────────────────────────────────────

def cvalSummary : CVal → String
  | .vneu (.nvar s)             => s!"vneu nvar {s}"
  | .vneu (.napp _ _)           => "vneu napp"
  | .vneu (.npapp _ _)          => "vneu npapp"
  | .vneu (.ntransp _ _ _ _)    => "vneu ntransp"
  | .vneu (.nhcomp _ _ _ _)     => "vneu nhcomp"
  | .vneu (.ncomp _ _ _ _ _)    => "vneu ncomp"
  | .vneu (.ncompN _ _ _ _ _)   => "vneu ncompN"
  | .vneu (.nglueIn _ _ _)      => "vneu nglueIn"
  | .vneu (.nunglue _ _ _)      => "vneu nunglue"
  | .vneu (.nfst _)             => "vneu nfst"
  | .vneu (.nsnd _)             => "vneu nsnd"
  | .vneu (.nIndElim _ _ _ _ _) => "vneu nIndElim"
  | .vlam _ x _                 => s!"vlam {x} ..."
  | .vplam _ i _                => s!"vplam {i.name} ..."
  | .vpair _ _                  => "vpair ..."
  | .vTranspFun _ _ _ _ _       => "vTranspFun"
  | .vHCompFun _ _ _ _          => "vHCompFun"
  | .vCompFun _ _ _ _ _ _ _     => "vCompFun"
  | .vTubeApp _ _               => "vTubeApp"
  | .vPathTransp _ _ _ _ _ _ _  => "vPathTransp"
  | .vctor _ c _ _              => s!"vctor {c} ..."
  | .vdimExpr _                 => "vdimExpr ..."

def ctermSummary : CTerm → String
  | .var x          => s!"var {x}"
  | .lam x _        => s!"lam {x} ..."
  | .app _ _        => "app ..."
  | .plam i _       => s!"plam {i.name} ..."
  | .pair _ _       => "pair ..."
  | .fst _          => "fst ..."
  | .snd _          => "snd ..."
  | .dimExpr _      => "dimExpr ..."
  | .ctor _ c _ _   => s!"ctor {c} ..."
  | .indElim _ _ _ _ _ => "indElim ..."
  | _               => "<other CTerm>"

-- ── Individual test definitions ────────────────────────────────────────────
-- Each returns (description, actual, expected) for runSmokeTests to print.

def tests : List (String × String × String) :=
  [ ("eval .nil (.var \"x\")",
     cvalSummary (eval .nil (.var "x")),
     "vneu nvar x"),
    ("eval .nil (.lam \"x\" (.var \"x\"))",
     cvalSummary (eval .nil (.lam "x" (.var "x"))),
     "vlam x ..."),
    ("(λx. x) y ⇓ y",
     cvalSummary (eval .nil (.app (.lam "x" (.var "x")) (.var "y"))),
     "vneu nvar y"),
    ("(a, b).fst ⇓ a",
     cvalSummary (eval .nil (.fst (.pair (.var "a") (.var "b")))),
     "vneu nvar a"),
    ("(a, b).snd ⇓ b",
     cvalSummary (eval .nil (.snd (.pair (.var "a") (.var "b")))),
     "vneu nvar b"),
    ("readback (eval .nil (.lam \"x\" (.var \"x\"))) ≡ .lam \"x\" ...",
     ctermSummary (readback (eval .nil (.lam "x" (.var "x")))),
     "lam x ..."),
    ("DimExpr.normalize (.inv .zero) ≡ .one",
     match DimExpr.normalize (.inv .zero) with
       | .one => "one"
       | _    => "<other>",
     "one"),
    ("DimExpr.normalize (.inv (.inv (.var i))) ≡ .var i",
     match DimExpr.normalize (.inv (.inv (.var ⟨"i"⟩))) with
       | .var j => s!"var {j.name}"
       | _      => "<other>",
     "var i"),
    ("FaceFormula.normalize (.meet .top (.eq0 i)) ≡ .eq0 i",
     match FaceFormula.normalize (.meet .top (.eq0 ⟨"i"⟩)) with
       | .eq0 j => s!"eq0 {j.name}"
       | _      => "<other>",
     "eq0 i"),
    -- ── β-rules: discharge the five cubical-closure axioms ─────────────────
    -- Each test exercises the path `Lean constructs a CVal closure →
    -- vApp/vPApp routes through Rust @[implemented_by] → forcer unfolds
    -- the CCHM RHS → result is no longer a stuck marker`.
    ("β vApp vTranspFun (const line, via beta::force_transp_fun)",
     cvalSummary (vApp
       (.vTranspFun ⟨"i"⟩ .univ .univ .bot (.vneu (.nvar "f")))
       (.vneu (.nvar "y"))),
     "vneu napp"),
    ("β vApp vHCompFun (stuck on .univ codA, via beta::force_hcomp_fun)",
     cvalSummary (vApp
       (.vHCompFun .univ .bot
         (.vplam .nil ⟨"j"⟩ (.var "tube_body"))
         (.vneu (.nvar "b")))
       (.vneu (.nvar "x"))),
     "vneu nhcomp"),
    ("β vApp vCompFun (φ=.bot collapses via C2, via beta::force_comp_fun)",
     cvalSummary (vApp
       (.vCompFun .nil ⟨"i"⟩ .univ .univ .bot (.var "u") (.var "t"))
       (.vneu (.nvar "y"))),
     "vneu napp"),
    ("β vPApp vTubeApp (via beta::force_tube_app)",
     cvalSummary (vPApp
       (.vTubeApp (.vplam .nil ⟨"j"⟩ (.var "tube_body")) (.vneu (.nvar "x")))
       (.var ⟨"r"⟩)),
     "vneu napp"),
    ("β vPApp vPathTransp at .zero ⇓ a(1)  (via beta::force_path_transp)",
     cvalSummary (vPApp
       (.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
       .zero),
     "vneu nvar a0"),
    ("β vPApp vPathTransp at .one ⇓ b(1)",
     cvalSummary (vPApp
       (.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
       .one),
     "vneu nvar b0"),
    ("β vPApp vPathTransp at var r ⇓ compN (CCHM 3-clause system)",
     cvalSummary (vPApp
       (.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p"))
       (.var ⟨"r"⟩)),
     "vneu ncompN"),
    -- ── REL1 inductive-type smoke tests ─────────────────────────────────────
    ("eval (zero : Nat) ⇓ vctor zero",
     cvalSummary (eval .nil zeroC),
     "vctor zero ..."),
    ("eval (succ (succ zero) : Nat) ⇓ vctor succ",
     cvalSummary (eval .nil (succC (succC zeroC))),
     "vctor succ ..."),
    ("eval (false : Bool) ⇓ vctor false",
     cvalSummary (eval .nil falseC),
     "vctor false ..."),
    ("eval (cons true nil : List Bool) ⇓ vctor cons",
     cvalSummary (eval .nil (consC CType.boolC trueC (nilC CType.boolC))),
     "vctor cons ..."),
    ("readback ∘ eval (succ zero : Nat) ≡ ctor succ",
     ctermSummary (readback (eval .nil (succC zeroC))),
     "ctor succ ..."),
    ("eval (base : S¹) ⇓ vctor base",
     cvalSummary (eval .nil baseC),
     "vctor base ..."),
    ("eval (loop @ r : S¹) ⇓ vctor loop",
     cvalSummary (eval .nil (loopC (.var ⟨"r"⟩))),
     "vctor loop ..."),
    ("indElim Bool false-case (true → \"yes\") on true ⇓ \"yes\"",
     cvalSummary (eval .nil
       (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") trueC)),
     "vneu nvar yes"),
    ("indElim Bool true-case on false ⇓ \"no\"",
     cvalSummary (eval .nil
       (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") falseC)),
     "vneu nvar no"),
    ("transp_ind T1: φ=.top is identity",
     cvalSummary (eval .nil
       (.transp ⟨"i"⟩ CType.natC .top zeroC)),
     "vctor zero ..."),
    ("transp_ind T2: constant Nat line is identity",
     cvalSummary (eval .nil
       (.transp ⟨"i"⟩ CType.natC (.eq0 ⟨"j"⟩) (succC zeroC))),
     "vctor succ ..."),
    ("comp_ind C1: φ=.top reduces to u[i:=1]",
     cvalSummary (eval .nil
       (.comp ⟨"i"⟩ CType.natC .top (succC zeroC) zeroC)),
     "vctor succ ...") ]

/-- Run every smoke test, print its actual vs expected.  Returns the
    number of failures. -/
def runSmokeTests : IO UInt32 := do
  IO.println "── Topolei cubical FFI smoke tests ──"
  let mut fails : UInt32 := 0
  for (desc, actual, expected) in tests do
    if actual == expected then
      IO.println s!"  ✅ {desc}"
    else
      IO.println s!"  ❌ {desc}"
      IO.println s!"       expected: {expected}"
      IO.println s!"       actual:   {actual}"
      fails := fails + 1
  IO.println s!"── {tests.length - fails.toNat} / {tests.length} passed ──"
  return fails

end CubicalTransportFFITest