/-
  Infoductor.Test — generic Foundation end-to-end tests
  =====================================================
  Compile-time exercise of the Foundation layer (Phases A–D'.5).
  Cubical-transport-specific tests live downstream in
  `infoductor-cubical/InfoductorCubical/Test.lean`.

  - Phase A: meta-mirror types.
  - Phase B: Edit monad + restructure.
  - Phase C: @[macroAlias].
  - Phase D'/D'.5: @[methodology] + @[metaPath] + cubical_search.
-/

import Infoductor.Foundation.Methodology
import Infoductor.Foundation.MetaPath
import Infoductor.Foundation.MetaParse

namespace Infoductor.Test

open Infoductor

-- ── 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.  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.  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

-- ── Source-rendering soundness ─────────────────────────────────────────────
-- The renderer's output, when elaborated by Lean, reconstructs the
-- same value.  These checks witness round-trip via the elaborator
-- itself: the rendered string is literally Lean source and the
-- expected term-on-the-RHS is what Lean parses it to.

/-- Empty MetaCTerm renders to its own constructor name. -/
example : MetaCTerm.toLeanSource .empty = "Infoductor.MetaCTerm.empty" := rfl

/-- The MetaClassifier renderer renders atomic arms by name. -/
example :
    MetaClassifier.toLeanSource .always = "Infoductor.MetaClassifier.always" :=
  rfl

example :
    MetaClassifier.toLeanSource .never = "Infoductor.MetaClassifier.never" := rfl

/-- The atomic MetaArtifact arm renders to its constructor name. -/
example :
    MetaArtifact.toLeanSource .empty = "Infoductor.MetaArtifact.empty" := rfl

-- Non-atomic arms involve `s!`-interpolation and `repr`, which
-- don't reduce in the kernel for `rfl`.  Their soundness claim
-- is round-trip via Lean's elaborator: parsing the rendered
-- string gives back an expression that elaborates to the same
-- value.  Live `#eval`s display the rendered forms for inspection.
#eval MetaCTerm.toLeanSource (.ident `Foo)
#eval MetaCTerm.toLeanSource (.sym "x")
#eval MetaCTerm.toLeanSource (.app (.ident `Foo) (.sym "x"))
#eval MetaClassifier.toLeanSource (.atDecl `Bar)
#eval MetaArtifact.toLeanSource (.cterm .empty)
#eval MetaArtifact.toLeanSource (.cterm (.ident `Foo))

-- ── String → MetaCTerm parser round-trip ───────────────────────────────────
-- The hand-written parser in `Foundation.MetaParse` is the inverse
-- of the renderer.  Each example below feeds a MetaCTerm through
-- the renderer, then through the parser, and demands identity.
-- Verified at compile time via `native_decide` — Lean compiles the
-- round-trip check to native code and runs it.

example :
    Infoductor.MetaCTerm.fromLeanSource? (MetaCTerm.toLeanSource .empty) = some .empty := by
  native_decide

example :
    Infoductor.MetaCTerm.fromLeanSource? (MetaCTerm.toLeanSource (.ident `Foo)) =
      some (.ident `Foo) := by
  native_decide

example :
    Infoductor.MetaCTerm.fromLeanSource? (MetaCTerm.toLeanSource (.sym "x")) =
      some (.sym "x") := by
  native_decide

example :
    Infoductor.MetaCTerm.fromLeanSource?
      (MetaCTerm.toLeanSource (.app (.ident `Foo) (.sym "x"))) =
      some (.app (.ident `Foo) (.sym "x")) := by
  native_decide

example :
    Infoductor.MetaCTerm.fromLeanSource?
      (MetaCTerm.toLeanSource (.lam "x" (.sym "x"))) =
      some (.lam "x" (.sym "x")) := by
  native_decide

example :
    Infoductor.MetaCTerm.fromLeanSource?
      (MetaCTerm.toLeanSource
        (.comp "i" (.ident `Univ) .always (.sym "u") (.sym "t"))) =
      some (.comp "i" (.ident `Univ) .always (.sym "u") (.sym "t")) := by
  native_decide

example :
    Infoductor.MetaCTerm.fromLeanSource?
      (MetaCTerm.toLeanSource
        (.transp "i" (.ident `Univ) (.atDecl `j) (.sym "t"))) =
      some (.transp "i" (.ident `Univ) (.atDecl `j) (.sym "t")) := by
  native_decide

example :
    Infoductor.MetaClassifier.fromLeanSource? (MetaClassifier.toLeanSource .always) =
      some .always := by
  native_decide

example :
    Infoductor.MetaClassifier.fromLeanSource?
      (MetaClassifier.toLeanSource (.meet .always (.atDecl `Foo))) =
      some (.meet .always (.atDecl `Foo)) := by
  native_decide

-- MetaArtifact has a `Lean.Syntax` arm (`.declAt`) which lacks
-- `DecidableEq`, so we compare round-trips up to rendering — i.e.,
-- the parsed value re-renders to the same string.  Since the
-- forward rendering is injective on the arms we exercise, this is
-- equivalent to structural equality on those arms.

example :
    ((Infoductor.MetaArtifact.fromLeanSource? (MetaArtifact.toLeanSource .empty)).map
      MetaArtifact.toLeanSource) =
      some (MetaArtifact.toLeanSource .empty) := by
  native_decide

example :
    ((Infoductor.MetaArtifact.fromLeanSource?
        (MetaArtifact.toLeanSource (.cterm (.ident `Foo)))).map
      MetaArtifact.toLeanSource) =
      some (MetaArtifact.toLeanSource (.cterm (.ident `Foo))) := by
  native_decide

-- ── 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. -/
def printRegistrySizes : Lean.CoreM Unit := do
  let aliases ← getAliases
  let methodologies ← getMethodologies
  let paths ← getMetaPaths
  IO.println s!"[Infoductor.Test] aliases={aliases.size} \
                methodologies={methodologies.size} paths={paths.size}"

end Infoductor.Test