module Quox.Whnf.Coercion import Quox.Whnf.Interface import Quox.Whnf.ComputeElimType import Quox.Whnf.TypeCase %default total private coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc -> ScopeTermN s d n -> ScopeTermN s d n coeScoped ty p q loc (S names (N body)) = S names $ N $ E $ Coe ty p q body loc coeScoped ty p q loc (S names (Y body)) = ST names $ E $ Coe (weakDS s ty) p q body loc where 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 parameters {auto _ : CanWhnf Term Interface.isRedexT} {auto _ : CanWhnf Elim Interface.isRedexE} (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty) ||| reduce a function application `App (Coe ty p q val) s loc` export covering piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val, s : Term d n) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg)) piCoe sty@(S [< i] ty) p q val s loc = 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 SZero $ getTerm ty (arg, res) <- tycasePi defs ctx1 ty let s0 = CoeT i arg q 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 q) (BV 0 i.loc) (s // shift 1) s.loc whnf defs ctx sg $ CoeT i (sub1 res s1) p q body loc ||| reduce a pair elimination `CasePair pi (Coe ty p q val) ret body loc` export 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) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg)) sigCoe qty sty@(S [< i] ty) p q val ret body loc = 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 SZero $ getTerm ty (tfst, tsnd) <- tycaseSig defs ctx1 ty let [< x, y] = body.names a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc tsnd' = tsnd.term // (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2)) (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2) b' = CoeT i tsnd' p q (BVT 0 noLoc) 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 q val) loc` export covering fstCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg)) fstCoe sty@(S [< i] ty) p q val loc = do -- fst (coe (𝑖 ⇒ (x : A) × B) @p @q s) -- ⇝ -- coe (𝑖 ⇒ A) @p @q (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 whnf defs ctx sg $ Coe (ST [< i] tfst) p q (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 d n) -> (p, q : Dim d) -> (val : Term d n) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg)) sndCoe sty@(S [< i] ty) p q val loc = do -- snd (coe (𝑖 ⇒ (x : A) × B) @p @q s) -- ⇝ -- coe (𝑖 ⇒ B[coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑖 (fst (s ∷ (x : A) × B))/x]) @p @q -- (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 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 q (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 d n) -> (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg)) eqCoe sty@(S [< j] ty) p q val r loc = 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; 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 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 q 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) -> (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) -> (ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc -> Eff Whnf (Subset (Elim d n) (No . isRedexE defs sg)) boxCoe qty sty@(S [< i] ty) p q val ret body loc = 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 SZero $ getTerm ty ta <- tycaseBOX defs ctx1 ty let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret (ST body.names $ body.term // (a' ::: shift 1)) loc ||| pushes a coercion inside a whnf-ed term export covering pushCoe : BindName -> (ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc -> (0 pc : So (canPushCoe sg ty s)) => Eff Whnf (NonRedex Elim d n defs sg) pushCoe i ty p q s loc = case ty of -- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ) TYPE l tyLoc => whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc -- η expand it so that whnf for App can deal with it -- -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) -- ⇝ -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖› Pi {} => let inner = Coe (SY [< i] ty) p q s loc in whnf defs ctx sg $ Ann (LamY !(mnb "y" loc) (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc) (ty // one q) loc -- no η!!! -- push into a pair constructor, otherwise still stuck -- -- s̃‹𝑘› ≔ coe (𝑗 ⇒ A‹𝑗/𝑖›) @p @𝑘 s -- ----------------------------------------------- -- (coe (𝑖 ⇒ (x : A) × B) @p @q (s, t)) -- ⇝ -- (s̃‹q›, coe (𝑖 ⇒ B[s̃‹𝑖›/x]) @p @q t) -- ∷ ((x : A) × B)‹q/𝑖› Sig tfst tsnd tyLoc => do let Pair fst snd sLoc = s fst' = CoeT i tfst p q fst fst.loc fstInSnd = CoeT !(fresh i) (tfst // (BV 0 loc ::: shift 2)) (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc whnf defs ctx sg $ Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc -- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄}) Enum cases tyLoc => whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc -- η expand, same as for Π -- -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) -- ⇝ -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖› Eq {} => let inner = Coe (SY [< i] ty) p q s loc in whnf defs ctx sg $ Ann (DLamY !(mnb "k" loc) (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc) (ty // one q) loc -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ) Nat tyLoc => whnf defs ctx sg $ Ann s (Nat tyLoc) loc -- η expand -- -- (coe (𝑖 ⇒ [π. A]) @p @q s) -- ⇝ -- [case1 coe (𝑖 ⇒ [π. A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}] -- ∷ [π. A]‹q/𝑖› BOX qty inner tyLoc => let inner = CaseBox { qty = One, box = Coe (SY [< i] ty) p q s loc, ret = SN $ ty // one q, body = SY [< !(mnb "x" loc)] $ BVT 0 loc, loc } in whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc