quox/lib/Quox/Whnf/Coercion.idr

190 lines
7.5 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 ty.term
(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 ⇒ Aj/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 [< 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 ⇒ Ar/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 ty.term
(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 ty.term
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) -> (0 npq : Not (p `Eqv` q)) =>
(s : Term d n) -> (0 pc : So (canPushCoe ty s)) => Loc ->
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 Aq/𝑖 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