max/infoductor
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
12 commits 1 branch 0 tags 218 KiB
Commit graph

2 commits

Author SHA1 Message Date
Maximus Gorog
92fc4f9682 Add String → MetaCTerm parser; round-trip via native_decide 
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>
 2026-05-01 12:20:03 -06:00
Maximus Gorog
ba0a49823b Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries 
Initial commit.  Six modules extracted from
cubical-transport-hott-lean4/CubicalTransport/Algebra/ and
re-namespaced as `Infoductor`:

- Foundation/Meta.lean         — MetaCType, MetaClassifier,
                                 MetaArtifact, MetaPosition
                                 (with manual mutual decEq for
                                 MetaClassifier's recursive
                                 lattice arms)
- Foundation/Edit.lean         — Edit monad + Context comonad +
                                 distributive law +
                                 MetaClassifier.atPosition
                                 with lattice laws as theorems
- Foundation/Restructure.lean  — universal `restructure` (5-field
                                 comp-shaped operation), 6 frozen
                                 aliases, headless apply +
                                 brokenRefs / selfConsistent /
                                 Edit.guarded
- Foundation/MacroAlias.lean   — @[macroAlias] attribute +
                                 EnvExtension registry
- Foundation/MetaPath.lean     — @[metaPath src target]
                                 attribute + registry +
                                 findPathsFromSource/ToTarget
- Foundation/Methodology.lean  — @[methodology classifier]
                                 attribute + registry +
                                 deriveByTransport (walks
                                 metaPath registry) +
                                 tryEntryAsClosed primitive +
                                 cubical_search reference
                                 demonstrator

Builds clean on lean4 v4.30.0-rc2, ten oleans.  No deps beyond
Lean stdlib.  Sub-libs Tactics / Pantograph / Runner are planned
under the same lakefile.toml but not yet implemented.

Pairs with Pantograph as the conductor sits atop the pantograph
on an electric train.  "Info-ductor" — conducts information
(structure / classifications / methodology) through a Lean
codebase.

Forgejo: http://maxgit.wg:3000/max/infoductor

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
 2026-05-01 07:20:36 -06:00