rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

add fst and snd

Browse source
This commit is contained in:
rhiannon morris 2023-09-18 21:52:51 +02:00
parent e6c06a5c81
commit bb8d2464af
17 changed files with 319 additions and 124 deletions
Download patch file Download diff file Expand all files Collapse all files

82
lib/Quox/Whnf/Coercion.idr
View file

@ -23,12 +23,12 @@ where
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (pi : SQty)
{d, n : Nat} (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 pi))
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›)
@ -42,17 +42,17 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
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 pi $ CoeT i (sub1 res s1) p q body 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 pi))
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,
@ -68,17 +68,57 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(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 pi $ CasePair qty (Ann val (ty // one p) val.loc) ret
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 pi))
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
@ -86,23 +126,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(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 pi $ CompH j a' p q val' r j s j t 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 pi))
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 pi $ CaseBox qty (Ann val (ty // one p) val.loc) ret
whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
(ST body.names $ body.term // (a' ::: shift 1)) loc
@ -110,13 +150,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
export covering
pushCoe : BindName ->
(ty : Term (S d) n) -> (p, q : Dim d) -> (s : Term d n) -> Loc ->
(0 pc : So (canPushCoe pi ty s)) =>
Eff Whnf (NonRedex Elim d n defs pi)
(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 pi $ Ann s (TYPE l tyLoc) loc
whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc
-- η expand it so that whnf for App can deal with it
--
@ -125,7 +165,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (λ 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 pi $
whnf defs ctx sg $
Ann (LamY !(mnb "y" loc)
(E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
(ty // one q) loc
@ -147,12 +187,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(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 pi $
whnf defs ctx sg $
Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc
-- (coe {𝐚̄} @_ @_ s) ⇝ (s ∷ {𝐚̄})
Enum cases tyLoc =>
whnf defs ctx pi $ Ann s (Enum cases tyLoc) loc
whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
-- η expand, same as for Π
--
@ -161,14 +201,14 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
-- (δ 𝑘 ⇒ (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 pi $
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 pi $ Ann s (Nat tyLoc) loc
whnf defs ctx sg $ Ann s (Nat tyLoc) loc
-- η expand
--
@ -185,4 +225,4 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
loc
}
in
whnf defs ctx pi $ Ann (Box (E inner) loc) (ty // one q) loc
whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc

12
lib/Quox/Whnf/ComputeElimType.idr
View file

@ -41,11 +41,21 @@ computeElimType defs ctx pi e {ne} =
App f s loc =>
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
t => throw $ ExpectedPi loc ctx.names t
ty => throw $ ExpectedPi loc ctx.names ty
CasePair {pair, ret, _} =>
pure $ sub1 ret pair
Fst pair loc =>
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
Sig {fst, _} => pure fst
ty => throw $ ExpectedSig loc ctx.names ty
Snd pair loc =>
case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
ty => throw $ ExpectedSig loc ctx.names ty
CaseEnum {tag, ret, _} =>
pure $ sub1 ret tag

94
lib/Quox/Whnf/Interface.idr
View file

@ -155,24 +155,24 @@ isK _ = False
||| - `val` is a constructor form
public export %inline
canPushCoe : SQty -> (ty, val : Term {}) -> Bool
canPushCoe pi (TYPE {}) _ = True
canPushCoe pi (Pi {}) _ = True
canPushCoe pi (Lam {}) _ = False
canPushCoe pi (Sig {}) (Pair {}) = True
canPushCoe pi (Sig {}) _ = False
canPushCoe pi (Pair {}) _ = False
canPushCoe pi (Enum {}) _ = True
canPushCoe pi (Tag {}) _ = False
canPushCoe pi (Eq {}) _ = True
canPushCoe pi (DLam {}) _ = False
canPushCoe pi (Nat {}) _ = True
canPushCoe pi (Zero {}) _ = False
canPushCoe pi (Succ {}) _ = False
canPushCoe pi (BOX {}) _ = True
canPushCoe pi (Box {}) _ = False
canPushCoe pi (E {}) _ = False
canPushCoe pi (CloT {}) _ = False
canPushCoe pi (DCloT {}) _ = False
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (Nat {}) _ = True
canPushCoe sg (Zero {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
mutual
@ -184,40 +184,44 @@ mutual
||| an application whose head is an annotated lambda,
||| a case expression whose head is an annotated constructor form, etc
||| 4. a redundant annotation, or one whose term or type is reducible
||| 5. a coercion `coe (𝑖 ⇒ A) @p @pi s` where:
||| 5. a coercion `coe (𝑖 ⇒ A) @p @q s` where:
||| a. `A` is reducible or a type constructor, or
||| b. `𝑖` is not mentioned in `A`
||| ([fixme] should be A‹0/𝑖› = A‹1/𝑖›), or
||| c. `p = pi`
||| 6. a composition `comp A @p @pi s @r {⋯}`
||| where `p = pi`, `r = 0`, or `r = 1`
||| c. `p = q`
||| 6. a composition `comp A @p @q s @r {⋯}`
||| where `p = q`, `r = 0`, or `r = 1`
||| 7. a closure
public export
isRedexE : RedexTest Elim
isRedexE defs pi (F {x, u, _}) {d, n} =
isRedexE defs sg (F {x, u, _}) {d, n} =
isJust $ lookupElim x u defs {d, n}
isRedexE _ pi (B {}) = False
isRedexE defs pi (App {fun, _}) =
isRedexE defs pi fun || isLamHead fun
isRedexE defs pi (CasePair {pair, _}) =
isRedexE defs pi pair || isPairHead pair
isRedexE defs pi (CaseEnum {tag, _}) =
isRedexE defs pi tag || isTagHead tag
isRedexE defs pi (CaseNat {nat, _}) =
isRedexE defs pi nat || isNatHead nat
isRedexE defs pi (CaseBox {box, _}) =
isRedexE defs pi box || isBoxHead box
isRedexE defs pi (DApp {fun, arg, _}) =
isRedexE defs pi fun || isDLamHead fun || isK arg
isRedexE defs pi (Ann {tm, ty, _}) =
isE tm || isRedexT defs pi tm || isRedexT defs SZero ty
isRedexE defs pi (Coe {ty = S _ (N _), _}) = True
isRedexE defs pi (Coe {ty = S _ (Y ty), p, q, val, _}) =
isRedexT defs SZero ty || canPushCoe pi ty val || isYes (p `decEqv` q)
isRedexE defs pi (Comp {ty, p, q, r, _}) =
isRedexE _ sg (B {}) = False
isRedexE defs sg (App {fun, _}) =
isRedexE defs sg fun || isLamHead fun
isRedexE defs sg (CasePair {pair, _}) =
isRedexE defs sg pair || isPairHead pair || isYes (sg `decEq` SZero)
isRedexE defs sg (Fst pair _) =
isRedexE defs sg pair || isPairHead pair
isRedexE defs sg (Snd pair _) =
isRedexE defs sg pair || isPairHead pair
isRedexE defs sg (CaseEnum {tag, _}) =
isRedexE defs sg tag || isTagHead tag
isRedexE defs sg (CaseNat {nat, _}) =
isRedexE defs sg nat || isNatHead nat
isRedexE defs sg (CaseBox {box, _}) =
isRedexE defs sg box || isBoxHead box
isRedexE defs sg (DApp {fun, arg, _}) =
isRedexE defs sg fun || isDLamHead fun || isK arg
isRedexE defs sg (Ann {tm, ty, _}) =
isE tm || isRedexT defs sg tm || isRedexT defs SZero ty
isRedexE defs sg (Coe {ty = S _ (N _), _}) = True
isRedexE defs sg (Coe {ty = S _ (Y ty), p, q, val, _}) =
isRedexT defs SZero ty || canPushCoe sg ty val || isYes (p `decEqv` q)
isRedexE defs sg (Comp {ty, p, q, r, _}) =
isYes (p `decEqv` q) || isK r
isRedexE defs pi (TypeCase {ty, ret, _}) =
isRedexE defs pi ty || isRedexT defs pi ret || isAnnTyCon ty
isRedexE defs sg (TypeCase {ty, ret, _}) =
isRedexE defs sg ty || isRedexT defs sg ret || isAnnTyCon ty
isRedexE _ _ (CloE {}) = True
isRedexE _ _ (DCloE {}) = True
@ -231,5 +235,5 @@ mutual
isRedexT : RedexTest Term
isRedexT _ _ (CloT {}) = True
isRedexT _ _ (DCloT {}) = True
isRedexT defs pi (E {e, _}) = isAnn e || isRedexE defs pi e
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
isRedexT _ _ _ = False

143
lib/Quox/Whnf/Main.idr
View file

@ -16,53 +16,88 @@ export covering CanWhnf Elim Interface.isRedexE
covering
CanWhnf Elim Interface.isRedexE where
whnf defs ctx rh (F x u loc) with (lookupElim x u defs) proof eq
_ | Just y = whnf defs ctx rh $ setLoc loc y
whnf defs ctx sg (F x u loc) with (lookupElim x u defs) proof eq
_ | Just y = whnf defs ctx sg $ setLoc loc y
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
whnf _ _ _ (B i loc) = pure $ nred $ B i loc
-- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
whnf defs ctx rh (App f s appLoc) = do
Element f fnf <- whnf defs ctx rh f
whnf defs ctx sg (App f s appLoc) = do
Element f fnf <- whnf defs ctx sg f
case nchoose $ isLamHead f of
Left _ => case f of
Ann (Lam {body, _}) (Pi {arg, res, _}) floc =>
let s = Ann s arg s.loc in
whnf defs ctx rh $ Ann (sub1 body s) (sub1 res s) appLoc
Coe ty p q val _ => piCoe defs ctx rh ty p q val s appLoc
whnf defs ctx sg $ Ann (sub1 body s) (sub1 res s) appLoc
Coe ty p q val _ => piCoe defs ctx sg ty p q val s appLoc
Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
-- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
-- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
whnf defs ctx rh (CasePair pi pair ret body caseLoc) = do
Element pair pairnf <- whnf defs ctx rh pair
--
-- 0 · case e return p ⇒ C of { (a, b) ⇒ u } ⇝
-- u[fst e/a, snd e/b] ∷ C[e/p]
whnf defs ctx sg (CasePair pi pair ret body caseLoc) = do
Element pair pairnf <- whnf defs ctx sg pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
let fst = Ann fst tfst fst.loc
snd = Ann snd (sub1 tsnd fst) snd.loc
in
whnf defs ctx rh $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
whnf defs ctx sg $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
Coe ty p q val _ => do
sigCoe defs ctx rh pi ty p q val ret body caseLoc
sigCoe defs ctx sg pi ty p q val ret body caseLoc
Right np =>
pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
case sg `decEq` SZero of
Yes Refl =>
whnf defs ctx SZero $
Ann (subN body [< Fst pair caseLoc, Snd pair caseLoc])
(sub1 ret pair)
caseLoc
No n0 =>
pure $ Element (CasePair pi pair ret body caseLoc)
(pairnf `orNo` np `orNo` notYesNo n0)
-- fst ((s, t) ∷ (x : A) × B) ⇝ s ∷ A
whnf defs ctx sg (Fst pair fstLoc) = do
Element pair pairnf <- whnf defs ctx sg pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
whnf defs ctx sg $ Ann fst tfst pairLoc
Coe ty p q val _ => do
fstCoe defs ctx sg ty p q val fstLoc
Right np =>
pure $ Element (Fst pair fstLoc) (pairnf `orNo` np)
-- snd ((s, t) ∷ (x : A) × B) ⇝ t ∷ B[(s ∷ A)/x]
whnf defs ctx sg (Snd pair sndLoc) = do
Element pair pairnf <- whnf defs ctx sg pair
case nchoose $ isPairHead pair of
Left _ => case pair of
Ann (Pair {fst, snd, _}) (Sig {fst = tfst, snd = tsnd, _}) pairLoc =>
whnf defs ctx sg $ Ann snd (sub1 tsnd (Ann fst tfst fst.loc)) sndLoc
Coe ty p q val _ => do
sndCoe defs ctx sg ty p q val sndLoc
Right np =>
pure $ Element (Snd pair sndLoc) (pairnf `orNo` np)
-- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
-- u ∷ C['a∷{a,…}/p]
whnf defs ctx rh (CaseEnum pi tag ret arms caseLoc) = do
Element tag tagnf <- whnf defs ctx rh tag
whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
Element tag tagnf <- whnf defs ctx sg tag
case nchoose $ isTagHead tag of
Left _ => case tag of
Ann (Tag t _) (Enum ts _) _ =>
let ty = sub1 ret tag in
case lookup t arms of
Just arm => whnf defs ctx rh $ Ann arm ty arm.loc
Just arm => whnf defs ctx sg $ Ann arm ty arm.loc
Nothing => throw $ MissingEnumArm caseLoc t (keys arms)
Coe ty p q val _ =>
-- there is nowhere an equality can be hiding inside an enum type
whnf defs ctx rh $
whnf defs ctx sg $
CaseEnum pi (Ann val (dsub1 ty q) val.loc) ret arms caseLoc
Right nt =>
pure $ Element (CaseEnum pi tag ret arms caseLoc) $ tagnf `orNo` nt
@ -72,37 +107,37 @@ CanWhnf Elim Interface.isRedexE where
--
-- case succ n ∷ ℕ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
-- u[n∷ℕ/n', (case n ∷ ℕ ⋯)/ih] ∷ C[succ n ∷ ℕ/p]
whnf defs ctx rh (CaseNat pi piIH nat ret zer suc caseLoc) = do
Element nat natnf <- whnf defs ctx rh nat
whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
Element nat natnf <- whnf defs ctx sg nat
case nchoose $ isNatHead nat of
Left _ =>
let ty = sub1 ret nat in
case nat of
Ann (Zero _) (Nat _) _ =>
whnf defs ctx rh $ Ann zer ty zer.loc
whnf defs ctx sg $ Ann zer ty zer.loc
Ann (Succ n succLoc) (Nat natLoc) _ =>
let nn = Ann n (Nat natLoc) succLoc
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
in
whnf defs ctx rh $ Ann tm ty caseLoc
whnf defs ctx sg $ Ann tm ty caseLoc
Coe ty p q val _ =>
-- same deal as Enum
whnf defs ctx rh $
whnf defs ctx sg $
CaseNat pi piIH (Ann val (dsub1 ty q) val.loc) ret zer suc caseLoc
Right nn => pure $
Element (CaseNat pi piIH nat ret zer suc caseLoc) (natnf `orNo` nn)
-- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
-- u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
whnf defs ctx rh (CaseBox pi box ret body caseLoc) = do
Element box boxnf <- whnf defs ctx rh box
whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
Element box boxnf <- whnf defs ctx sg box
case nchoose $ isBoxHead box of
Left _ => case box of
Ann (Box val boxLoc) (BOX q bty tyLoc) _ =>
let ty = sub1 ret box in
whnf defs ctx rh $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
whnf defs ctx sg $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
Coe ty p q val _ =>
boxCoe defs ctx rh pi ty p q val ret body caseLoc
boxCoe defs ctx sg pi ty p q val ret body caseLoc
Right nb =>
pure $ Element (CaseBox pi box ret body caseLoc) (boxnf `orNo` nb)
@ -110,35 +145,35 @@ CanWhnf Elim Interface.isRedexE where
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
--
-- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
whnf defs ctx rh (DApp f p appLoc) = do
Element f fnf <- whnf defs ctx rh f
whnf defs ctx sg (DApp f p appLoc) = do
Element f fnf <- whnf defs ctx sg f
case nchoose $ isDLamHead f of
Left _ => case f of
Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ =>
whnf defs ctx rh $
whnf defs ctx sg $
Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
(dsub1 ty p) appLoc
Coe ty p' q' val _ =>
eqCoe defs ctx rh ty p' q' val p appLoc
eqCoe defs ctx sg ty p' q' val p appLoc
Right ndlh => case p of
K e _ => do
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx rh f
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
| ty => throw $ ExpectedEq ty.loc ctx.names ty
whnf defs ctx rh $
whnf defs ctx sg $
ends (Ann (setLoc appLoc l) ty.zero appLoc)
(Ann (setLoc appLoc r) ty.one appLoc) e
B {} => pure $ Element (DApp f p appLoc) (fnf `orNo` ndlh `orNo` Ah)
-- e ∷ A ⇝ e
whnf defs ctx rh (Ann s a annLoc) = do
Element s snf <- whnf defs ctx rh s
whnf defs ctx sg (Ann s a annLoc) = do
Element s snf <- whnf defs ctx sg s
case nchoose $ isE s of
Left _ => let E e = s in pure $ Element e $ noOr2 snf
Right ne => do
Element a anf <- whnf defs ctx SZero a
pure $ Element (Ann s a annLoc) (ne `orNo` snf `orNo` anf)
whnf defs ctx rh (Coe sty p q val coeLoc) =
whnf defs ctx sg (Coe sty p q val coeLoc) =
-- 𝑖 ∉ fv(A)
-- -------------------------------
-- coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
@ -148,30 +183,30 @@ CanWhnf Elim Interface.isRedexE where
([< i], Left ty) =>
case p `decEqv` q of
-- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ A‹p/𝑖›)
Yes _ => whnf defs ctx rh $ Ann val (dsub1 sty p) coeLoc
Yes _ => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
No npq => do
Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
case nchoose $ canPushCoe rh ty val of
Left pc => pushCoe defs ctx rh i ty p q val coeLoc
case nchoose $ canPushCoe sg ty val of
Left pc => pushCoe defs ctx sg i ty p q val coeLoc
Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
(tynf `orNo` npc `orNo` notYesNo npq)
(_, Right ty) =>
whnf defs ctx rh $ Ann val ty coeLoc
whnf defs ctx sg $ Ann val ty coeLoc
whnf defs ctx rh (Comp ty p q val r zero one compLoc) =
whnf defs ctx sg (Comp ty p q val r zero one compLoc) =
case p `decEqv` q of
-- comp [A] @p @p s @r { ⋯ } ⇝ s ∷ A
Yes y => whnf defs ctx rh $ Ann val ty compLoc
Yes y => whnf defs ctx sg $ Ann val ty compLoc
No npq => case r of
-- comp [A] @p @q s @0 { 0 𝑗 ⇒ t₀; ⋯ } ⇝ t₀‹q/𝑗› ∷ A
K Zero _ => whnf defs ctx rh $ Ann (dsub1 zero q) ty compLoc
K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc
-- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁‹q/𝑗› ∷ A
K One _ => whnf defs ctx rh $ Ann (dsub1 one q) ty compLoc
K One _ => whnf defs ctx sg $ Ann (dsub1 one q) ty compLoc
B {} => pure $ Element (Comp ty p q val r zero one compLoc)
(notYesNo npq `orNo` Ah)
whnf defs ctx rh (TypeCase ty ret arms def tcLoc) =
case rh `decEq` SZero of
whnf defs ctx sg (TypeCase ty ret arms def tcLoc) =
case sg `decEq` SZero of
Yes Refl => do
Element ty tynf <- whnf defs ctx SZero ty
Element ret retnf <- whnf defs ctx SZero ret
@ -181,12 +216,12 @@ CanWhnf Elim Interface.isRedexE where
Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
(tynf `orNo` retnf `orNo` nt)
No _ =>
throw $ ClashQ tcLoc rh.qty Zero
throw $ ClashQ tcLoc sg.qty Zero
whnf defs ctx rh (CloE (Sub el th)) =
whnf defs ctx rh $ pushSubstsWith' id th el
whnf defs ctx rh (DCloE (Sub el th)) =
whnf defs ctx rh $ pushSubstsWith' th id el
whnf defs ctx sg (CloE (Sub el th)) =
whnf defs ctx sg $ pushSubstsWith' id th el
whnf defs ctx sg (DCloE (Sub el th)) =
whnf defs ctx sg $ pushSubstsWith' th id el
covering
CanWhnf Term Interface.isRedexT where
@ -206,13 +241,13 @@ CanWhnf Term Interface.isRedexT where
whnf _ _ _ t@(Box {}) = pure $ nred t
-- s ∷ A ⇝ s (in term context)
whnf defs ctx rh (E e) = do
Element e enf <- whnf defs ctx rh e
whnf defs ctx sg (E e) = do
Element e enf <- whnf defs ctx sg e
case nchoose $ isAnn e of
Left _ => let Ann {tm, _} = e in pure $ Element tm $ noOr1 $ noOr2 enf
Right na => pure $ Element (E e) $ na `orNo` enf
whnf defs ctx rh (CloT (Sub tm th)) =
whnf defs ctx rh $ pushSubstsWith' id th tm
whnf defs ctx rh (DCloT (Sub tm th)) =
whnf defs ctx rh $ pushSubstsWith' th id tm
whnf defs ctx sg (CloT (Sub tm th)) =
whnf defs ctx sg $ pushSubstsWith' id th tm
whnf defs ctx sg (DCloT (Sub tm th)) =
whnf defs ctx sg $ pushSubstsWith' th id tm