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