commit ba0a49823bf33adca771365f03db6a757f318b0a Author: Maximus Gorog Date: Fri May 1 07:20:36 2026 -0600 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) diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..a4c7621 --- /dev/null +++ b/.gitignore @@ -0,0 +1,19 @@ +# Lean build cache +/.lake/ +/build/ + +# Compiled Lean object files (in case they leak outside .lake/) +*.olean +*.ilean + +# Editor / OS cruft +.DS_Store +.vscode/ +.idea/ +*.swp +*.swo +*~ + +# Logs / temp +*.log +/tmp/ diff --git a/Infoductor.lean b/Infoductor.lean new file mode 100644 index 0000000..d4b40bb --- /dev/null +++ b/Infoductor.lean @@ -0,0 +1,10 @@ +/- + Infoductor — generic methodology / repo-organization library. + + Root umbrella module. Imports each sub-library so that downstream + consumers can `import Infoductor` to bring everything into scope, + or pick specific sub-modules via fully qualified imports for + tighter compile-time graphs. +-/ + +import Infoductor.Foundation diff --git a/Infoductor/Foundation.lean b/Infoductor/Foundation.lean new file mode 100644 index 0000000..5a7e56d --- /dev/null +++ b/Infoductor/Foundation.lean @@ -0,0 +1,14 @@ +/- + Infoductor.Foundation — pure algebra of methodology organisation. + + Imports every Foundation sub-module. Downstream consumers can + either `import Infoductor.Foundation` for the whole bundle, or + pick individual modules. +-/ + +import Infoductor.Foundation.Meta +import Infoductor.Foundation.Edit +import Infoductor.Foundation.Restructure +import Infoductor.Foundation.MacroAlias +import Infoductor.Foundation.MetaPath +import Infoductor.Foundation.Methodology diff --git a/Infoductor/Foundation/Edit.lean b/Infoductor/Foundation/Edit.lean new file mode 100644 index 0000000..eb6cafc --- /dev/null +++ b/Infoductor/Foundation/Edit.lean @@ -0,0 +1,179 @@ +/- + Infoductor.Foundation.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 Infoductor.Foundation.Meta + +namespace Infoductor + +-- ── 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 Infoductor diff --git a/Infoductor/Foundation/MacroAlias.lean b/Infoductor/Foundation/MacroAlias.lean new file mode 100644 index 0000000..02e99db --- /dev/null +++ b/Infoductor/Foundation/MacroAlias.lean @@ -0,0 +1,97 @@ +/- + Infoductor.Foundation.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 Infoductor.Foundation.Restructure + +namespace Infoductor + +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 := `Infoductor.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 `Infoductor.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 Infoductor diff --git a/Infoductor/Foundation/Meta.lean b/Infoductor/Foundation/Meta.lean new file mode 100644 index 0000000..5490538 --- /dev/null +++ b/Infoductor/Foundation/Meta.lean @@ -0,0 +1,242 @@ +/- + Infoductor.Foundation.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 Infoductor + +-- ── 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()" + | .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 Infoductor diff --git a/Infoductor/Foundation/MetaPath.lean b/Infoductor/Foundation/MetaPath.lean new file mode 100644 index 0000000..d2b5c10 --- /dev/null +++ b/Infoductor/Foundation/MetaPath.lean @@ -0,0 +1,127 @@ +/- + Infoductor.Foundation.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 Infoductor.Foundation.Meta + +namespace Infoductor + +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 := `Infoductor.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 Infoductor diff --git a/Infoductor/Foundation/Methodology.lean b/Infoductor/Foundation/Methodology.lean new file mode 100644 index 0000000..a8c81d2 --- /dev/null +++ b/Infoductor/Foundation/Methodology.lean @@ -0,0 +1,285 @@ +/- + Infoductor.Foundation.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 Infoductor.Foundation.MacroAlias +import Infoductor.Foundation.MetaPath + +namespace Infoductor + +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 := `Infoductor.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 Infoductor diff --git a/Infoductor/Foundation/Restructure.lean b/Infoductor/Foundation/Restructure.lean new file mode 100644 index 0000000..c498421 --- /dev/null +++ b/Infoductor/Foundation/Restructure.lean @@ -0,0 +1,185 @@ +/- + Infoductor.Foundation.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 Infoductor.Foundation.Edit + +namespace Infoductor + +-- ── 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 Infoductor diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..b92876f --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) 2026 Maximus Gorog. All rights reserved. + +This software and the associated source files, documentation, build +scripts, configuration, and other materials in this repository +(collectively, the "Software") are the proprietary and confidential +property of the copyright holder. + +NO LICENSE IS GRANTED. The presence of this Software in a publicly +accessible repository does not, by itself, grant any permission to +use, copy, modify, merge, publish, distribute, sublicense, link +against, embed, or create derivative works of the Software, in whole +or in part, for any purpose. + +Use of any kind — including but not limited to compilation, execution, +incorporation into other software, or redistribution in any form — +requires express prior written consent from the copyright holder. +Unauthorized use is prohibited. + +For licensing inquiries, contact: mgorog@gmail.com + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, AND +NONINFRINGEMENT. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE +FOR ANY CLAIM, DAMAGES, OR OTHER LIABILITY, WHETHER IN AN ACTION OF +CONTRACT, TORT, OR OTHERWISE, ARISING FROM, OUT OF, OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/NOTICE b/NOTICE new file mode 100644 index 0000000..b8cb991 --- /dev/null +++ b/NOTICE @@ -0,0 +1,38 @@ +NOTICE — Development methodology and authorship + +This Software was developed under direct human creative direction with +the assistance of AI tooling (Claude, by Anthropic). AI assistance +was used analogously to an IDE, compiler, or code-completion engine: +a tool operating under continuous human supervision and review. + +The Software's design, architecture, system specifications, naming, +module organisation, interface contracts, integration strategy, and +verification plan are the work of the copyright holder. AI-generated +fragments were directed, selected, audited, refined, and integrated +by the human author, who exercised final judgment on every substantive +design and correctness decision. + +Per Anthropic's published Terms of Service, output ownership is +assigned to the user; the AI provider claims no rights in the +resulting code. Per United States Copyright Office guidance (August +2023, "Copyright Registration Guidance: Works Containing Material +Generated by Artificial Intelligence"), purely machine-generated +output is not eligible for copyright, while the selection, +arrangement, and creative human direction supplied by a human author +are. Those human-authored contributions — architectural decisions, +problem framing, design rationale, integration, and verification — +are the load-bearing creative contributions to this Software, and the +accompanying LICENSE asserts proprietary rights on the resulting +human-directed creative whole. + +"Co-Authored-By: Claude Opus 4.7 (1M context) " +footers in commit messages document the development methodology in +the customary tooling-honesty convention. They are not a claim of +legal authorship by the AI and effect no transfer of rights to any +third party. + +Trade-secret protection, contract law, and access controls applying +to this repository remain in force independent of the copyright +analysis above. + +For licensing inquiries, contact: mgorog@gmail.com diff --git a/README.md b/README.md new file mode 100644 index 0000000..2072552 --- /dev/null +++ b/README.md @@ -0,0 +1,100 @@ +# Infoductor + +Generic Lean 4 library + tooling for algebraic organization of code +repositories. Provides the *mechanism* for declaring methodologies +that organize a Lean codebase — registries, attributes, the universal +`restructure` operation, the `Edit` monad / `Context` comonad pair — +without committing to *which* methodology a downstream project uses. + +Pairs naturally with the +[Pantograph](https://github.com/leanprover/Pantograph) project (the +conductor of an electric train sits atop the pantograph hardware). +"Info-ductor" — it conducts information (structure, classifications, +methodology) through your codebase. + +## Status + +Phase A: Foundation lib landed (2026-05-01). Tactics, Pantograph +plugin, and headless Runner sub-libs are planned but not yet +present. + +## Sub-libraries + +| Library | Status | Role | +|---|---|---| +| `Infoductor.Foundation` | ✅ landed | Pure algebra: meta-mirror types, `Edit` monad, `Context` comonad, `restructure`, `@[macroAlias]` / `@[methodology]` / `@[metaPath]` attributes + registries. No domain commitments. | +| `Infoductor.Tactics` | planned | Reference dispatcher tactics (`cubical_search`-shaped) built on Foundation primitives. | +| `Infoductor.Pantograph` | planned | Plugin routing Pantograph commands into Foundation registries. | +| `Infoductor.Runner` | planned | Headless deployment surface for `Edit.runHeadless` etc. Lands when concrete deployment need arises. | + +## Foundation API + +### Meta-mirror types (`Infoductor.Foundation.Meta`) + +- `MetaCType` — the meta-types of source artifacts (theorem, + definition, instance, structure, …). +- `MetaClassifier` — a lattice of "where in the codebase" + predicates (`always`, `never`, `atDecl n`, `inFile p`, + `underAttribute a`, `dependencyOf n`, `inNamespace n`, plus + `meet` / `join`). +- `MetaArtifact` — what gets placed at a meta-position + (`source` / `declAt` / `refTo` / `empty`). +- `MetaPosition` — `(declName, filePath, range?)` addressing. + +### Edit / Context (`Infoductor.Foundation.Edit`) + +- `Edit α` — monad of source mutations. `result : α` paired with + `ops : List EditOp`. +- `Context α` — comonad of "what's around here": focal artifact, + position, siblings. `extract` / `extend` operations. +- `contextualEdit` — distributive law lifting context-aware + decisions into edits. + +### Restructure (`Infoductor.Foundation.Restructure`) + +- `restructure (i ctx φ witness fallback)` — the universal source- + mutation operation. Same five-field shape as cubical `comp`, + promoted to source-code level. +- Frozen aliases: `transport_artifact`, `relocate_invariant`, + `rename_throughout`, `define_question_shape`, + `compose_proof_fragments`, `materialize`. +- Headless interpreter: `EditOp.apply`, `Edit.runHeadless`. +- Structural soundness: `Edit.brokenRefs`, `Edit.selfConsistent`, + `Edit.guarded`. + +### Registries + +- `@[macroAlias]` (`Infoductor.Foundation.MacroAlias`) — register + a `def` as a frozen `restructure` alias. +- `@[methodology Classifier]` + (`Infoductor.Foundation.Methodology`) — register a theorem as a + proof methodology indexed by classifier name. +- `@[metaPath Source Target]` + (`Infoductor.Foundation.MetaPath`) — declare a structural Path + between two classifiers; powers `deriveByTransport`. +- `tryEntryAsClosed` primitive — try a methodology entry as a + goal closer; restores tactic state on failure. + +## Inspecting registries + +`#eval` inside a Lean session: + +```lean +#eval Infoductor.printAliases +#eval Infoductor.printMethodologies +#eval Infoductor.printMetaPaths +``` + +## Building + +```sh +lake build +``` + +## Forgejo + +`http://maxgit.wg:3000/max/infoductor` + +## License + +See `LICENSE`. diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..0602039 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "infoductor", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..0c04120 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,29 @@ +name = "infoductor" +version = "0.1.0" +defaultTargets = ["Infoductor"] + +# Generic Lean library + tooling for algebraic organization of code +# repositories: `restructure` macro layer, `Edit` monad, `Context` +# comonad, the `@[macroAlias]` / `@[methodology]` / `@[metaPath]` +# attribute registries, and reference dispatch tactics. +# +# Consumers (cubical-transport-hott-lean4, topolei, …) depend on +# `Infoductor.Foundation` (and, when wanted, the other lean_libs +# below) to organise their proofs without committing to a specific +# methodology — the methodology is the consumer's choice. +# +# Pairs naturally with the Pantograph project (the conductor of an +# electric train sits atop the pantograph hardware). + +[[lean_lib]] +name = "Infoductor" +# Default lib root. Subdirectories below carve out cherry-pickable +# sub-libs; downstream `import Infoductor.Foundation.Meta` only +# pulls Foundation's subgraph. + +# Subdirectory `lean_lib`s — declared as we land each in turn. +# Foundation: pure algebra (Meta types, Edit/Context, restructure, +# registries). Lands first. +# Tactics: reference dispatchers built on Foundation. +# Pantograph: plugin / live integration (when ready). +# Runner: headless surface (when concrete need arises). diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..6c7e31f --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0-rc2