From ae675a1eede7f4d90085d734a50a23388541612e Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 12:05:43 -0600 Subject: [PATCH] Add MetaCTerm/MetaClassifier/MetaArtifact source renderer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Each meta-mirror value renders to a Lean expression that, when elaborated, reconstructs the same value. The bridge's loop now closes at the source level: an Edit's .cterm content can be written to a .lean file and parsed back via Lean's own parser/elaborator — no custom parser required. · nameToLeanSource — Lean.Name → constructor-call source. · MetaClassifier.toLeanSource — lattice → Infoductor.MetaClassifier.* calls. · MetaCTerm.toLeanSource — full structural mirror → constructor source. · MetaArtifact.toLeanSource — artifact layer wrapping the above. Foundation.Restructure's EditOp.apply for .cterm now uses MetaCTerm.toLeanSource instead of toString (repr t). The headless interpreter writes valid Lean source. The recursive helper for Lean.Name lives at Infoductor.nameToLeanSource rather than Lean.Name.toLeanSource — defining a Lean.Name.* function inside `namespace Infoductor` would otherwise create an Infoductor.Lean namespace and shadow the global Lean library. Co-Authored-By: Claude Opus 4.7 (1M context) --- Infoductor/Foundation/Meta.lean | 84 ++++++++++++++++++++++++++ Infoductor/Foundation/Restructure.lean | 6 +- Infoductor/Test.lean | 33 ++++++++++ 3 files changed, 122 insertions(+), 1 deletion(-) diff --git a/Infoductor/Foundation/Meta.lean b/Infoductor/Foundation/Meta.lean index 770071f..2bf3cd5 100644 --- a/Infoductor/Foundation/Meta.lean +++ b/Infoductor/Foundation/Meta.lean @@ -285,6 +285,90 @@ def MetaArtifact.toString : MetaArtifact → String instance : ToString MetaArtifact := ⟨MetaArtifact.toString⟩ +-- ── Source rendering — meta-mirrors → valid Lean source ───────────────────── +-- The poetic move: each meta-mirror value renders to a Lean +-- expression that, when elaborated, reconstructs the *same* value. +-- This closes the bridge's loop at the source level: an `Edit`'s +-- `.cterm` content can be written to a `.lean` file and parsed +-- back via Lean's own parser/elaborator without us having to +-- write a parser. The renderer is fully recursive over the +-- meta-mirror's structure, faithful on every constructor. + +/-- Render a `Lean.Name` as Lean source that reconstructs it via + the `Lean.Name` constructors. Faithful on `.anonymous`, + `.str`, and `.num` arms — the `.str` arm uses `repr` for + proper string-literal escaping. + + Local helper inside `namespace Infoductor` (full name + `Infoductor.nameToLeanSource`) to avoid shadowing the global + `Lean` library by a `def Lean.Name.…` here. -/ +def nameToLeanSource : Lean.Name → String + | .anonymous => "Lean.Name.anonymous" + | .str p s => + s!"(Lean.Name.str ({nameToLeanSource p}) {repr s})" + | .num p n => + s!"(Lean.Name.num ({nameToLeanSource p}) {n})" + +/-- Render a `MetaClassifier` as Lean source. Each lattice arm + becomes a constructor call in the `Infoductor.MetaClassifier` + namespace; recursive arms (`meet`, `join`) render their + children parenthesised. -/ +def MetaClassifier.toLeanSource : MetaClassifier → String + | .always => "Infoductor.MetaClassifier.always" + | .never => "Infoductor.MetaClassifier.never" + | .atDecl n => + s!"(Infoductor.MetaClassifier.atDecl {nameToLeanSource n})" + | .inFile s => + s!"(Infoductor.MetaClassifier.inFile {repr s})" + | .underAttribute n => + s!"(Infoductor.MetaClassifier.underAttribute {nameToLeanSource n})" + | .dependencyOf n => + s!"(Infoductor.MetaClassifier.dependencyOf {nameToLeanSource n})" + | .inNamespace n => + s!"(Infoductor.MetaClassifier.inNamespace {nameToLeanSource n})" + | .meet a b => + s!"(Infoductor.MetaClassifier.meet {toLeanSource a} {toLeanSource b})" + | .join a b => + s!"(Infoductor.MetaClassifier.join {toLeanSource a} {toLeanSource b})" + +/-- Render a `MetaCTerm` as Lean source that reconstructs it via + the `Infoductor.MetaCTerm` constructors. Every arm renders + to a parenthesised constructor call; sub-`MetaCTerm`s recurse, + sub-`MetaClassifier`s use `MetaClassifier.toLeanSource`, + sub-`Lean.Name`s use `nameToLeanSource`. -/ +def MetaCTerm.toLeanSource : MetaCTerm → String + | .ident n => + s!"(Infoductor.MetaCTerm.ident {nameToLeanSource n})" + | .sym s => + s!"(Infoductor.MetaCTerm.sym {repr s})" + | .app f a => + s!"(Infoductor.MetaCTerm.app {toLeanSource f} {toLeanSource a})" + | .lam x t => + s!"(Infoductor.MetaCTerm.lam {repr x} {toLeanSource t})" + | .plam i t => + s!"(Infoductor.MetaCTerm.plam {repr i} {toLeanSource t})" + | .comp s A φ u t => + s!"(Infoductor.MetaCTerm.comp {repr s} {toLeanSource A} \ + {MetaClassifier.toLeanSource φ} {toLeanSource u} {toLeanSource t})" + | .transp s A φ t => + s!"(Infoductor.MetaCTerm.transp {repr s} {toLeanSource A} \ + {MetaClassifier.toLeanSource φ} {toLeanSource t})" + | .empty => "Infoductor.MetaCTerm.empty" + +/-- Render a `MetaArtifact` as Lean source. The structural arm + (`cterm`) recurses through `MetaCTerm.toLeanSource`; `source` + arms wrap the raw string in a `.source` constructor; `declAt` + cannot be source-rendered (parsed Syntax is opaque) and + yields a placeholder. -/ +def MetaArtifact.toLeanSource : MetaArtifact → String + | .source s => s!"(Infoductor.MetaArtifact.source {repr s})" + | .declAt _ => "/- declAt with opaque Syntax — not source-renderable -/" + | .cterm m => + s!"(Infoductor.MetaArtifact.cterm {MetaCTerm.toLeanSource m})" + | .refTo n => + s!"(Infoductor.MetaArtifact.refTo {nameToLeanSource n})" + | .empty => "Infoductor.MetaArtifact.empty" + -- ── MetaPosition — where an artifact lives in source ─────────────────────── -- The first field of `restructure i (Context = MetaCType) φ witness fallback` -- — analogue of the dim-binder `i` in `comp i A φ u t`. diff --git a/Infoductor/Foundation/Restructure.lean b/Infoductor/Foundation/Restructure.lean index e7995ec..89ecde1 100644 --- a/Infoductor/Foundation/Restructure.lean +++ b/Infoductor/Foundation/Restructure.lean @@ -135,7 +135,11 @@ def EditOp.apply (op : EditOp) (buf : SourceBuffer) : IO SourceBuffer := do return buf | .cterm t => IO.eprintln s!"[restructure] writing {path} (decl {op.position.declName}) — meta-term" - return buf.insert path (toString (repr t)) + -- Render the structural meta-term as Lean source that, when + -- elaborated, reconstructs the same `MetaCTerm`. Lean's own + -- parser/elaborator is the round-trip mechanism; no custom + -- parser required. + return buf.insert path (MetaCTerm.toLeanSource 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 index 6f8a6cf..a7e8bbf 100644 --- a/Infoductor/Test.lean +++ b/Infoductor/Test.lean @@ -138,6 +138,39 @@ 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)) + -- ── Compile-time registry diagnostics ─────────────────────────────────────── /-- A diagnostic action that prints registry sizes. Run via `#eval`