quox/lib/Quox/Whnf/Coercion.idr

253 lines
11 KiB
Idris
Raw Normal View History

2023-08-24 12:42:26 -04:00
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)) =
2024-05-28 11:00:01 -04:00
SY names $ E $ Coe (weakDS s ty) p q body loc
2023-08-24 12:42:26 -04:00
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}
2023-10-15 10:23:38 -04:00
(defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
2023-08-24 12:42:26 -04:00
||| 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))
2023-08-24 12:42:26 -04:00
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
2023-08-24 12:42:26 -04:00
(arg, res) <- tycasePi defs ctx1 ty
2024-05-28 11:00:01 -04:00
let s0 = CoeY i arg q p s s.loc
2023-08-24 12:42:26 -04:00
body = E $ App (Ann val (ty // one p) val.loc) (E s0) loc
2024-05-28 11:00:01 -04:00
s1 = CoeY i (arg // (BV 0 i.loc ::: shift 2)) (weakD 1 q) (BV 0 i.loc)
2023-08-24 12:42:26 -04:00
(s // shift 1) s.loc
2024-05-28 11:00:01 -04:00
whnf defs ctx sg $ CoeY i (sub1 res s1) p q body loc
2023-08-24 12:42:26 -04:00
||| 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))
2023-08-24 12:42:26 -04:00
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 }
2023-09-18 15:52:51 -04:00
-- ⇝
2023-08-24 12:42:26 -04:00
-- 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
2023-08-24 12:42:26 -04:00
(tfst, tsnd) <- tycaseSig defs ctx1 ty
let [< x, y] = body.names
2024-05-28 11:00:01 -04:00
a' = CoeY i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
2023-08-24 12:42:26 -04:00
tsnd' = tsnd.term //
2024-05-28 11:00:01 -04:00
(CoeY i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
2023-11-27 15:01:36 -05:00
(weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
2024-05-28 11:00:01 -04:00
b' = CoeY i tsnd' p q (BVT 0 y.loc) y.loc
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
2024-05-28 11:00:01 -04:00
(SY body.names $ body.term // (a' ::: b' ::: shift 2)) loc
2023-08-24 12:42:26 -04:00
2023-09-18 15:52:51 -04:00
||| 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))
2023-09-18 15:52:51 -04:00
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 $
2024-05-28 11:00:01 -04:00
Coe (SY [< i] tfst) p q
2023-09-18 15:52:51 -04:00
(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))
2023-09-18 15:52:51 -04:00
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 $
2024-05-28 11:00:01 -04:00
Coe (SY [< i] $ sub1 tsnd $
Coe (SY [< !(fresh i)] $ tfst // (BV 0 i.loc ::: shift 2))
2023-09-18 15:52:51 -04:00
(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
2023-08-24 12:42:26 -04:00
||| 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))
2023-08-24 12:42:26 -04:00
eqCoe sty@(S [< j] ty) p q val r loc = do
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
2023-09-18 15:52:51 -04:00
-- ⇝
-- comp [j ⇒ Ar/i] @p @q ((eq ∷ (Eq [i ⇒ A] L R)p/j) @r)
2023-08-24 12:42:26 -04:00
-- @r { 0 j ⇒ L; 1 j ⇒ R }
let ctx1 = extendDim j ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
2023-08-24 12:42:26 -04:00
(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
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ CompH j a' p q val' r j s j t loc
2023-08-24 12:42:26 -04:00
||| 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))
2023-08-24 12:42:26 -04:00
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 }
2023-09-18 15:52:51 -04:00
-- ⇝
2023-08-28 14:03:06 -04:00
-- caseπ s ∷ [ρ. A]p/i return z ⇒ C of { [a] ⇒ e[(coe [i ⇒ A] p q a)/a] }
2023-08-24 12:42:26 -04:00
let ctx1 = extendDim i ctx
Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
2023-08-24 12:42:26 -04:00
ta <- tycaseBOX defs ctx1 ty
2023-11-27 15:01:36 -05:00
let xloc = body.name.loc
2024-05-28 11:00:01 -04:00
let a' = CoeY i (weakT 1 ta) p q (BVT 0 xloc) xloc
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
2024-05-28 11:00:01 -04:00
(SY body.names $ body.term // (a' ::: shift 1)) loc
2023-08-24 12:42:26 -04:00
-- 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 d n) (sg : SQty)
2023-08-24 12:42:26 -04:00
||| pushes a coercion inside a whnf-ed term
export covering
pushCoe : BindName ->
2023-08-28 14:03:06 -04:00
(ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
2023-09-18 15:52:51 -04:00
(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 =>
2023-09-18 15:52:51 -04:00
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 @q s)
-- ⇝
-- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)q/𝑖
-- ⇝ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
-- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)q/𝑖 -- 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 q (weakT 1 s) (BVT 0 loc) loc
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
Ann (LamY x (E body.fst) loc) (ty // one q) loc
-- no η!!!
-- push into a pair constructor, otherwise still stuck
2023-08-24 12:42:26 -04:00
--
-- 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
2024-05-28 11:00:01 -04:00
fst' = CoeY i tfst p q fst fst.loc
fstInSnd =
2024-05-28 11:00:01 -04:00
CoeY !(fresh i)
(tfst // (BV 0 loc ::: shift 2))
2024-03-21 16:29:01 -04:00
(weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
2024-05-28 11:00:01 -04:00
snd' = CoeY i (sub1 tsnd fstInSnd) p q snd snd.loc
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
Enum cases tyLoc =>
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
-- η expand/simplify, same as for Π
2023-08-24 12:42:26 -04:00
--
-- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
-- ⇝
-- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)q/𝑖
-- ⇝ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
-- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)q/𝑖 -- 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 q)
(dweakT 1 s) (BV 0 loc) loc
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
Ann (DLamY i (E body.fst) loc) (ty // one q) loc
-- (coe @_ @_ s) ⇝ (s ∷ )
2023-11-02 13:14:22 -04:00
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
2023-08-24 12:42:26 -04:00
--
-- (coe (𝑖 ⇒ [π.A]) @p @q s)
-- ⇝
-- [case coe (𝑖 ⇒ [π.A]) @p @q s return Aq/𝑖 of {[x] ⇒ x}]
-- ⇝
-- [case1 s ∷ [π.A]p/𝑖 ⋯] ∷ [π.A]q/𝑖 -- see `boxCoe`
--
-- do the eqCoe 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 q s
(SN $ inner // one q)
(SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc