cubical-transport-hott-lean4/CubicalTransport/Algebra/Test.lean

/-
  CubicalTransport.Algebra.Test — end-to-end tests
  ================================================
  Exercises the Phase A–D' Algebra layer at compile time:

  - Phase A: construct meta-mirror values; verify decidable
    equality.
  - Phase B: build an `Edit Unit` value via `restructure` and check
    `selfConsistent`; run the headless interpreter.
  - Phase C: register an alias via `@[macroAlias]` and verify it
    appears in the registry.
  - Phase D': register a methodology via `@[methodology]` and verify
    `cubical_search` finds it on a representative goal.

  These are compile-time correctness tests; the runtime smoke tests
  live in `FFITest.lean`.
-/

import CubicalTransport.Algebra.Methodology
import CubicalTransport.Algebra.MetaPath
import CubicalTransport.Algebra.EngineMethodologies
import CubicalTransport.Question

namespace CubicalTransport.Algebra.Test

open CubicalTransport.Algebra
open Question

-- ── Phase A: meta-mirror types ─────────────────────────────────────────────

/-- Meta-mirror types are inhabited and well-formed. -/
example : MetaCType := .theorem_
example : MetaCType := .file
example : MetaCType := .classifierSet

example : MetaClassifier := .always
example : MetaClassifier := .never
example : MetaClassifier := .meet (.atDecl `Foo) (.inFile "Bar.lean")

example : MetaArtifact := .source "def x := 1"
example : MetaArtifact := .empty
example : MetaArtifact := .refTo `Existing

example : MetaPosition :=
  { declName := `Test, filePath := "Test.lean", range := none }

/-- DecidableEq fires correctly on MetaClassifier. -/
example : decide (MetaClassifier.always = .always) = true := by decide
example : decide (MetaClassifier.always = .never) = false := by decide
example : decide ((.meet .always (.atDecl `Foo) : MetaClassifier) =
                  (.meet .always (.atDecl `Foo))) = true := by decide

-- ── Phase B: Edit + Context + restructure ───────────────────────────────────

/-- A simple restructure call produces an Edit with one op. -/
example :
    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let e := restructure pos .theorem_ .always (.source "def x := 1") .empty
    e.ops.length = 1 := by
  rfl

/-- The restructure picks `witness` when the classifier is `.always`. -/
example :
    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let e := restructure pos .theorem_ .always (.source "yes") (.source "no")
    (e.ops.head?).isSome = true := by
  rfl

/-- The restructure picks `fallback` when the classifier is `.never`. -/
example :
    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let e := restructure pos .theorem_ .never (.source "yes") (.source "no")
    (e.ops.head?).isSome = true := by
  rfl

/-- Self-consistency check on a single restructure op. -/
example :
    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let e := restructure pos .theorem_ .always (.source "x") .empty
    e.selfConsistent = true := by
  rfl

/-- A batch that removes a decl AND references it by `refTo` is
    flagged as inconsistent. -/
example :
    let pos₁ : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let pos₂ : MetaPosition := { declName := `Bar, filePath := "F.lean", range := none }
    let e : Edit Unit := do
      restructure pos₁ .theorem_ .always .empty .empty       -- removes Foo
      restructure pos₂ .theorem_ .always (.refTo `Foo) .empty  -- refs Foo
    e.selfConsistent = false := by
  rfl

-- ── Frozen aliases ──────────────────────────────────────────────────────────

/-- The `transport_artifact` alias produces a single Edit op. -/
example :
    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let e := transport_artifact pos .theorem_ (.source "x")
    e.ops.length = 1 := by rfl

/-- The `materialize` alias emits raw Lean source. -/
example :
    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
    let e := materialize pos .theorem_ "theorem x : True := trivial"
    e.ops.length = 1 := by rfl

-- ── Phase C: @[macroAlias] registration ─────────────────────────────────────

/-- A custom alias for testing.  Registered via the attribute below. -/
@[macroAlias]
def custom_alias_test (i : MetaPosition) : Edit Unit :=
  restructure i .definition .always (.source "test") .empty

-- ── Phase D': @[methodology] registration ───────────────────────────────────

/-- A trivial methodology: solves `True` goals.  Registered against
    a placeholder classifier name `IsTrueGoal`. -/
@[methodology IsTrueGoal]
theorem trueMethodology : True := True.intro

/-- `cubical_search` finds the registered methodology for `True`
    goals.  Demonstrates the dispatch loop end-to-end. -/
example : True := by cubical_search

/-- Methodology for `Eq.refl`-shaped goals.  Lean's `rfl` tactic
    handles these natively — registering as a methodology
    demonstrates that `cubical_search` can dispatch to non-trivial
    universe-equality goals. -/
@[methodology IsReflGoal]
theorem reflMethodologyNat (n : Nat) : n = n := rfl

example : 7 = 7 := by cubical_search

-- ── Phase D'.5: @[metaPath] + methodology-transport ─────────────────────────

/-- A trivial structural Path: every reflexivity goal is also a
    "trivial-truth" goal.  This declares the meta-Path so
    methodology-transport can lift `IsTrueGoal` methodologies onto
    `IsReflGoal` targets and vice versa. -/
@[metaPath IsReflGoal IsTrueGoal]
theorem refl_path_to_true (n : Nat) (_ : n = n) : True := True.intro

/-- An identity methodology that closes any `Iff.refl`-shaped goal. -/
@[methodology IsIffReflGoal]
theorem iffRefl (P : Prop) : P ↔ P := Iff.rfl

example : True ↔ True := by cubical_search

-- ── Engine-bound methodologies — concrete CompQ closers ─────────────────────
-- These register classifier-conditioned engine theorems as
-- `cubical_search`-applicable methodologies.  Each one fully
-- discharges its classifier via `decide` (since the classifier
-- predicates are Decidable for concrete `.top`/`.bot`/`.interval`
-- shapes), turning a hypothesis-bearing simp lemma into a stand-
-- alone closer.

/-- Closing methodology for full-face CompQ: literal `.top` face
    questions reduce to `eval env (u.substDim i .one)`.  Discharges
    `IsFullFace` via `rfl` (`.top = .top` after struct projection). -/
@[methodology IsCompQFullFace]
theorem compq_top_concrete (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) :=
  CompQ.ask_of_full_face _ rfl

/-- Closing methodology for full-face TranspQ: literal `.top` face
    transports reduce to identity. -/
@[methodology IsTranspQFullFace]
theorem transpq_top_concrete (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) :
    (TranspQ.mk env i A .top t).ask = eval env t :=
  TranspQ.ask_of_full_face _ rfl

/-- Closing methodology for interval-line TranspQ: any face on
    `.interval` reduces to identity. -/
@[methodology IsTranspQInterval]
theorem transpq_interval_concrete (env : CEnv) (i : DimVar)
    (φ : FaceFormula) (t : CTerm) :
    (TranspQ.mk env i .interval φ t).ask = eval env t :=
  TranspQ.ask_of_interval_line _ rfl

/-- `cubical_search` on a concrete CompQ full-face goal. -/
example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) := by
  cubical_search

/-- `cubical_search` on a concrete TranspQ interval-line goal. -/
example (env : CEnv) (i : DimVar) (t : CTerm) :
    (TranspQ.mk env i .interval .top t).ask = eval env t := by
  cubical_search

-- ── cubical_close: composite closer ─────────────────────────────────────────

/-- `cubical_close` succeeds on a CompQ goal that needs reduction. -/
example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) := by
  cubical_close

/-- `cubical_close` succeeds on a goal that's already trivial. -/
example : True := by cubical_close

/-- `cubical_close` succeeds on a TranspQ goal via simp routing. -/
example (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) :
    (TranspQ.mk env i A .top t).ask = eval env t := by
  cubical_close

-- ── Compile-time registry diagnostics ───────────────────────────────────────

/-- A diagnostic action that prints registry sizes.  Run via `#eval`
    inside a Lean session to verify that @[methodology] /
    @[macroAlias] / @[metaPath] declarations have populated the
    EnvExtensions.  This is the live way to inspect the registries
    (the standalone CLI in `AlgebraRestructure.lean` cannot — see
    its docstring for the Lean 4 EnvExtension limitation). -/
def printRegistrySizes : Lean.CoreM Unit := do
  let aliases ← getAliases
  let methodologies ← getMethodologies
  let paths ← getMetaPaths
  IO.println s!"[Algebra.Test] aliases={aliases.size} \
                methodologies={methodologies.size} paths={paths.size}"

end CubicalTransport.Algebra.Test