# 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`.