92fc4f9682
A hand-written tokenizer + recursive-descent parser that reads
the Lean source emitted by `toLeanSource` and reconstructs the
original meta-mirror value. Foundation/MetaParse.lean: 300
lines, faithful to the renderer's exact format.
Components:
· Token type (parens, ident chains, string literals, num literals).
· `tokenize : List Char → List Token` (partial; structural
decrease is implicit via helpers).
· `parseName?`, `parseClassifier?`, `parseMetaCTerm?`,
`parseArtifact?` — recursive-descent, return Option (T × tail).
· `MetaCTerm.fromLeanSource?` / `MetaClassifier.fromLeanSource?`
/ `MetaArtifact.fromLeanSource?` — top-level wrappers
demanding full input consumption.
Foundation/Meta.lean: derive `DecidableEq` on `MetaCTerm` (its
field types — Lean.Name, String, MetaClassifier — all have
DecidableEq). Switch FaceFormula.eq0/eq1 encoding from
`Name.appendAfter "_eq_0"` (string suffix) to a 2-component
`Name.mkStr (.mkSimple "eq0") i.name` form so reflection
round-trips by rfl with no string-suffix munging.
Foundation/MetaParse.lean: parsers are `partial def` because
the recursive calls land on output tails of helper readers,
which Lean can't see as structurally smaller without auxiliary
"consumes input" lemmas. Kernel-reducible round-trip is
deferred — `native_decide`-based tests in Infoductor/Test.lean
witness round-trip operationally for every meta-mirror arm.
Tests: 11 native_decide examples covering empty/ident/sym/app/
lam/comp/transp on MetaCTerm, always/meet on MetaClassifier,
empty/cterm on MetaArtifact (artifact uses rendering-equivalence
since Lean.Syntax in `.declAt` lacks DecidableEq).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
265 lines
11 KiB
Text
265 lines
11 KiB
Text
/-
|
||
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
|