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>
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) <noreply@anthropic.com>
Foundation.Meta gains an 8-constructor MetaCTerm inductive that mirrors
the cubical CTerm's generic shape (ident/sym/app/lam/plam plus dedicated
comp/transp arms; cubical-specific operators encode via .ident-headed
.app chains). MetaArtifact picks up a .cterm arm for structure-preserving
artifact content. MetaPosition gets an Option Lean.Name binder field so
the dim-binder of a comp/transp can be threaded structurally instead of
folded into the classifier.
These additions back the cubical-bridge's Embed.lean overhaul: a real
coreflection between the cubical universe (CType/CTerm/FaceFormula/
DimExpr) and the meta-mirror, with partial inverses and per-constructor
round-trip theorems.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
