module Quox.Reduce

import Quox.No
import Quox.Syntax
import Quox.Definition
import Quox.Typing.Context
import Quox.Typing.Error
import Data.SnocVect
import Data.Maybe
import Data.List

%default total


public export
0 RedexTest : TermLike -> Type
RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool

public export
interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
  whnf : {d, n : Nat} -> (defs : Definitions) ->
         (ctx : WhnfContext d n) ->
         tm d n -> Either Error (Subset (tm d n) (No . isRedex defs))

public export %inline
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
        (defs : Definitions) ->
        WhnfContext d n -> tm d n -> Either Error (tm d n)
whnf0 defs ctx t = fst <$> whnf defs ctx t

public export
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
                      Definitions -> Pred (tm d n)
IsRedex  defs = So . isRedex defs
NotRedex defs = No . isRedex defs

public export
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
             Whnf tm isRedex => (d, n : Nat) ->
             (defs : Definitions) -> Type
NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)

public export %inline
nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
       (t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
nred t = Element t nr


public export %inline
isLamHead : Elim {} -> Bool
isLamHead (Lam {} :# Pi {}) = True
isLamHead (Coe {})          = True
isLamHead _                 = False

public export %inline
isDLamHead : Elim {} -> Bool
isDLamHead (DLam {} :# Eq {}) = True
isDLamHead (Coe {})           = True
isDLamHead _                  = False

public export %inline
isPairHead : Elim {} -> Bool
isPairHead (Pair {} :# Sig {}) = True
isPairHead (Coe {})            = True
isPairHead _                   = False

public export %inline
isTagHead : Elim {} -> Bool
isTagHead (Tag t :# Enum _) = True
isTagHead (Coe {})          = True
isTagHead _ = False

public export %inline
isNatHead : Elim {} -> Bool
isNatHead (Zero   :# Nat) = True
isNatHead (Succ n :# Nat) = True
isNatHead (Coe {})        = True
isNatHead _ = False

public export %inline
isBoxHead : Elim {} -> Bool
isBoxHead (Box {} :# BOX {}) = True
isBoxHead (Coe {})           = True
isBoxHead _ = False

public export %inline
isE : Term {} -> Bool
isE (E _) = True
isE _     = False

public export %inline
isAnn : Elim {} -> Bool
isAnn (_ :# _) = True
isAnn _        = False

||| true if a term is syntactically a type.
public export %inline
isTyCon : Term {} -> Bool
isTyCon (TYPE     {}) = True
isTyCon (Pi       {}) = True
isTyCon (Lam      {}) = False
isTyCon (Sig      {}) = True
isTyCon (Pair     {}) = False
isTyCon (Enum     {}) = True
isTyCon (Tag      {}) = False
isTyCon (Eq       {}) = True
isTyCon (DLam     {}) = False
isTyCon Nat           = True
isTyCon Zero          = False
isTyCon (Succ     {}) = False
isTyCon (BOX      {}) = True
isTyCon (Box      {}) = False
isTyCon (E        {}) = False
isTyCon (CloT     {}) = False
isTyCon (DCloT    {}) = False

||| true if a term is syntactically a type, or a neutral.
public export %inline
isTyConE : Term {} -> Bool
isTyConE s = isTyCon s || isE s

||| true if a term is syntactically a type.
public export %inline
isAnnTyCon : Elim {} -> Bool
isAnnTyCon (ty :# TYPE _) = isTyCon ty
isAnnTyCon _              = False

public export %inline
isK : Dim d -> Bool
isK (K _) = True
isK _     = False


mutual
  public export
  isRedexE : RedexTest Elim
  isRedexE defs (F x) {d, n} =
    isJust $ lookupElim x defs {d, n}
  isRedexE _ (B _) = False
  isRedexE defs (f :@ _) =
    isRedexE defs f || isLamHead f
  isRedexE defs (CasePair {pair, _}) =
    isRedexE defs pair || isPairHead pair
  isRedexE defs (CaseEnum {tag, _}) =
    isRedexE defs tag || isTagHead tag
  isRedexE defs (CaseNat {nat, _}) =
    isRedexE defs nat || isNatHead nat
  isRedexE defs (CaseBox {box, _}) =
    isRedexE defs box || isBoxHead box
  isRedexE defs (f :% p) =
    isRedexE defs f || isDLamHead f || isK p
  isRedexE defs (t :# a) =
    isE t || isRedexT defs t || isRedexT defs a
  isRedexE defs (Coe {val, _}) =
    isRedexT defs val || not (isE val)
  isRedexE defs (Comp {ty, r, _}) =
    isRedexT defs ty || isK r
  isRedexE defs (TypeCase {ty, ret, _}) =
    isRedexE defs ty || isRedexT defs ret || isAnnTyCon ty
  isRedexE _ (CloE  {}) = True
  isRedexE _ (DCloE {}) = True

  public export
  isRedexT : RedexTest Term
  isRedexT _    (CloT  {}) = True
  isRedexT _    (DCloT {}) = True
  isRedexT defs (E e)      = isAnn e || isRedexE defs e
  isRedexT _    _          = False


public export
tycaseRhs : (k : TyConKind) -> TypeCaseArms d n ->
            Maybe (ScopeTermN (arity k) d n)
tycaseRhs k arms = lookupPrecise k arms

public export
tycaseRhsDef : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
               ScopeTermN (arity k) d n
tycaseRhsDef def k arms = fromMaybe (SN def) $ tycaseRhs k arms

public export
tycaseRhs0 : (k : TyConKind) -> TypeCaseArms d n ->
             (0 eq : arity k = 0) => Maybe (Term d n)
tycaseRhs0 k arms {eq} with (tycaseRhs k arms) | (arity k)
  tycaseRhs0 k arms {eq = Refl} | res | 0 = map (.term) res

public export
tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
                (0 eq : arity k = 0) => Term d n
tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms



private
weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
weakDS by (S names (Y body)) = S names $ Y $ weakT by body
weakDS by (S names (N body)) = S names $ N $ weakT by body

private
dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n
dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
dweakS by (S names (N body)) = S names $ N $ dweakT by body

private
coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d ->
            ScopeTermN s d n -> ScopeTermN s d n
coeScoped ty p q (S names (Y body)) =
  S names $ Y $ E $ Coe (weakDS s ty) p q body
coeScoped ty p q (S names (N body)) =
  S names $ N $ E $ Coe ty p q body


mutual
  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
    ||| performs the minimum work required to recompute the type of an elim.
    |||
    ||| ⚠ **assumes the elim is already typechecked.** ⚠
    export covering
    computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
                      Either Error (Term d n)
    computeElimType (F x) = do
      let Just def = lookup x defs | Nothing => Left $ NotInScope x
      pure $ def.type
    computeElimType (B i) = pure $ ctx.tctx !! i
    computeElimType (f :@ s) {ne} = do
      -- can't use `expectPi` (or `expectEq` below) without making this
      -- mutual block from hell even worse lol
      Pi {arg, res, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
        | t => Left $ ExpectedPi ctx.names t
      pure $ sub1 res (s :# arg)
    computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
    computeElimType (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag
    computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
    computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
    computeElimType (f :% p) {ne} = do
      Eq {ty, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
        | t => Left $ ExpectedEq ctx.names t
      pure $ dsub1 ty p
    computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q
    computeElimType (Comp {ty, _}) = pure ty
    computeElimType (TypeCase {ret, _}) = pure ret
    computeElimType (_ :# ty) = pure ty

  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
    ||| for π.(x : A) → B, returns (A, B);
    ||| for an elim returns a pair of type-cases that will reduce to that;
    ||| for other intro forms error
    private covering
    tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
               Either Error (Term (S d) n, ScopeTerm (S d) n)
    tycasePi (Pi {arg, res, _}) = pure (arg, res)
    tycasePi (E e) {tnf} = do
      ty <- computeElimType defs ctx e @{noOr2 tnf}
      let arg  = E $ typeCase1Y e ty KPi [< "Arg", "Ret"] (BVT 1)
          res' = typeCase1Y e (Arr Zero arg ty) KPi [< "Arg", "Ret"] (BVT 0)
          res  = SY [< "Arg"] $ E $ weakE 1 res' :@ BVT 0
      pure (arg, res)
    tycasePi t = Left $ ExpectedPi ctx.names t

    ||| for (x : A) × B, returns (A, B);
    ||| for an elim returns a pair of type-cases that will reduce to that;
    ||| for other intro forms error
    private covering
    tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
                Either Error (Term (S d) n, ScopeTerm (S d) n)
    tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
    tycaseSig (E e) {tnf} = do
      ty <- computeElimType defs ctx e @{noOr2 tnf}
      let fst  = E $ typeCase1Y e ty KSig [< "Fst", "Snd"] (BVT 1)
          snd' = typeCase1Y e (Arr Zero fst ty) KSig [< "Fst", "Snd"] (BVT 0)
          snd  = SY [< "Fst"] $ E $ weakE 1 snd' :@ BVT 0
      pure (fst, snd)
    tycaseSig t = Left $ ExpectedSig ctx.names t

    ||| for [π. A], returns A;
    ||| for an elim returns a type-case that will reduce to that;
    ||| for other intro forms error
    private covering
    tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
                Either Error (Term (S d) n)
    tycaseBOX (BOX _ a) = pure a
    tycaseBOX (E e) {tnf} = do
      ty <- computeElimType defs ctx e @{noOr2 tnf}
      pure $ E $ typeCase1Y e ty KBOX [< "Ty"] (BVT 0)
    tycaseBOX t = Left $ ExpectedBOX ctx.names t

    ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r);
    ||| for an elim returns five type-cases that will reduce to that;
    ||| for other intro forms error
    private covering
    tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
               Either Error (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
                             Term (S d) n, Term (S d) n)
    tycaseEq (Eq {ty, l, r}) = pure (ty.zero, ty.one, ty, l, r)
    tycaseEq (E e) {tnf} = do
      ty <- computeElimType defs ctx e @{noOr2 tnf}
      let names = [< "A0", "A1", "A", "L", "R"]
          a0 = E $ typeCase1Y e ty KEq names (BVT 4)
          a1 = E $ typeCase1Y e ty KEq names (BVT 3)
          a' = typeCase1Y e (Eq0 ty a0 a1) KEq names (BVT 2)
          a  = SY [< "i"] $ E $ dweakE 1 a' :% BV 0
          l  = E $ typeCase1Y e a0 KEq names (BVT 1)
          r  = E $ typeCase1Y e a1 KEq names (BVT 0)
      pure (a0, a1, a, l, r)
    tycaseEq t = Left $ ExpectedEq ctx.names t

  -- new block because the functions below might pass a different ctx
  -- into the ones above
  parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
    ||| reduce a function application `Coe ty p q val :@ s`
    private covering
    piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val, s : Term d n) ->
            Either Error (Subset (Elim d n) (No . isRedexE defs))
    piCoe sty@(S [< i] ty) p q val s = do
      -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
      -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
      --   where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s
      --
      -- type-case is used to expose A,B if the type is neutral
      let ctx1 = extendDim i ctx
      Element ty tynf <- whnf defs ctx1 ty.term
      (arg, res) <- tycasePi defs ctx1 ty
      let s0   = CoeT i arg q p s
          body = E $ (val :# (ty // one p)) :@ E s0
          s1   = CoeT i (arg // (BV 0 ::: shift 2)) (weakD 1 q) (BV 0)
                      (s // shift 1)
      whnf defs ctx $ CoeT i (sub1 res s1) p q body

    ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body`
    private covering
    sigCoe : (qty : Qty) ->
             (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
             (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) ->
             Either Error (Subset (Elim d n) (No . isRedexE defs))
    sigCoe qty sty@(S [< i] ty) p q val ret body = do
      -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
      -- ⇝
      -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
      -- of { (a, b) ⇒
      --   e[(coe [i ⇒ A] @p @q a)/a,
      --     (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] }
      --
      -- type-case is used to expose A,B if the type is neutral
      let ctx1 = extendDim i ctx
      Element ty tynf <- whnf defs ctx1 ty.term
      (tfst, tsnd) <- tycaseSig defs ctx1 ty
      let a' = CoeT i (weakT 2 tfst) p q (BVT 1)
          tsnd' = tsnd.term //
            (CoeT i (weakT 2 $ tfst // (BV 0 ::: shift 2))
              (weakD 1 p) (BV 0) (BVT 1) ::: shift 2)
          b' = CoeT i tsnd' p q (BVT 0)
      whnf defs ctx $ CasePair qty (val :# (ty // one p)) ret $
        ST body.names $ body.term // (a' ::: b' ::: shift 2)

    ||| reduce a dimension application `Coe ty p q val :% r`
    private covering
    eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
            (r : Dim d) ->
            Either Error (Subset (Elim d n) (No . isRedexE defs))
    eqCoe sty@(S [< j] ty) p q val r = do
      -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
      -- ⇝
      -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
      --   { (r=0) j ⇒ L; (r=1) j ⇒ R }
      let ctx1 = extendDim j ctx
      Element ty tynf <- whnf defs ctx1 ty.term
      (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
      let a'   = dsub1 a (weakD 1 r)
          val' = E $ (val :# (ty // one p)) :% r
      whnf defs ctx $ CompH j a' p q val' r j s j t

    ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
    private covering
    boxCoe : (qty : Qty) ->
             (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
             (ret : ScopeTerm d n) -> (body : ScopeTerm d n) ->
             Either Error (Subset (Elim d n) (No . isRedexE defs))
    boxCoe qty sty@(S [< i] ty) p q val ret body = do
      -- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
      -- ⇝
      -- caseπ s ∷ [ρ. A]‹p/i› return z ⇒ C
      -- of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
      let ctx1 = extendDim i ctx
      Element ty tynf <- whnf defs ctx1 ty.term
      ta <- tycaseBOX defs ctx1 ty
      let a' = CoeT i (weakT 1 ta) p q $ BVT 0
      whnf defs ctx $ CaseBox qty (val :# (ty // one p)) ret $
        ST body.names $ body.term // (a' ::: shift 1)


  export covering
  Whnf Elim Reduce.isRedexE where
    whnf defs ctx (F x) with (lookupElim x defs) proof eq
      _ | Just y  = whnf defs ctx y
      _ | Nothing = pure $ Element (F x) $ rewrite eq in Ah

    whnf _ _ (B i) = pure $ nred $ B i

    -- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
    whnf defs ctx (f :@ s) = do
      Element f fnf <- whnf defs ctx f
      case nchoose $ isLamHead f of
        Left _ => case f of
          Lam body :# Pi {arg, res, _} =>
            let s = s :# arg in
            whnf defs ctx $ sub1 body s :# sub1 res s
          Coe ty p q val => piCoe defs ctx ty p q val s
        Right nlh => pure $ Element (f :@ s) $ fnf `orNo` nlh

    -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
    -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
    whnf defs ctx (CasePair pi pair ret body) = do
      Element pair pairnf <- whnf defs ctx pair
      case nchoose $ isPairHead pair of
        Left _ => case pair of
          Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} =>
            let fst = fst :# tfst
                snd = snd :# sub1 tsnd fst
            in
            whnf defs ctx $ subN body [< fst, snd] :# sub1 ret pair
          Coe ty p q val => do
            sigCoe defs ctx pi ty p q val ret body
        Right np =>
          pure $ Element (CasePair pi pair ret body) $ pairnf `orNo` np

    -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
    -- u ∷ C['a∷{a,…}/p]
    whnf defs ctx (CaseEnum pi tag ret arms) = do
      Element tag tagnf <- whnf defs ctx tag
      case nchoose $ isTagHead tag of
        Left t => case tag of
          Tag t :# Enum ts =>
            let ty = sub1 ret tag in
            case lookup t arms of
              Just arm => whnf defs ctx $ arm :# ty
              Nothing  => Left $ MissingEnumArm t (keys arms)
          Coe ty p q val =>
            -- there is nowhere an equality can be hiding inside an Enum
            whnf defs ctx $ CaseEnum pi (val :# dsub1 ty q) ret arms
        Right nt =>
          pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt

    -- case zero ∷ ℕ return p ⇒ C of { zero ⇒ u; … } ⇝
    --   u ∷ C[zero∷ℕ/p]
    --
    -- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
    --   u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
    whnf defs ctx (CaseNat pi piIH nat ret zer suc) = do
      Element nat natnf <- whnf defs ctx nat
      case nchoose $ isNatHead nat of
        Left _ =>
          let ty = sub1 ret nat in
          case nat of
            Zero :# Nat => whnf defs ctx (zer :# ty)
            Succ n :# Nat =>
              let nn = n :# Nat
                  tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc]
              in
              whnf defs ctx $ tm :# ty
            Coe ty p q val =>
              -- same deal as Enum
              whnf defs ctx $ CaseNat pi piIH (val :# dsub1 ty q) ret zer suc
        Right nn =>
          pure $ Element (CaseNat pi piIH nat ret zer suc) $ natnf `orNo` nn

    -- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
    --   u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
    whnf defs ctx (CaseBox pi box ret body) = do
      Element box boxnf <- whnf defs ctx box
      case nchoose $ isBoxHead box of
        Left _ => case box of
          Box val :# BOX q bty =>
            let ty = sub1 ret box in
            whnf defs ctx $ sub1 body (val :# bty) :# ty
          Coe ty p q val =>
            boxCoe defs ctx pi ty p q val ret body
        Right nb =>
          pure $ Element (CaseBox pi box ret body) $ boxnf `orNo` nb

    -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @0 ⇝ t ∷ A‹0/𝑗›
    -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗›
    -- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
    --   (if 𝑘 is a variable)
    whnf defs ctx (f :% p) = do
      Element f fnf <- whnf defs ctx f
      case nchoose $ isDLamHead f of
        Left _ => case f of
          DLam body :# Eq {ty = ty, l, r, _} =>
            let body = endsOr l r (dsub1 body p) p in
            whnf defs ctx $ body :# dsub1 ty p
          Coe ty p' q' val =>
            eqCoe defs ctx ty p' q' val p
        Right ndlh => case p of
          K e => do
            Eq {l, r, ty, _} <- whnf0 defs ctx =<< computeElimType defs ctx f
              | ty => Left $ ExpectedEq ctx.names ty
            whnf defs ctx $ ends (l :# ty.zero) (r :# ty.one) e
          B _ => pure $ Element (f :% p) $ fnf `orNo` ndlh `orNo` Ah

    -- e ∷ A ⇝ e
    whnf defs ctx (s :# a) = do
      Element s snf <- whnf defs ctx s
      case nchoose $ isE s of
        Left  _  => let E e = s in pure $ Element e $ noOr2 snf
        Right ne => do
          Element a anf <- whnf defs ctx a
          pure $ Element (s :# a) $ ne `orNo` snf `orNo` anf

    whnf defs ctx (Coe (S _ (N ty)) _ _ val) =
      whnf defs ctx $ val :# ty
    whnf defs ctx (Coe (S [< i] ty) p q val) = do
      Element ty  tynf  <- whnf defs (extendDim i ctx) ty.term
      Element val valnf <- whnf defs ctx val
      pushCoe defs ctx i ty p q val

    whnf defs ctx (Comp ty p q val r zero one) =
      -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
      if p == q then whnf defs ctx $ val :# ty else
      case nchoose (isK r) of
        -- comp [A] @p @q s { (0=0) j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
        -- comp [A] @p @q s { (1=1) j ⇒ t; ⋯ } ⇝ t‹q/j› ∷ A
        Left y => case r of
          K Zero => whnf defs ctx $ dsub1 zero q :# ty
          K One  => whnf defs ctx $ dsub1 one  q :# ty
        Right nk => do
          Element ty tynf <- whnf defs ctx ty
          pure $ Element (Comp ty p q val r zero one) $ tynf `orNo` nk
      -- [todo] anything other than just the boundaries??

    whnf defs ctx (TypeCase ty ret arms def) = do
      Element ty  tynf  <- whnf defs ctx ty
      Element ret retnf <- whnf defs ctx ret
      case nchoose $ isAnnTyCon ty of
        Left  y  => let ty :# TYPE u = ty in
                    reduceTypeCase defs ctx ty u ret arms def
        Right nt => pure $ Element (TypeCase ty ret arms def) $
                             tynf `orNo` retnf `orNo` nt

    whnf defs ctx (CloE  el th) = whnf defs ctx $ pushSubstsWith' id th el
    whnf defs ctx (DCloE el th) = whnf defs ctx $ pushSubstsWith' th id el

  export covering
  Whnf Term Reduce.isRedexT where
    whnf _ _ t@(TYPE {}) = pure $ nred t
    whnf _ _ t@(Pi   {}) = pure $ nred t
    whnf _ _ t@(Lam  {}) = pure $ nred t
    whnf _ _ t@(Sig  {}) = pure $ nred t
    whnf _ _ t@(Pair {}) = pure $ nred t
    whnf _ _ t@(Enum {}) = pure $ nred t
    whnf _ _ t@(Tag  {}) = pure $ nred t
    whnf _ _ t@(Eq   {}) = pure $ nred t
    whnf _ _ t@(DLam {}) = pure $ nred t
    whnf _ _    Nat      = pure $ nred Nat
    whnf _ _    Zero     = pure $ nred Zero
    whnf _ _ t@(Succ {}) = pure $ nred t
    whnf _ _ t@(BOX  {}) = pure $ nred t
    whnf _ _ t@(Box  {}) = pure $ nred t

    -- s ∷ A ⇝ s   (in term context)
    whnf defs ctx (E e) = do
      Element e enf <- whnf defs ctx e
      case nchoose $ isAnn e of
        Left  _  => let tm :# _ = e in pure $ Element tm $ noOr1 $ noOr2 enf
        Right na => pure $ Element (E e) $ na `orNo` enf

    whnf defs ctx (CloT  tm th) = whnf defs ctx $ pushSubstsWith' id th tm
    whnf defs ctx (DCloT tm th) = whnf defs ctx $ pushSubstsWith' th id tm

  ||| reduce a type-case applied to a type constructor
  private covering
  reduceTypeCase : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
                   (ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
                   (arms : TypeCaseArms d n) -> (def : Term d n) ->
                   (0 _ : So (isTyCon ty)) =>
                   Either Error (Subset (Elim d n) (No . isRedexE defs))
  reduceTypeCase defs ctx ty u ret arms def = case ty of
    -- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
    TYPE _ =>
      whnf defs ctx $ tycaseRhsDef0 def KTYPE arms :# ret

    -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
    Pi _ arg res =>
      let arg = arg :# TYPE u
          res = Lam res :# Arr Zero (TYPE u) (TYPE u)
      in
      whnf defs ctx $ subN (tycaseRhsDef def KPi arms) [< arg, res] :# ret

    -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
    -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ ★ᵢ
    Sig fst snd =>
      let fst = fst :# TYPE u
          snd = Lam snd :# Arr Zero (TYPE u) (TYPE u)
      in
      whnf defs ctx $ subN (tycaseRhsDef def KSig arms) [< fst, snd] :# ret

    -- (type-case {⋯} ∷ _ return Q of { {} ⇒ s; ⋯ }) ⇝ s ∷ Q
    Enum _ =>
      whnf defs ctx $ tycaseRhsDef0 def KEnum arms :# ret

    -- (type-case Eq [i ⇒ A] L R ∷ ★ᵢ return Q
    --  of { Eq a₀ a₁ a l r ⇒ s; ⋯ }) ⇝
    -- s[(A‹0/i› ∷ ★ᵢ)/a₀, (A‹1/i› ∷ ★ᵢ)/a₁,
    --   ((δ i ⇒ A) ∷ Eq [★ᵢ] A‹0/i› A‹1/i›)/a,
    --   (L ∷ A‹0/i›)/l, (R ∷ A‹1/i›)/r] ∷ Q
    Eq a l r =>
      let a0 = a.zero; a1 = a.one in
      whnf defs ctx $
        subN (tycaseRhsDef def KEq arms)
          [< a0 :# TYPE u, a1 :# TYPE u,
             DLam a :# Eq0 (TYPE u) a0 a1, l :# a0, r :# a1]
        :# ret

    -- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
    Nat =>
      whnf defs ctx $ tycaseRhsDef0 def KNat arms :# ret

    -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
    BOX _ s =>
      whnf defs ctx $ sub1 (tycaseRhsDef def KBOX arms) (s :# TYPE u) :# ret

  ||| pushes a coercion inside a whnf-ed term
  private covering
  pushCoe : {n, d : Nat} -> (defs : Definitions) -> WhnfContext d n ->
            BaseName ->
            (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
            Dim d -> Dim d ->
            (s : Term d n) -> (0 snf : No (isRedexT defs s)) =>
            Either Error (NonRedex Elim d n defs)
  pushCoe defs ctx i ty p q s =
    if p == q then whnf defs ctx $ s :# (ty // one q) else
    case s of
      -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
      TYPE {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
      Pi   {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
      Sig  {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
      Enum {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
      Eq   {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
      Nat     => pure $ nred $ s :# TYPE !(unwrapTYPE ty)
      BOX  {} => pure $ nred $ s :# TYPE !(unwrapTYPE ty)

      -- just η expand it. then whnf for (:@) will handle it later
      -- this is how @xtt does it
      Lam body => do
        let body' = CoeT i ty p q $ Lam body
            term' = [< "y"] :\\ E (weakE 1 body' :@ BVT 0)
            type' = ty // one q
        whnf defs ctx $ term' :# type'

      {-
      -- maybe:
      -- (coe [i ⇒ π.(x : A) → B] @p @q (λ x ⇒ s)) ⇝
      -- (λ x ⇒ coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @q @i x)/x]] @p @q s)
      --   ∷ (π.(x: A‹q/i›) → B‹q/i›)
      Lam body => do
        let Pi {qty, arg, res} = ty
          | _ => Left $ ?err
        let arg' = ST [< "j"] $ weakT 1 $ arg // (BV 0 ::: shift 2)
            res' = ST [< i] $ res.term //
                      (Coe arg' (weakD 1 q) (BV 0) (BVT 0) ::: shift 1)
            body = ST body.names $ E $ Coe res' p q body.term
        pure $ Element (Lam body :# Pi qty (arg // one q) (res // one q)) Ah
      -}

      -- (coe [i ⇒ (x : A) × B] @p @q (s, t)) ⇝
      -- (coe [i ⇒ A] @p @q s,
      --  coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t)
      --   ∷ (x : A‹q/i›) × B‹q/i›
      --
      -- can't use η here because... it doesn't exist
      Pair fst snd => do
        let Sig {fst = tfst, snd = tsnd} = ty
          | _ => Left $ ExpectedSig (extendDim i ctx.names) ty
        let fst'  = E $ CoeT i tfst p q fst
            tfst' = tfst // (BV 0 ::: shift 2)
            tsnd' = sub1 tsnd $ CoeT "j" tfst' (weakD 1 p) (BV 0) $ dweakT 1 fst
            snd'  = E $ CoeT i tsnd' p q snd
        pure $
          Element (Pair fst' snd' :# Sig (tfst // one q) (tsnd // one q)) Ah

      -- η expand like λ
      DLam body => do
        let body' = CoeT i ty p q $ DLam body
            term' = [< "j"] :\\% E (dweakE 1 body' :% BV 0)
            type' = ty // one q
        whnf defs ctx $ term' :# type'

      -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
      Tag tag => do
        let Enum ts = ty
          | _ => Left $ ExpectedEnum (extendDim i ctx.names) ty
        pure $ Element (Tag tag :# Enum ts) Ah

      -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ)
      Zero   => pure $ Element (Zero :# Nat) Ah
      Succ t => pure $ Element (Succ t :# Nat) Ah

      -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
      -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›]
      Box val => do
        let BOX {qty, ty = a} = ty
          | _ => Left $ ExpectedBOX (extendDim i ctx.names) ty
        pure $ Element (Box (E $ CoeT i a p q s) :# BOX qty (a // one q)) Ah

      E e => pure $ Element (CoeT i ty p q (E e)) (snf `orNo` Ah)
  where
    unwrapTYPE : Term (S d) n -> Either Error Universe
    unwrapTYPE (TYPE u) = pure u
    unwrapTYPE ty       = Left $ ExpectedTYPE (extendDim i ctx.names) ty