189 lines
7.4 KiB
Idris
189 lines
7.4 KiB
Idris
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}
|
||
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
||
||| 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))
|
||
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 $ 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 $ 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))
|
||
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 $ 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 $ CasePair qty (Ann val (ty // one p) val.loc) ret
|
||
(ST body.names $ body.term // (a' ::: b' ::: shift 2)) 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))
|
||
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 $ 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 $ 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))
|
||
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 $ 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 $ 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 ty s)) =>
|
||
Eff Whnf (NonRedex Elim d n defs)
|
||
pushCoe i ty p q s loc =
|
||
case ty of
|
||
-- (coe ★ᵢ @_ @_ s) ⇝ (s ∷ ★ᵢ)
|
||
TYPE l tyLoc =>
|
||
whnf defs ctx $ 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 $
|
||
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 $
|
||
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
|
||
|
||
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
|
||
Enum cases tyLoc =>
|
||
whnf defs ctx $ 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 $
|
||
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 $ 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 $ Ann (Box (E inner) loc) (ty // one q) loc
|