Extract Algebra/ foundation to Infoductor; require it from forgejo
Some checks are pending
Lean Action CI / build (push) Waiting to run
Some checks are pending
Lean Action CI / build (push) Waiting to run
The six generic methodology / repo-organization modules (Meta / Edit / Restructure / MacroAlias / MetaPath / Methodology) move out of CubicalTransport/Algebra/ into the new Infoductor repo at http://maxgit.wg:3000/max/infoductor. cubical-transport-hott-lean4 now `require`s `infoductor` from that forgejo URL. Imports updated: - import CubicalTransport.Algebra.X → import Infoductor.Foundation.X - open CubicalTransport.Algebra → open Infoductor Files that stay (cubical-domain-specific): - CubicalTransport/Algebra/EngineMethodologies.lean (cubical closing-form @[methodology] tags) - CubicalTransport/Algebra/Test.lean (integration tests) Files deleted (moved to Infoductor.Foundation): - CubicalTransport/Algebra/Meta.lean - CubicalTransport/Algebra/Edit.lean - CubicalTransport/Algebra/Restructure.lean - CubicalTransport/Algebra/MacroAlias.lean - CubicalTransport/Algebra/MetaPath.lean - CubicalTransport/Algebra/Methodology.lean Architecture rationale (per memory: "Infoductor — generic methodology / repo-organization project"): - Foundation primitives are domain-agnostic; anyone can register their own methodology atop them, regardless of cubical interest. - Cubical-transport keeps the question-form (CompQ etc.) and cubical-specific @[methodology] / @[metaPath] decls. - topolei (next, separate work) will consume both Infoductor.Foundation and cubical-transport, picking cubical as its methodology. - "Info-ductor" — conducts information through a codebase; pairs with Pantograph (the conductor sits atop the pantograph hardware on an electric train). 93/93 tests pass (47 smoke + 46 property). 53 build jobs total (43 cubical + 10 Infoductor.Foundation + linker stages). No new axioms, no behavioural change — pure code-organization refactor. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog
parent
de56626059
commit
e26ada2fbc
12 changed files with 32 additions and 1129 deletions
|
|
@ -23,12 +23,12 @@ import CubicalTransport.Soundness
|
|||
import CubicalTransport.Inductive
|
||||
import CubicalTransport.Bridge
|
||||
import CubicalTransport.Question
|
||||
import CubicalTransport.Algebra.Meta
|
||||
import CubicalTransport.Algebra.Edit
|
||||
import CubicalTransport.Algebra.Restructure
|
||||
import CubicalTransport.Algebra.MacroAlias
|
||||
import CubicalTransport.Algebra.MetaPath
|
||||
import CubicalTransport.Algebra.Methodology
|
||||
import Infoductor.Foundation.Meta
|
||||
import Infoductor.Foundation.Edit
|
||||
import Infoductor.Foundation.Restructure
|
||||
import Infoductor.Foundation.MacroAlias
|
||||
import Infoductor.Foundation.MetaPath
|
||||
import Infoductor.Foundation.Methodology
|
||||
import CubicalTransport.Algebra.EngineMethodologies
|
||||
import CubicalTransport.Algebra.Test
|
||||
import CubicalTransport.PropertyTest
|
||||
|
|
|
|||
|
|
@ -1,179 +0,0 @@
|
|||
/-
|
||||
CubicalTransport.Algebra.Edit — Edit monad + Context comonad
|
||||
============================================================
|
||||
Phase B of `docs/ALGEBRA_PLAN.md`. Defines the abstract `Edit`
|
||||
monad (a thread of source mutations) and the abstract `Context`
|
||||
comonad (ambient information at a code position), plus the
|
||||
distributive law that lets `Context`-aware functions produce
|
||||
`Edit`-valued results.
|
||||
|
||||
This module is *pure data*: it does not depend on the Lean LSP,
|
||||
Lean.Elab APIs, or any I/O backend. LSP-specific bindings
|
||||
(a real `MakeEditLinkProps.ofReplaceRange` integration; a Code
|
||||
Action provider; a `Lean.Server.CodeActionContext` consumer) live
|
||||
in a separate `Algebra/EditLSP.lean` module and import this one.
|
||||
|
||||
The headless interpreter `runHeadless` applies an `Edit` to an
|
||||
in-memory source buffer and emits the post-edit text. This is
|
||||
what `lake exe algebra-restructure` uses (per ALGEBRA_PLAN §5.3
|
||||
No-LSP fallback).
|
||||
-/
|
||||
|
||||
import CubicalTransport.Algebra.Meta
|
||||
|
||||
namespace CubicalTransport.Algebra
|
||||
|
||||
-- ── EditOp — the leaf of every edit ──────────────────────────────────────────
|
||||
|
||||
/-- A single source-mutation request. The `position` field names the
|
||||
spot in source; `newContent` is what to write there; `oldContent`
|
||||
(if known) is recorded for audit / undo.
|
||||
|
||||
`EditOp` is the meta-CTerm leaf — emitted by `restructure` as part
|
||||
of an `Edit α` computation. -/
|
||||
structure EditOp where
|
||||
position : MetaPosition
|
||||
newContent : MetaArtifact
|
||||
oldContent : Option MetaArtifact := none
|
||||
description : String := ""
|
||||
deriving Inhabited
|
||||
|
||||
instance : Repr EditOp where
|
||||
reprPrec e _ := s!"EditOp(at={repr e.position}, new={e.newContent.toString}, desc={e.description})"
|
||||
|
||||
-- ── The Edit monad ──────────────────────────────────────────────────────────
|
||||
-- A computation that may emit zero or more `EditOp`s. Pure value α
|
||||
-- is the result of the computation; the list is the side-effect.
|
||||
|
||||
/-- The Edit monad: a value-and-edit-list pair. Composition appends
|
||||
edit lists; `pure` emits nothing.
|
||||
|
||||
Implementation note: we use the bare-bones `α × List EditOp`
|
||||
representation rather than the IO-threaded `run :
|
||||
CodeActionContext → IO (...)` form proposed in ALGEBRA_PLAN §3.1.
|
||||
The IO and LSP threading are *implementation choices* that don't
|
||||
affect the algebraic structure; lifting from this pure form into
|
||||
the LSP form is a `MonadLift Edit (ReaderT … IO)` instance in
|
||||
`EditLSP.lean`.
|
||||
|
||||
See `docs/ALGEBRA_PLAN.md` §3.1 for the design discussion. -/
|
||||
structure Edit (α : Type) where
|
||||
result : α
|
||||
ops : List EditOp
|
||||
deriving Inhabited
|
||||
|
||||
namespace Edit
|
||||
|
||||
/-- Lift a value into the trivial edit (zero ops). -/
|
||||
def pure {α : Type} (a : α) : Edit α := { result := a, ops := [] }
|
||||
|
||||
/-- Sequence: concatenate edit lists. -/
|
||||
def bind {α β : Type} (m : Edit α) (f : α → Edit β) : Edit β :=
|
||||
let n := f m.result
|
||||
{ result := n.result, ops := m.ops ++ n.ops }
|
||||
|
||||
/-- Emit a single edit op with no result. -/
|
||||
def emit (op : EditOp) : Edit Unit := { result := (), ops := [op] }
|
||||
|
||||
/-- Emit several edit ops. -/
|
||||
def emitMany (ops : List EditOp) : Edit Unit := { result := (), ops := ops }
|
||||
|
||||
instance : Monad Edit where
|
||||
pure := Edit.pure
|
||||
bind := Edit.bind
|
||||
|
||||
/-- Functor instance. Maps the result; leaves ops untouched. -/
|
||||
instance : Functor Edit where
|
||||
map f m := { result := f m.result, ops := m.ops }
|
||||
|
||||
end Edit
|
||||
|
||||
-- ── The Context comonad ─────────────────────────────────────────────────────
|
||||
-- "What's around here?" At each meta-position, expose ambient info:
|
||||
-- the current artifact, the position, the namespace, and whatever
|
||||
-- additional metadata the elaborator pass populates.
|
||||
|
||||
/-- Ambient information at a meta-position.
|
||||
|
||||
`here` is the focal artifact; `pos` is its location; `siblings`
|
||||
is a list of nearby artifacts that the restructuring might wish
|
||||
to consult (e.g., to rename a definition consistently with its
|
||||
consumers).
|
||||
|
||||
Per ALGEBRA_PLAN §3.1 the full Context carries `Lean.Environment`
|
||||
and `QuestionGraph` fields too; those are populated only when
|
||||
running inside the elaborator (post-import). The pure-data form
|
||||
here works headless. -/
|
||||
structure Context (α : Type) where
|
||||
here : α
|
||||
pos : MetaPosition
|
||||
siblings : List MetaArtifact := []
|
||||
deriving Inhabited
|
||||
|
||||
namespace Context
|
||||
|
||||
/-- Comonad `extract`: the focal artifact at the current position. -/
|
||||
def extract {α : Type} (c : Context α) : α := c.here
|
||||
|
||||
/-- Comonad `extend`: relocate an `α` value to a context-dependent
|
||||
`β` value, i.e. apply a context-aware function pointwise. -/
|
||||
def extend {α β : Type} (f : Context α → β) (c : Context α) : Context β :=
|
||||
{ here := f c, pos := c.pos, siblings := c.siblings }
|
||||
|
||||
instance : Functor Context where
|
||||
map f c := { here := f c.here, pos := c.pos, siblings := c.siblings }
|
||||
|
||||
end Context
|
||||
|
||||
-- ── The distributive law: Context → Edit ────────────────────────────────────
|
||||
-- The standard "comonad-to-monad" distributive setup. A context-
|
||||
-- aware decision produces an edit; lifting it into a Context-keyed
|
||||
-- Edit yields the contextualized edit.
|
||||
|
||||
/-- Lift a context-aware decision into an `Edit`. Per ALGEBRA_PLAN
|
||||
§3.2 this is the *distributive law* between the Context comonad
|
||||
and the Edit monad. -/
|
||||
def Context.contextualEdit {α β : Type}
|
||||
(decide : Context α → Edit β) (c : Context α) : Edit β :=
|
||||
decide c
|
||||
|
||||
-- ── Classifier-at-position evaluation ───────────────────────────────────────
|
||||
-- Decide whether a `MetaClassifier` matches a `MetaPosition`. Used
|
||||
-- by `restructure` to pick `witness` vs `fallback`.
|
||||
|
||||
/-- Decide whether `φ` matches `pos`, syntactically. For
|
||||
`.underAttribute` and `.dependencyOf` we conservatively answer
|
||||
`false` here — those require Lean.Environment and live in the
|
||||
LSP integration module.
|
||||
|
||||
The lattice operations `.meet` and `.join` are the obvious
|
||||
Boolean combinations; `.always` is `true`, `.never` is `false`. -/
|
||||
def MetaClassifier.atPosition : MetaClassifier → MetaPosition → Bool
|
||||
| .always, _ => true
|
||||
| .never, _ => false
|
||||
| .atDecl n, p => decide (n = p.declName)
|
||||
| .inFile s, p => decide (s = p.filePath)
|
||||
| .underAttribute _, _ => false -- needs environment; resolved in LSP module
|
||||
| .dependencyOf _, _ => false -- needs dep graph; resolved in LSP module
|
||||
| .inNamespace n, p =>
|
||||
-- syntactic prefix check: is `p.declName` lexically under `n`?
|
||||
n.isPrefixOf p.declName
|
||||
| .meet a b, p => a.atPosition p && b.atPosition p
|
||||
| .join a b, p => a.atPosition p || b.atPosition p
|
||||
|
||||
/-- Lattice laws on `atPosition` — the meta-mirror of the cubical
|
||||
face-formula laws (`FaceFormula.eval`). `meet` is conjunction,
|
||||
`join` is disjunction, `always`/`never` are top/bottom. -/
|
||||
theorem MetaClassifier.atPosition_always (p : MetaPosition) :
|
||||
MetaClassifier.always.atPosition p = true := rfl
|
||||
|
||||
theorem MetaClassifier.atPosition_never (p : MetaPosition) :
|
||||
MetaClassifier.never.atPosition p = false := rfl
|
||||
|
||||
theorem MetaClassifier.atPosition_meet (a b : MetaClassifier) (p : MetaPosition) :
|
||||
(a.meet b).atPosition p = (a.atPosition p && b.atPosition p) := rfl
|
||||
|
||||
theorem MetaClassifier.atPosition_join (a b : MetaClassifier) (p : MetaPosition) :
|
||||
(a.join b).atPosition p = (a.atPosition p || b.atPosition p) := rfl
|
||||
|
||||
end CubicalTransport.Algebra
|
||||
|
|
@ -30,12 +30,12 @@
|
|||
their own concrete closers; they land in a follow-up.
|
||||
-/
|
||||
|
||||
import CubicalTransport.Algebra.Methodology
|
||||
import Infoductor.Foundation.Methodology
|
||||
import CubicalTransport.Question
|
||||
|
||||
namespace CubicalTransport.Algebra.EngineMethodologies
|
||||
|
||||
open CubicalTransport.Algebra
|
||||
open Infoductor
|
||||
open Question
|
||||
|
||||
-- ── CompQ closers ───────────────────────────────────────────────────────────
|
||||
|
|
|
|||
|
|
@ -1,97 +0,0 @@
|
|||
/-
|
||||
CubicalTransport.Algebra.MacroAlias — `@[macroAlias]` attribute
|
||||
===============================================================
|
||||
Phase C of `docs/ALGEBRA_PLAN.md`. Provides the user-extensible
|
||||
registry of frozen `restructure` invocations.
|
||||
|
||||
When a developer notices that a `restructure` invocation pattern
|
||||
recurs ("oh, this is just a relocate-with-namespace-fixup"), they
|
||||
attach `@[macroAlias]` to a `def` that wraps the pattern. The
|
||||
attribute records the alias in a global registry (`AliasRegistry`)
|
||||
keyed by name. The widget can then suggest "name this pattern as
|
||||
X" when an instantiation matches an existing alias's signature.
|
||||
|
||||
Per ALGEBRA_PLAN §2.3:
|
||||
> The codebase ships with `restructure` itself (~150 lines). Each
|
||||
> `@[macroAlias] def …` is a 1–3-line shorthand.
|
||||
|
||||
This module provides the attribute and the registry; concrete
|
||||
alias declarations (`transport_artifact`, `relocate_invariant`,
|
||||
…) live in `Algebra/Restructure.lean`.
|
||||
-/
|
||||
|
||||
import Lean
|
||||
import CubicalTransport.Algebra.Restructure
|
||||
|
||||
namespace CubicalTransport.Algebra
|
||||
|
||||
open Lean
|
||||
|
||||
-- ── The alias registry ──────────────────────────────────────────────────────
|
||||
|
||||
/-- An entry in the alias registry: a `Name` paired with its
|
||||
documentary description (extracted from the `def`'s docstring
|
||||
if present). -/
|
||||
structure AliasEntry where
|
||||
name : Name
|
||||
description : String := ""
|
||||
deriving Repr, Inhabited
|
||||
|
||||
/-- Global registry of `@[macroAlias]`-tagged declarations, indexed
|
||||
by name. Implemented as a Lean `EnvExtension` so that adds in
|
||||
one module are visible from any importing module.
|
||||
|
||||
Per ALGEBRA_PLAN §10 OQ #2 the registry is on-the-fly; persistence
|
||||
via `lake exe algebra-cache` is deferred. -/
|
||||
initialize aliasRegistryExt :
|
||||
SimplePersistentEnvExtension AliasEntry (Array AliasEntry) ←
|
||||
registerSimplePersistentEnvExtension {
|
||||
name := `Algebra.aliasRegistry
|
||||
addEntryFn := fun arr e => arr.push e
|
||||
addImportedFn := fun arrs => arrs.foldl (init := #[]) Array.append
|
||||
asyncMode := .sync
|
||||
}
|
||||
|
||||
/-- Look up every registered alias. Order is unspecified (no
|
||||
guarantees beyond "all registered entries are in the array"). -/
|
||||
def getAliases : CoreM (Array AliasEntry) := do
|
||||
let env ← getEnv
|
||||
return aliasRegistryExt.getState env
|
||||
|
||||
/-- Register an alias entry. Inserts into the env extension. -/
|
||||
def registerAlias (entry : AliasEntry) : CoreM Unit := do
|
||||
modifyEnv (aliasRegistryExt.addEntry · entry)
|
||||
|
||||
-- ── The `@[macroAlias]` attribute ───────────────────────────────────────────
|
||||
|
||||
/-- Lean attribute syntax registered as `@[macroAlias]`. Attached to
|
||||
a `def` to register it as a frozen `restructure` invocation
|
||||
accessible via `Algebra.getAliases`. -/
|
||||
initialize macroAliasAttr : Unit ←
|
||||
registerBuiltinAttribute {
|
||||
name := `macroAlias
|
||||
descr := "Register this declaration as a `restructure` alias \
|
||||
(Phase C of ALGEBRA_PLAN.md). The decl's name and \
|
||||
docstring become an `AliasEntry` in the global \
|
||||
`aliasRegistryExt`."
|
||||
add := fun declName _stx _kind => do
|
||||
let env ← getEnv
|
||||
let docstring? := (← findDocString? env declName).getD ""
|
||||
registerAlias { name := declName, description := docstring? }
|
||||
}
|
||||
|
||||
-- ── Diagnostics ─────────────────────────────────────────────────────────────
|
||||
|
||||
/-- Print the current alias registry to `IO.println`. Used by
|
||||
`lake exe algebra-list-aliases` and the widget's "show registered
|
||||
aliases" button. -/
|
||||
def printAliases : CoreM Unit := do
|
||||
let aliases ← getAliases
|
||||
IO.println s!"── Algebra macro-alias registry ({aliases.size}) ──"
|
||||
for entry in aliases do
|
||||
if entry.description.isEmpty then
|
||||
IO.println s!" {entry.name}"
|
||||
else
|
||||
IO.println s!" {entry.name} — {entry.description}"
|
||||
|
||||
end CubicalTransport.Algebra
|
||||
|
|
@ -1,242 +0,0 @@
|
|||
/-
|
||||
CubicalTransport.Algebra.Meta — meta-mirror types
|
||||
=================================================
|
||||
Phase A of `docs/ALGEBRA_PLAN.md`. Defines the meta-level
|
||||
vocabulary on which the universal `restructure` macro is built —
|
||||
the meta-mirror of the cubical AST (`CType`, `FaceFormula`,
|
||||
`CTerm`).
|
||||
|
||||
These types are pure data; no semantic content is committed in
|
||||
this module. Their semantics — how `restructure` consumes them
|
||||
to emit `MakeEditLinkProps.ofReplaceRange` calls in the `Edit`
|
||||
monad — lives in `Algebra/Restructure.lean`.
|
||||
|
||||
| Cubical-AST type | Meta-mirror | Role |
|
||||
|------------------|-------------|--------------------------------|
|
||||
| `CType` | `MetaCType` | meta-types of source artifacts |
|
||||
| `FaceFormula` | `MetaClassifier` | "where in the codebase" |
|
||||
| `CTerm` | `MetaArtifact` | the new content / fallback |
|
||||
|
||||
The point: every restructuring operation has the *same five
|
||||
fields* as `comp i A φ u t`, with each field promoted from the
|
||||
cubical CTerm world to the meta-Lean-source world.
|
||||
|
||||
See `docs/ALGEBRA_PLAN.md` §2.2 for the formal table.
|
||||
-/
|
||||
|
||||
import Lean.Syntax
|
||||
import Lean.Data.Name
|
||||
|
||||
namespace CubicalTransport.Algebra
|
||||
|
||||
-- ── MetaCType — the meta-mirror of `CType` ──────────────────────────────────
|
||||
-- Every artifact in a Lean source has a meta-type that classifies its
|
||||
-- structural role. These are the "cubical-types" of the source-code
|
||||
-- universe: a theorem is an artifact whose meta-type is `theorem`,
|
||||
-- a `def` is an artifact whose meta-type is `definition`, etc.
|
||||
|
||||
/-- Meta-mirror of `CType`: classifies the structural role of an
|
||||
artifact in Lean source code.
|
||||
|
||||
Each constructor names a kind of declaration / structural unit
|
||||
that `restructure` can operate on. The list is closed: extending
|
||||
it requires updating the universal macro to handle the new
|
||||
artifact kind.
|
||||
|
||||
See `docs/ALGEBRA_PLAN.md` §2.2 for the design rationale. -/
|
||||
inductive MetaCType where
|
||||
/-- A `theorem` declaration: `theorem foo : T := proof`. -/
|
||||
| theorem_ : MetaCType
|
||||
/-- A `def` declaration: `def foo := body`. -/
|
||||
| definition : MetaCType
|
||||
/-- An `instance` declaration. -/
|
||||
| instance_ : MetaCType
|
||||
/-- A `structure` declaration. -/
|
||||
| structure_ : MetaCType
|
||||
/-- A Lean `inductive` declaration. -/
|
||||
| inductive_ : MetaCType
|
||||
/-- An entire file. -/
|
||||
| file : MetaCType
|
||||
/-- A `namespace` block. -/
|
||||
| namespace_ : MetaCType
|
||||
/-- A `class` declaration. -/
|
||||
| class_ : MetaCType
|
||||
/-- A logical "set of classifiers" — abstract collection used by
|
||||
methodology dispatch. -/
|
||||
| classifierSet : MetaCType
|
||||
/-- An edge in the dependency graph between declarations. Used
|
||||
by `transp`-along-MetaPath to identify what gets reorganised
|
||||
together. -/
|
||||
| dependencyEdge : MetaCType
|
||||
/-- A custom-attribute annotation site (e.g., the position of a
|
||||
`@[simp]` or `@[methodology]` annotation on a declaration). -/
|
||||
| attributeSite : MetaCType
|
||||
deriving Repr, Inhabited, DecidableEq
|
||||
|
||||
-- ── MetaClassifier — the meta-mirror of `FaceFormula` ──────────────────────
|
||||
-- "Where in the codebase does this restructuring apply?" The face
|
||||
-- lattice on dimensions has its analogue at the meta level: face = a
|
||||
-- predicate over dimension-coordinates picking out a sub-cube; meta-
|
||||
-- classifier = a predicate over codebase-coordinates picking out a
|
||||
-- sub-region.
|
||||
|
||||
/-- Meta-mirror of `FaceFormula`: a predicate over codebase
|
||||
positions. Combined via `meet` and `join` to form composite
|
||||
"where in the codebase" predicates.
|
||||
|
||||
The lattice structure mirrors the cubical face lattice:
|
||||
`meet` is intersection, `join` is union; `always` is the top
|
||||
(`.top` analogue), `never` is the bottom (`.bot` analogue). -/
|
||||
inductive MetaClassifier where
|
||||
/-- "Everywhere" — the top of the meta-classifier lattice;
|
||||
analogue of `FaceFormula.top`. -/
|
||||
| always : MetaClassifier
|
||||
/-- "Nowhere" — the bottom; analogue of `FaceFormula.bot`. -/
|
||||
| never : MetaClassifier
|
||||
/-- "At this declaration"; analogue of `FaceFormula.eq0`/`eq1`
|
||||
on a specific dim coordinate. -/
|
||||
| atDecl : Lean.Name → MetaClassifier
|
||||
/-- "In this file." -/
|
||||
| inFile : String → MetaClassifier
|
||||
/-- "Under this attribute" — anywhere a particular attribute is
|
||||
attached. -/
|
||||
| underAttribute : Lean.Name → MetaClassifier
|
||||
/-- "In any declaration that depends on this one." -/
|
||||
| dependencyOf : Lean.Name → MetaClassifier
|
||||
/-- "In the same namespace as this name." -/
|
||||
| inNamespace : Lean.Name → MetaClassifier
|
||||
/-- Conjunction; analogue of `FaceFormula.meet`. -/
|
||||
| meet : MetaClassifier → MetaClassifier → MetaClassifier
|
||||
/-- Disjunction; analogue of `FaceFormula.join`. -/
|
||||
| join : MetaClassifier → MetaClassifier → MetaClassifier
|
||||
deriving Repr, Inhabited
|
||||
|
||||
-- DecidableEq for MetaClassifier — manual mutual decision because
|
||||
-- the type is recursive (meet/join arms) and mixes Lean.Name / String
|
||||
-- carriers.
|
||||
|
||||
def MetaClassifier.decEq : (a b : MetaClassifier) → Decidable (a = b)
|
||||
| .always, .always => isTrue rfl
|
||||
| .never, .never => isTrue rfl
|
||||
| .atDecl n, .atDecl m =>
|
||||
if h : n = m then isTrue (by rw [h])
|
||||
else isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .inFile s, .inFile t =>
|
||||
if h : s = t then isTrue (by rw [h])
|
||||
else isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .underAttribute n, .underAttribute m =>
|
||||
if h : n = m then isTrue (by rw [h])
|
||||
else isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .dependencyOf n, .dependencyOf m =>
|
||||
if h : n = m then isTrue (by rw [h])
|
||||
else isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .inNamespace n, .inNamespace m =>
|
||||
if h : n = m then isTrue (by rw [h])
|
||||
else isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .meet a₁ b₁, .meet a₂ b₂ =>
|
||||
match MetaClassifier.decEq a₁ a₂, MetaClassifier.decEq b₁ b₂ with
|
||||
| isTrue ha, isTrue hb => isTrue (by rw [ha, hb])
|
||||
| isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
|
||||
| _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .join a₁ b₁, .join a₂ b₂ =>
|
||||
match MetaClassifier.decEq a₁ a₂, MetaClassifier.decEq b₁ b₂ with
|
||||
| isTrue ha, isTrue hb => isTrue (by rw [ha, hb])
|
||||
| isFalse h, _ => isFalse (fun heq => h (by cases heq; rfl))
|
||||
| _, isFalse h => isFalse (fun heq => h (by cases heq; rfl))
|
||||
| .always, .never | .always, .atDecl _ | .always, .inFile _
|
||||
| .always, .underAttribute _ | .always, .dependencyOf _
|
||||
| .always, .inNamespace _ | .always, .meet _ _ | .always, .join _ _
|
||||
| .never, .always | .never, .atDecl _ | .never, .inFile _
|
||||
| .never, .underAttribute _ | .never, .dependencyOf _
|
||||
| .never, .inNamespace _ | .never, .meet _ _ | .never, .join _ _
|
||||
| .atDecl _, .always | .atDecl _, .never | .atDecl _, .inFile _
|
||||
| .atDecl _, .underAttribute _ | .atDecl _, .dependencyOf _
|
||||
| .atDecl _, .inNamespace _ | .atDecl _, .meet _ _ | .atDecl _, .join _ _
|
||||
| .inFile _, .always | .inFile _, .never | .inFile _, .atDecl _
|
||||
| .inFile _, .underAttribute _ | .inFile _, .dependencyOf _
|
||||
| .inFile _, .inNamespace _ | .inFile _, .meet _ _ | .inFile _, .join _ _
|
||||
| .underAttribute _, .always | .underAttribute _, .never
|
||||
| .underAttribute _, .atDecl _ | .underAttribute _, .inFile _
|
||||
| .underAttribute _, .dependencyOf _ | .underAttribute _, .inNamespace _
|
||||
| .underAttribute _, .meet _ _ | .underAttribute _, .join _ _
|
||||
| .dependencyOf _, .always | .dependencyOf _, .never
|
||||
| .dependencyOf _, .atDecl _ | .dependencyOf _, .inFile _
|
||||
| .dependencyOf _, .underAttribute _ | .dependencyOf _, .inNamespace _
|
||||
| .dependencyOf _, .meet _ _ | .dependencyOf _, .join _ _
|
||||
| .inNamespace _, .always | .inNamespace _, .never
|
||||
| .inNamespace _, .atDecl _ | .inNamespace _, .inFile _
|
||||
| .inNamespace _, .underAttribute _ | .inNamespace _, .dependencyOf _
|
||||
| .inNamespace _, .meet _ _ | .inNamespace _, .join _ _
|
||||
| .meet _ _, .always | .meet _ _, .never | .meet _ _, .atDecl _
|
||||
| .meet _ _, .inFile _ | .meet _ _, .underAttribute _
|
||||
| .meet _ _, .dependencyOf _ | .meet _ _, .inNamespace _
|
||||
| .meet _ _, .join _ _
|
||||
| .join _ _, .always | .join _ _, .never | .join _ _, .atDecl _
|
||||
| .join _ _, .inFile _ | .join _ _, .underAttribute _
|
||||
| .join _ _, .dependencyOf _ | .join _ _, .inNamespace _
|
||||
| .join _ _, .meet _ _ =>
|
||||
isFalse (fun heq => by cases heq)
|
||||
|
||||
instance : DecidableEq MetaClassifier := MetaClassifier.decEq
|
||||
|
||||
-- ── 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
|
||||
-- to another decl, or "remove this" (the empty artifact).
|
||||
|
||||
/-- Meta-mirror of `CTerm`: the content placed at a meta-position by a
|
||||
restructuring operation.
|
||||
|
||||
Four shapes: raw source text (string), parsed syntax (Lean.Syntax),
|
||||
a reference to an existing decl by `Name`, and the empty artifact
|
||||
(used for deletion).
|
||||
|
||||
`Lean.Syntax` is opaque-by-default in Lean 4 — its internal
|
||||
structure is large. We don't derive `DecidableEq` on `MetaArtifact`
|
||||
because comparing arbitrary Syntax trees structurally is heavy and
|
||||
not needed by `restructure`'s dispatch logic. Use `MetaArtifact.toString`
|
||||
for printable comparisons. -/
|
||||
inductive MetaArtifact where
|
||||
/-- Raw Lean source text (will be parsed at apply time). -/
|
||||
| source : String → MetaArtifact
|
||||
/-- A parsed Lean syntax tree. -/
|
||||
| declAt : Lean.Syntax → MetaArtifact
|
||||
/-- A reference to an existing declaration by name; resolved at
|
||||
apply time. -/
|
||||
| refTo : Lean.Name → MetaArtifact
|
||||
/-- The empty artifact — "remove this position." -/
|
||||
| empty : MetaArtifact
|
||||
deriving Inhabited
|
||||
|
||||
/-- A printable summary of an artifact, useful for diagnostics and
|
||||
widget rendering. -/
|
||||
def MetaArtifact.toString : MetaArtifact → String
|
||||
| .source s => s!"source({s})"
|
||||
| .declAt _ => "declAt(<syntax>)"
|
||||
| .refTo n => s!"refTo({n})"
|
||||
| .empty => "empty"
|
||||
|
||||
instance : ToString MetaArtifact := ⟨MetaArtifact.toString⟩
|
||||
|
||||
-- ── 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`.
|
||||
|
||||
/-- 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`. -/
|
||||
structure MetaPosition where
|
||||
/-- The fully qualified declaration name (or namespace) the
|
||||
position lives under. `Name.anonymous` for file-level. -/
|
||||
declName : Lean.Name
|
||||
/-- Path to the source file (or empty for in-memory). -/
|
||||
filePath : String
|
||||
/-- Optional byte offset / range info; `none` if positional via
|
||||
declName alone is sufficient. -/
|
||||
range : Option (Nat × Nat)
|
||||
deriving Inhabited
|
||||
|
||||
instance : Repr MetaPosition where
|
||||
reprPrec p _ := s!"MetaPosition(declName={p.declName}, filePath={p.filePath}, range={repr p.range})"
|
||||
|
||||
end CubicalTransport.Algebra
|
||||
|
|
@ -1,127 +0,0 @@
|
|||
/-
|
||||
CubicalTransport.Algebra.MetaPath — `@[metaPath]` attribute
|
||||
===========================================================
|
||||
Phase D'.5 of `docs/ALGEBRA_PLAN.md`. Provides the structural-Path
|
||||
declaration system that powers methodology-transport in
|
||||
`cubical_search`.
|
||||
|
||||
A `MetaPath` is the meta-level analogue of a cubical `Path`: a
|
||||
declared equivalence between two `MetaClassifier` shapes, witnessed
|
||||
by a Lean theorem that exhibits the equivalence.
|
||||
|
||||
Example use:
|
||||
|
||||
@[metaPath IsFullFace IsConstLine]
|
||||
theorem fullFace_implies_constLine_on_path (q : CompQ) :
|
||||
IsFullFace q → IsConstLine q := …
|
||||
|
||||
Once such a Path is registered, every methodology indexed against
|
||||
`IsFullFace` automatically becomes a candidate for `IsConstLine`
|
||||
via `transp` at the methodology level.
|
||||
|
||||
Per ALGEBRA_PLAN §10.1 OQ: the witness theorem is required (a
|
||||
declared MetaPath without a propositional witness would be
|
||||
unsound). In v0 we trust the `metaPath` annotation; future REL3+
|
||||
work can verify the witness type-checks against an expected shape.
|
||||
-/
|
||||
|
||||
import Lean
|
||||
import CubicalTransport.Algebra.Meta
|
||||
|
||||
namespace CubicalTransport.Algebra
|
||||
|
||||
open Lean
|
||||
|
||||
-- ── MetaPath entries ────────────────────────────────────────────────────────
|
||||
|
||||
/-- A registered structural Path between two classifiers.
|
||||
|
||||
`sourceClassifier` and `targetClassifier` are `Name`s pointing
|
||||
to classifier predicates (typically defined in `Question.lean` —
|
||||
`IsFullFace`, `IsConstLine`, `IsPathLine`, etc.).
|
||||
`witnessName` names a theorem exhibiting the equivalence /
|
||||
implication between them.
|
||||
|
||||
Direction matters: a Path `A ↦ B` means "every methodology for
|
||||
A produces a methodology for B" (via post-composition with the
|
||||
witness). The reverse direction needs a separate `metaPath B A`
|
||||
declaration. -/
|
||||
structure MetaPathEntry where
|
||||
sourceClassifier : Name
|
||||
targetClassifier : Name
|
||||
witnessName : Name
|
||||
description : String := ""
|
||||
deriving Repr, Inhabited
|
||||
|
||||
-- ── The MetaPath registry ───────────────────────────────────────────────────
|
||||
|
||||
initialize metaPathRegistryExt :
|
||||
SimplePersistentEnvExtension MetaPathEntry (Array MetaPathEntry) ←
|
||||
registerSimplePersistentEnvExtension {
|
||||
name := `Algebra.metaPathRegistry
|
||||
addEntryFn := fun arr e => arr.push e
|
||||
addImportedFn := fun arrs => arrs.foldl (init := #[]) Array.append
|
||||
asyncMode := .sync
|
||||
}
|
||||
|
||||
def getMetaPaths : CoreM (Array MetaPathEntry) := do
|
||||
let env ← getEnv
|
||||
return metaPathRegistryExt.getState env
|
||||
|
||||
def registerMetaPath (entry : MetaPathEntry) : CoreM Unit := do
|
||||
modifyEnv (metaPathRegistryExt.addEntry · entry)
|
||||
|
||||
/-- Find every Path whose source matches a given classifier name. -/
|
||||
def findPathsFromSource (source : Name) : CoreM (Array MetaPathEntry) := do
|
||||
let all ← getMetaPaths
|
||||
return all.filter (·.sourceClassifier == source)
|
||||
|
||||
/-- Find every Path whose target matches a given classifier name. -/
|
||||
def findPathsToTarget (target : Name) : CoreM (Array MetaPathEntry) := do
|
||||
let all ← getMetaPaths
|
||||
return all.filter (·.targetClassifier == target)
|
||||
|
||||
-- ── The `@[metaPath]` attribute ─────────────────────────────────────────────
|
||||
|
||||
/-- Parser-level data for the `@[metaPath]` attribute: takes the
|
||||
source classifier and the target classifier as identifiers.
|
||||
The witness is the tagged declaration itself. -/
|
||||
syntax (name := metaPath) "metaPath" ident ident : attr
|
||||
|
||||
/-- The `@[metaPath]` attribute itself. Records the tagged
|
||||
declaration as a structural Path between two classifiers. -/
|
||||
initialize metaPathAttr : Unit ←
|
||||
registerBuiltinAttribute {
|
||||
name := `metaPath
|
||||
descr := "Register this declaration as a structural Path \
|
||||
between two classifiers (Phase D'.5 of \
|
||||
ALGEBRA_PLAN.md). Usage: `@[metaPath SourceClassifier \
|
||||
TargetClassifier]`."
|
||||
add := fun declName stx _kind => do
|
||||
let parsed? : Option (Name × Name) :=
|
||||
match stx with
|
||||
| `(attr| metaPath $src:ident $tgt:ident) =>
|
||||
some (src.getId, tgt.getId)
|
||||
| _ => none
|
||||
let some (src, tgt) := parsed?
|
||||
| throwError "@[metaPath] requires source and target classifier names"
|
||||
let env ← getEnv
|
||||
let docstring? := (← findDocString? env declName).getD ""
|
||||
registerMetaPath
|
||||
{ sourceClassifier := src
|
||||
, targetClassifier := tgt
|
||||
, witnessName := declName
|
||||
, description := docstring? }
|
||||
}
|
||||
|
||||
-- ── Diagnostics ─────────────────────────────────────────────────────────────
|
||||
|
||||
def printMetaPaths : CoreM Unit := do
|
||||
let entries ← getMetaPaths
|
||||
IO.println s!"── MetaPath registry ({entries.size}) ──"
|
||||
for entry in entries do
|
||||
let d := if entry.description.isEmpty then "" else s!" — {entry.description}"
|
||||
IO.println
|
||||
s!" {entry.sourceClassifier} ↦ {entry.targetClassifier} via {entry.witnessName}{d}"
|
||||
|
||||
end CubicalTransport.Algebra
|
||||
|
|
@ -1,285 +0,0 @@
|
|||
/-
|
||||
CubicalTransport.Algebra.Methodology — `@[methodology]` + `cubical_search`
|
||||
==========================================================================
|
||||
Phase D' of `docs/ALGEBRA_PLAN.md`. Provides the autodiscovery
|
||||
layer that crowns the metacoding stack:
|
||||
|
||||
- `@[methodology]` attribute: registers a Lean theorem as a "proof
|
||||
fragment" indexed by a classifier shape. When `cubical_search`
|
||||
encounters a question matching that shape, it tries the
|
||||
registered theorem.
|
||||
|
||||
- `cubical_search` tactic: walks the methodology library by
|
||||
classifier dispatch and applies matches; on miss, attempts
|
||||
methodology-transport along declared structural Paths
|
||||
(`transp`-at-the-meta-level).
|
||||
|
||||
Per ALGEBRA_PLAN §4.3:
|
||||
> Once a small library of base methodologies exists, every new
|
||||
> structural Path declared in the codebase **automatically generates
|
||||
> new methodology candidates** by transporting existing methodologies
|
||||
> across the path.
|
||||
|
||||
This module ships the registry + the basic tactic; the
|
||||
methodology-transport clause is scaffolded as `deriveByTransport`
|
||||
(a stub returning `[]` until the structural-Path infrastructure
|
||||
arrives in REL2.6+).
|
||||
-/
|
||||
|
||||
import Lean
|
||||
import CubicalTransport.Algebra.MacroAlias
|
||||
import CubicalTransport.Algebra.MetaPath
|
||||
|
||||
namespace CubicalTransport.Algebra
|
||||
|
||||
open Lean Lean.Elab Lean.Elab.Tactic
|
||||
|
||||
-- ── Methodology entries ─────────────────────────────────────────────────────
|
||||
|
||||
/-- A registered methodology. Indexes a Lean theorem by the
|
||||
classifier shape it solves.
|
||||
|
||||
`classifierName` is a `Name` referring to a `MetaClassifier`-
|
||||
valued `def` (or one of the syntactic classifier predicates from
|
||||
`Question.lean`). `theoremName` is the `Name` of the theorem
|
||||
that `cubical_search` will try when the question matches.
|
||||
|
||||
Priority is used for ordering: higher priority methodologies are
|
||||
tried first. Default 100; specialised methodologies bump higher,
|
||||
catch-alls run lower. -/
|
||||
structure MethodologyEntry where
|
||||
classifierName : Name
|
||||
theoremName : Name
|
||||
priority : Nat := 100
|
||||
description : String := ""
|
||||
deriving Repr, Inhabited
|
||||
|
||||
-- ── The methodology registry ────────────────────────────────────────────────
|
||||
|
||||
/-- Global registry of methodologies, indexed by classifier name.
|
||||
Built up via `@[methodology]`-tagged declarations.
|
||||
|
||||
Implementation: `EnvExtension` so adds are visible across
|
||||
modules. Lookup is linear in the registry size (acceptable for
|
||||
REL2.5; a discrtree-indexed version is REL2.6 work per
|
||||
ALGEBRA_PLAN §10.4). -/
|
||||
initialize methodologyRegistryExt :
|
||||
SimplePersistentEnvExtension MethodologyEntry (Array MethodologyEntry) ←
|
||||
registerSimplePersistentEnvExtension {
|
||||
name := `Algebra.methodologyRegistry
|
||||
addEntryFn := fun arr e => arr.push e
|
||||
addImportedFn := fun arrs => arrs.foldl (init := #[]) Array.append
|
||||
asyncMode := .sync
|
||||
}
|
||||
|
||||
def getMethodologies : CoreM (Array MethodologyEntry) := do
|
||||
let env ← getEnv
|
||||
return methodologyRegistryExt.getState env
|
||||
|
||||
def registerMethodology (entry : MethodologyEntry) : CoreM Unit := do
|
||||
modifyEnv (methodologyRegistryExt.addEntry · entry)
|
||||
|
||||
/-- Find every methodology indexed against a given classifier name. -/
|
||||
def findMethodologies (classifier : Name) : CoreM (Array MethodologyEntry) := do
|
||||
let all ← getMethodologies
|
||||
return all.filter (·.classifierName == classifier)
|
||||
|
||||
-- ── The `@[methodology]` attribute ──────────────────────────────────────────
|
||||
-- Attached to a theorem. Attribute parser parses the classifier
|
||||
-- name and optional priority. Registration adds an entry to the
|
||||
-- methodology registry pointing back to the tagged theorem.
|
||||
|
||||
/-- Parser-level data for the `@[methodology]` attribute. We accept
|
||||
a plain identifier naming the classifier. Priority configuration
|
||||
via `priority := n` is Phase D'.1 work; the v0 attribute uses a
|
||||
fixed default of 100.
|
||||
|
||||
The syntax `name :=` matches the attribute name registered below;
|
||||
Lean's attribute system looks up attributes by syntax kind, not
|
||||
by leading keyword. -/
|
||||
syntax (name := methodology) "methodology" ident : attr
|
||||
|
||||
/-- The `@[methodology]` attribute itself. Records the tagged
|
||||
theorem under the named classifier (priority defaults to 100). -/
|
||||
initialize methodologyAttr : Unit ←
|
||||
registerBuiltinAttribute {
|
||||
name := `methodology
|
||||
descr := "Register this theorem as a proof methodology indexed \
|
||||
by a classifier (Phase D' of ALGEBRA_PLAN.md). Usage: \
|
||||
`@[methodology IsFullFace]`."
|
||||
add := fun declName stx _kind => do
|
||||
-- Parse classifier name from the attribute syntax.
|
||||
let classifierName? : Option Name :=
|
||||
match stx with
|
||||
| `(attr| methodology $cls:ident) => some cls.getId
|
||||
| _ => none
|
||||
let some classifierName := classifierName?
|
||||
| throwError "@[methodology] requires a classifier name"
|
||||
let env ← getEnv
|
||||
let docstring? := (← findDocString? env declName).getD ""
|
||||
registerMethodology
|
||||
{ classifierName := classifierName
|
||||
, theoremName := declName
|
||||
, priority := 100
|
||||
, description := docstring? }
|
||||
}
|
||||
|
||||
-- ── The methodology-transport clause (scaffold) ─────────────────────────────
|
||||
-- ALGEBRA_PLAN §4.3: when a structural Path connects classifierA to
|
||||
-- classifierB and the methodology library has an entry for
|
||||
-- classifierA, transport derives a candidate for classifierB.
|
||||
--
|
||||
-- Full implementation requires (a) declared structural Paths in the
|
||||
-- codebase, (b) reification of methodology bodies as CTerms, (c)
|
||||
-- application of `transp` at the methodology level. REL2.6+ work.
|
||||
--
|
||||
-- The scaffold below returns `[]` so the surrounding tactic remains
|
||||
-- well-typed; uses are guarded by feature flags.
|
||||
|
||||
/-- Derive new methodology candidates by transporting existing ones
|
||||
along declared structural Paths.
|
||||
|
||||
Per ALGEBRA_PLAN §4.3:
|
||||
> Twenty starting methodologies + a hundred declared paths →
|
||||
> potentially thousands of derived methodologies, each formally
|
||||
> certified-by-construction.
|
||||
|
||||
Implementation: for every methodology M registered against a
|
||||
classifier C₁, and every MetaPath C₁ ↦ C₂ in the registry,
|
||||
derive a candidate methodology against C₂ whose witness is M's
|
||||
body composed with the path witness.
|
||||
|
||||
For the v0 dispatch tactic, the "composed witness" is just M's
|
||||
theorem name — `cubical_search` will try both M and the path
|
||||
witness directly via apply/exact. A future Phase D'.6 will use
|
||||
actual Lean term composition to produce a single derived
|
||||
theorem. See `Algebra/MetaPath.lean` for the path attribute. -/
|
||||
def deriveByTransport (targetClassifier : Name) : CoreM (Array MethodologyEntry) := do
|
||||
let paths ← findPathsToTarget targetClassifier
|
||||
let mut out := #[]
|
||||
for path in paths do
|
||||
-- For every methodology M against the source classifier of this
|
||||
-- path, produce a derived candidate against the target classifier.
|
||||
let sourceMethodologies ← findMethodologies path.sourceClassifier
|
||||
for M in sourceMethodologies do
|
||||
out := out.push
|
||||
{ classifierName := targetClassifier
|
||||
, theoremName := M.theoremName -- v0: try the source method directly
|
||||
, priority := M.priority - 10 -- derived; lower priority
|
||||
, description := s!"derived via metaPath {path.sourceClassifier} ↦ {path.targetClassifier} from {M.theoremName}" }
|
||||
-- Also add the path witness itself as a candidate; cubical_search
|
||||
-- can apply it to convert the goal to the source classifier form.
|
||||
out := out.push
|
||||
{ classifierName := targetClassifier
|
||||
, theoremName := path.witnessName
|
||||
, priority := M.priority - 20
|
||||
, description := s!"path witness {path.witnessName} for transport" }
|
||||
return out
|
||||
|
||||
-- ── Tactic primitive: try one entry as a goal closer ───────────────────────
|
||||
-- Foundation primitive for any methodology-dispatching tactic.
|
||||
-- Anyone can build different orderings, retry strategies, or
|
||||
-- failure-reporting on top of this.
|
||||
|
||||
/-- Try to close the current goal by applying the registered
|
||||
methodology entry's theorem.
|
||||
|
||||
**Contract.** Attempts `exact entry.theoremName`, falling back
|
||||
to `apply entry.theoremName`. Returns `true` if the goal closes
|
||||
completely (no subgoals remaining); `false` otherwise.
|
||||
|
||||
Tactic state is restored on `false` — neither a partial-apply nor
|
||||
a thrown elaboration error leaks past the call. Never throws.
|
||||
Order of attempts (`exact` before `apply`) is fixed by this
|
||||
primitive; alternative orderings can be implemented by composing
|
||||
different primitives.
|
||||
|
||||
Use this as the building block for goal-closing dispatch loops;
|
||||
no opinion baked in beyond the fixed exact/apply order. -/
|
||||
def tryEntryAsClosed (entry : MethodologyEntry) : TacticM Bool := do
|
||||
let stx := mkIdent entry.theoremName
|
||||
let initialState ← saveState
|
||||
try
|
||||
evalTactic (← `(tactic| (first | exact $stx | apply $stx)))
|
||||
if (← getUnsolvedGoals).isEmpty then
|
||||
return true
|
||||
else
|
||||
restoreState initialState
|
||||
return false
|
||||
catch _ =>
|
||||
restoreState initialState
|
||||
return false
|
||||
|
||||
-- ── Reference dispatcher: `cubical_search` ─────────────────────────────────
|
||||
-- A reference composition of `findMethodologies` + `deriveByTransport`
|
||||
-- + `tryEntryAsClosed` in one obvious order. This is a *demonstrator*,
|
||||
-- not a normative tactic — anyone wanting different ordering, priority
|
||||
-- handling, or failure reporting writes their own using the
|
||||
-- primitives above.
|
||||
|
||||
/-- Reference-composition tactic: walk every registered methodology;
|
||||
on miss, walk the `@[metaPath]`-derived transport candidates;
|
||||
emit a structured failure report on full miss.
|
||||
|
||||
Stages (fixed in this demonstrator; anyone can write a different
|
||||
composition):
|
||||
1. Direct registry: `getMethodologies`, try each via
|
||||
`tryEntryAsClosed` in registry order.
|
||||
2. Transport: walk `getMetaPaths` and try each path's source
|
||||
methodologies and the path witness itself.
|
||||
3. Failure: structured report with per-candidate "didn't fire"
|
||||
reasons.
|
||||
|
||||
This is a tactic *demonstrator*, exposing the primitive composition
|
||||
pattern. Tag your goal-closing methodologies with `@[methodology
|
||||
Classifier]` and they enter this dispatcher's stage 1; declare
|
||||
`@[metaPath A B]` and stage 2 lifts methodologies from A to B
|
||||
automatically. No opinion about ordering, retry strategy, or
|
||||
priority interpretation beyond what's stated here. -/
|
||||
syntax (name := cubicalSearch) "cubical_search" : tactic
|
||||
|
||||
elab_rules : tactic
|
||||
| `(tactic| cubical_search) => do
|
||||
let goal ← getMainGoal
|
||||
let goalType ← goal.getType
|
||||
let methodologies ← getMethodologies
|
||||
let mut tried : Array Name := #[]
|
||||
-- Stage 1: direct methodology dispatch.
|
||||
for entry in methodologies do
|
||||
tried := tried.push entry.theoremName
|
||||
if (← tryEntryAsClosed entry) then return
|
||||
-- Stage 2: methodology-transport candidates from every
|
||||
-- declared `@[metaPath]`.
|
||||
let allPaths ← getMetaPaths
|
||||
for path in allPaths do
|
||||
let sourceMethods ← findMethodologies path.sourceClassifier
|
||||
for M in sourceMethods do
|
||||
tried := tried.push M.theoremName
|
||||
if (← tryEntryAsClosed M) then return
|
||||
let witnessEntry : MethodologyEntry :=
|
||||
{ classifierName := path.targetClassifier
|
||||
, theoremName := path.witnessName
|
||||
, priority := 0, description := "" }
|
||||
tried := tried.push path.witnessName
|
||||
if (← tryEntryAsClosed witnessEntry) then return
|
||||
-- Structured failure (demonstrator format; no normative
|
||||
-- commitment — alternative composers may emit any shape).
|
||||
let lines := tried.map (fun n => s!" ✗ {n}")
|
||||
let report := String.intercalate "\n" lines.toList
|
||||
let pathCount := allPaths.size
|
||||
let methCount := methodologies.size
|
||||
throwError s!"cubical_search: no registered methodology closed the goal\n {← Meta.ppExpr goalType}\n\ncandidates considered ({methCount} direct + {pathCount} paths):\n{report}\n\nregister a new @[methodology] (or build a custom dispatcher from `tryEntryAsClosed`)."
|
||||
|
||||
-- ── Diagnostics ─────────────────────────────────────────────────────────────
|
||||
|
||||
/-- Print the methodology registry — what's currently available to
|
||||
`cubical_search`. -/
|
||||
def printMethodologies : CoreM Unit := do
|
||||
let entries ← getMethodologies
|
||||
IO.println s!"── Methodology registry ({entries.size}) ──"
|
||||
for entry in entries do
|
||||
let p := if entry.priority == 100 then "" else s!" (prio {entry.priority})"
|
||||
let d := if entry.description.isEmpty then "" else s!" — {entry.description}"
|
||||
IO.println s!" {entry.classifierName} → {entry.theoremName}{p}{d}"
|
||||
|
||||
end CubicalTransport.Algebra
|
||||
|
|
@ -1,185 +0,0 @@
|
|||
/-
|
||||
CubicalTransport.Algebra.Restructure — the universal macro
|
||||
==========================================================
|
||||
Phase B of `docs/ALGEBRA_PLAN.md`. Defines the `restructure`
|
||||
operation — a function with the same five-field shape as
|
||||
`comp i A φ u t`, lifted to the meta-source-code level.
|
||||
|
||||
Per ALGEBRA_PLAN §0:
|
||||
> One macro. Built from `comp`. Aliases accrue by usage; tactics
|
||||
> are search over a library that grows under structural-Path
|
||||
> declarations alone.
|
||||
|
||||
All 32 enumerated macros from the original sketch are *frozen
|
||||
partial applications* of this single `restructure`; the alias
|
||||
layer in `Algebra/MacroAlias.lean` lets users (or the system)
|
||||
name recurring patterns.
|
||||
-/
|
||||
|
||||
import CubicalTransport.Algebra.Edit
|
||||
|
||||
namespace CubicalTransport.Algebra
|
||||
|
||||
-- ── The universal `restructure` operation ───────────────────────────────────
|
||||
|
||||
/-- `restructure i ctx φ witness fallback` — the universal source-
|
||||
mutation operation. Five fields, each mirroring a field of
|
||||
`comp i A φ u t`:
|
||||
|
||||
· `i : MetaPosition` — where in source.
|
||||
· `ctx : MetaCType` — meta-type of the artifact.
|
||||
· `φ : MetaClassifier` — when this restructuring applies.
|
||||
· `witness : MetaArtifact` — new content valid on φ.
|
||||
· `fallback : MetaArtifact` — existing content off-φ.
|
||||
|
||||
The result is an `Edit Unit`: a single `EditOp` whose content is
|
||||
`witness` (when `φ` matches at `i`) or `fallback` (otherwise).
|
||||
|
||||
The `ctx` argument is currently used only for documentation /
|
||||
diagnostics — Phase C's `@[macroAlias]` attribute consumes it
|
||||
when binding aliases. Future Phase D' may use it to dispatch
|
||||
different rendering / preview modes in the widget. -/
|
||||
def restructure (i : MetaPosition) (_ctx : MetaCType)
|
||||
(φ : MetaClassifier) (witness fallback : MetaArtifact) : Edit Unit :=
|
||||
let active := φ.atPosition i
|
||||
let chosen := if active then witness else fallback
|
||||
let label := if active then "hit" else "miss"
|
||||
Edit.emit
|
||||
{ position := i
|
||||
, newContent := chosen
|
||||
, oldContent := none
|
||||
, description := s!"restructure φ={label} at {repr i}" }
|
||||
|
||||
-- ── The 32 macros as frozen aliases ─────────────────────────────────────────
|
||||
-- Per ALGEBRA_PLAN §2.3 every "macro" in the original 32-item list
|
||||
-- is a frozen partial application. These are the foundational
|
||||
-- aliases; a downstream user / agent can register more via
|
||||
-- `@[macroAlias]` (Phase C).
|
||||
|
||||
/-- Frozen alias: `transport_artifact i ctx w` — `restructure` with
|
||||
`φ = .always`, `witness = fallback = w`. Always applies; just
|
||||
relocates `w` to `i`. -/
|
||||
@[reducible]
|
||||
def transport_artifact (i : MetaPosition) (ctx : MetaCType) (w : MetaArtifact) :
|
||||
Edit Unit :=
|
||||
restructure i ctx .always w w
|
||||
|
||||
/-- Frozen alias: `relocate_invariant i src dst` — moves a file's
|
||||
content from `src` to `dst`, classifier set to "in source file." -/
|
||||
@[reducible]
|
||||
def relocate_invariant (decl : Lean.Name) (src dst : String) : Edit Unit :=
|
||||
restructure { declName := decl, filePath := dst, range := none }
|
||||
.file (.inFile src) (.refTo decl) .empty
|
||||
|
||||
/-- Frozen alias: `rename_throughout x y` — emit a rename edit for
|
||||
declaration `x` (witness on `.atDecl x`, fallback `.empty`). -/
|
||||
@[reducible]
|
||||
def rename_throughout (oldName newName : Lean.Name) : Edit Unit :=
|
||||
restructure { declName := oldName, filePath := "", range := none }
|
||||
.definition (.atDecl oldName) (.refTo newName) .empty
|
||||
|
||||
/-- Frozen alias: `define_question_shape S` — register a new question
|
||||
schema as an inductive declaration. -/
|
||||
@[reducible]
|
||||
def define_question_shape (declName : Lean.Name) (witness : MetaArtifact) :
|
||||
Edit Unit :=
|
||||
restructure { declName := declName, filePath := "", range := none }
|
||||
.inductive_ .always witness .empty
|
||||
|
||||
/-- Frozen alias: `compose_proof_fragments` — pure `restructure` with
|
||||
no freezing. This is the "raw" `restructure` exposed under a
|
||||
documentary name; identical in behaviour. -/
|
||||
@[reducible]
|
||||
def compose_proof_fragments
|
||||
(i : MetaPosition) (ctx : MetaCType) (φ : MetaClassifier)
|
||||
(w f : MetaArtifact) : Edit Unit :=
|
||||
restructure i ctx φ w f
|
||||
|
||||
/-- Frozen alias: `materialize` — emit a piece of raw Lean source at
|
||||
a position. The leaf operation; everything else composes from
|
||||
here. -/
|
||||
@[reducible]
|
||||
def materialize (i : MetaPosition) (ctx : MetaCType) (src : String) :
|
||||
Edit Unit :=
|
||||
restructure i ctx .always (.source src) .empty
|
||||
|
||||
-- ── Headless interpreter: apply edits to an in-memory buffer ────────────────
|
||||
-- Phase 5.3 No-LSP fallback: same operations as `lake exe
|
||||
-- algebra-restructure` subcommands. Useful for batch CI runs.
|
||||
|
||||
/-- A simple in-memory source buffer. Maps file paths to current
|
||||
contents. `applyOp` mutates the buffer in place. -/
|
||||
abbrev SourceBuffer := Std.HashMap String String
|
||||
|
||||
/-- Apply a single `EditOp` to a source buffer. For now this is a
|
||||
crude full-file overwrite when `position.range` is `none`; range-
|
||||
based partial overwrites are scheduled for the LSP-backed
|
||||
integration in `Algebra/EditLSP.lean`.
|
||||
|
||||
Returns the updated buffer. Diagnostic lines printed to
|
||||
`IO.stderr` describe what changed. -/
|
||||
def EditOp.apply (op : EditOp) (buf : SourceBuffer) : IO SourceBuffer := do
|
||||
let path := op.position.filePath
|
||||
match op.newContent with
|
||||
| .source s =>
|
||||
IO.eprintln s!"[restructure] writing {path} (decl {op.position.declName})"
|
||||
return buf.insert path s
|
||||
| .empty =>
|
||||
IO.eprintln s!"[restructure] removing {path} (decl {op.position.declName})"
|
||||
return buf.erase path
|
||||
| .refTo n =>
|
||||
IO.eprintln s!"[restructure] {path}: rename / link → {n}"
|
||||
return buf
|
||||
| .declAt _ =>
|
||||
IO.eprintln s!"[restructure] {path}: emit syntax (LSP-bound; headless skipped)"
|
||||
return buf
|
||||
|
||||
/-- Run an `Edit` headless: apply every emitted op in order to an
|
||||
initial source buffer. Returns the final buffer plus the
|
||||
computation's value. -/
|
||||
def Edit.runHeadless {α : Type} (e : Edit α) (initial : SourceBuffer) :
|
||||
IO (α × SourceBuffer) := do
|
||||
let mut buf := initial
|
||||
for op in e.ops do
|
||||
buf ← op.apply buf
|
||||
return (e.result, buf)
|
||||
|
||||
-- ── Soundness guard scaffold ────────────────────────────────────────────────
|
||||
-- ALGEBRA_PLAN §3.3: every Edit passes through `preserve_typing`.
|
||||
-- The full integration requires invoking `lean` on a fresh source
|
||||
-- buffer; the data-level guard here checks that no edit deletes
|
||||
-- a declaration that other edits in the same batch reference.
|
||||
|
||||
/-- The names referenced by an `EditOp` (as a `MetaArtifact.refTo`). -/
|
||||
def EditOp.referenced : EditOp → List Lean.Name
|
||||
| { newContent := .refTo n, .. } => [n]
|
||||
| _ => []
|
||||
|
||||
/-- The decl-name *removed* by an `EditOp` (when content is `.empty`). -/
|
||||
def EditOp.removed : EditOp → List Lean.Name
|
||||
| { newContent := .empty, position := p, .. } => [p.declName]
|
||||
| _ => []
|
||||
|
||||
/-- A "broken reference" predicate: does this batch reference any
|
||||
name that the same batch removes? The structural check that
|
||||
runs in any environment, headless or not. -/
|
||||
def Edit.brokenRefs {α : Type} (e : Edit α) : List Lean.Name :=
|
||||
let removed := e.ops.flatMap EditOp.removed
|
||||
let referenced := e.ops.flatMap EditOp.referenced
|
||||
referenced.filter (· ∈ removed)
|
||||
|
||||
/-- The structural soundness check: an `Edit` is *self-consistent*
|
||||
if no op references a name another op in the batch removes.
|
||||
Full type-checking of the post-edit buffer is the LSP-integrated
|
||||
layer's job (`Algebra/EditLSP.lean`). -/
|
||||
def Edit.selfConsistent {α : Type} (e : Edit α) : Bool :=
|
||||
e.brokenRefs.isEmpty
|
||||
|
||||
/-- Guarded wrapper: aborts the edit if its self-consistency check
|
||||
fails. Mirrors the `Edit.guarded` shape in ALGEBRA_PLAN §3.3. -/
|
||||
def Edit.guarded {α : Type} [Inhabited α] (e : Edit α) :
|
||||
Except String (Edit α) :=
|
||||
if e.selfConsistent then .ok e
|
||||
else .error s!"restructure batch breaks references: {repr e.brokenRefs}"
|
||||
|
||||
end CubicalTransport.Algebra
|
||||
|
|
@ -16,14 +16,14 @@
|
|||
live in `FFITest.lean`.
|
||||
-/
|
||||
|
||||
import CubicalTransport.Algebra.Methodology
|
||||
import CubicalTransport.Algebra.MetaPath
|
||||
import Infoductor.Foundation.Methodology
|
||||
import Infoductor.Foundation.MetaPath
|
||||
import CubicalTransport.Algebra.EngineMethodologies
|
||||
import CubicalTransport.Question
|
||||
|
||||
namespace CubicalTransport.Algebra.Test
|
||||
|
||||
open CubicalTransport.Algebra
|
||||
open Infoductor
|
||||
open Question
|
||||
|
||||
-- ── Phase A: meta-mirror types ─────────────────────────────────────────────
|
||||
|
|
|
|||
|
|
@ -23,13 +23,13 @@ import CubicalTransport.FFI
|
|||
import CubicalTransport.Inductive
|
||||
import CubicalTransport.Bridge
|
||||
import CubicalTransport.Question
|
||||
import CubicalTransport.Algebra.Restructure
|
||||
import Infoductor.Foundation.Restructure
|
||||
|
||||
open CubicalTransport.Inductive
|
||||
open CubicalTransport.Inductive.CTerm
|
||||
open CubicalTransport.Bridge
|
||||
open Question
|
||||
open CubicalTransport.Algebra
|
||||
open Infoductor
|
||||
|
||||
namespace CubicalTransportFFITest
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,16 @@
|
|||
{"version": "1.2.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages": [],
|
||||
"packages":
|
||||
[{"url": "https://maxgit.wg/max/infoductor.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "ba0a49823bf33adca771365f03db6a757f318b0a",
|
||||
"name": "infoductor",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.toml"}],
|
||||
"name": "cubicalTransport",
|
||||
"lakeDir": ".lake",
|
||||
"fixedToolchain": false}
|
||||
|
|
|
|||
|
|
@ -2,6 +2,14 @@ name = "cubicalTransport"
|
|||
version = "0.1.0"
|
||||
defaultTargets = ["cubical-test"]
|
||||
|
||||
# Generic methodology / repo-organization machinery — registries,
|
||||
# restructure operation, Edit/Context monad-comonad pair, attribute
|
||||
# infrastructure — extracted to its own repo on 2026-05-01.
|
||||
[[require]]
|
||||
name = "infoductor"
|
||||
git = "https://maxgit.wg/max/infoductor.git"
|
||||
rev = "master"
|
||||
|
||||
[[lean_lib]]
|
||||
name = "CubicalTransport"
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue