From cb5bd6c98c7a284c99e7691372a0742f3dc3903e Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 20 Feb 2023 21:42:31 +0100 Subject: [PATCH] make overloaded reduce stuff into interfaces this is kinda a pain so i might change it back i guess --- lib/Quox/Reduce.idr | 340 +++++++++++++++++++++----------------------- 1 file changed, 165 insertions(+), 175 deletions(-) diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr index f985624..5aec6a2 100644 --- a/lib/Quox/Reduce.idr +++ b/lib/Quox/Reduce.idr @@ -9,120 +9,129 @@ import Data.Maybe %default total -namespace Elim - public export %inline - isClo : Elim {} -> Bool - isClo (CloE {}) = True - isClo (DCloE {}) = True - isClo _ = False - - public export - 0 NotClo : Pred $ Elim {} - NotClo = No . isClo - -namespace Term - public export %inline - isClo : Term {} -> Bool - isClo (CloT {}) = True - isClo (DCloT {}) = True - isClo (E e) = isClo e - isClo _ = False - - public export - 0 NotClo : Pred $ Term {} - NotClo = No . isClo public export -0 NonCloElim : TermLike -NonCloElim q d n = Subset (Elim q d n) NotClo +0 CloTest : TermLike -> Type +CloTest tm = forall q, d, n. tm q d n -> Bool + +interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where + pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to -> + tm q dfrom from -> Subset (tm q dto to) (No . isClo) public export -0 NonCloTerm : TermLike -NonCloTerm q d n = Subset (Term q d n) NotClo +0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm q d n) +NotClo = No . isClo +public export +0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} -> + PushSubsts tm isClo => TermLike +NonClo tm q d n = Subset (tm q d n) NotClo public export %inline -ncloT : (t : Term q d n) -> (0 nc : NotClo t) => NonCloTerm q d n -ncloT t = Element t nc +nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) => + (t : tm q d n) -> (0 nc : NotClo t) => NonClo tm q d n +nclo t = Element t nc -public export %inline -ncloE : (e : Elim q d n) -> (0 nc : NotClo e) => NonCloElim q d n -ncloE e = Element e nc +parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo} + ||| if the input term has any top-level closures, push them under one layer of + ||| syntax + export %inline + pushSubsts : tm q d n -> NonClo tm q d n + pushSubsts s = pushSubstsWith id id s + export %inline + pushSubstsWith' : DSubst dfrom dto -> TSubst q dto from to -> + tm q dfrom from -> tm q dto to + pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x mutual - namespace Term - ||| if the input term has any top-level closures, push them under one layer of - ||| syntax - export %inline - pushSubsts : Term q d n -> NonCloTerm q d n - pushSubsts s = pushSubstsWith id id s + public export + isCloT : CloTest Term + isCloT (CloT {}) = True + isCloT (DCloT {}) = True + isCloT (E e) = isCloE e + isCloT _ = False - export - pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to -> - Term q dfrom from -> NonCloTerm q dto to + public export + isCloE : CloTest Elim + isCloE (CloE {}) = True + isCloE (DCloE {}) = True + isCloE _ = False + +mutual + export + PushSubsts Term Reduce.isCloT where pushSubstsWith th ph (TYPE l) = - ncloT $ TYPE l + nclo $ TYPE l pushSubstsWith th ph (Pi qty x a body) = - ncloT $ Pi qty x (subs a th ph) (subs body th ph) + nclo $ Pi qty x (subs a th ph) (subs body th ph) pushSubstsWith th ph (Lam x body) = - ncloT $ Lam x $ subs body th ph + nclo $ Lam x $ subs body th ph pushSubstsWith th ph (Sig x a b) = - ncloT $ Sig x (subs a th ph) (subs b th ph) + nclo $ Sig x (subs a th ph) (subs b th ph) pushSubstsWith th ph (Pair s t) = - ncloT $ Pair (subs s th ph) (subs t th ph) + nclo $ Pair (subs s th ph) (subs t th ph) pushSubstsWith th ph (Eq i ty l r) = - ncloT $ Eq i (subs ty th ph) (subs l th ph) (subs r th ph) + nclo $ Eq i (subs ty th ph) (subs l th ph) (subs r th ph) pushSubstsWith th ph (DLam i body) = - ncloT $ DLam i $ subs body th ph + nclo $ DLam i $ subs body th ph pushSubstsWith th ph (E e) = - let Element e nc = pushSubstsWith th ph e in ncloT $ E e + let Element e nc = pushSubstsWith th ph e in nclo $ E e pushSubstsWith th ph (CloT s ps) = pushSubstsWith th (comp th ps ph) s pushSubstsWith th ph (DCloT s ps) = pushSubstsWith (ps . th) ph s - namespace Elim - ||| if the input elimination has any top-level closures, push them under one - ||| layer of syntax - export %inline - pushSubsts : Elim q d n -> NonCloElim q d n - pushSubsts e = pushSubstsWith id id e - - export - pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to -> - Elim q dfrom from -> NonCloElim q dto to + export + PushSubsts Elim Reduce.isCloE where pushSubstsWith th ph (F x) = - ncloE $ F x + nclo $ F x pushSubstsWith th ph (B i) = let res = ph !! i in - case nchoose $ isClo res of + case nchoose $ isCloE res of Left yes => assert_total pushSubsts res Right no => Element res no pushSubstsWith th ph (f :@ s) = - ncloE $ subs f th ph :@ subs s th ph + nclo $ subs f th ph :@ subs s th ph pushSubstsWith th ph (CasePair pi p x r y z b) = - ncloE $ CasePair pi (subs p th ph) x (subs r th ph) y z (subs b th ph) + nclo $ CasePair pi (subs p th ph) x (subs r th ph) y z (subs b th ph) pushSubstsWith th ph (f :% d) = - ncloE $ subs f th ph :% (d // th) + nclo $ subs f th ph :% (d // th) pushSubstsWith th ph (s :# a) = - ncloE $ subs s th ph :# subs a th ph + nclo $ subs s th ph :# subs a th ph pushSubstsWith th ph (CloE e ps) = pushSubstsWith th (comp th ps ph) e pushSubstsWith th ph (DCloE e ps) = pushSubstsWith (ps . th) ph e -parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to) - namespace Term - public export %inline - pushSubstsWith' : Term q dfrom from -> Term q dto to - pushSubstsWith' s = (pushSubstsWith th ph s).fst - namespace Elim - public export %inline - pushSubstsWith' : Elim q dfrom from -> Elim q dto to - pushSubstsWith' e = (pushSubstsWith th ph e).fst +public export +0 RedexTest : TermLike -> Type +RedexTest tm = forall q, d, n, g. Definitions' q g -> tm q d n -> Bool + +public export +interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm where + whnf : (defs : Definitions' q g) -> + tm q d n -> Subset (tm q d n) (No . isRedex defs) + +public export +0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex => + Definitions' q g -> Pred (tm q d n) +IsRedex defs = So . isRedex defs +NotRedex defs = No . isRedex defs + +public export +0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} -> Whnf tm isRedex => + (q : Type) -> (d, n : Nat) -> {g : _} -> + (defs : Definitions' q g) -> Type +NonRedex tm q d n defs = Subset (tm q d n) (NotRedex defs) + +public export %inline +nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) => + (t : tm q d n) -> (0 nr : NotRedex defs t) => + NonRedex tm q d n defs +nred t = Element t nr public export %inline @@ -150,118 +159,99 @@ isAnn : Elim {} -> Bool isAnn (_ :# _) = True isAnn _ = False -parameters (defs : Definitions' q g) - mutual - namespace Elim - public export - isRedex : Elim q d n -> Bool - isRedex (F x) {d, n} = isJust $ lookupElim x defs {d, n} - isRedex (B _) = False - isRedex (f :@ _) = isRedex f || isLamHead f - isRedex (CasePair {pair, _}) = isRedex pair || isPairHead pair - isRedex (f :% _) = isRedex f || isDLamHead f - isRedex (t :# a) = isE t || isRedex t || isRedex a - isRedex (CloE {}) = True - isRedex (DCloE {}) = True - namespace Term - public export - isRedex : Term q d n -> Bool - isRedex (CloT {}) = True - isRedex (DCloT {}) = True - isRedex (E e) = isAnn e || isRedex e - isRedex _ = False - - namespace Elim - public export - 0 IsRedex, NotRedex : Pred $ Elim q d n - IsRedex = So . isRedex - NotRedex = No . isRedex - - namespace Term - public export - 0 IsRedex, NotRedex : Pred $ Term q d n - IsRedex = So . isRedex - NotRedex = No . isRedex - -parameters (q : Type) (d, n : Nat) {g : q -> Type} (defs : Definitions' q g) +mutual public export - 0 NonRedexElim, NonRedexTerm : Type - NonRedexElim = Subset (Elim q d n) (NotRedex defs) - NonRedexTerm = Subset (Term q d n) (NotRedex defs) + isRedexE : RedexTest Elim + isRedexE defs (F x) {d, n} = + isJust $ lookupElim x defs {d, n} + isRedexE _ (B _) = False + isRedexE defs (f :@ _) = + isRedexE defs f || isLamHead f + isRedexE defs (CasePair {pair, _}) = + isRedexE defs pair || isPairHead pair + isRedexE defs (f :% _) = + isRedexE defs f || isDLamHead f + isRedexE defs (t :# a) = + isE t || isRedexT defs t || isRedexT defs a + isRedexE _ (CloE {}) = True + isRedexE _ (DCloE {}) = True + public export + isRedexT : RedexTest Term + isRedexT _ (CloT {}) = True + isRedexT _ (DCloT {}) = True + isRedexT defs (E e) = isAnn e || isRedexE defs e + isRedexT _ _ = False -parameters (defs : Definitions' q g) - mutual - namespace Elim - export covering - whnf : Elim q d n -> NonRedexElim q d n defs - whnf (F x) with (lookupElim x defs) proof eq - _ | Just y = whnf y - _ | Nothing = Element (F x) $ rewrite eq in Ah +mutual + export covering + Whnf Elim Reduce.isRedexE where + whnf defs (F x) with (lookupElim x defs) proof eq + _ | Just y = whnf defs y + _ | Nothing = Element (F x) $ rewrite eq in Ah - whnf (B i) = Element (B i) Ah + whnf _ (B i) = nred $ B i - whnf (f :@ s) = - let Element f fnf = whnf f in - case nchoose $ isLamHead f of - Left _ => - let Lam {body, _} :# Pi {arg, res, _} = f - s = s :# arg - in - whnf $ sub1 body s :# sub1 res s - Right nlh => Element (f :@ s) $ fnf `orNo` nlh + whnf defs (f :@ s) = + let Element f fnf = whnf defs f in + case nchoose $ isLamHead f of + Left _ => + let Lam {body, _} :# Pi {arg, res, _} = f + s = s :# arg + in + whnf defs $ sub1 body s :# sub1 res s + Right nlh => Element (f :@ s) $ fnf `orNo` nlh - whnf (CasePair pi pair r ret x y body) = - let Element pair pairnf = whnf pair in - case nchoose $ isPairHead pair of - Left _ => - let Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} = pair - fst = fst :# tfst - snd = snd :# sub1 tsnd fst - in - whnf $ subN body [fst, snd] :# sub1 ret pair - Right np => - Element (CasePair pi pair r ret x y body) $ pairnf `orNo` np + whnf defs (CasePair pi pair r ret x y body) = + let Element pair pairnf = whnf defs pair in + case nchoose $ isPairHead pair of + Left _ => + let Pair {fst, snd} :# Sig {fst = tfst, snd = tsnd, _} = pair + fst = fst :# tfst + snd = snd :# sub1 tsnd fst + in + whnf defs $ subN body [fst, snd] :# sub1 ret pair + Right np => + Element (CasePair pi pair r ret x y body) $ pairnf `orNo` np - whnf (f :% p) = - let Element f fnf = whnf f in - case nchoose $ isDLamHead f of - Left _ => - let DLam {body, _} :# Eq {ty, l, r, _} = f - body = endsOr l r (dsub1 body p) p - in - whnf $ body :# dsub1 ty p - Right ndlh => - Element (f :% p) $ fnf `orNo` ndlh + whnf defs (f :% p) = + let Element f fnf = whnf defs f in + case nchoose $ isDLamHead f of + Left _ => + let DLam {body, _} :# Eq {ty, l, r, _} = f + body = endsOr l r (dsub1 body p) p + in + whnf defs $ body :# dsub1 ty p + Right ndlh => + Element (f :% p) $ fnf `orNo` ndlh - whnf (s :# a) = - let Element s snf = whnf s in - case nchoose $ isE s of - Left _ => let E e = s in Element e $ noOr2 snf - Right ne => - let Element a anf = whnf a in - Element (s :# a) $ ne `orNo` snf `orNo` anf + whnf defs (s :# a) = + let Element s snf = whnf defs s in + case nchoose $ isE s of + Left _ => let E e = s in Element e $ noOr2 snf + Right ne => + let Element a anf = whnf defs a in + Element (s :# a) $ ne `orNo` snf `orNo` anf - whnf (CloE el th) = whnf $ pushSubstsWith' id th el - whnf (DCloE el th) = whnf $ pushSubstsWith' th id el + whnf defs (CloE el th) = whnf defs $ pushSubstsWith' id th el + whnf defs (DCloE el th) = whnf defs $ pushSubstsWith' th id el - namespace Term - export covering - whnf : Term q d n -> NonRedexTerm q d n defs - whnf t@(TYPE {}) = Element t Ah - whnf t@(Pi {}) = Element t Ah - whnf t@(Lam {}) = Element t Ah - whnf t@(Sig {}) = Element t Ah - whnf t@(Pair {}) = Element t Ah - whnf t@(Eq {}) = Element t Ah - whnf t@(DLam {}) = Element t Ah + export covering + Whnf Term Reduce.isRedexT where + whnf _ t@(TYPE {}) = nred t + whnf _ t@(Pi {}) = nred t + whnf _ t@(Lam {}) = nred t + whnf _ t@(Sig {}) = nred t + whnf _ t@(Pair {}) = nred t + whnf _ t@(Eq {}) = nred t + whnf _ t@(DLam {}) = nred t - whnf (E e) = - let Element e enf = whnf e in - case nchoose $ isAnn e of - Left _ => let tm :# _ = e in Element tm $ noOr1 $ noOr2 enf - Right na => Element (E e) $ na `orNo` enf + whnf defs (E e) = + let Element e enf = whnf defs e in + case nchoose $ isAnn e of + Left _ => let tm :# _ = e in Element tm $ noOr1 $ noOr2 enf + Right na => Element (E e) $ na `orNo` enf - whnf (CloT tm th) = whnf $ pushSubstsWith' id th tm - whnf (DCloT tm th) = whnf $ pushSubstsWith' th id tm + whnf defs (CloT tm th) = whnf defs $ pushSubstsWith' id th tm + whnf defs (DCloT tm th) = whnf defs $ pushSubstsWith' th id tm