From 7895fa37e52c6571325fe55f5c5546c6bac11a95 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 19 Feb 2023 18:22:53 +0100 Subject: [PATCH] =?UTF-8?q?Q.S.T.Reduce=20=E2=87=92=20Q.Reduce=20and=20mak?= =?UTF-8?q?e=20it=20use=20Definition=20directly?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/Quox/Definition.idr | 40 --------------------------- lib/Quox/Equal.idr | 20 ++++++-------- lib/Quox/{Syntax/Term => }/Reduce.idr | 31 ++++++++++----------- lib/Quox/Syntax/Term.idr | 1 - lib/Quox/Typing.idr | 15 ++++------ lib/quox-lib.ipkg | 2 +- tests/Tests/Reduce.idr | 27 ++++++++---------- tests/TypingImpls.idr | 4 +-- 8 files changed, 43 insertions(+), 97 deletions(-) rename lib/Quox/{Syntax/Term => }/Reduce.idr (92%) diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index 557e115..a434cdc 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -88,43 +88,3 @@ public export %inline lookupElim : forall isGlobal. Name -> Definitions' q isGlobal -> Maybe (Elim q d n) lookupElim x defs = toElim !(lookup x defs) - - -parameters {0 isGlobal : _} (defs : Definitions' q isGlobal) - namespace Term - public export %inline - isRedex : Term q d n -> Bool - isRedex = isRedex $ \x => lookupElim x defs - - public export - 0 IsRedex, NotRedex : Pred $ Term q d n - IsRedex = So . isRedex - NotRedex = No . isRedex - - namespace Elim - public export %inline - isRedex : Elim q d n -> Bool - isRedex = isRedex $ \x => lookupElim x defs - - public export - 0 IsRedex, NotRedex : Pred $ Elim q d n - IsRedex = So . isRedex - NotRedex = No . isRedex - -public export -0 NonRedexElim, NonRedexTerm : - (q : Type) -> (d, n : Nat) -> {isGlobal : Pred q} -> - Definitions' q isGlobal -> Type -NonRedexElim q d n defs = Subset (Elim q d n) (NotRedex defs) -NonRedexTerm q d n defs = Subset (Term q d n) (NotRedex defs) - -parameters {0 isGlobal : _} (defs : Definitions' q isGlobal) - namespace Term - export covering %inline - whnfD : Term q d n -> NonRedexTerm q d n defs - whnfD = whnf $ \x => lookupElim x defs - - namespace Elim - export covering %inline - whnfD : Elim q d n -> NonRedexElim q d n defs - whnfD = whnf $ \x => lookupElim x defs diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index f741131..444b920 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -1,7 +1,5 @@ module Quox.Equal -import public Quox.Syntax -import public Quox.Definition import public Quox.Typing import public Control.Monad.Either import public Control.Monad.Reader @@ -83,7 +81,7 @@ parameters (defs : Definitions' q g) public export isSubSing : Term q 0 n -> Bool isSubSing ty = - let Element ty nc = whnfD defs ty in + let Element ty nc = whnf defs ty in case ty of TYPE _ => False Pi {res, _} => isSubSing res.term @@ -118,9 +116,9 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0 : TContext q 0 n -> (ty, s, t : Term q 0 n) -> m () compare0 ctx ty s t = wrapErr (WhileComparingT (MkTyContext new ctx) !mode ty s t) $ do - let Element ty nty = whnfD defs ty - Element s ns = whnfD defs s - Element t nt = whnfD defs t + let Element ty nty = whnf defs ty + Element s ns = whnf defs s + Element t nt = whnf defs t tty <- ensureTyCon ty compare0' ctx ty s t @@ -192,8 +190,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} export covering %inline compareType : TContext q 0 n -> (s, t : Term q 0 n) -> m () compareType ctx s t = do - let Element s ns = whnfD defs s - Element t nt = whnfD defs t + let Element s ns = whnf defs s + Element t nt = whnf defs t ts <- ensureTyCon s tt <- ensureTyCon t st <- either pure (const $ clashT (TYPE UAny) s t) $ @@ -245,7 +243,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compareType' ctx (E e) (E f) = do -- no fanciness needed here cos anything other than a neutral - -- has been inlined by whnfD + -- has been inlined by whnf Elim.compare0 ctx e f ||| performs the minimum work required to recompute the type of an elim. @@ -291,8 +289,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)} compare0 : TContext q 0 n -> (e, f : Elim q 0 n) -> m () compare0 ctx e f = wrapErr (WhileComparingE (MkTyContext new ctx) !mode e f) $ do - let Element e ne = whnfD defs e - Element f nf = whnfD defs f + let Element e ne = whnf defs e + Element f nf = whnf defs f -- [fixme] there is a better way to do this "isSubSing" stuff for sure unless (isSubSing defs !(computeElimType ctx e ne)) $ compare0' ctx e f ne nf diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Reduce.idr similarity index 92% rename from lib/Quox/Syntax/Term/Reduce.idr rename to lib/Quox/Reduce.idr index b101dc8..f985624 100644 --- a/lib/Quox/Syntax/Term/Reduce.idr +++ b/lib/Quox/Reduce.idr @@ -1,8 +1,8 @@ -module Quox.Syntax.Term.Reduce +module Quox.Reduce import Quox.No -import Quox.Syntax.Term.Base -import Quox.Syntax.Term.Subst +import Quox.Syntax +import Quox.Definition import Data.Vect import Data.Maybe @@ -125,10 +125,6 @@ parameters (th : DSubst dfrom dto) (ph : TSubst q dto from to) pushSubstsWith' e = (pushSubstsWith th ph e).fst -public export 0 -Lookup : TermLike -Lookup q d n = Name -> Maybe $ Elim q d n - public export %inline isLamHead : Elim {} -> Bool isLamHead (Lam {} :# Pi {}) = True @@ -154,12 +150,12 @@ isAnn : Elim {} -> Bool isAnn (_ :# _) = True isAnn _ = False -parameters (g : Lookup q d n) +parameters (defs : Definitions' q g) mutual namespace Elim public export isRedex : Elim q d n -> Bool - isRedex (F x) = isJust $ g x + 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 @@ -188,18 +184,19 @@ parameters (g : Lookup q d n) IsRedex = So . isRedex NotRedex = No . isRedex -public export -0 NonRedexElim, NonRedexTerm : (q, d, n : _) -> Lookup q d n -> Type -NonRedexElim q d n g = Subset (Elim q d n) (NotRedex g) -NonRedexTerm q d n g = Subset (Term q d n) (NotRedex g) +parameters (q : Type) (d, n : Nat) {g : q -> Type} (defs : Definitions' q g) + public export + 0 NonRedexElim, NonRedexTerm : Type + NonRedexElim = Subset (Elim q d n) (NotRedex defs) + NonRedexTerm = Subset (Term q d n) (NotRedex defs) -parameters (g : Lookup q d n) +parameters (defs : Definitions' q g) mutual namespace Elim export covering - whnf : Elim q d n -> NonRedexElim q d n g - whnf (F x) with (g x) proof eq + 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 @@ -251,7 +248,7 @@ parameters (g : Lookup q d n) namespace Term export covering - whnf : Term q d n -> NonRedexTerm q d n g + 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 diff --git a/lib/Quox/Syntax/Term.idr b/lib/Quox/Syntax/Term.idr index f9acfe6..76894ec 100644 --- a/lib/Quox/Syntax/Term.idr +++ b/lib/Quox/Syntax/Term.idr @@ -3,5 +3,4 @@ module Quox.Syntax.Term import public Quox.Syntax.Term.Base import public Quox.Syntax.Term.Split import public Quox.Syntax.Term.Subst -import public Quox.Syntax.Term.Reduce import public Quox.Syntax.Term.Pretty diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index f473788..7de1e4c 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -1,14 +1,11 @@ module Quox.Typing import public Quox.Syntax -import public Quox.Context import public Quox.Definition +import public Quox.Reduce -import Data.Nat import public Data.SortedMap -import Control.Monad.Either -import Control.Monad.Reader -import Control.Monad.State +import public Control.Monad.Either import Generics.Derive %hide TT.Name @@ -206,27 +203,27 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _) export covering %inline expectTYPE : Term q d n -> m Universe expectTYPE s = - case fst $ whnfD defs s of + case fst $ whnf defs s of TYPE l => pure l _ => throwError $ ExpectedTYPE s export covering %inline expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n) expectPi s = - case fst $ whnfD defs s of + case fst $ whnf defs s of Pi {qty, arg, res, _} => pure (qty, arg, res) _ => throwError $ ExpectedPi s export covering %inline expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n) expectSig s = - case fst $ whnfD defs s of + case fst $ whnf defs s of Sig {fst, snd, _} => pure (fst, snd) _ => throwError $ ExpectedSig s export covering %inline expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) expectEq s = - case fst $ whnfD defs s of + case fst $ whnf defs s of Eq {ty, l, r, _} => pure (ty, l, r) _ => throwError $ ExpectedEq s diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 2407bf9..064cee6 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -22,12 +22,12 @@ modules = Quox.Syntax.Term, Quox.Syntax.Term.Base, Quox.Syntax.Term.Pretty, - Quox.Syntax.Term.Reduce, Quox.Syntax.Term.Split, Quox.Syntax.Term.Subst, Quox.Syntax.Universe, Quox.Syntax.Var, Quox.Definition, + Quox.Reduce, Quox.Context, Quox.Equal, Quox.Name, diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index bb5b3a8..59e8348 100644 --- a/tests/Tests/Reduce.idr +++ b/tests/Tests/Reduce.idr @@ -8,35 +8,30 @@ import TAP testWhnf : Eq b => Show b => (a -> (Subset b _)) -> String -> a -> b -> Test -testWhnf whnf label from to = test "\{label} (whnf)" $ - let result = fst (whnf from) in - if result == to - then Right () - else with Prelude.(::) - Left [("expected", to), ("received", result)] +testWhnf whnf label from to = test "\{label} (whnf)" $ do + let result = fst (whnf from) + unless (result == to) $ + Left [("exp", to), ("got", result)] {a = List (String, b)} testNoStep : Eq a => Show a => (a -> (Subset a _)) -> String -> a -> Test -testNoStep whnf label e = test "\{label} (no step)" $ - let result = fst (whnf e) in - if result == e - then Right () - else with Prelude.(::) - Left [("reduced", result)] +testNoStep whnf label e = test "\{label} (no step)" $ do + let result = fst (whnf e) + unless (result == e) $ Left [("reduced", result)] {a = List (String, a)} parameters {default empty defs : Definitions Three} {default 0 d, n : Nat} testWhnfT : String -> Term Three d n -> Term Three d n -> Test - testWhnfT = testWhnf (whnfD defs) + testWhnfT = testWhnf (whnf defs) testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test - testWhnfE = testWhnf (whnfD defs) + testWhnfE = testWhnf (whnf defs) testNoStepE : String -> Elim Three d n -> Test - testNoStepE = testNoStep (whnfD defs) + testNoStepE = testNoStep (whnf defs) testNoStepT : String -> Term Three d n -> Test - testNoStepT = testNoStep (whnfD defs) + testNoStepT = testNoStep (whnf defs) tests = "whnf" :- [ diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index be9ebb8..c09139c 100644 --- a/tests/TypingImpls.idr +++ b/tests/TypingImpls.idr @@ -50,8 +50,8 @@ PrettyHL q => ToInfo (Error q) where ("left", prettyStr True p), ("right", prettyStr True q)] toInfo (NotType ty) = - [("type", "NotType"), - ("actual", prettyStr True ty)] + [("type", "NotType"), + ("got", prettyStr True ty)] toInfo (WrongType ty s t) = [("type", "WrongType"), ("ty", prettyStr True ty),