module Quox.Whnf.Coercion

import Quox.Whnf.Interface
import Quox.Whnf.ComputeElimType
import Quox.Whnf.TypeCase

%default total



private
coeScoped : {s, q : Nat} -> DScopeTerm q d n -> Dim d -> Dim d -> Loc ->
            ScopeTermN s q d n -> ScopeTermN s q d n
coeScoped ty p p' loc (S names (N body)) =
  S names $ N $ E $ Coe ty p p' body loc
coeScoped ty p p' loc (S names (Y body)) =
  ST names $ E $ Coe (weakDS s ty) p p' body loc
where
  weakDS : (by : Nat) -> DScopeTerm q d n -> DScopeTerm q 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


parameters {auto _ : CanWhnf Term Interface.isRedexT}
           {auto _ : CanWhnf Elim Interface.isRedexE}
           (defs : Definitions) (ctx : WhnfContext q d n) (sg : SQty)
  ||| reduce a function application `App (Coe ty p p' val) s loc`
  export covering
  piCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) ->
          (val, s : Term q d n) -> Loc ->
          Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
  piCoe sty@(S [< i] ty) p p' val s loc = do
    -- (coe [i ⇒ π.(x : A) → B] @p @p' t) s ⇝
    -- coe [i ⇒ B[𝒔‹i›/x] @p @p' ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
    --   where 𝒔‹j› ≔ coe [i ⇒ A] @p' @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 SZero $ getTerm ty
    (arg, res) <- tycasePi defs ctx1 ty
    let Val q = ctx.qtyLen
        s0    = CoeT i arg p' p s s.loc
        body  = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
        s1    = CoeT i (arg // (BV 0 i.loc ::: shift 2))
                  (weakD 1 p') (BV 0 i.loc)
                  (s // shift 1) s.loc
    whnf defs ctx sg $ CoeT i (sub1 res s1) p p' body loc

  ||| reduce a pair elimination `CasePair pi (Coe ty p p' val) ret body loc`
  export covering
  sigCoe : (qty : Qty q) ->
           (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
           (ret : ScopeTerm q d n) -> (body : ScopeTermN 2 q d n) -> Loc ->
           Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
  sigCoe qty sty@(S [< i] ty) p p' val ret body loc = do
    -- caseπ (coe [i ⇒ (x : A) × B] @p @p' 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 @p' a)/a,
    --     (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @p' 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 SZero $ getTerm ty
    (tfst, tsnd) <- tycaseSig defs ctx1 ty
    let Val q = ctx.qtyLen
        [< x, y] = body.names
        a' = CoeT i (weakT 2 tfst) p p' (BVT 1 x.loc) x.loc
        tsnd' = tsnd.term //
          (CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
            (weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
        b' = CoeT i tsnd' p p' (BVT 0 y.loc) y.loc
    whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
      (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc

  ||| reduce a pair projection `Fst (Coe ty p p' val) loc`
  export covering
  fstCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
           Loc -> Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
  fstCoe sty@(S [< i] ty) p p' val loc = do
    -- fst (coe (𝑖 ⇒ (x : A) × B) @p @p' s)
    --   ⇝
    -- coe (𝑖 ⇒ A) @p @p' (fst (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
    --
    -- type-case is used to expose A,B if the type is neutral
    let ctx1 = extendDim i ctx
    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
    (tfst, _) <- tycaseSig defs ctx1 ty
    let Val q = ctx.qtyLen
    whnf defs ctx sg $
      Coe (ST [< i] tfst) p p'
          (E (Fst (Ann val (ty // one p) val.loc) val.loc)) loc

  ||| reduce a pair projection `Snd (Coe ty p q val) loc`
  export covering
  sndCoe : (ty : DScopeTerm q d n) -> (p, p' : Dim d) -> (val : Term q d n) ->
           Loc -> Eff Whnf (Subset (Elim q d n) (No . isRedexE defs ctx sg))
  sndCoe sty@(S [< i] ty) p p' val loc = do
    -- snd (coe (𝑖 ⇒ (x : A) × B) @p @p' s)
    --   ⇝
    -- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @p'
    --     (snd (s ∷ (x : A‹p/𝑖›) × B‹p/𝑖›))
    --
    -- type-case is used to expose A,B if the type is neutral
    let ctx1 = extendDim i ctx
    Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
    (tfst, tsnd) <- tycaseSig defs ctx1 ty
    let Val q = ctx.qtyLen
    whnf defs ctx sg $
      Coe (ST [< i] $ sub1 tsnd $
            Coe (ST [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
                (weakD 1 p) (BV 0 loc)
                (E (Fst (Ann (dweakT 1 val) ty val.loc) val.loc)) loc)
          p p'
          (E (Snd (Ann val (ty // one p) val.loc) val.loc))
          loc

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

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


-- new params block to call the above functions at different `n`
parameters {auto _ : CanWhnf Term Interface.isRedexT}
           {auto _ : CanWhnf Elim Interface.isRedexE}
           (defs : Definitions) (ctx : WhnfContext q d n) (sg : SQty)
  ||| pushes a coercion inside a whnf-ed term
  export covering
  pushCoe : BindName ->
            (ty : Term q (S d) n) -> (p, p' : Dim d) -> (s : Term q d n) ->
            Loc -> (0 pc : So (canPushCoe sg ty s)) =>
            Eff Whnf (NonRedex Elim q d n defs ctx sg)
  pushCoe i ty p p' s loc =
    case ty of
      -- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
      TYPE l tyLoc =>
        whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc

      -- (coe IOState @_ @_ s) ⇝ (s ∷ IOState)
      IOState tyLoc =>
        whnf defs ctx sg $ Ann s (IOState tyLoc) loc

      -- η expand, then simplify the Coe/App in the body
      --
      -- (coe (𝑖 ⇒ π.(x : A) → B) @p @p' s)
      --   ⇝
      -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @p' s) y) ∷ (π.(x : A) → B)‹p'/𝑖›
      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
      -- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹p'/𝑖›   -- see `piCoe`
      --
      -- do the piCoe step here because otherwise equality checking keeps
      -- doing the η forever
      Pi {arg, res = S [< x] _, _} => do
        let ctx' = extendTy x (arg // one p) ctx
        body <- piCoe defs ctx' sg
          (weakDS 1 $ SY [< i] ty) p p' (weakT 1 s) (BVT 0 loc) loc
        whnf defs ctx sg $
          Ann (LamY x (E body.fst) loc) (ty // one p') loc

      -- push into a pair constructor, otherwise still stuck
      --
      --   s̃‹𝑘› ≔ coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑘 s
      -- -----------------------------------------------
      --   (coe (𝑖 ⇒ (x : A) × B) @p @p' (s, t))
      --     ⇝
      --   (s̃‹p'›, coe (𝑖 ⇒ B[s̃‹𝑖›/x]) @p @p' t)
      --     ∷ ((x : A) × B)‹p'/𝑖›
      Sig tfst tsnd tyLoc => do
        let Val q = ctx.qtyLen
            Pair fst snd sLoc = s
            fst' = CoeT i tfst p p' fst fst.loc
            fstInSnd =
              CoeT !(fresh i)
                   (tfst // (BV 0 loc ::: shift 2))
                   (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
            snd' = CoeT i (sub1 tsnd fstInSnd) p p' snd snd.loc
        whnf defs ctx sg $
          Ann (Pair (E fst') (E snd') sLoc) (ty // one p') loc

      -- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
      Enum cases tyLoc =>
        whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc

      -- η expand/simplify, same as for Π
      --
      -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @p' s)
      --   ⇝
      -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @p' s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹p'/𝑖›
      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
      -- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹p'/𝑖›   -- see `eqCoe`
      --
      -- do the eqCoe step here because otherwise equality checking keeps
      -- doing the η forever
      Eq {ty = S [< j] _, _} => do
        let ctx' = extendDim j ctx
        body <- eqCoe defs ctx' sg
          (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 p')
          (dweakT 1 s) (BV 0 loc) loc
        whnf defs ctx sg $
          Ann (DLamY i (E body.fst) loc) (ty // one p') loc

      -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
      NAT tyLoc =>
        whnf defs ctx sg $ Ann s (NAT tyLoc) loc

      -- (coe String @_ @_ s) ⇝ (s ∷ String)
      STRING tyLoc =>
        whnf defs ctx sg $ Ann s (STRING tyLoc) loc

      -- η expand/simplify
      --
      -- (coe (𝑖 ⇒ [π.A]) @p @p' s)
      --   ⇝
      -- [case coe (𝑖 ⇒ [π.A]) @p @p' s return A‹p'/𝑖› of {[x] ⇒ x}]
      --   ⇝
      -- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹p'/𝑖›   -- see `boxCoe`
      --
      -- do the boxCoe step here because otherwise equality checking keeps
      -- doing the η forever
      BOX qty inner tyLoc => do
        body <- boxCoe defs ctx sg qty
          (SY [< i] ty) p p' s
          (SN $ inner // one p')
          (SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
        whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one p') loc