diff --git a/Infoductor.lean b/Infoductor.lean index d4b40bb..6434327 100644 --- a/Infoductor.lean +++ b/Infoductor.lean @@ -8,3 +8,4 @@ -/ import Infoductor.Foundation +import Infoductor.Test diff --git a/Infoductor/Foundation/Meta.lean b/Infoductor/Foundation/Meta.lean index 5490538..770071f 100644 --- a/Infoductor/Foundation/Meta.lean +++ b/Infoductor/Foundation/Meta.lean @@ -179,6 +179,65 @@ def MetaClassifier.decEq : (a b : MetaClassifier) → Decidable (a = b) instance : DecidableEq MetaClassifier := MetaClassifier.decEq +-- ── MetaCTerm — the structural meta-mirror of `CTerm` ────────────────────── +-- A faithful AST-level mirror of the cubical term language. Cubical +-- `CTerm` constructors map onto `MetaCTerm` constructors structurally, +-- so embedding round-trips through a partial inverse (`toCTerm?`). +-- See `Embed.lean` in the cubical bridge for the concrete maps and the +-- coreflection theorems. +-- +-- Generative basis (8 constructors): +-- · `ident n` — closed reference to a Lean declaration. +-- · `sym s` — open leaf (string-named local or dim-binder). +-- · `app f a` — universal application; encodes `papp`, `fst`, +-- `snd`, `pair`, `glueIn`, `unglue`, schema +-- ctors, and eliminators via `.ident`-headed +-- chains. +-- · `lam x t` — term-level lambda (binds `x`). +-- · `plam i t` — path-level lambda (binds dim-name `i`). +-- · `comp i A φ u t` — five-field composition, mirroring `compⁱ A φ u t`. +-- · `transp i A φ t` — four-field transport, mirroring `transpⁱ A φ t`. +-- · `empty` — placeholder for deletion / missing content. +-- +-- The `comp` and `transp` arms keep their face-formula slot as a +-- `MetaClassifier` (rather than a nested `MetaCTerm` encoding) so that +-- classifier-at-position semantics flow through unchanged from +-- `Edit.lean`. + +inductive MetaCTerm where + /-- A reference to a Lean declaration — the closed leaf shape. -/ + | ident : Lean.Name → MetaCTerm + /-- A symbolic name — open leaf (string-named local variable or + dim-binder). Distinct from `ident` so the round-trip through + `CTerm.var` preserves the original string. -/ + | sym : String → MetaCTerm + /-- Application — the universal combinator. `papp`, `fst`, `snd`, + `pair`, schema ctors, and eliminators all encode as `.ident`- + headed `.app` chains. -/ + | app : MetaCTerm → MetaCTerm → MetaCTerm + /-- Term-level lambda — binds `x` in the body. -/ + | lam : String → MetaCTerm → MetaCTerm + /-- Path-level lambda — binds a dim-name `i`. Distinct from `lam` + because dim-binders inhabit a different kind of universe; the + structural distinction is preserved here for downstream + analyses that care. -/ + | plam : String → MetaCTerm → MetaCTerm + /-- Five-field composition — mirrors `compⁱ A φ u t`. The dim- + binder is stored as a string (the `DimVar.name`); the body and + the witness are `MetaCTerm`s; the face is a `MetaClassifier`. -/ + | comp : String → MetaCTerm → MetaClassifier + → MetaCTerm → MetaCTerm → MetaCTerm + /-- Four-field transport — mirrors `transpⁱ A φ t`. -/ + | transp : String → MetaCTerm → MetaClassifier + → MetaCTerm → MetaCTerm + /-- The empty meta-term — placeholder for deletion or missing + content. Distinct from `MetaArtifact.empty` (which is at the + artifact level). -/ + | empty : MetaCTerm + deriving Repr + +instance : Inhabited MetaCTerm := ⟨MetaCTerm.empty⟩ + -- ── MetaArtifact — the meta-mirror of `CTerm` ─────────────────────────────── -- The "content" half of restructure. An artifact is what gets put in -- the source: a chunk of raw text, a parsed syntax tree, a reference @@ -201,6 +260,13 @@ inductive MetaArtifact where | source : String → MetaArtifact /-- A parsed Lean syntax tree. -/ | declAt : Lean.Syntax → MetaArtifact + /-- A structural meta-term — the AST-level representation of a + cubical-flavoured artifact. Preserves the cubical shape so + downstream tooling can decompose / reflect it without parsing. + The structural mirror is a real coreflection: every cubical + `CTerm` embeds losslessly via `CTerm.toMetaCTerm` (in the + cubical bridge) and reflects back via `MetaCTerm.toCTerm?`. -/ + | cterm : MetaCTerm → MetaArtifact /-- A reference to an existing declaration by name; resolved at apply time. -/ | refTo : Lean.Name → MetaArtifact @@ -213,6 +279,7 @@ inductive MetaArtifact where def MetaArtifact.toString : MetaArtifact → String | .source s => s!"source({s})" | .declAt _ => "declAt()" + | .cterm t => s!"cterm({repr t})" | .refTo n => s!"refTo({n})" | .empty => "empty" @@ -224,7 +291,14 @@ instance : ToString MetaArtifact := ⟨MetaArtifact.toString⟩ /-- The position of an artifact within a Lean source file or project. Used as the `MetaPosition` argument of `restructure`, - analogous to the dim-binder `i` of `comp`. -/ + analogous to the dim-binder `i` of `comp`. + + The `binder` field carries the dim-binder identity when the + position represents a comp-style operation; `none` for + non-cubical positions. This is the meta-mirror of the dim- + binder slot in `comp i A φ u t` — kept as a position-level + field rather than folded into the classifier so the binder + role is preserved structurally. -/ structure MetaPosition where /-- The fully qualified declaration name (or namespace) the position lives under. `Name.anonymous` for file-level. -/ @@ -234,9 +308,13 @@ structure MetaPosition where /-- Optional byte offset / range info; `none` if positional via declName alone is sufficient. -/ range : Option (Nat × Nat) + /-- Dim-binder identity for cubical-shaped positions. `none` for + non-cubical or unbound positions. Preserves the comp-style + binder slot structurally. -/ + binder : Option Lean.Name := none deriving Inhabited instance : Repr MetaPosition where - reprPrec p _ := s!"MetaPosition(declName={p.declName}, filePath={p.filePath}, range={repr p.range})" + reprPrec p _ := s!"MetaPosition(declName={p.declName}, filePath={p.filePath}, range={repr p.range}, binder={repr p.binder})" end Infoductor diff --git a/Infoductor/Foundation/Restructure.lean b/Infoductor/Foundation/Restructure.lean index c498421..e7995ec 100644 --- a/Infoductor/Foundation/Restructure.lean +++ b/Infoductor/Foundation/Restructure.lean @@ -133,6 +133,9 @@ def EditOp.apply (op : EditOp) (buf : SourceBuffer) : IO SourceBuffer := do | .declAt _ => IO.eprintln s!"[restructure] {path}: emit syntax (LSP-bound; headless skipped)" return buf + | .cterm t => + IO.eprintln s!"[restructure] writing {path} (decl {op.position.declName}) — meta-term" + return buf.insert path (toString (repr t)) /-- Run an `Edit` headless: apply every emitted op in order to an initial source buffer. Returns the final buffer plus the diff --git a/Infoductor/Test.lean b/Infoductor/Test.lean new file mode 100644 index 0000000..6f8a6cf --- /dev/null +++ b/Infoductor/Test.lean @@ -0,0 +1,154 @@ +/- + 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 + +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 + +-- ── 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