quox/lib/Quox/Whnf/Main.idr

268 lines
11 KiB
Idris
Raw Normal View History

2023-08-24 12:42:26 -04:00
module Quox.Whnf.Main
import Quox.Whnf.Interface
import Quox.Whnf.ComputeElimType
import Quox.Whnf.TypeCase
import Quox.Whnf.Coercion
import Quox.Displace
import Data.SnocVect
%default total
export covering CanWhnf Term Interface.isRedexT
export covering CanWhnf Elim Interface.isRedexE
covering
CanWhnf Elim Interface.isRedexE where
2023-10-15 10:23:38 -04:00
whnf defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
_ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y
2023-08-24 12:42:26 -04:00
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
whnf _ _ _ (B i loc) = pure $ nred $ B i loc
2023-08-24 12:42:26 -04:00
-- ((λ x ⇒ t) ∷ (π.x : A) → B) s ⇝ t[s∷A/x] ∷ B[s∷A/x]
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (App f s appLoc) = do
Element f fnf <- whnf defs ctx sg f
2023-08-24 12:42:26 -04:00
case nchoose $ isLamHead f of
Left _ => case f of
Ann (Lam {body, _}) (Pi {arg, res, _}) floc =>
let s = Ann s arg s.loc in
2023-09-18 15:52:51 -04:00
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
2023-08-24 12:42:26 -04:00
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]
2023-09-18 15:52:51 -04:00
--
-- 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
2023-08-24 12:42:26 -04:00
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
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ Ann (subN body [< fst, snd]) (sub1 ret pair) caseLoc
Coe ty p q val _ => do
sigCoe defs ctx sg pi ty p q val ret body caseLoc
Right 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
2023-08-24 12:42:26 -04:00
Coe ty p q val _ => do
2023-09-18 15:52:51 -04:00
sndCoe defs ctx sg ty p q val sndLoc
2023-08-24 12:42:26 -04:00
Right np =>
2023-09-18 15:52:51 -04:00
pure $ Element (Snd pair sndLoc) (pairnf `orNo` np)
2023-08-24 12:42:26 -04:00
-- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
-- u ∷ C['a∷{a,…}/p]
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (CaseEnum pi tag ret arms caseLoc) = do
Element tag tagnf <- whnf defs ctx sg tag
2023-08-24 12:42:26 -04:00
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
2023-09-18 15:52:51 -04:00
Just arm => whnf defs ctx sg $ Ann arm ty arm.loc
2023-08-24 12:42:26 -04:00
Nothing => throw $ MissingEnumArm caseLoc t (keys arms)
Coe ty p q val _ =>
-- there is nowhere an equality can be hiding inside an enum type
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
2023-08-24 12:42:26 -04:00
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
-- case zero ∷ return p ⇒ C of { zero ⇒ u; … } ⇝
-- u ∷ C[zero∷/p]
--
-- case succ n ∷ return p ⇒ C of { succ n', π.ih ⇒ u; … } ⇝
-- u[n∷/n', (case n ∷ ⋯)/ih] ∷ C[succ n ∷ /p]
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (CaseNat pi piIH nat ret zer suc caseLoc) = do
Element nat natnf <- whnf defs ctx sg nat
2023-08-24 12:42:26 -04:00
case nchoose $ isNatHead nat of
Left _ =>
let ty = sub1 ret nat in
case nat of
Ann (Nat 0 _) (NAT _) _ =>
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ Ann zer ty zer.loc
Ann (Nat (S n) succLoc) (NAT natLoc) _ =>
let nn = Ann (Nat n succLoc) (NAT natLoc) succLoc
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
in
whnf defs ctx sg $ Ann tm ty caseLoc
2023-11-02 13:14:22 -04:00
Ann (Succ n succLoc) (NAT natLoc) _ =>
let nn = Ann n (NAT natLoc) succLoc
2023-08-24 12:42:26 -04:00
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
in
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ Ann tm ty caseLoc
2023-08-24 12:42:26 -04:00
Coe ty p q val _ =>
-- same deal as Enum
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
2023-08-24 12:42:26 -04:00
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)
2023-08-24 12:42:26 -04:00
-- case [t] ∷ [π.A] return p ⇒ C of { [x] ⇒ u } ⇝
-- u[t∷A/x] ∷ C[[t] ∷ [π.A]/p]
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (CaseBox pi box ret body caseLoc) = do
Element box boxnf <- whnf defs ctx sg box
2023-08-24 12:42:26 -04:00
case nchoose $ isBoxHead box of
Left _ => case box of
Ann (Box val boxLoc) (BOX q bty tyLoc) _ =>
let ty = sub1 ret box in
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ Ann (sub1 body (Ann val bty val.loc)) ty caseLoc
2023-08-24 12:42:26 -04:00
Coe ty p q val _ =>
2023-09-18 15:52:51 -04:00
boxCoe defs ctx sg pi ty p q val ret body caseLoc
2023-08-24 12:42:26 -04:00
Right nb =>
pure $ Element (CaseBox pi box ret body caseLoc) (boxnf `orNo` nb)
2023-08-24 12:42:26 -04:00
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @0 ⇝ t ∷ A0/𝑗
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A1/𝑗
--
-- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s𝑘/𝑖 ∷ A𝑘/𝑗
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (DApp f p appLoc) = do
Element f fnf <- whnf defs ctx sg f
2023-08-24 12:42:26 -04:00
case nchoose $ isDLamHead f of
Left _ => case f of
Ann (DLam {body, _}) (Eq {ty, l, r, _}) _ =>
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
2023-08-24 12:42:26 -04:00
Ann (endsOr (setLoc appLoc l) (setLoc appLoc r) (dsub1 body p) p)
(dsub1 ty p) appLoc
Coe ty p' q' val _ =>
2023-09-18 15:52:51 -04:00
eqCoe defs ctx sg ty p' q' val p appLoc
2023-08-24 12:42:26 -04:00
Right ndlh => case p of
K e _ => do
2023-09-18 15:52:51 -04:00
Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
2023-08-24 12:42:26 -04:00
| ty => throw $ ExpectedEq ty.loc ctx.names ty
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $
2023-08-24 12:42:26 -04:00
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)
2023-08-24 12:42:26 -04:00
-- e ∷ A ⇝ e
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (Ann s a annLoc) = do
Element s snf <- whnf defs ctx sg s
2023-08-24 12:42:26 -04:00
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)
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (Coe sty p q val coeLoc) =
-- 𝑖 ∉ fv(A)
-- -------------------------------
-- coe (𝑖 ⇒ A) @p @q s ⇝ s ∷ A
--
2023-09-17 07:54:26 -04:00
-- [fixme] needs a real equality check between A0/𝑖 and A1/𝑖
case dsqueeze sty {f = Term} of
2023-09-17 13:06:07 -04:00
([< i], Left ty) =>
case p `decEqv` q of
-- coe (𝑖 ⇒ A) @p @p s ⇝ (s ∷ Ap/𝑖)
2023-09-18 15:52:51 -04:00
Yes _ => whnf defs ctx sg $ Ann val (dsub1 sty p) coeLoc
No npq => do
Element ty tynf <- whnf defs (extendDim i ctx) SZero ty
2023-09-18 15:52:51 -04:00
case nchoose $ canPushCoe sg ty val of
Left pc => pushCoe defs ctx sg i ty p q val coeLoc
2023-09-17 07:54:26 -04:00
Right npc => pure $ Element (Coe (SY [< i] ty) p q val coeLoc)
(tynf `orNo` npc `orNo` notYesNo npq)
2023-09-17 13:06:07 -04:00
(_, Right ty) =>
2023-09-18 15:52:51 -04:00
whnf defs ctx sg $ Ann val ty coeLoc
2023-08-24 12:42:26 -04:00
2023-09-18 15:52:51 -04:00
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
2023-09-18 15:52:51 -04:00
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
2023-09-18 15:52:51 -04:00
K Zero _ => whnf defs ctx sg $ Ann (dsub1 zero q) ty compLoc
-- comp [A] @p @q s @1 { 1 𝑗 ⇒ t₁; ⋯ } ⇝ t₁q/𝑗 ∷ A
2023-09-18 15:52:51 -04:00
K One _ => whnf defs ctx sg $ Ann (dsub1 one q) ty compLoc
2023-09-17 07:54:26 -04:00
B {} => pure $ Element (Comp ty p q val r zero one compLoc)
(notYesNo npq `orNo` Ah)
2023-08-24 12:42:26 -04:00
2023-09-18 15:52:51 -04:00
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
case nchoose $ isAnnTyCon ty of
Left y => let Ann ty (TYPE u _) _ = ty in
reduceTypeCase defs ctx ty u ret arms def tcLoc
Right nt => pure $ Element (TypeCase ty ret arms def tcLoc)
(tynf `orNo` retnf `orNo` nt)
No _ =>
2023-09-18 15:52:51 -04:00
throw $ ClashQ tcLoc sg.qty Zero
2023-09-18 15:52:51 -04:00
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
2023-08-24 12:42:26 -04:00
covering
CanWhnf Term Interface.isRedexT where
whnf _ _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ _ t@(IOState {}) = pure $ nred t
whnf _ _ _ t@(Pi {}) = pure $ nred t
whnf _ _ _ t@(Lam {}) = pure $ nred t
whnf _ _ _ t@(Sig {}) = pure $ nred t
whnf _ _ _ t@(Pair {}) = pure $ nred t
whnf _ _ _ t@(Enum {}) = pure $ nred t
whnf _ _ _ t@(Tag {}) = pure $ nred t
whnf _ _ _ t@(Eq {}) = pure $ nred t
whnf _ _ _ t@(DLam {}) = pure $ nred t
2023-11-02 13:14:22 -04:00
whnf _ _ _ t@(NAT {}) = pure $ nred t
whnf _ _ _ t@(Nat {}) = pure $ nred t
whnf _ _ _ t@(STRING {}) = pure $ nred t
whnf _ _ _ t@(Str {}) = pure $ nred t
whnf _ _ _ t@(BOX {}) = pure $ nred t
whnf _ _ _ t@(Box {}) = pure $ nred t
2023-08-24 12:42:26 -04:00
whnf _ _ _ (Succ p loc) =
case nchoose $ isNatConst p of
Left _ => case p of
Nat p _ => pure $ nred $ Nat (S p) loc
E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
Right nc => pure $ Element (Succ p loc) $ ?cc
2023-08-24 12:42:26 -04:00
-- s ∷ A ⇝ s (in term context)
2023-09-18 15:52:51 -04:00
whnf defs ctx sg (E e) = do
Element e enf <- whnf defs ctx sg e
2023-08-24 12:42:26 -04:00
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
2023-09-18 15:52:51 -04:00
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