/-
  Topolei.Cubical.Eval
  ====================
  Environment-based evaluator for the cubical calculus (cells-spec §5.4,
  Phase 1 Week 2).

  `eval env t` reduces `t` to weak-head normal form in environment `env`.
  Three mutually-recursive pieces:

    · `eval`   : `CEnv → CTerm → CVal`  — main evaluator
    · `vApp`   : `CVal → CVal → CVal`   — function application at the value level
    · `vPApp`  : `CVal → DimExpr → CVal` — path (dimension) application at value level

  Coverage: the *λ-calculus fragment* — `var`/`lam`/`app`/`plam`/`papp`.
  `transp`/`comp` produce stuck neutrals (`ntransp`/`ncomp`); their real
  reduction rules come with `Transport.lean` and `Comp.lean` (Weeks 3–4).

  These are `partial def`s.  Termination isn't statically checked because the
  `vPApp` β-step substitutes inside the closure body and re-evaluates; the
  result is the same `CTerm` size, but Lean's structural recursion can't see
  through that.  A future total version will measure on a subject-reduction
  metric.  For now, `partial def` is the honest choice.
-/

import CubicalTransport.Value
import CubicalTransport.Transport

-- ── Rust FFI declarations (Phase C.2) ──────────────────────────────────────
-- `@[extern "topolei_cubical_*"] opaque *Rust ...` declares the Rust
-- entry point.  `@[implemented_by]` on each partial def routes runtime
-- calls to Rust (kernel-level proof reasoning still uses the axioms).

@[extern "topolei_cubical_eval"]
opaque evalRust (env : CEnv) : CTerm → CVal

@[extern "topolei_cubical_vapp"]
opaque vAppRust : CVal → CVal → CVal

@[extern "topolei_cubical_vpapp"]
opaque vPAppRust : CVal → DimExpr → CVal

@[extern "topolei_cubical_vhcomp"]
opaque vHCompValueRust (A : CType) (φ : FaceFormula) (tube base : CVal) : CVal

