quox/lib/Quox/Whnf/Coercion.idr

239 lines
9.7 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}
(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 ctx 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 ctx 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 ⇒ 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 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 ctx 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 : Ap/𝑖) × Bp/𝑖))
--
-- 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 ctx 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 : Ap/𝑖) × Bp/𝑖))
--
-- 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 ctx 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 ⇒ 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 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 ctx 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 ctx 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
-- (coe IOState @_ @_ s) ⇝ (s ∷ IOState)
IOState tyLoc =>
whnf defs ctx sg $ Ann s (IOState 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
-- (coe String @_ @_ s) ⇝ (s ∷ String)
STRING tyLoc =>
whnf defs ctx sg $ Ann s (STRING tyLoc) loc
-- η expand.... kinda
--
-- (coe (𝑖 ⇒ [π. A]) @p @q s)
-- ⇝
-- [case1 s ∷ [π.A]p/𝑖 return Aq/𝑖
-- of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]q/𝑖
--
-- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
-- the equality checker because whnf of `case e ⋯` requires whnf of `e`
BOX qty inner tyLoc => do
let inner = CaseBox {
qty = One,
box = Ann s (ty // one p) s.loc,
ret = SN $ inner // one q,
body = SY [< !(mnb "x" loc)] $ E $
Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
loc
}
whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc