cubical-transport-hott-lean4/CubicalTransport/Algebra/MetaPath.lean

/-
  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