/-
  Topolei.Cubical.Transport
  =========================
  Value-level transport (cells-spec §5.5, Phase 1 Weeks 3–4).

  `vTransp i A φ v` reduces `transp^i A φ v` at the value level.

  Reducing cases (in match order, highest priority first):

    1. **φ = .top** — full face — return `v` unchanged.
       Evaluator-level analogue of axiom `transp_id` (T1).
    2. **`CType.dimAbsent i A = true`** — line is constant — return `v`
       unchanged.  Evaluator-level analogue of `transp_const_id` (T2).
       Covers `univ`, fully-constant `pi`, fully-constant `path`.
    3. **`A = pi domA codA`** — produce a `vTranspFun i domA codA φ v`
       closure.  This is the **full CCHM Π rule** — when the closure is
       later applied to an argument, `vApp` inversely transports the
       argument through `domA` and forward-transports the result through
       `codA`.  Both constant-domain and varying-domain lines are handled
       by the same constructor; `vTranspInv` degenerates to identity in
       the constant-domain case via `CType.substDimExpr_of_absent` + T2,
       so no special-case logic is needed at this level.
    4. **Otherwise** — stuck.  Produce `vneu (.ntransp i A φ v)`.

  Deferred to later passes:

    · Σ case — `CType` has no Σ yet.
    · Path case — Week 4, alongside homogeneous composition.

  vTransp is a `partial def` for the same reason as `eval`.  Its reduction
  equations are stated as axioms below.  `vTranspInv` is a *total `def`*
  because it is a thin wrapper that delegates to `vTransp` after line
  reversal.
-/

import CubicalTransport.Value
import CubicalTransport.DimLine  -- for CType.dimAbsent and substDimExpr

-- ── Rust FFI declaration (Phase C.2) ──────────────────────────────────────

@[extern "topolei_cubical_vtransp"]
opaque vTranspRust (i : DimVar) (A : CType) (φ : FaceFormula) (v : CVal) : CVal

/-- Value-level transport.  Dispatches in priority order; see file header. -/
@[implemented_by vTranspRust]
partial def vTransp (i : DimVar) (A : CType) (φ : FaceFormula) (v : CVal) :
    CVal :=
  match φ with
  | .top => v   -- (1) T1 at eval level.
  | _ =>
    if CType.dimAbsent i A then
      v  -- (2) T2 at eval level.
    else
      match A with
      | .pi domA codA =>
          -- (3) Full CCHM Π rule — no specialisation here.  The behaviour
          -- at constant-domain vs. varying-domain is absorbed into the
          -- later reduction of `vApp` on `vTranspFun`, which calls
          -- `vTranspInv` on `domA` (identity when `domA` is constant).
          .vTranspFun i domA codA φ v
      | _ =>
          -- (4) non-pi stuck (e.g. path with varying endpoints).
          .vneu (.ntransp i A φ v)

/-- **Inverse transport** along the line `(i, A)`: transport `v : A(1)` back
    to `A(0)`.  Implemented as forward transport along the *reversed* line
    `A[i := inv i]`.

    Line reversal properties at the endpoints:
      `A[i := inv i]  at 0`  = `A  at (inv 0)` = `A at 1`
      `A[i := inv i]  at 1`  = `A  at (inv 1)` = `A at 0`
    So forward transport along the reversed line takes `A(1) ↦ A(0)`,
    which is exactly the inverse of forward transport along `A`. -/
def vTranspInv (i : DimVar) (A : CType) (φ : FaceFormula) (v : CVal) : CVal :=
  vTransp i (A.substDimExpr i (.inv (.var i))) φ v

/-!
## Reduction axioms and theorems

One axiom per reducing match arm of `vTransp`.  The arms are disjoint
(ordered pattern match), so the axiom set is consistent.
-/

/-- (1) Reduction under a full face: transport is identity. -/
axiom vTransp_top (i : DimVar) (A : CType) (v : CVal) :
    vTransp i A .top v = v

/-- (2) Reduction under a constant line. -/
axiom vTransp_const (i : DimVar) (A : CType) (φ : FaceFormula) (v : CVal)
    (h : CType.dimAbsent i A = true) :
    vTransp i A φ v = v

/-- (3) Π case (full CCHM rule): produces a transported-function closure
    that stores both domain and codomain.  Preconditions:
      · `φ ≠ .top`                                   — else (1) fires,
      · `CType.dimAbsent i (.pi domA codA) = false`  — else (2) fires.
    When `dimAbsent i domA = true`, the inverse transport inside the
    later `vApp` reduction degenerates to identity by `vTranspInv_const`
    below, recovering the const-domain specialisation. -/
axiom vTransp_pi
    (i : DimVar) (domA codA : CType) (φ : FaceFormula) (v : CVal)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i (.pi domA codA) = false) :
    vTransp i (.pi domA codA) φ v = .vTranspFun i domA codA φ v

/-- (4) Stuck: not face-top, not constant, and not a `.pi`.  The third
    precondition rules out arm (3). -/
axiom vTransp_stuck (i : DimVar) (A : CType) (φ : FaceFormula) (v : CVal)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i A = false)
    (h_not_pi : ∀ domA codA, A ≠ .pi domA codA) :
    vTransp i A φ v = .vneu (.ntransp i A φ v)

-- ── vTranspInv on constant domain ────────────────────────────────────────────

/-- Inverse transport along a line whose body is absent from `i` is the
    identity.  Proof: the reversed line `A[i := inv i] = A` when `i ∉ A`
    (by `CType.substDimExpr_of_absent`), so the outer `vTransp` call has a
    constant line and reduces via T2 to `v`.  This lemma is what makes the
    unified `vTranspFun` constructor degenerate correctly when the domain
    is constant. -/
theorem vTranspInv_const (i : DimVar) (A : CType) (φ : FaceFormula) (v : CVal)
    (h : CType.dimAbsent i A = true) :
    vTranspInv i A φ v = v := by
  -- `vTranspInv` unfolds to `vTransp i (A[i := inv i]) φ v`.
  unfold vTranspInv
  -- Line reversal is a no-op on constant-in-`i` types.
  rw [CType.substDimExpr_of_absent i _ A h]
  -- T2 on the (unchanged) constant line.
  exact vTransp_const i A φ v h

/-- Inverse transport under a full face is identity — direct consequence of
    T1 composed with reversal. -/
theorem vTranspInv_top (i : DimVar) (A : CType) (v : CVal) :
    vTranspInv i A .top v = v := by
  unfold vTranspInv
  exact vTransp_top i _ v

-- ── Convenience wrappers ──────────────────────────────────────────────────────

/-- Transport along a `DimLine` with an already-evaluated argument.  Unpacks
    the line's binder and body and dispatches through `vTransp`. -/
def vTranspLine (L : DimLine) (φ : FaceFormula) (v : CVal) : CVal :=
  vTransp L.binder L.body φ v

@[simp] theorem vTranspLine_top (L : DimLine) (v : CVal) :
    vTranspLine L .top v = v := by
  simp [vTranspLine, vTransp_top]

theorem vTranspLine_const (L : DimLine) (φ : FaceFormula) (v : CVal)
    (h : CType.dimAbsent L.binder L.body = true) :
    vTranspLine L φ v = v := by
  simp [vTranspLine, vTransp_const _ _ _ _ h]