@[extern "topolei_cubical_vcomp_term"]
opaque vCompAtTermRust (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (u t : CTerm) : CVal

@[extern "topolei_cubical_vcompn_term"]
opaque vCompNAtTermRust (env : CEnv) (i : DimVar) (A : CType)
    (clauses : List (FaceFormula × CTerm)) (t : CTerm) : CVal

@[extern "topolei_cubical_vfst"]
opaque vFstRust : CVal → CVal

@[extern "topolei_cubical_vsnd"]
opaque vSndRust : CVal → CVal

mutual
  /-- Evaluate a term in an environment.  λ-fragment + dimension abstraction
      are reduced immediately; transport dispatches through `vTransp`;
      heterogeneous composition dispatches through `vCompAtTerm` (which has
      access to the raw CTerms so it can substitute at the term level for
      `comp_full`).

      This is a `partial def` because the β-step in `vPApp` substitutes inside
      a closure body (via `CTerm.substDim`) and re-evaluates — the resulting
      term is the same CTerm size, but Lean's structural-recursion checker
      can't see through that, and indeed an untyped Ω-like term genuinely
      diverges.  A well-typed total evaluator arrives in a later phase. -/
  @[implemented_by evalRust]
  partial def eval (env : CEnv) : CTerm → CVal
    | .var x          => (env.lookup x).getD (.vneu (.nvar x))
    | .lam x body     => .vlam env x body
    | .app f a        => vApp (eval env f) (eval env a)
    | .plam i body    => .vplam env i body
    | .papp t r       => vPApp (eval env t) r
    | .transp i A φ t =>
        -- Priority order: (1) full face, (2) constant line, (3) path
        -- (needs env), (4) glue (dispatched via dedicated axioms in
        -- `Glue.lean`; the partial def produces a stuck neutral as a
        -- runtime placeholder), (5) other via value-level `vTransp`.
        match φ with
        | .top => eval env t                                             -- (1) T1
        | _ =>
          if CType.dimAbsent i A then
            eval env t                                                    -- (2) T2
          else
            match A with
            | .path A₀ a b => .vPathTransp env i A₀ a b φ t              -- (3)
            | .glue _ _ _ _ _ _ _ _ =>                                   -- (4) Glue
                -- Real reduction rules live in `Glue.lean` as dedicated
                -- axioms keyed on specific sub-cases (e.g. constant
                -- equivalence components).  The partial def produces
                -- `ntransp` as a placeholder — the same shape vTransp
                -- would produce on stuck glue — so that kernel-level
                -- proofs go exclusively through the Glue axioms.
                .vneu (.ntransp i A φ (eval env t))
            | _ => vTransp i A φ (eval env t)                            -- (5)
    | .comp i A φ u t => vCompAtTerm env i A φ u t
    | .compN i A clauses t => vCompNAtTerm env i A clauses t
    | .glueIn φ t a =>
        -- Face-priority dispatch: φ = .top → t-side, φ = .bot → a-side,
        -- else stuck `.nglueIn` preserving both face-on / face-off values.
        match φ with
        | .top => eval env t
        | .bot => eval env a
        | _    => .vneu (.nglueIn φ (eval env t) (eval env a))
    | .unglue φ f g =>
        -- Face-priority dispatch:
        --   φ = .top: apply the forward map; the argument is a T-value.
        --   φ = .bot: identity — on the empty face, the glued term is the
        --     A-value `g` itself (consistent with `glueIn .bot t a → a`).
        --   Else: stuck `.nunglue` preserving `f` and `g`.
        match φ with
        | .top => vApp (eval env f) (eval env g)
        | .bot => eval env g
        | _    => .vneu (.nunglue φ (eval env f) (eval env g))
    | .pair a b      => .vpair (eval env a) (eval env b)
    | .fst t         => vFst (eval env t)
    | .snd t         => vSnd (eval env t)
    -- REL1 inductive-type constructors.
    | .dimExpr r     => .vdimExpr r
    | .ctor S c params args =>
        -- Produce a canonical constructor value with all args evaluated.
        -- (Boundary firing for path ctors lands in a follow-up — REL1
        -- design doc §4: when a `.dim`-typed arg evaluates to .zero/.one
        -- and matches a clause in `S.ctors[c].boundary`, we should fire
        -- that clause body instead.  TODO REL1.1.)
        .vctor S c params (args.map (eval env))
    | .indElim S params motive branches target =>
        -- β-reduce on a canonical `vctor`; otherwise build a stuck
        -- `.nIndElim` that preserves env-evaluated motive and branches
        -- so it can unstick when target later resolves.
        match eval env target with
        | .vctor _ c _ argsV =>
            match List.lookup c branches with
            | some body =>
                -- Apply branch body to constructor's args via repeated
                -- `vApp` — the body is curried: λ a₁ … aₙ. result.
                -- Recursive-arg hypotheses (the IH passed alongside each
                -- `.self` arg in the design doc §5) are not yet wired
                -- here; an `indElim` of a non-recursive ctor is fully
                -- handled, but recursive ctors land their branch body
                -- with only the constructor args (no IH) — TODO REL1.1.
                argsV.foldl (fun f a => vApp f a) (eval env body)
            | none =>
                .vneu (.nvar s!"<indElim: no branch for {c}>")
        | .vneu n =>
            .vneu (.nIndElim S params (eval env motive)
                    (branches.map (fun (nm, b) => (nm, eval env b))) n)
        | _ =>
            .vneu (.nvar "<indElim: target is not canonical>")

  /-- First projection at the value level.  β-reduces `vpair`; pushes a
      stuck neutral into `nfst`.  Projecting any other value shape is a
      type error (marker neutral). -/
  @[implemented_by vFstRust]
  partial def vFst : CVal → CVal
    | .vpair a _ => a
    | .vneu n    => .vneu (.nfst n)
    | _          => .vneu (.nvar "<vFst: non-pair projection>")

  /-- Second projection at the value level.  Mirror of `vFst`. -/
  @[implemented_by vSndRust]
  partial def vSnd : CVal → CVal
    | .vpair _ b => b
    | .vneu n    => .vneu (.nsnd n)
    | _          => .vneu (.nvar "<vSnd: non-pair projection>")

  /-- Apply one value to another.  β-reduces `vlam` closures; pushes stuck
      neutrals into `napp`.  `vTranspFun` unfolds per the *full* CCHM Π rule.
      `vHCompFun` unfolds per the CCHM Π hcomp rule: apply pointwise
      through the tube, then recursively hcomp on the codomain.  Applying
      a `vplam` or `vTubeApp` as a function is a type error. -/
  @[implemented_by vAppRust]
  partial def vApp : CVal → CVal → CVal
    | .vlam env x body,             arg => eval (env.extend x arg) body
    | .vneu n,                      arg => .vneu (.napp n arg)
    | .vTranspFun i domA codA φ f,  arg =>
        vTransp i codA φ (vApp f (vTranspInv i domA φ arg))
    | .vHCompFun codA φ tube base,  arg =>
        vHCompValue codA φ (.vTubeApp tube arg) (vApp base arg)
    -- Full CCHM Π hetero comp β-rule.  See file-level comment below for
    -- the fill construction.
    | .vCompFun env i domA codA φ u t, arg =>
        let yName := "$y"
        let fj    : DimVar := ⟨"$fj"⟩
        let newEnv := env.extend yName arg
        -- `filled_y_at_i`: a line in the *outer* binder `i` giving y_at_i:A(i).
        -- Build as `transp^{fj} (domA[i := (inv fj) ∨ i]) φ ($y)`:
        --   at fj=0: line slice is A(1)  (source: y : A(1))
        --   at fj=1: line slice is A(i)  (target we want)
        let filled_y_at_i : CTerm :=
          .transp fj
            (domA.substDimExpr i (.join (.inv (.var fj)) (.var i)))
            φ (.var yName)
        -- `filled_y_at_0`: substitute i := 0 in the above — the reversed
        -- line is `A[i := inv fj]`, taking A(1) → A(0).
        let filled_y_at_0 : CTerm :=
          .transp fj
            (domA.substDimExpr i (.inv (.var fj)))
            φ (.var yName)
        eval newEnv (.comp i codA φ
          (.app u filled_y_at_i)
          (.app t filled_y_at_0))
    | .vplam _ _ _,                 _   => .vneu (.nvar "<vApp: vplam applied as function>")
    | .vTubeApp _ _,                _   => .vneu (.nvar "<vApp: vTubeApp applied as function>")
    | .vPathTransp _ _ _ _ _ _ _,   _   => .vneu (.nvar "<vApp: vPathTransp applied as function>")
    | .vpair _ _,                   _   => .vneu (.nvar "<vApp: vpair applied as function>")
    | .vctor _ _ _ _,               _   => .vneu (.nvar "<vApp: vctor applied as function>")
    | .vdimExpr _,                  _   => .vneu (.nvar "<vApp: vdimExpr applied as function>")

  /-- Apply a value to a dimension expression.  β-reduces `vplam` closures
      by substituting the dim in the body and re-evaluating; pushes stuck
      neutrals into `npapp`.  `vTubeApp tube arg` applied to dim `r` reduces
      to `vApp (vPApp tube r) arg` — the semantic meaning of
      `λj. (tube @ j) arg`.  Marker neutrals for ill-typed applications. -/
  @[implemented_by vPAppRust]
  partial def vPApp : CVal → DimExpr → CVal
    | .vplam env i body,        r => eval env (body.substDim i r)
    | .vneu n,                  r => .vneu (.npapp n r)
    | .vTubeApp tube arg,       r => vApp (vPApp tube r) arg
    -- Path transport endpoint reductions: at `.zero` / `.one` the CCHM
    -- multi-clause system degenerates (the (j=0) or (j=1) clause fires)
    -- and the result is the specified endpoint at i=1.  At generic `r`
    -- we fall through to `vCompNAtTerm` on the CCHM multi-clause system
    -- `[φ ↦ p@r, (r=0) ↦ a, (r=1) ↦ b]` with base `p@r` — which reduces
    -- further if the face substitutions happen to simplify.
    | .vPathTransp env i _ a _ _ _,  .zero => eval env (a.substDim i .one)
    | .vPathTransp env i _ _ b _ _,  .one  => eval env (b.substDim i .one)
    | .vPathTransp env i A a b φ p,  r     =>
        vCompNAtTerm env i A
          [ (φ,                       .papp p r)
          , (FaceFormula.dimExprEq0 r, a)
          , (FaceFormula.dimExprEq1 r, b) ]
          (.papp p r)
    | .vlam _ _ _,              _ => .vneu (.nvar "<vPApp: vlam applied as path>")
    | .vTranspFun _ _ _ _ _,    _ => .vneu (.nvar "<vPApp: vTranspFun applied as path>")
    | .vHCompFun _ _ _ _,       _ => .vneu (.nvar "<vPApp: vHCompFun applied as path>")
    | .vCompFun _ _ _ _ _ _ _,  _ => .vneu (.nvar "<vPApp: vCompFun applied as path>")
    | .vpair _ _,               _ => .vneu (.nvar "<vPApp: vpair applied as path>")
    | .vctor _ _ _ _,           _ => .vneu (.nvar "<vPApp: vctor applied as path>")
    | .vdimExpr _,              _ => .vneu (.nvar "<vPApp: vdimExpr applied as path>")

  /-- Homogeneous composition at the value level.  The type `A` is
      *homogeneous* (doesn't vary along `i`); the tube and base are
      already-evaluated values.

      Reducing cases (in match order):
        1. `φ = .top`    — tube covers everything, result is `tube @ 1`.
        2. `A = .pi`     — CCHM Π hcomp: construct a `vHCompFun` closure
                           that applies pointwise when the function is
                           applied to an argument.
        3. Otherwise     — stuck `.vneu (.nhcomp ...)`.

      Note the crucial difference from `vTransp`: no constant-line check,
      because hcomp is *already* homogeneous — constancy is built in. -/
  @[implemented_by vHCompValueRust]
  partial def vHCompValue (A : CType) (φ : FaceFormula) (tube base : CVal) :
      CVal :=
    match φ with
    | .top => vPApp tube .one
    | _ =>
      match A with
      | .pi _domA codA => .vHCompFun codA φ tube base
      | _              => .vneu (.nhcomp A φ tube base)

  /-- Heterogeneous composition at the term level.  Takes `u` and `t` as
      `CTerm`s (not `CVal`s) so that the `comp_full` reduction can perform
      substitution *at the term level* — `eval env (u.substDim i .one)` —
      which is in general different from `vPApp (eval env u) .one`.

      Reducing cases (in match order):
        1. `φ = .top`                    — C1: `eval env (u[i := 1])`.
        2. `φ = .bot`                    — C2: `eval env (transp i A .bot t)`.
        3. `CType.dimAbsent i A = true`  — constant line: heterogeneous
                                           comp reduces to hcomp on the
                                           fixed type `A`, with `.plam i u`
                                           as the tube.
        4. Otherwise                     — stuck `.vneu (.ncomp ...)`.

      Note cases (1) and (2) are decidable at the `.top`/`.bot` head of
      `φ`; case (3) discriminates on `A` only after `.top`/`.bot` are
      ruled out.  All four cases are mutually exclusive. -/
  @[implemented_by vCompAtTermRust]
  partial def vCompAtTerm (env : CEnv) (i : DimVar) (A : CType)
      (φ : FaceFormula) (u t : CTerm) : CVal :=
    match φ with
    | .top => eval env (u.substDim i .one)
    | .bot => eval env (.transp i A .bot t)
    | _ =>
      if CType.dimAbsent i A then
        -- Constant line: hetero comp reduces to hcomp.  `.plam i u` is the
        -- tube as a dim-closure.
        vHCompValue A φ (eval env (.plam i u)) (eval env t)
      else
        match A with
        | .pi domA codA =>
            -- Hetero Π comp: package into a `vCompFun` closure.  The CCHM
            -- β-rule runs at `vApp`-time with a full fill-based tube.
            .vCompFun env i domA codA φ u t
        | _ =>
            .vneu (.ncomp i A φ (eval env u) (eval env t))

  /-- Multi-clause heterogeneous composition at the term level.  Dispatches
      by scanning the clause list:
        · If any clause has face `.top`, that clause's body substituted at
          `i := .one` is the result (CCHM multi-clause full-system rule).
        · If all clause faces are `.bot` or the list is empty, no clause
          fires — reduces to plain transport of the base.
        · If exactly one clause has a non-trivial face, delegate to
          `vCompAtTerm` (single-clause specialisation).
        · Otherwise produce a stuck `ncompN` neutral preserving env, line
          binder, type, evaluated clauses, and evaluated base. -/
  @[implemented_by vCompNAtTermRust]
  partial def vCompNAtTerm (env : CEnv) (i : DimVar) (A : CType)
      (clauses : List (FaceFormula × CTerm)) (t : CTerm) : CVal :=
    -- Scan for a `.top` clause first.
    match clauses.find? (fun ⟨φ, _⟩ => match φ with | .top => true | _ => false) with
    | some ⟨_, u⟩ => eval env (u.substDim i .one)
    | none =>
      -- Strip `.bot` clauses (they never fire).
      let live := clauses.filter
        (fun ⟨φ, _⟩ => match φ with | .bot => false | _ => true)
      match live with
      | []          => eval env (.transp i A .bot t)
      | [⟨φ, u⟩]    => vCompAtTerm env i A φ u t
      | _           =>
          .vneu (.ncompN env i A
            (live.map (fun ⟨φ, u⟩ => (φ, eval env u)))
            (eval env t))
end

/-!
## Reduction lemmas (axioms)

`partial def` is opaque at the kernel level, so the defining cases of
`eval`, `vApp`, and `vPApp` are not reducible by `rfl`.  We state them as
axioms — the same pattern used for `CTerm.step` and `step_papp_plam` in
`Syntax.lean`.  They exactly mirror the `partial def` match arms above,
so they are consistent with the runtime implementation while also being
usable in kernel-level proofs.
-/

-- Reduction lemmas for `eval`.

axiom eval_var (env : CEnv) (x : String) :
    eval env (.var x) = (env.lookup x).getD (.vneu (.nvar x))

axiom eval_lam (env : CEnv) (x : String) (body : CTerm) :
    eval env (.lam x body) = .vlam env x body

axiom eval_app (env : CEnv) (f a : CTerm) :
    eval env (.app f a) = vApp (eval env f) (eval env a)

axiom eval_plam (env : CEnv) (i : DimVar) (body : CTerm) :
    eval env (.plam i body) = .vplam env i body

axiom eval_papp (env : CEnv) (t : CTerm) (r : DimExpr) :
    eval env (.papp t r) = vPApp (eval env t) r

/-!
### `eval` on `.transp` — four disjoint cases

Replaces the earlier coarse `eval_transp` axiom.  Match-arm priority is:
  1. `.top` face                       → identity (T1 at eval level).
  2. Constant line                     → identity (T2 at eval level).
  3. `.path A₀ a b` line, non-constant → `vPathTransp` closure.
  4. Non-path, non-constant line       → delegate to value-level `vTransp`.
The four cases are mutually exclusive by precondition, so the axiom set
is consistent. -/

/-- (1) T1 at eval level: transport under a full face is identity. -/
axiom eval_transp_top (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) :
    eval env (.transp i A .top t) = eval env t

/-- (2) T2 at eval level: transport along a constant line is identity.
    Covers `.univ`, constant-`pi`, and constant-`path` lines uniformly. -/
axiom eval_transp_const (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i A = true) :
    eval env (.transp i A φ t) = eval env t

/-- (3) Path transport: when the line's body is `.path A₀ a b` with the
    whole path-line genuinely varying, produce a `vPathTransp` closure
    that captures the endpoint CTerms `a`/`b` along with the env and the
    path term `t` (kept as a CTerm so later `.papp t r` constructions
    work for the multi-clause reduction at generic dim).  Reduces
    further under `vPApp` at endpoints. -/
axiom eval_transp_path (env : CEnv) (i : DimVar) (A₀ : CType)
    (a b : CTerm) (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i (.path A₀ a b) = false) :
    eval env (.transp i (.path A₀ a b) φ t) =
    .vPathTransp env i A₀ a b φ t

/-- (4) Non-path non-glue non-constant transport: delegate to the value-level
    `vTransp`, which is env-agnostic and handles `.pi` via `vTranspFun`.
    `.glue` is excluded because its CCHM transport formula lives in dedicated
    Glue-specific axioms (see `Glue.lean`); routing it through `vTransp`
    here would claim it reduces to a stuck neutral, which would contradict
    those axioms in their specific sub-cases. -/
axiom eval_transp_nonpath (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i A = false)
    (h_not_path : ∀ A₀ a b, A ≠ .path A₀ a b)
    (h_not_glue : ∀ φG T f fInv sec ret coh Ai,
        A ≠ .glue φG T f fInv sec ret coh Ai) :
    eval env (.transp i A φ t) = vTransp i A φ (eval env t)

/-- Π-case theorem (full CCHM): transport along any `pi domA codA` line
    produces a `vTranspFun` closure.  Derived via `eval_transp_nonpath`
    (`pi ≠ path` and `pi ≠ glue` by constructor disjointness) plus
    `vTransp_pi`. -/
theorem eval_transp_pi (env : CEnv) (i : DimVar)
    (domA codA : CType) (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i (.pi domA codA) = false) :
    eval env (.transp i (.pi domA codA) φ t) =
    .vTranspFun i domA codA φ (eval env t) := by
  rw [eval_transp_nonpath env i _ φ t hφ hA
        (by intro _ _ _ h; nomatch h)
        (by intro _ _ _ _ _ _ _ _ h; nomatch h)]
  exact vTransp_pi _ _ _ _ _ hφ hA

/-- Stuck fallback theorem.  In our current `CType` universe
    `{univ, pi, path, glue}`, this never actually fires in practice: `univ`
    always has `dimAbsent = true`, so the const case wins; `pi` is handled
    by `eval_transp_pi`; `path` is handled by `eval_transp_path`; `glue` is
    handled by the dedicated Glue-transport axioms in `Glue.lean`.  Kept
    here for parity with `vTransp_stuck` and future CType extensions. -/
theorem eval_transp_stuck (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (t : CTerm)
    (hφ : φ ≠ .top)
    (hA : CType.dimAbsent i A = false)
    (h_not_pi : ∀ domA codA, A ≠ .pi domA codA)
    (h_not_path : ∀ A₀ a b, A ≠ .path A₀ a b)
    (h_not_glue : ∀ φG T f fInv sec ret coh Ai,
        A ≠ .glue φG T f fInv sec ret coh Ai) :
    eval env (.transp i A φ t) =
    .vneu (.ntransp i A φ (eval env t)) := by
  rw [eval_transp_nonpath env i A φ t hφ hA h_not_path h_not_glue]
  exact vTransp_stuck _ _ _ _ hφ hA h_not_pi

/-- **T5 at eval level**: face-formula congruence for transport.  When
    two face formulas are semantically equal — i.e. `φ.eval env =
    ψ.eval env` for every env — transport under them computes the same
    result.

    This is a claim about Rust's evaluator: it inspects face formulas
    only through their truth-value semantics, not their syntactic form.
    Two faces that classify the same set of environments produce the
    same transport reduction, regardless of their concrete tree
    structure (e.g. `(i=0) ∧ ⊤` vs `(i=0)`).

    Stated at the eval level (rather than augmenting the partial def
    with a face-normalisation prepass) so the existing eval-axiom set is
    not re-audited.  The Rust backend's discharge: a face-normalisation
    routine ensures syntactically distinct but semantically equal faces
    take the same dispatch branch. -/
axiom eval_transp_face_congr (env : CEnv) (i : DimVar) (A : CType)
    (φ ψ : FaceFormula) (t : CTerm)
    (h : ∀ ε, φ.eval ε = ψ.eval ε) :
    eval env (.transp i A φ t) = eval env (.transp i A ψ t)

/-!
### `eval` on `.comp` — four disjoint cases

The old coarse `eval_comp` (which asserted the stuck form unconditionally)
is replaced by four case-axioms mirroring the arms of `vCompAtTerm`.  The
cases are disjoint by precondition, so the axiom set is consistent.
-/

/-- **C1 at eval level**: with a full face, heterogeneous composition
    reduces to the system body substituted at `i := 1`.  Crucially this
    is *term-level* substitution, not `vPApp` on the evaluated body —
    `u` may be e.g. a free variable whose value doesn't look like a
    function. -/
axiom eval_comp_top (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    eval env (.comp i A .top u t) = eval env (u.substDim i .one)

/-- **C2 at eval level**: with an empty face, the system contributes
    nothing and composition reduces to plain transport. -/
axiom eval_comp_bot (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
    eval env (.comp i A .bot u t) = eval env (.transp i A .bot t)

/-- **Constant-line comp = hcomp**: when the type `A` doesn't vary along
    `i`, heterogeneous composition reduces to homogeneous composition on
    the (fixed) type `A`.  The tube is `.plam i u` — the system body `u`
    packaged as a dim-closure over the line binder. -/
axiom eval_comp_const (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (u t : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (hA : CType.dimAbsent i A = true) :
    eval env (.comp i A φ u t) =
    vHCompValue A φ (eval env (.plam i u)) (eval env t)

/-- **Heterogeneous Π comp**: when A is a pi type with a genuinely-varying
    line, `vCompAtTerm` packages the comp into a `vCompFun` closure that
    will run the CCHM β-rule when the function is applied. -/
axiom eval_comp_pi (env : CEnv) (i : DimVar) (domA codA : CType)
    (φ : FaceFormula) (u t : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (hA : CType.dimAbsent i (.pi domA codA) = false) :
    eval env (.comp i (.pi domA codA) φ u t) =
    .vCompFun env i domA codA φ u t

/-- Stuck fallback: `.comp` whose face is neither `.top` nor `.bot`, whose
    line genuinely varies, and whose type is neither `.pi` nor a constant
    produces a neutral. -/
axiom eval_comp_stuck (env : CEnv) (i : DimVar) (A : CType)
    (φ : FaceFormula) (u t : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (hA : CType.dimAbsent i A = false)
    (h_not_pi : ∀ domA codA, A ≠ .pi domA codA) :
    eval env (.comp i A φ u t) =
    .vneu (.ncomp i A φ (eval env u) (eval env t))

/-- `eval` on `.compN` delegates to `vCompNAtTerm`. -/
axiom eval_compN (env : CEnv) (i : DimVar) (A : CType)
    (clauses : List (FaceFormula × CTerm)) (t : CTerm) :
    eval env (.compN i A clauses t) = vCompNAtTerm env i A clauses t

/-!
### `vHCompValue` — three disjoint cases
-/

/-- Homogeneous composition under a full face: the tube covers everything,
    and the result is the tube evaluated at `1`. -/
axiom vHCompValue_top (A : CType) (tube base : CVal) :
    vHCompValue A .top tube base = vPApp tube .one

/-- **CCHM Π hcomp rule**: homogeneous composition on a Π type produces
    a `vHCompFun` closure that applies pointwise when its function is
    applied to an argument.  `domA` is stored in the type but unused in
    the resulting closure because hcomp on the domain is trivial (A is
    fixed, not varying). -/
axiom vHCompValue_pi (domA codA : CType) (φ : FaceFormula) (tube base : CVal)
    (hφ : φ ≠ .top) :
    vHCompValue (.pi domA codA) φ tube base = .vHCompFun codA φ tube base

/-- Stuck fallback: hcomp on a non-pi type under a non-top face.  Uses
    `nhcomp` (separate from `ncomp` because hcomp's type is fixed). -/
axiom vHCompValue_stuck (A : CType) (φ : FaceFormula) (tube base : CVal)
    (hφ : φ ≠ .top)
    (h_not_pi : ∀ domA codA, A ≠ .pi domA codA) :
    vHCompValue A φ tube base = .vneu (.nhcomp A φ tube base)

-- Reduction lemmas for `vApp`.

axiom vApp_vlam (env : CEnv) (x : String) (body : CTerm) (arg : CVal) :
    vApp (.vlam env x body) arg = eval (env.extend x arg) body

axiom vApp_vneu (n : CNeu) (arg : CVal) :
    vApp (.vneu n) arg = .vneu (.napp n arg)

/-- Full CCHM Π β-rule at the value level: applying a transported-function
    closure to an argument `arg` inversely transports `arg` through the
    domain, applies the underlying function `f`, and forward-transports the
    result through the codomain.

    When `CType.dimAbsent i domA = true`, `vTranspInv` reduces to identity
    (by `vTranspInv_const`) and this specialises to the simpler
    const-domain rule `vTransp i codA φ (vApp f arg)`. -/
axiom vApp_vTranspFun (i : DimVar) (domA codA : CType) (φ : FaceFormula)
    (f : CVal) (arg : CVal) :
    vApp (.vTranspFun i domA codA φ f) arg =
    vTransp i codA φ (vApp f (vTranspInv i domA φ arg))

/-- **CCHM Π hcomp β-rule** at the value level: applying a homogeneously
    composed function closure to `arg` yields hcomp on the codomain with:
      · tube  = `λj. (tube @ j) arg` (represented by `vTubeApp`),
      · base  = `base arg`.
    No inverse transport — hcomp's type is fixed, so the argument passes
    through unchanged. -/
axiom vApp_vHCompFun (codA : CType) (φ : FaceFormula) (tube base arg : CVal) :
    vApp (.vHCompFun codA φ tube base) arg =
    vHCompValue codA φ (.vTubeApp tube arg) (vApp base arg)

/-- **Full CCHM Π hetero comp β-rule**: applying `comp^i (pi A B) φ u u₀` to
    `y : A(1)` unfolds via the *fill* construction.  For a fresh dim `$fj`
    and argument name `$y`:
      · `y_at_i = transp^{$fj} (A[i := inv $fj ∨ i]) φ y`  —  fill from A(1) down to A(i).
      · `y_at_0 = transp^{$fj} (A[i := inv $fj]) φ y`      —  reversed-line transport A(1) → A(0).
    The result is `comp^i B(i) φ (u (y_at_i)) (u₀ (y_at_0))` evaluated in
    an env extending `$y` with the argument.

    When `CType.dimAbsent i domA = true`, both fills degenerate to `y`
    (by T2 on the constant line), recovering the simpler const-domain
    formula `comp^i B(i) φ (u y) (u₀ y)`.

    Hygiene assumption: `$y` is not a user variable in `env`, and `$fj`
    is not a user DimVar in `domA`, `codA`, `φ`, `u`, `t`.  These reserved
    names are chosen to minimise collision probability. -/
axiom vApp_vCompFun (env : CEnv) (i : DimVar) (domA codA : CType)
    (φ : FaceFormula) (u t : CTerm) (arg : CVal) :
    vApp (.vCompFun env i domA codA φ u t) arg =
    eval (env.extend "$y" arg) (.comp i codA φ
      (.app u (.transp ⟨"$fj"⟩
                 (domA.substDimExpr i (.join (.inv (.var ⟨"$fj"⟩)) (.var i)))
                 φ (.var "$y")))
      (.app t (.transp ⟨"$fj"⟩
                 (domA.substDimExpr i (.inv (.var ⟨"$fj"⟩)))
                 φ (.var "$y"))))

-- Reduction lemmas for `vPApp`.

axiom vPApp_vplam (env : CEnv) (i : DimVar) (body : CTerm) (r : DimExpr) :
    vPApp (.vplam env i body) r = eval env (body.substDim i r)

axiom vPApp_vneu (n : CNeu) (r : DimExpr) :
    vPApp (.vneu n) r = .vneu (.npapp n r)

/-- `vTubeApp tube arg` under dim application reduces to `(tube @ r) arg`.
    Encodes the semantic meaning of `λj. (tube @ j) arg`. -/
axiom vPApp_vTubeApp (tube arg : CVal) (r : DimExpr) :
    vPApp (.vTubeApp tube arg) r = vApp (vPApp tube r) arg

/-!
### `vCompNAtTerm` — compound equation mirroring the partial-def arms

Single axiom exposing the full case analysis so that derived theorems can
pattern-match on the clause list's structure. -/

axiom vCompNAtTerm_def (env : CEnv) (i : DimVar) (A : CType)
    (clauses : List (FaceFormula × CTerm)) (t : CTerm) :
    vCompNAtTerm env i A clauses t =
      match clauses.find?
        (fun ⟨φ, _⟩ => match φ with | .top => true | _ => false) with
      | some ⟨_, u⟩ => eval env (u.substDim i .one)
      | none =>
        let live := clauses.filter
          (fun ⟨φ, _⟩ => match φ with | .bot => false | _ => true)
        match live with
        | []        => eval env (.transp i A .bot t)
        | [⟨φ, u⟩] => vCompAtTerm env i A φ u t
        | _         => .vneu (.ncompN env i A
                          (live.map (fun ⟨φ, u⟩ => (φ, eval env u)))
                          (eval env t))

/-!
### Path transport endpoint reductions

Applied at `.zero`, the CCHM `(j=0)` clause fires, giving `a(1)`.
Applied at `.one`, the `(j=1)` clause fires, giving `b(1)`.
Applied at any other DimExpr, the multi-clause comp can't be computed
without machinery we haven't built yet — stalls at `npathTranspApp`.
The three axioms are disjoint by the shape of the DimExpr argument.
-/

/-- Path transport at left endpoint: result is `a(1)`, i.e. `a` evaluated
    with `i` substituted by `.one`.  This is *not* a transport of `a(0)` —
    it's the line's specified endpoint at `i=1`, made forced by CCHM's
    multi-clause `(j=0)` constraint. -/
axiom vPApp_vPathTransp_zero
    (env : CEnv) (i : DimVar) (A : CType) (a b : CTerm) (φ : FaceFormula)
    (p : CTerm) :
    vPApp (.vPathTransp env i A a b φ p) .zero =
    eval env (a.substDim i .one)

/-- Path transport at right endpoint: result is `b(1)`. -/
axiom vPApp_vPathTransp_one
    (env : CEnv) (i : DimVar) (A : CType) (a b : CTerm) (φ : FaceFormula)
    (p : CTerm) :
    vPApp (.vPathTransp env i A a b φ p) .one =
    eval env (b.substDim i .one)

/-- **Full CCHM path transport at a generic dim**: apply the path
    transport at `r` by evaluating the CCHM multi-clause comp
    `comp^i A [φ ↦ p@r, (r=0) ↦ a, (r=1) ↦ b] (p@r)` via `vCompNAtTerm`.
    This genuinely unsticks when `r`'s face substitution simplifies:
      · `r = .zero` → `(r=0)` becomes `.top`, firing the left clause → `a(1)`.
      · `r = .one`  → `(r=1)` becomes `.top`, firing the right clause → `b(1)`.
      · `r = .var k` generic → both clauses are non-trivial; stalls at a
        structured `ncompN` neutral that can still unstick if `k` later
        becomes an endpoint. -/
axiom vPApp_vPathTransp_general
    (env : CEnv) (i : DimVar) (A : CType) (a b : CTerm) (φ : FaceFormula)
    (p : CTerm) (r : DimExpr)
    (h_zero : r ≠ .zero) (h_one : r ≠ .one) :
    vPApp (.vPathTransp env i A a b φ p) r =
    vCompNAtTerm env i A
      [ (φ,                       .papp p r)
      , (FaceFormula.dimExprEq0 r, a)
      , (FaceFormula.dimExprEq1 r, b) ]
      (.papp p r)

/-!
### `eval` on `.glueIn` — three disjoint cases

`glueIn [φ ↦ t] a` evaluates differently on/off/between the face `φ`:
  · `φ = .top`: the face is full, the result is `t` (only the T-side
    matters).
  · `φ = .bot`: the face is empty, the result is `a` (only the A-side
    matters).
  · Otherwise: a structurally stuck `nglueIn` neutral preserving both
    face-on and face-off values — later dim substitution into `φ` may
    collapse it.

The three cases are mutually exclusive by precondition. -/

/-- (1) Full-face glueIn reduces to the T-side. -/
axiom eval_glueIn_top (env : CEnv) (t a : CTerm) :
    eval env (.glueIn .top t a) = eval env t

/-- (2) Empty-face glueIn reduces to the A-side. -/
axiom eval_glueIn_bot (env : CEnv) (t a : CTerm) :
    eval env (.glueIn .bot t a) = eval env a

/-- (3) Neutral-face glueIn produces an `nglueIn` stuck neutral preserving
    both evaluated sides.  The face formula is kept syntactic so that
    later dim substitution can resolve it to `.top` or `.bot`.

    The `h_not_unglue` precondition rules out the η-redex shape
    `.glueIn φ t (.unglue φ f g)`, which reduces via
    `eval_glueIn_of_unglue` to `eval env g` instead of a stuck form.
    Without this restriction, the stuck rule and the η-rule would
    disagree on a common instance. -/
axiom eval_glueIn_stuck (env : CEnv) (φ : FaceFormula) (t a : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (h_not_unglue : ∀ f g, a ≠ .unglue φ f g) :
    eval env (.glueIn φ t a) = .vneu (.nglueIn φ (eval env t) (eval env a))

/-!
### `eval` on `.unglue` — three disjoint cases

`unglue [φ ↦ f] g` — extracting an A-value from a glued term:
  · `φ = .top`: apply the forward map: `vApp (eval f) (eval g)`.
  · `φ = .bot`: identity.  `glueIn .bot t a` reduces to `a`, so the
    argument is already an A-value; unglue is the identity there.
  · Otherwise: stuck `nunglue` preserving `f` and `g`.

All three cases are mutually exclusive. -/

/-- (1) Full-face unglue: apply the forward map pointwise. -/
axiom eval_unglue_top (env : CEnv) (f g : CTerm) :
    eval env (.unglue .top f g) = vApp (eval env f) (eval env g)

/-- (2) Empty-face unglue: identity on `g`.  This is the definitional
    content of `Glue [bot ↦ (T, e)] A = A`: values are already A-values. -/
axiom eval_unglue_bot (env : CEnv) (f g : CTerm) :
    eval env (.unglue .bot f g) = eval env g

/-- (3) Neutral-face unglue: produce a stuck `nunglue` neutral preserving
    `f` and `g`.  Later dim substitution into `φ` may resolve it to
    `.top` (→ forward-map application) or `.bot` (→ identity).

    The `h_not_glueIn` precondition rules out the β-redex shape
    `.unglue φ f (.glueIn φ t a)`, which reduces via
    `eval_unglue_of_glueIn` to `eval env a` under the overlap
    condition.  Without this restriction, the stuck rule and the
    β-rule would disagree on a common instance. -/
axiom eval_unglue_stuck (env : CEnv) (φ : FaceFormula) (f g : CTerm)
    (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot)
    (h_not_glueIn : ∀ t a, g ≠ .glueIn φ t a) :
    eval env (.unglue φ f g) = .vneu (.nunglue φ (eval env f) (eval env g))

/-!
### Glue β- and η-rules (eval level)

The β-rule (`unglue · glueIn`) and η-rule (`glueIn · unglue`) on
matching face formulas fire *regardless* of whether `φ` is `.top`,
`.bot`, or stuck.  On `.top` / `.bot` the existing face-dispatched
axioms reduce to the same result under the overlap condition
(consistency check below); on stuck faces, these rules are the only
way the redex reduces — `eval_unglue_stuck` and `eval_glueIn_stuck`
carry `h_not_glueIn` / `h_not_unglue` preconditions to avoid conflict.

The `h_overlap` condition encodes the CCHM typing-side constraint
`e.f t = a` (or `t = e.f g`) that accompanies a well-typed glueIn /
unglue — the evaluator assumes it and short-circuits.
-/

/-- β-rule: `unglue φ f (glueIn φ t a)` reduces to `a` under the
    overlap condition.  Rust-discharge: the evaluator recognises the
    nested pattern and short-circuits when the overlap invariant holds
    (typing guarantees it). -/
axiom eval_unglue_of_glueIn (env : CEnv) (φ : FaceFormula) (f t a : CTerm)
    (h_overlap : eval env (.app f t) = eval env a) :
    eval env (.unglue φ f (.glueIn φ t a)) = eval env a

/-- η-rule: `glueIn φ t (unglue φ f g)` reduces to `g` under the
    overlap condition.  Rust-discharge: dual to `eval_unglue_of_glueIn`. -/
axiom eval_glueIn_of_unglue (env : CEnv) (φ : FaceFormula) (f t g : CTerm)
    (h_overlap : eval env t = eval env (.app f g)) :
    eval env (.glueIn φ t (.unglue φ f g)) = eval env g

/-!
### `eval` on Σ constructors — three arms

`.pair a b` evaluates component-wise to `.vpair`; `.fst t` / `.snd t`
project through `vFst` / `vSnd`, which themselves β-reduce on `vpair`
and produce stuck `.nfst` / `.nsnd` on neutrals.
-/

/-- Pair construction evaluates component-wise. -/
axiom eval_pair (env : CEnv) (a b : CTerm) :
    eval env (.pair a b) = .vpair (eval env a) (eval env b)

/-- First projection delegates to `vFst`. -/
axiom eval_fst (env : CEnv) (t : CTerm) :
    eval env (.fst t) = vFst (eval env t)

/-- Second projection delegates to `vSnd`. -/
axiom eval_snd (env : CEnv) (t : CTerm) :
    eval env (.snd t) = vSnd (eval env t)

/-- β-rule for `vFst` on a pair. -/
axiom vFst_vpair (a b : CVal) : vFst (.vpair a b) = a

/-- β-rule for `vSnd` on a pair. -/
axiom vSnd_vpair (a b : CVal) : vSnd (.vpair a b) = b

/-- `vFst` on a neutral produces a stuck `nfst` neutral. -/
axiom vFst_vneu (n : CNeu) : vFst (.vneu n) = .vneu (.nfst n)

/-- `vSnd` on a neutral produces a stuck `nsnd` neutral. -/
axiom vSnd_vneu (n : CNeu) : vSnd (.vneu n) = .vneu (.nsnd n)