From 92617a2e4a5aaa4d4664b1a77a91f96a8cc8f246 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 23 Jan 2023 00:53:34 +0100 Subject: [PATCH] whnf actually reduces to whnf now (probably) --- exe/Main.idr | 2 +- lib/Quox/Definition.idr | 52 ++++ lib/Quox/Equal.idr | 330 ++++++++++------------ lib/Quox/No.idr | 54 ++++ lib/Quox/Syntax/Dim.idr | 5 + lib/Quox/Syntax/Term/Base.idr | 19 +- lib/Quox/Syntax/Term/Reduce.idr | 468 +++++++++++++------------------- lib/Quox/Typechecker.idr | 30 +- lib/quox-lib.ipkg | 1 + tests/Tests/Equal.idr | 378 ++++++++++++++------------ tests/Tests/Reduce.idr | 33 ++- 11 files changed, 693 insertions(+), 679 deletions(-) create mode 100644 lib/Quox/No.idr diff --git a/exe/Main.idr b/exe/Main.idr index bee32d7..1470184 100644 --- a/exe/Main.idr +++ b/exe/Main.idr @@ -64,4 +64,4 @@ main : IO Unit main = do putStrLn $ banner defPrettyOpts prettyTermDef tm - prettyTermDef $ pushSubstsT tm + prettyTermDef $ pushSubsts tm diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index eb7bcd4..b8c55fe 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -1,5 +1,6 @@ module Quox.Definition +import public Quox.No import public Quox.Syntax import public Data.SortedMap import public Control.Monad.Reader @@ -47,6 +48,11 @@ public export %inline g.qtyP = Element g.qty g.qtyGlobal +public export %inline +toElim : Definition' q _ -> Maybe $ Elim q d n +toElim def = pure $ (!def.term).get :# def.type.get + + public export 0 IsZero : IsQty q => Pred $ Definition q IsZero g = IsZero g.qty @@ -72,3 +78,49 @@ HasDefs' q isGlobal = MonadReader (Definitions' q isGlobal) public export 0 HasDefs : (q : Type) -> IsQty q => (Type -> Type) -> Type HasDefs q = HasDefs' q IsGlobal + + +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 %inline + whnf : Term q d n -> NonRedexTerm q d n defs + whnf = whnf $ \x => lookupElim x defs + + namespace Elim + export %inline + whnf : Elim q d n -> NonRedexElim q d n defs + whnf = whnf $ \x => lookupElim x defs diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 7a3185f..fb15c82 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -14,63 +14,40 @@ ClashE mode = ClashT mode `on` E public export -record Env' q (isGlobal : q -> Type) where +record Env where constructor MakeEnv - defs : Definitions' q isGlobal mode : EqMode -public export -0 Env : (q : Type) -> IsQty q => Type -Env q = Env' q IsGlobal public export -0 HasEnv' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type -HasEnv' q isGlobal = MonadReader (Env' q isGlobal) +0 HasEnv : (Type -> Type) -> Type +HasEnv = MonadReader Env public export -0 HasEnv : (q : Type) -> IsQty q => (Type -> Type) -> Type -HasEnv q = HasEnv' q IsGlobal - - -public export -0 CanEqual' : (q : Type) -> (q -> Type) -> (Type -> Type) -> Type -CanEqual' q isGlobal m = (HasErr q m, HasEnv' q isGlobal m) - -public export -0 CanEqual : (q : Type) -> IsQty q => (Type -> Type) -> Type -CanEqual q = CanEqual' q IsGlobal +0 CanEqual : (q : Type) -> (Type -> Type) -> Type +CanEqual q m = (HasErr q m, HasEnv m) private %inline -mode : HasEnv' _ _ m => m EqMode +mode : HasEnv m => m EqMode mode = asks mode private %inline -clashT : CanEqual' q _ m => Term q d n -> Term q d n -> m a +clashT : CanEqual q m => Term q d n -> Term q d n -> m a clashT s t = throwError $ ClashT !mode s t private %inline -clashE : CanEqual' q _ m => Elim q d n -> Elim q d n -> m a +clashE : CanEqual q m => Elim q d n -> Elim q d n -> m a clashE e f = throwError $ ClashE !mode e f -private %inline -defE : HasEnv' q _ m => Name -> m (Maybe (Elim q d n)) -defE x = asks $ \env => do - g <- lookup x env.defs - pure $ (!g.term).get :# g.type.get - -private %inline -defT : HasEnv' q _ m => Name -> m (Maybe (Term q d n)) -defT x = map E <$> defE x - export %inline -compareU' : HasEnv' q _ m => Universe -> Universe -> m Bool +compareU' : HasEnv m => Universe -> Universe -> m Bool compareU' i j = pure $ case !mode of Equal => i == j; Sub => i <= j export %inline -compareU : CanEqual' q _ m => Universe -> Universe -> m () +compareU : CanEqual q m => Universe -> Universe -> m () compareU k l = unless !(compareU' k l) $ throwError $ ClashU !mode k l @@ -79,185 +56,150 @@ compareD : HasErr q m => Dim d -> Dim d -> m () compareD p q = unless (p == q) $ throwError $ ClashD p q -mutual - private covering - compareTN' : CanEqual' q _ m => Eq q => - (s, t : Term q 0 n) -> - (0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m () - compareTN' (E e) (E f) ps pt = compareE0 e f - -- if either term is a def, try to unfold it - compareTN' s@(E (F x)) t ps pt = do - Just s' <- defT x | Nothing => clashT s t - compareT0 s' t - compareTN' s t@(E (F y)) ps pt = do - Just t' <- defT y | Nothing => clashT s t - compareT0 s t' - compareTN' s@(E _) t _ _ = clashT s t +parameters {0 isGlobal : _} (defs : Definitions' q isGlobal) + mutual + namespace Term + export covering + compareN' : CanEqual q m => Eq q => + (s, t : Term q 0 n) -> + (0 _ : NotRedex defs s) -> (0 _ : NotRedex defs t) -> + m () - compareTN' (TYPE k) (TYPE l) _ _ = compareU k l - compareTN' s@(TYPE _) t _ _ = clashT s t + compareN' (TYPE k) (TYPE l) _ _ = compareU k l + compareN' s@(TYPE _) t _ _ = clashT s t - compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do - unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2 - compareT0 arg2 arg1 -- reversed for contravariant domain - compareST0 res1 res2 - compareTN' s@(Pi {}) t _ _ = clashT s t + compareN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do + unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2 + compare0 arg2 arg1 -- reversed for contravariant domain + compare0 res1 res2 + compareN' s@(Pi {}) t _ _ = clashT s t - -- [todo] eta - compareTN' (Lam _ body1) (Lam _ body2) _ _ = - local {mode := Equal} $ compareST0 body1 body2 - compareTN' s@(Lam {}) t _ _ = clashT s t + -- [todo] eta + compareN' (Lam _ body1) (Lam _ body2) _ _ = + local {mode := Equal} $ compare0 body1 body2 + compareN' s@(Lam {}) t _ _ = clashT s t - compareTN' (Eq _ ty1 l1 r1) (Eq _ ty2 l2 r2) _ _ = do - compareDST0 ty1 ty2 - local {mode := Equal} $ do - compareT0 l1 l2 - compareT0 r1 r2 - compareTN' s@(Eq {}) t _ _ = clashT s t + compareN' (Eq _ ty1 l1 r1) (Eq _ ty2 l2 r2) _ _ = do + compare0 ty1 ty2 + local {mode := Equal} $ do + compare0 l1 l2 + compare0 r1 r2 + compareN' s@(Eq {}) t _ _ = clashT s t - compareTN' (DLam _ body1) (DLam _ body2) _ _ = - compareDST0 body1 body2 - compareTN' s@(DLam {}) t _ _ = clashT s t + compareN' (DLam _ body1) (DLam _ body2) _ _ = + compare0 body1 body2 + compareN' s@(DLam {}) t _ _ = clashT s t - compareTN' (CloT {}) _ ps _ = void $ ps IsCloT - compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT + compareN' (E e) (E f) ne nf = compareN' e f (noOr2 ne) (noOr2 nf) + compareN' s@(E e) t _ _ = clashT s t - private covering - compareEN' : CanEqual' q _ m => Eq q => - (e, f : Elim q 0 n) -> - (0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m () + namespace Elim + export covering + compareN' : CanEqual q m => Eq q => + (e, f : Elim q 0 n) -> + (0 _ : NotRedex defs e) -> (0 _ : NotRedex defs f) -> + m () - compareEN' e@(F x) f@(F y) _ _ = - if x == y then pure () else - case (!(defE x), !(defE y)) of - (Nothing, Nothing) => clashE e f - (s', t') => compareE0 (fromMaybe e s') (fromMaybe f t') - compareEN' e@(F x) f _ _ = do - Just e' <- defE x | Nothing => clashE e f - compareE0 e' f - compareEN' e f@(F y) _ _ = do - Just f' <- defE y | Nothing => clashE e f - compareE0 e f' + compareN' e@(F x) f@(F y) _ _ = + unless (x == y) $ clashE e f + compareN' e@(F _) f _ _ = clashE e f - compareEN' e@(B i) f@(B j) _ _ = - unless (i == j) $ clashE e f - compareEN' e@(B _) f _ _ = clashE e f + compareN' e@(B i) f@(B j) _ _ = + unless (i == j) $ clashE e f + compareN' e@(B _) f _ _ = clashE e f - -- [todo] tracking variance of functions? maybe??? - -- probably not - compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ = - local {mode := Equal} $ do - compareE0 fun1 fun2 - compareT0 arg1 arg2 - compareEN' e@(_ :@ _) f _ _ = clashE e f + -- [todo] tracking variance of functions? maybe??? + -- probably not + compareN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ = + local {mode := Equal} $ do + compare0 fun1 fun2 + compare0 arg1 arg2 + compareN' e@(_ :@ _) f _ _ = clashE e f - compareEN' (fun1 :% dim1) (fun2 :% dim2) _ _ = do - compareE0 fun1 fun2 - compareD dim1 dim2 - compareEN' e@(_ :% _) f _ _ = clashE e f + -- retain the mode unlike above because dimensions can't do + -- anything that would mess up variance + compareN' (fun1 :% dim1) (fun2 :% dim2) _ _ = do + compare0 fun1 fun2 + compareD dim1 dim2 + compareN' e@(_ :% _) f _ _ = clashE e f - -- [todo] is always checking the types are equal correct? - compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do - compareT0 tm1 tm2 - local {mode := Equal} $ compareT0 ty1 ty2 - compareEN' e@(_ :# _) f _ _ = clashE e f - - compareEN' (CloE {}) _ pe _ = void $ pe IsCloE - compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE + -- using the same mode for the type allows, e.g. + -- A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B + -- which, since A : ★₁ implies A : ★₃, should be fine + compareN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do + compare0 tm1 tm2 + compare0 ty1 ty2 + compareN' e@(_ :# _) f _ _ = clashE e f - private covering %inline - compareTN : CanEqual' q _ m => Eq q => - NonRedexTerm q 0 n -> NonRedexTerm q 0 n -> m () - compareTN s t = compareTN' s.fst t.fst s.snd t.snd + namespace Term + export covering %inline + compareN : CanEqual q m => Eq q => + NonRedexTerm q 0 n defs -> NonRedexTerm q 0 n defs -> m () + compareN s t = compareN' s.fst t.fst s.snd t.snd - private covering %inline - compareEN : CanEqual' q _ m => Eq q => - NonRedexElim q 0 n -> NonRedexElim q 0 n -> m () - compareEN e f = compareEN' e.fst f.fst e.snd f.snd + export covering %inline + compare : CanEqual q m => Eq q => + DimEq d -> Term q d n -> Term q d n -> m () + compare eqs s t = + for_ (splits eqs) $ \th => compare0 (s /// th) (t /// th) + + export covering %inline + compare0 : CanEqual q m => Eq q => Term q 0 n -> Term q 0 n -> m () + compare0 s t = compareN (whnf defs s) (whnf defs t) + + namespace Elim + covering %inline + compareN : CanEqual q m => Eq q => + NonRedexElim q 0 n defs -> NonRedexElim q 0 n defs -> m () + compareN e f = compareN' e.fst f.fst e.snd f.snd + + export covering %inline + compare : CanEqual q m => Eq q => + DimEq d -> Elim q d n -> Elim q d n -> m () + compare eqs e f = + for_ (splits eqs) $ \th => compare0 (e /// th) (f /// th) + + export covering %inline + compare0 : CanEqual q m => Eq q => Elim q 0 n -> Elim q 0 n -> m () + compare0 e f = compareN (whnf defs e) (whnf defs f) + + namespace ScopeTerm + export covering %inline + compare0 : CanEqual q m => Eq q => + ScopeTerm q 0 n -> ScopeTerm q 0 n -> m () + compare0 (TUnused body0) (TUnused body1) = compare0 body0 body1 + compare0 body0 body1 = compare0 body0.term body1.term + + namespace DScopeTerm + export covering %inline + compare0 : CanEqual q m => Eq q => + DScopeTerm q 0 n -> DScopeTerm q 0 n -> m () + compare0 (DUnused body0) (DUnused body1) = compare0 body0 body1 + compare0 body0 body1 = do + compare0 body0.zero body1.zero + compare0 body0.one body1.one - export covering %inline - compareT : CanEqual' q _ m => Eq q => - DimEq d -> Term q d n -> Term q d n -> m () - compareT eqs s t = - for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th) + namespace Term + export covering %inline + equal : HasErr q m => Eq q => + DimEq d -> Term q d n -> Term q d n -> m () + equal eqs s t {m} = runReaderT {m} (MakeEnv Equal) $ compare eqs s t - export covering %inline - compareE : CanEqual' q _ m => Eq q => - DimEq d -> Elim q d n -> Elim q d n -> m () - compareE eqs e f = - for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th) + export covering %inline + sub : HasErr q m => HasDefs' q _ m => Eq q => + DimEq d -> Term q d n -> Term q d n -> m () + sub eqs s t {m} = runReaderT {m} (MakeEnv Sub) $ compare eqs s t + namespace Elim + export covering %inline + equal : HasErr q m => Eq q => + DimEq d -> Elim q d n -> Elim q d n -> m () + equal eqs e f {m} = runReaderT {m} (MakeEnv Equal) $ compare eqs e f - export covering %inline - compareT0 : CanEqual' q _ m => Eq q => Term q 0 n -> Term q 0 n -> m () - compareT0 s t = compareTN (whnfT s) (whnfT t) - - export covering %inline - compareE0 : CanEqual' q _ m => Eq q => Elim q 0 n -> Elim q 0 n -> m () - compareE0 e f = compareEN (whnfE e) (whnfE f) - - export covering %inline - compareST0 : CanEqual' q _ m => Eq q => - ScopeTerm q 0 n -> ScopeTerm q 0 n -> m () - compareST0 (TUnused body0) (TUnused body1) = compareT0 body0 body1 - compareST0 body0 body1 = compareT0 body0.term body1.term - - export covering %inline - compareDST0 : CanEqual' q _ m => Eq q => - DScopeTerm q 0 n -> DScopeTerm q 0 n -> m () - compareDST0 (DUnused body0) (DUnused body1) = compareT0 body0 body1 - compareDST0 body0 body1 = do - compareT0 body0.zero body1.zero - compareT0 body0.one body1.one - - -private %inline -into : HasErr q m => HasDefs' q isg m => Eq q => - (forall n. HasErr q n => HasEnv' q isg n => d -> a -> a -> n ()) -> - EqMode -> d -> a -> a -> m () -into f mode eqs a b = - runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b - -export covering %inline -equalTWith : HasErr q m => HasDefs' q _ m => Eq q => - DimEq d -> Term q d n -> Term q d n -> m () -equalTWith = into compareT Equal - -export covering %inline -equalEWith : HasErr q m => HasDefs' q _ m => Eq q => - DimEq d -> Elim q d n -> Elim q d n -> m () -equalEWith = into compareE Equal - -export covering %inline -subTWith : HasErr q m => HasDefs' q _ m => Eq q => - DimEq d -> Term q d n -> Term q d n -> m () -subTWith = into compareT Sub - -export covering %inline -subEWith : HasErr q m => HasDefs' q _ m => Eq q => - DimEq d -> Elim q d n -> Elim q d n -> m () -subEWith = into compareE Sub - - -export covering %inline -equalT : HasErr q m => HasDefs' q _ m => Eq q => - {d : Nat} -> Term q d n -> Term q d n -> m () -equalT = equalTWith DimEq.new - -export covering %inline -equalE : HasErr q m => HasDefs' q _ m => Eq q => - {d : Nat} -> Elim q d n -> Elim q d n -> m () -equalE = equalEWith DimEq.new - -export covering %inline -subT : HasErr q m => HasDefs' q _ m => Eq q => - {d : Nat} -> Term q d n -> Term q d n -> m () -subT = subTWith DimEq.new - -export covering %inline -subE : HasErr q m => HasDefs' q _ m => Eq q => - {d : Nat} -> Elim q d n -> Elim q d n -> m () -subE = subEWith DimEq.new + export covering %inline + sub : HasErr q m => HasDefs' q _ m => Eq q => + DimEq d -> Elim q d n -> Elim q d n -> m () + sub eqs e f {m} = runReaderT {m} (MakeEnv Sub) $ compare eqs e f diff --git a/lib/Quox/No.idr b/lib/Quox/No.idr new file mode 100644 index 0000000..948eaf6 --- /dev/null +++ b/lib/Quox/No.idr @@ -0,0 +1,54 @@ +||| like Data.So, but for False instead. +||| less messing about with `not` (and constantly rewriting everything) +||| or `Not` (unfriendly to proof search). +module Quox.No + +import public Data.So +import public Quox.Decidable +import Data.Bool + +public export +data No : Pred Bool where + Ah : No False + +export Uninhabited (No True) where uninhabited _ impossible + +export %inline +soNo : So b -> No b -> Void +soNo Oh Ah impossible + + +private +0 orFalse : (a, b : Bool) -> (a || b) = False -> (a = False, b = False) +orFalse a b eq1 with (a || b) proof eq2 + orFalse False False Refl | False = (Refl, Refl) + orFalse False True Refl | False = absurd eq2 + orFalse True False Refl | False = absurd eq2 + orFalse True True Refl | False = absurd eq2 + +parameters {0 a, b : Bool} + export %inline + noOr : No (a || b) -> (No a, No b) + noOr n with 0 (a || b) proof eq + noOr Ah | False = + let 0 eqs = orFalse a b eq in + (rewrite fst eqs in Ah, rewrite snd eqs in Ah) + + export %inline + noOr1 : No (a || b) -> No a + noOr1 = fst . noOr + + export %inline + noOr2 : No (a || b) -> No b + noOr2 = snd . noOr + + +infixr 1 `orNo` +export %inline +orNo : No a -> No b -> No (a || b) +orNo Ah Ah = Ah + +export %inline +nchoose : (b : Bool) -> Either (So b) (No b) +nchoose True = Left Oh +nchoose False = Right Ah diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr index 102f6f7..01cd6dc 100644 --- a/lib/Quox/Syntax/Dim.idr +++ b/lib/Quox/Syntax/Dim.idr @@ -19,6 +19,11 @@ data DimConst = Zero | One %runElab derive "DimConst" [Generic, Meta, Eq, Ord, DecEq, Show] +public export +pick : a -> a -> DimConst -> a +pick x y Zero = x +pick x y One = y + public export data Dim : Nat -> Type where diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 665e0fc..afff7e2 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -22,18 +22,27 @@ import Data.Vect %default total +public export +0 TermLike : Type +TermLike = Type -> Nat -> Nat -> Type + +public export +0 TSubstLike : Type +TSubstLike = Type -> Nat -> Nat -> Nat -> Type + + infixl 8 :# infixl 9 :@, :% mutual public export - 0 TSubst : Type -> Nat -> Nat -> Nat -> Type + 0 TSubst : TSubstLike TSubst q d = Subst $ Elim q d ||| first argument `q` is quantity type; ||| second argument `d` is dimension scope size; ||| third `n` is term scope size public export - data Term : (q : Type) -> (d, n : Nat) -> Type where + data Term : TermLike where ||| type of types TYPE : (l : Universe) -> Term q d n @@ -61,7 +70,7 @@ mutual ||| first argument `d` is dimension scope size, second `n` is term scope size public export - data Elim : (q : Type) -> (d, n : Nat) -> Type where + data Elim : TermLike where ||| free variable F : (x : Name) -> Elim q d n ||| bound variable @@ -85,7 +94,7 @@ mutual ||| a scope with one more bound variable public export - data ScopeTerm : (q : Type) -> (d, n : Nat) -> Type where + data ScopeTerm : TermLike where ||| variable is used TUsed : (body : Term q d (S n)) -> ScopeTerm q d n ||| variable is unused @@ -93,7 +102,7 @@ mutual ||| a scope with one more bound dimension variable public export - data DScopeTerm : (q : Type) -> (d, n : Nat) -> Type where + data DScopeTerm : TermLike where ||| variable is used DUsed : (body : Term q (S d) n) -> DScopeTerm q d n ||| variable is unused diff --git a/lib/Quox/Syntax/Term/Reduce.idr b/lib/Quox/Syntax/Term/Reduce.idr index 44e65fa..b51662a 100644 --- a/lib/Quox/Syntax/Term/Reduce.idr +++ b/lib/Quox/Syntax/Term/Reduce.idr @@ -1,136 +1,121 @@ module Quox.Syntax.Term.Reduce +import Quox.No import Quox.Syntax.Term.Base import Quox.Syntax.Term.Subst +import Data.Maybe %default total -mutual - public export - data NotCloT : Term {} -> Type where - NCTYPE : NotCloT $ TYPE _ - NCPi : NotCloT $ Pi {} - NCLam : NotCloT $ Lam {} - NCEq : NotCloT $ Eq {} - NCDLam : NotCloT $ DLam {} - NCE : NotCloE e -> NotCloT $ E e +namespace Elim + public export %inline + isClo : Elim {} -> Bool + isClo (CloE {}) = True + isClo (DCloE {}) = True + isClo _ = False public export - data NotCloE : Elim {} -> Type where - NCF : NotCloE $ F _ - NCB : NotCloE $ B _ - NCApp : NotCloE $ _ :@ _ - NCDApp : NotCloE $ _ :% _ - NCAnn : NotCloE $ _ :# _ + 0 NotClo : Pred $ Elim {} + NotClo = No . isClo -mutual - export - notCloT : (t : Term {}) -> Dec (NotCloT t) - notCloT (TYPE _) = Yes NCTYPE - notCloT (Pi {}) = Yes NCPi - notCloT (Lam {}) = Yes NCLam - notCloT (Eq {}) = Yes NCEq - notCloT (DLam {}) = Yes NCDLam - notCloT (E e) = case notCloE e of - Yes nc => Yes $ NCE nc - No c => No $ \case NCE nc => c nc - notCloT (CloT {}) = No $ \case _ impossible - notCloT (DCloT {}) = No $ \case _ impossible +namespace Term + public export %inline + isClo : Term {} -> Bool + isClo (CloT {}) = True + isClo (DCloT {}) = True + isClo (E e) = isClo e + isClo _ = False - export - notCloE : (e : Elim {}) -> Dec (NotCloE e) - notCloE (F _) = Yes NCF - notCloE (B _) = Yes NCB - notCloE (_ :@ _) = Yes NCApp - notCloE (_ :% _) = Yes NCDApp - notCloE (_ :# _) = Yes NCAnn - notCloE (CloE {}) = No $ \case _ impossible - notCloE (DCloE {}) = No $ \case _ impossible + public export + 0 NotClo : Pred $ Term {} + NotClo = No . isClo -||| a term which is not a top level closure public export -NonCloTerm : Type -> Nat -> Nat -> Type -NonCloTerm q d n = Subset (Term q d n) NotCloT +0 NonCloElim : TermLike +NonCloElim q d n = Subset (Elim q d n) NotClo -||| an elimination which is not a top level closure public export -NonCloElim : Type -> Nat -> Nat -> Type -NonCloElim q d n = Subset (Elim q d n) NotCloE +0 NonCloTerm : TermLike +NonCloTerm q d n = Subset (Term q d n) NotClo + public export %inline -ncloT : (t : Term q d n) -> (0 _ : NotCloT t) => NonCloTerm q d n -ncloT t @{p} = Element t p +ncloT : (t : Term q d n) -> (0 nc : NotClo t) => NonCloTerm q d n +ncloT t = Element t nc public export %inline -ncloE : (e : Elim q d n) -> (0 _ : NotCloE e) => NonCloElim q d n -ncloE e @{p} = Element e p - +ncloE : (e : Elim q d n) -> (0 nc : NotClo e) => NonCloElim q d n +ncloE e = Element e nc mutual - ||| if the input term has any top-level closures, push them under one layer of - ||| syntax - export %inline - pushSubstsT : Term q d n -> NonCloTerm q d n - pushSubstsT s = pushSubstsTWith id id s + 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 - ||| if the input elimination has any top-level closures, push them under one - ||| layer of syntax - export %inline - pushSubstsE : Elim q d n -> NonCloElim q d n - pushSubstsE e = pushSubstsEWith id id e + export + pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to -> + Term q dfrom from -> NonCloTerm q dto to + pushSubstsWith th ph (TYPE l) = + ncloT $ TYPE l + pushSubstsWith th ph (Pi qty x a body) = + ncloT $ Pi qty x (subs a th ph) (subs body th ph) + pushSubstsWith th ph (Lam x body) = + ncloT $ Lam x $ subs body 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) + pushSubstsWith th ph (DLam i body) = + ncloT $ DLam i $ subs body th ph + pushSubstsWith th ph (E e) = + let Element e nc = pushSubstsWith th ph e in ncloT $ 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 - export - pushSubstsTWith : DSubst dfrom dto -> TSubst q dto from to -> - Term q dfrom from -> NonCloTerm q dto to - pushSubstsTWith th ph (TYPE l) = - ncloT $ TYPE l - pushSubstsTWith th ph (Pi qty x a body) = - ncloT $ Pi qty x (subs a th ph) (subs body th ph) - pushSubstsTWith th ph (Lam x body) = - ncloT $ Lam x $ subs body th ph - pushSubstsTWith th ph (Eq i ty l r) = - ncloT $ Eq i (subs ty th ph) (subs l th ph) (subs r th ph) - pushSubstsTWith th ph (DLam i body) = - ncloT $ DLam i $ subs body th ph - pushSubstsTWith th ph (E e) = - let Element e nc = pushSubstsEWith th ph e in ncloT $ E e - pushSubstsTWith th ph (CloT s ps) = - pushSubstsTWith th (comp th ps ph) s - pushSubstsTWith th ph (DCloT s ps) = - pushSubstsTWith (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 - pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to -> - Elim q dfrom from -> NonCloElim q dto to - pushSubstsEWith th ph (F x) = - ncloE $ F x - pushSubstsEWith th ph (B i) = - let res = ph !! i in - case notCloE res of - Yes _ => ncloE res - No _ => assert_total pushSubstsE res - pushSubstsEWith th ph (f :@ s) = - ncloE $ subs f th ph :@ subs s th ph - pushSubstsEWith th ph (f :% d) = - ncloE $ subs f th ph :% (d // th) - pushSubstsEWith th ph (s :# a) = - ncloE $ subs s th ph :# subs a th ph - pushSubstsEWith th ph (CloE e ps) = - pushSubstsEWith th (comp th ps ph) e - pushSubstsEWith th ph (DCloE e ps) = - pushSubstsEWith (ps . th) ph e + export + pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to -> + Elim q dfrom from -> NonCloElim q dto to + pushSubstsWith th ph (F x) = + ncloE $ F x + pushSubstsWith th ph (B i) = + let res = ph !! i in + case nchoose $ isClo 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 + pushSubstsWith th ph (f :% d) = + ncloE $ subs f th ph :% (d // th) + pushSubstsWith th ph (s :# a) = + ncloE $ 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) - public export %inline - pushSubstsTWith' : Term q dfrom from -> Term q dto to - pushSubstsTWith' s = (pushSubstsTWith th ph s).fst + namespace Term + public export %inline + pushSubstsWith' : Term q dfrom from -> Term q dto to + pushSubstsWith' s = (pushSubstsWith th ph s).fst - public export %inline - pushSubstsEWith' : Elim q dfrom from -> Elim q dto to - pushSubstsEWith' e = (pushSubstsEWith th ph e).fst + namespace Elim + public export %inline + pushSubstsWith' : Elim q dfrom from -> Elim q dto to + pushSubstsWith' e = (pushSubstsWith th ph e).fst public export %inline @@ -142,197 +127,126 @@ weakE : Elim q d n -> Elim q d (S n) weakE t = t //. shift 1 -mutual - public export - data IsRedexT : Term q d n -> Type where - IsUpsilonT : IsRedexT $ E (_ :# _) - IsCloT : IsRedexT $ CloT {} - IsDCloT : IsRedexT $ DCloT {} - IsERedex : IsRedexE e -> IsRedexT $ E e - - public export - data IsRedexE : Elim q d n -> Type where - IsUpsilonE : IsRedexE $ E _ :# _ - IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _ - IsBetaDLam : IsRedexE $ (DLam {} :# Eq {}) :% _ - IsCloE : IsRedexE $ CloE {} - IsDCloE : IsRedexE $ DCloE {} +public export 0 +Lookup : TermLike +Lookup q d n = Name -> Maybe $ Elim q d n public export %inline -NotRedexT : Term q d n -> Type -NotRedexT = Not . IsRedexT +isLamHead : Elim {} -> Bool +isLamHead (Lam {} :# Pi {}) = True +isLamHead _ = False public export %inline -NotRedexE : Elim q d n -> Type -NotRedexE = Not . IsRedexE - - -mutual - -- [todo] PLEASE replace these with macros omfg - export - isRedexT : (t : Term {}) -> Dec (IsRedexT t) - isRedexT (E (tm :# ty)) = Yes IsUpsilonT - isRedexT (CloT {}) = Yes IsCloT - isRedexT (DCloT {}) = Yes IsDCloT - isRedexT (E (CloE {})) = Yes $ IsERedex IsCloE - isRedexT (E (DCloE {})) = Yes $ IsERedex IsDCloE - isRedexT (E e@(_ :@ _)) with (isRedexE e) - _ | Yes yes = Yes $ IsERedex yes - _ | No no = No $ \case IsERedex p => no p - isRedexT (E e@(_ :% _)) with (isRedexE e) - _ | Yes yes = Yes $ IsERedex yes - _ | No no = No $ \case IsERedex p => no p - isRedexT (TYPE {}) = No $ \case _ impossible - isRedexT (Pi {}) = No $ \case _ impossible - isRedexT (Lam {}) = No $ \case _ impossible - isRedexT (Eq {}) = No $ \case _ impossible - isRedexT (DLam {}) = No $ \case _ impossible - isRedexT (E (F _)) = No $ \case IsERedex _ impossible - isRedexT (E (B _)) = No $ \case IsERedex _ impossible - - export - isRedexE : (e : Elim {}) -> Dec (IsRedexE e) - isRedexE (E _ :# _) = Yes IsUpsilonE - isRedexE ((Lam {} :# Pi {}) :@ _) = Yes IsBetaLam - isRedexE ((DLam {} :# Eq {}) :% _) = Yes IsBetaDLam - isRedexE (CloE {}) = Yes IsCloE - isRedexE (DCloE {}) = Yes IsDCloE - isRedexE (F x) = No $ \case _ impossible - isRedexE (B i) = No $ \case _ impossible - isRedexE (F _ :@ _) = No $ \case _ impossible - isRedexE (B _ :@ _) = No $ \case _ impossible - isRedexE (_ :@ _ :@ _) = No $ \case _ impossible - isRedexE (_ :% _ :@ _) = No $ \case _ impossible - isRedexE (CloE {} :@ _) = No $ \case _ impossible - isRedexE (DCloE {} :@ _) = No $ \case _ impossible - isRedexE ((TYPE _ :# _) :@ _) = No $ \case _ impossible - isRedexE ((Pi {} :# _) :@ _) = No $ \case _ impossible - isRedexE ((Eq {} :# _) :@ _) = No $ \case _ impossible - isRedexE ((DLam {} :# _) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# TYPE _) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# Lam {}) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# Eq {}) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# DLam {}) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# E _) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# CloT {}) :@ _) = No $ \case _ impossible - isRedexE ((Lam {} :# DCloT {}) :@ _) = No $ \case _ impossible - isRedexE ((E _ :# _) :@ _) = No $ \case _ impossible - isRedexE ((CloT {} :# _) :@ _) = No $ \case _ impossible - isRedexE ((DCloT {} :# _) :@ _) = No $ \case _ impossible - isRedexE ((TYPE _ :# _) :% _) = No $ \case _ impossible - isRedexE ((Pi {} :# _) :% _) = No $ \case _ impossible - isRedexE ((Eq {} :# _) :% _) = No $ \case _ impossible - isRedexE ((Lam {} :# _) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# TYPE _) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# Pi {}) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# Lam {}) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# DLam {}) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# E _) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# CloT {}) :% _) = No $ \case _ impossible - isRedexE ((DLam {} :# DCloT {}) :% _) = No $ \case _ impossible - isRedexE ((E _ :# _) :% _) = No $ \case _ impossible - isRedexE ((CloT {} :# _) :% _) = No $ \case _ impossible - isRedexE ((DCloT {} :# _) :% _) = No $ \case _ impossible - isRedexE (F _ :% _) = No $ \case _ impossible - isRedexE (B _ :% _) = No $ \case _ impossible - isRedexE (_ :@ _ :% _) = No $ \case _ impossible - isRedexE (_ :% _ :% _) = No $ \case _ impossible - isRedexE (CloE {} :% _) = No $ \case _ impossible - isRedexE (DCloE {} :% _) = No $ \case _ impossible - isRedexE (TYPE _ :# _) = No $ \case _ impossible - isRedexE (Pi {} :# _) = No $ \case _ impossible - isRedexE (Lam {} :# _) = No $ \case _ impossible - isRedexE (Eq {} :# _) = No $ \case _ impossible - isRedexE (DLam {} :# _) = No $ \case _ impossible - isRedexE (CloT {} :# _) = No $ \case _ impossible - isRedexE (DCloT {} :# _) = No $ \case _ impossible - +isDLamHead : Elim {} -> Bool +isDLamHead (DLam {} :# Eq {}) = True +isDLamHead _ = False public export %inline -RedexTerm : Type -> Nat -> Nat -> Type -RedexTerm q d n = Subset (Term q d n) IsRedexT +isE : Term {} -> Bool +isE (E _) = True +isE _ = False public export %inline -NonRedexTerm : Type -> Nat -> Nat -> Type -NonRedexTerm q d n = Subset (Term q d n) NotRedexT +isAnn : Elim {} -> Bool +isAnn (_ :# _) = True +isAnn _ = False -public export %inline -RedexElim : Type -> Nat -> Nat -> Type -RedexElim q d n = Subset (Elim q d n) IsRedexE +parameters (g : Lookup q d n) + mutual + namespace Elim + public export + isRedex : Elim q d n -> Bool + isRedex (F x) = isJust $ g x + isRedex (B _) = False + isRedex (f :@ _) = isRedex f || isLamHead f + isRedex (f :% _) = isRedex f || isDLamHead f + isRedex (t :# a) = isE t || isRedex t || isRedex a + isRedex (CloE {}) = True + isRedex (DCloE {}) = True -public export %inline -NonRedexElim : Type -> Nat -> Nat -> Type -NonRedexElim q d n = Subset (Elim q d n) NotRedexE + 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 + +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) -||| substitute a term with annotation for the bound variable of a `ScopeTerm` -export %inline -substScope : (arg, argTy : Term q d n) -> (body : ScopeTerm q d n) -> Term q d n -substScope arg argTy body = sub1 body (arg :# argTy) +parameters (g : Lookup q d n) + mutual + namespace Elim + export covering + whnf : Elim q d n -> NonRedexElim q d n g + whnf (F x) with (g x) proof eq + _ | Just y = whnf y + _ | Nothing = Element (F x) $ rewrite eq in Ah -mutual - export %inline - stepT' : (s : Term q d n) -> IsRedexT s -> Term q d n - stepT' (E (s :# _)) IsUpsilonT = s - stepT' (CloT s th) IsCloT = pushSubstsTWith' id th s - stepT' (DCloT s th) IsDCloT = pushSubstsTWith' th id s - stepT' (E e) (IsERedex p) = E $ stepE' e p + whnf (B i) = Element (B i) Ah - export %inline - stepE' : (e : Elim q d n) -> IsRedexE e -> Elim q d n - stepE' (E e :# _) IsUpsilonE = e - stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam = - let s = s :# arg in sub1 body s :# sub1 res s - stepE' ((DLam {body, _} :# Eq {ty, l, r, _}) :% dim) IsBetaDLam = - case dim of - K Zero => l :# ty.zero - K One => r :# ty.one - B _ => dsub1 body dim :# dsub1 ty dim - stepE' (CloE e th) IsCloE = pushSubstsEWith' id th e - stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e + 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 -export %inline -stepT : (s : Term q d n) -> Either (NotRedexT s) (Term q d n) -stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n + 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 = case p of K e => pick l r e; _ => dsub1 body p + in + whnf $ body :# dsub1 ty p + Right ndlh => + Element (f :% p) $ fnf `orNo` ndlh -export %inline -stepE : (e : Elim q d n) -> Either (NotRedexE e) (Elim q d n) -stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n + whnf (s :# a) = + let Element s snf = whnf s + Element a anf = whnf a + in + case nchoose $ isE s of + Left _ => let E e = s in Element e $ noOr2 snf + Right ne => Element (s :# a) $ ne `orNo` snf `orNo` anf -export covering -whnfT : Term q d n -> NonRedexTerm q d n -whnfT s = case stepT s of Right s' => whnfT s'; Left done => Element s done + whnf (CloE el th) = whnf $ pushSubstsWith' id th el + whnf (DCloE el th) = whnf $ pushSubstsWith' th id el -export covering -whnfE : Elim q d n -> NonRedexElim q d n -whnfE e = case stepE e of Right e' => whnfE e'; Left done => Element e done + namespace Term + export covering + whnf : Term q d n -> NonRedexTerm q d n g + whnf (TYPE l) = Element (TYPE l) Ah + whnf (Pi qty x arg res) = Element (Pi qty x arg res) Ah + whnf (Lam x body) = Element (Lam x body) Ah + whnf (Eq i ty l r) = Element (Eq i ty l r) Ah + whnf (DLam i body) = Element (DLam i body) Ah + 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 -export -notRedexNotCloE : (e : Elim {}) -> NotRedexE e -> NotCloE e -notRedexNotCloE (F x) f = NCF -notRedexNotCloE (B i) f = NCB -notRedexNotCloE (fun :@ arg) f = NCApp -notRedexNotCloE (fun :% arg) f = NCDApp -notRedexNotCloE (tm :# ty) f = NCAnn -notRedexNotCloE (CloE el th) f = absurd $ f IsCloE -notRedexNotCloE (DCloE el th) f = absurd $ f IsDCloE - -export -notRedexNotCloT : (t : Term {}) -> NotRedexT t -> NotCloT t -notRedexNotCloT (TYPE _) _ = NCTYPE -notRedexNotCloT (Pi {}) _ = NCPi -notRedexNotCloT (Lam {}) _ = NCLam -notRedexNotCloT (Eq {}) _ = NCEq -notRedexNotCloT (DLam {}) _ = NCDLam -notRedexNotCloT (E e) f = NCE $ notRedexNotCloE e $ f . IsERedex -notRedexNotCloT (CloT {}) f = absurd $ f IsCloT -notRedexNotCloT (DCloT {}) f = absurd $ f IsDCloT - -export -toNotCloE : NonRedexElim q d n -> NonCloElim q d n -toNotCloE (Element e prf) = Element e $ notRedexNotCloE e prf - -export -toNotCloT : NonRedexTerm q d n -> NonCloTerm q d n -toNotCloT (Element t prf) = Element t $ notRedexNotCloT t prf + whnf (CloT tm th) = whnf $ pushSubstsWith' id th tm + whnf (DCloT tm th) = whnf $ pushSubstsWith' th id tm diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 87473fb..5fd45cc 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -19,25 +19,25 @@ CanTC q = CanTC' q IsGlobal private covering %inline -expectTYPE : HasErr q m => Term q d n -> m Universe +expectTYPE : CanTC' q _ m => Term q d n -> m Universe expectTYPE s = - case (whnfT s).fst of - TYPE l => pure l - _ => throwError $ ExpectedTYPE s + case whnf !ask s of + Element (TYPE l) _ => pure l + _ => throwError $ ExpectedTYPE s private covering %inline -expectPi : HasErr q m => Term q d n -> +expectPi : CanTC' q _ m => Term q d n -> m (q, Term q d n, ScopeTerm q d n) expectPi ty = - case whnfT ty of + case whnf !ask ty of Element (Pi qty _ arg res) _ => pure (qty, arg, res) _ => throwError $ ExpectedPi ty private covering %inline -expectEq : HasErr q m => Term q d n -> +expectEq : CanTC' q _ m => Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n) expectEq ty = - case whnfT ty of + case whnf !ask ty of Element (Eq _ ty l r) _ => pure (ty, l, r) _ => throwError $ ExpectedEq ty @@ -102,7 +102,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} check : TyContext q d n -> SQty q -> Term q d n -> Term q d n -> m (CheckResult q n) check ctx sg subj ty = - let Element subj nc = pushSubstsT subj in + let Element subj nc = pushSubsts subj in check' ctx sg subj nc ty ||| `infer ctx sg subj` infers the type of `subj` in the context `ctx`, @@ -110,13 +110,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} export covering %inline infer : TyContext q d n -> SQty q -> Elim q d n -> m (InferResult q d n) infer ctx sg subj = - let Element subj nc = pushSubstsE subj in + let Element subj nc = pushSubsts subj in infer' ctx sg subj nc export covering check' : TyContext q d n -> SQty q -> - (subj : Term q d n) -> (0 nc : NotCloT subj) -> Term q d n -> + (subj : Term q d n) -> (0 nc : NotClo subj) -> Term q d n -> m (CheckResult q n) check' ctx sg (TYPE l) _ ty = do @@ -153,19 +153,19 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m} (ty, l, r) <- expectEq ty qout <- check (extendDim ctx) sg body.term ty.term let eqs = makeDimEq ctx.dctx - equalTWith eqs body.zero l - equalTWith eqs body.one r + equal !ask eqs body.zero l + equal !ask eqs body.one r pure qout check' ctx sg (E e) _ ty = do infres <- infer ctx sg e ignore $ check ctx szero ty (TYPE UAny) - subTWith (makeDimEq ctx.dctx) infres.type ty + sub !ask (makeDimEq ctx.dctx) infres.type ty pure infres.qout export covering infer' : TyContext q d n -> SQty q -> - (subj : Elim q d n) -> (0 nc : NotCloE subj) -> + (subj : Elim q d n) -> (0 nc : NotClo subj) -> m (InferResult q d n) infer' ctx sg (F x) _ = do diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 5f4be39..539d352 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -10,6 +10,7 @@ depends = base, contrib, elab-util, sop, snocvect modules = Quox.NatExtra, Quox.Decidable, + Quox.No, -- Quox.Unicode, -- Quox.OPE, Quox.Pretty, diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index f933f33..0b57561 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -55,198 +55,228 @@ parameters (label : String) (act : Lazy (M ())) testNeq = testThrows label (const True) $ runReaderT globals act -subT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M () -subT = Lib.subT -%hide Lib.subT +parameters {default 0 d, n : Nat} + {default new eqs : DimEq d} + subT : Term Three d n -> Term Three d n -> M () + subT s t = Term.sub !ask eqs s t -equalT : {default 0 d, n : Nat} -> Term Three d n -> Term Three d n -> M () -equalT = Lib.equalT -%hide Lib.equalT + equalT : Term Three d n -> Term Three d n -> M () + equalT s t = Term.equal !ask eqs s t -subE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M () -subE = Lib.subE -%hide Lib.subE + subE : Elim Three d n -> Elim Three d n -> M () + subE e f = Elim.sub !ask eqs e f -equalE : {default 0 d, n : Nat} -> Elim Three d n -> Elim Three d n -> M () -equalE = Lib.equalE -%hide Lib.equalE + equalE : Elim Three d n -> Elim Three d n -> M () + equalE e f = Elim.equal !ask eqs e f export tests : Test tests = "equality & subtyping" :- [ - "universes" :- [ - testEq "★₀ ≡ ★₀" $ - equalT (TYPE 0) (TYPE 0), - testNeq "★₀ ≢ ★₁" $ - equalT (TYPE 0) (TYPE 1), - testNeq "★₁ ≢ ★₀" $ - equalT (TYPE 1) (TYPE 0), - testEq "★₀ <: ★₀" $ - subT (TYPE 0) (TYPE 0), - testEq "★₀ <: ★₁" $ - subT (TYPE 0) (TYPE 1), - testNeq "★₁ ≮: ★₀" $ - subT (TYPE 1) (TYPE 0) - ], + note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#, - "pi" :- [ - -- ⊸ for →₁, ⇾ for →₀ - testEq "A ⊸ B ≡ A ⊸ B" $ - let tm = Arr One (FT "A") (FT "B") in - equalT tm tm, - testNeq "A ⇾ B ≢ A ⇾ B" $ - let tm1 = Arr Zero (FT "A") (FT "B") - tm2 = Arr One (FT "A") (FT "B") in - equalT tm1 tm2, - testEq "A ⊸ B <: A ⊸ B" $ - let tm = Arr One (FT "A") (FT "B") in - subT tm tm, - testNeq "A ⇾ B ≮: A ⊸ B" $ - let tm1 = Arr Zero (FT "A") (FT "B") - tm2 = Arr One (FT "A") (FT "B") in - subT tm1 tm2, - testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $ - let tm = Arr Zero (TYPE 0) (TYPE 0) in - equalT tm tm, - testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $ - let tm = Arr Zero (TYPE 0) (TYPE 0) in - subT tm tm, - testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $ - let tm1 = Arr Zero (TYPE 1) (TYPE 0) - tm2 = Arr Zero (TYPE 0) (TYPE 0) in - equalT tm1 tm2, - testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $ - let tm1 = Arr One (TYPE 1) (TYPE 0) - tm2 = Arr One (TYPE 0) (TYPE 0) in - subT tm1 tm2, - testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $ - let tm1 = Arr Zero (TYPE 0) (TYPE 0) - tm2 = Arr Zero (TYPE 0) (TYPE 1) in - equalT tm1 tm2, - testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $ - let tm1 = Arr One (TYPE 0) (TYPE 0) - tm2 = Arr One (TYPE 0) (TYPE 1) in - subT tm1 tm2, - testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $ - let tm1 = Arr One (TYPE 0) (TYPE 0) - tm2 = Arr One (TYPE 0) (TYPE 1) in - subT tm1 tm2 - ], + "universes" :- [ + testEq "★₀ ≡ ★₀" $ + equalT (TYPE 0) (TYPE 0), + testNeq "★₀ ≢ ★₁" $ + equalT (TYPE 0) (TYPE 1), + testNeq "★₁ ≢ ★₀" $ + equalT (TYPE 1) (TYPE 0), + testEq "★₀ <: ★₀" $ + subT (TYPE 0) (TYPE 0), + testEq "★₀ <: ★₁" $ + subT (TYPE 0) (TYPE 1), + testNeq "★₁ ≮: ★₀" $ + subT (TYPE 1) (TYPE 0) + ], - "eq type" :- [ - testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $ - let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in - equalT tm tm, - testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)" - {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $ - equalT (Eq0 (TYPE 1) (TYPE 0) (TYPE 0)) - (Eq0 (FT "A") (TYPE 0) (TYPE 0)) - ], + "pi" :- [ + note #""A ⊸ B" for (1 _ : A) → B"#, + note #""A ⇾ B" for (0 _ : A) → B"#, + testEq "A ⊸ B ≡ A ⊸ B" $ + let tm = Arr One (FT "A") (FT "B") in + equalT tm tm, + testNeq "A ⇾ B ≢ A ⊸ B" $ + let tm1 = Arr Zero (FT "A") (FT "B") + tm2 = Arr One (FT "A") (FT "B") in + equalT tm1 tm2, + testEq "0=1 ⊢ A ⇾ B ≢ A ⊸ B" $ + let tm1 = Arr Zero (FT "A") (FT "B") + tm2 = Arr One (FT "A") (FT "B") in + equalT tm1 tm2 {eqs = ZeroIsOne}, + testEq "A ⊸ B <: A ⊸ B" $ + let tm = Arr One (FT "A") (FT "B") in + subT tm tm, + testNeq "A ⇾ B ≮: A ⊸ B" $ + let tm1 = Arr Zero (FT "A") (FT "B") + tm2 = Arr One (FT "A") (FT "B") in + subT tm1 tm2, + testEq "★₀ ⇾ ★₀ ≡ ★₀ ⇾ ★₀" $ + let tm = Arr Zero (TYPE 0) (TYPE 0) in + equalT tm tm, + testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $ + let tm = Arr Zero (TYPE 0) (TYPE 0) in + subT tm tm, + testNeq "★₁ ⊸ ★₀ ≢ ★₀ ⇾ ★₀" $ + let tm1 = Arr Zero (TYPE 1) (TYPE 0) + tm2 = Arr Zero (TYPE 0) (TYPE 0) in + equalT tm1 tm2, + testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $ + let tm1 = Arr One (TYPE 1) (TYPE 0) + tm2 = Arr One (TYPE 0) (TYPE 0) in + subT tm1 tm2, + testNeq "★₀ ⊸ ★₀ ≢ ★₀ ⇾ ★₁" $ + let tm1 = Arr Zero (TYPE 0) (TYPE 0) + tm2 = Arr Zero (TYPE 0) (TYPE 1) in + equalT tm1 tm2, + testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $ + let tm1 = Arr One (TYPE 0) (TYPE 0) + tm2 = Arr One (TYPE 0) (TYPE 1) in + subT tm1 tm2, + testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $ + let tm1 = Arr One (TYPE 0) (TYPE 0) + tm2 = Arr One (TYPE 0) (TYPE 1) in + subT tm1 tm2 + ], - "lambda" :- [ - testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $ - equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0), - testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ - equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0), - testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $ - equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0), - testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ - equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0), - testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $ - equalT (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1) - (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0), - testEq "λ x ⇒ [a] ≡ λ x ⇒ [a] (TUsed vs TUnused)" $ - equalT (Lam "x" $ TUsed $ FT "a") - (Lam "x" $ TUnused $ FT "a"), - skipWith "(no η yet)" $ - testEq "λ x ⇒ [f [x]] ≡ [f] (η)" $ - equalT (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0) - (FT "f") - ], + "eq type" :- [ + testEq "(★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : ★₁)" $ + let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in + equalT tm tm, + testEq "A ≔ ★₁ ⊢ (★₀ = ★₀ : ★₁) ≡ (★₀ = ★₀ : A)" + {globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $ + equalT (Eq0 (TYPE 1) (TYPE 0) (TYPE 0)) + (Eq0 (FT "A") (TYPE 0) (TYPE 0)) + ], - "term closure" :- [ - testEq "[x]{} ≡ [x]" $ - equalT (CloT (BVT 0) id) (BVT 0) {n = 1}, - testEq "[x]{a/x} ≡ [a]" $ - equalT (CloT (BVT 0) (F "a" ::: id)) (FT "a"), - testEq "[x]{a/x,b/y} ≡ [a]" $ - equalT (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"), - testEq "(λy. [x]){y/y, a/x} ≡ λy. [a] (TUnused)" $ - equalT (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id)) - (Lam "y" $ TUnused $ FT "a"), - testEq "(λy. [x]){y/y, a/x} ≡ λy. [a] (TUsed)" $ - equalT (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id)) - (Lam "y" $ TUsed $ FT "a") - ], + "lambda" :- [ + testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $ + equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0), + testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $ + equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0), + testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $ + equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0), + testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $ + equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0), + testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $ + equalT (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1) + (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0), + testEq "λ x ⇒ [a] ≡ λ x ⇒ [a] (TUsed vs TUnused)" $ + equalT (Lam "x" $ TUsed $ FT "a") + (Lam "x" $ TUnused $ FT "a"), + skipWith "(no η yet)" $ + testEq "λ x ⇒ [f [x]] ≡ [f] (η)" $ + equalT (Lam "x" $ TUsed $ E $ F "f" :@ BVT 0) + (FT "f") + ], - todo "term d-closure", + "term closure" :- [ + note "𝑖, 𝑗 for bound variables pointing outside of the current expr", + testEq "[𝑖]{} ≡ [𝑖]" $ + equalT (CloT (BVT 0) id) (BVT 0) {n = 1}, + testEq "[𝑖]{a/𝑖} ≡ [a]" $ + equalT (CloT (BVT 0) (F "a" ::: id)) (FT "a"), + testEq "[𝑖]{a/𝑖,b/𝑗} ≡ [a]" $ + equalT (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"), + testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a] (TUnused)" $ + equalT (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id)) + (Lam "y" $ TUnused $ FT "a"), + testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a] (TUsed)" $ + equalT (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id)) + (Lam "y" $ TUsed $ FT "a") + ], - "free var" :- - let au_bu = fromList - [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))), - ("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))] - au_ba = fromList - [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))), - ("B", mkDef Any (TYPE (U 1)) (FT "A"))] - in [ - testEq "A ≡ A" $ - equalE (F "A") (F "A"), - testNeq "A ≢ B" $ - equalE (F "A") (F "B"), - testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $ - equalE (F "A") (F "B"), - testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $ - equalE (F "A") (F "B"), - testEq "A <: A" $ - subE (F "A") (F "A"), - testNeq "A ≮: B" $ - subE (F "A") (F "B") - ], + todo "term d-closure", - "bound var" :- [ - testEq "#0 ≡ #0" $ - equalE (BV 0) (BV 0) {n = 1}, - testNeq "#0 ≢ #1" $ - equalE (BV 0) (BV 1) {n = 2} - ], + "free var" :- + let au_bu = fromList + [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))), + ("B", mkDef Any (TYPE (U 1)) (TYPE (U 0)))] + au_ba = fromList + [("A", mkDef Any (TYPE (U 1)) (TYPE (U 0))), + ("B", mkDef Any (TYPE (U 1)) (FT "A"))] + in [ + testEq "A ≡ A" $ + equalE (F "A") (F "A"), + testNeq "A ≢ B" $ + equalE (F "A") (F "B"), + testEq "0=1 ⊢ A ≡ B" $ + equalE {eqs = ZeroIsOne} (F "A") (F "B"), + testEq "A : ★₁ ≔ ★₀ ⊢ A ≡ (★₀ ∷ ★₁)" {globals = au_bu} $ + equalE (F "A") (TYPE 0 :# TYPE 1), + testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A ≡ B" {globals = au_bu} $ + equalE (F "A") (F "B"), + testEq "A ≔ ★₀, B ≔ A ⊢ A ≡ B" {globals = au_ba} $ + equalE (F "A") (F "B"), + testEq "A <: A" $ + subE (F "A") (F "A"), + testNeq "A ≮: B" $ + subE (F "A") (F "B"), + testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B" + {globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)), + ("B", mkDef Any (TYPE 3) (TYPE 2))]} $ + subE (F "A") (F "B"), + testEq "A : ★₁👈 ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B" + {globals = fromList [("A", mkDef Any (TYPE 1) (TYPE 0)), + ("B", mkDef Any (TYPE 3) (TYPE 2))]} $ + subE (F "A") (F "B"), + testEq "0=1 ⊢ A <: B" $ + subE (F "A") (F "B") {eqs = ZeroIsOne} + ], - "application" :- [ - testEq "f [a] ≡ f [a]" $ - equalE (F "f" :@ FT "a") (F "f" :@ FT "a"), - testEq "f [a] <: f [a]" $ - subE (F "f" :@ FT "a") (F "f" :@ FT "a"), - testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A) (β)" $ - equalE - ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) - :@ FT "a") - (E (FT "a" :# FT "A") :# FT "A"), - testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a (βυ)" $ - equalE - ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) - :@ FT "a") - (F "a"), - testEq "(λ g ⇒ [g [x]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [x] (β↘↙)" $ - let a = FT "A"; a2a = (Arr One a a) in - equalE - ((Lam "g" (TUsed (E (BV 0 :@ FT "x"))) :# Arr One a2a a) :@ FT "f") - ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "x"), - testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ - subE - ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) - :@ FT "a") - (F "a") - ], + "bound var" :- [ + note "𝑖, 𝑗 for distinct bound variables", + testEq "𝑖 ≡ 𝑖" $ + equalE (BV 0) (BV 0) {n = 1}, + testNeq "𝑖 ≢ 𝑗" $ + equalE (BV 0) (BV 1) {n = 2}, + testEq "0=1 ⊢ 𝑖 ≡ 𝑗" $ + equalE {n = 2, eqs = ZeroIsOne} (BV 0) (BV 1) + ], - todo "annotation", + "application" :- [ + testEq "f [a] ≡ f [a]" $ + equalE (F "f" :@ FT "a") (F "f" :@ FT "a"), + testEq "f [a] <: f [a]" $ + subE (F "f" :@ FT "a") (F "f" :@ FT "a"), + testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ ([a ∷ A] ∷ A) (β)" $ + equalE + ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) + :@ FT "a") + (E (FT "a" :# FT "A") :# FT "A"), + testEq "(λ x ⇒ [x] ∷ A ⊸ A) a ≡ a (βυ)" $ + equalE + ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) + :@ FT "a") + (F "a"), + testEq "(λ g ⇒ [g [x]] ∷ ⋯)) [f] ≡ (λ y ⇒ [f [y]] ∷ ⋯) [x] (β↘↙)" $ + let a = FT "A"; a2a = (Arr One a a) in + equalE + ((Lam "g" (TUsed (E (BV 0 :@ FT "x"))) :# Arr One a2a a) :@ FT "f") + ((Lam "y" (TUsed (E (F "f" :@ BVT 0))) :# a2a) :@ FT "x"), + testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $ + subE + ((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A"))) + :@ FT "a") + (F "a"), + testEq "f : A ⊸ A ≔ λ x ⇒ [x] ⊢ f [x] ≡ x" + {globals = fromList + [("f", mkDef Any (Arr One (FT "A") (FT "A")) + (Lam "x" (TUsed (BVT 0))))]} $ + equalE (F "f" :@ FT "x") (F "x") + ], - todo "elim closure", + todo "annotation", - todo "elim d-closure", + todo "elim closure", - "clashes" :- [ - testNeq "★₀ ≢ ★₀ ⇾ ★₀" $ - equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), - todo "others" - ] + todo "elim d-closure", + + "clashes" :- [ + testNeq "★₀ ≢ ★₀ ⇾ ★₀" $ + equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)), + testEq "0=1 ⊢ ★₀ ≡ ★₀ ⇾ ★₀" $ + equalT (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)) {eqs = ZeroIsOne}, + todo "others" ] +] diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index b1671c3..de08dae 100644 --- a/tests/Tests/Reduce.idr +++ b/tests/Tests/Reduce.idr @@ -2,12 +2,12 @@ module Tests.Reduce import Quox.Syntax as Lib import Quox.Syntax.Qty.Three +import Quox.Equal import TermImpls import TAP -testWhnf : (Eq b, Show b) => (a -> (Subset b _)) -> - String -> a -> b -> Test +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 @@ -15,27 +15,28 @@ testWhnf whnf label from to = test "\{label} (whnf)" $ else with Prelude.(::) Left [("expected", to), ("received", result)] -testNoStep : forall p. Show a => ((x : a) -> Either (p x) a) -> - String -> a -> Test -testNoStep step label e = test "\{label} (no step)" $ - case step e of - Left _ => Right () - Right e' => with Prelude.(::) Left [("reduced", e')] +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)] -parameters {default 0 d, n : Nat} +parameters {default empty defs : Definitions Three} {default 0 d, n : Nat} testWhnfT : String -> Term Three d n -> Term Three d n -> Test - testWhnfT = testWhnf whnfT + testWhnfT = testWhnf (whnf defs) testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test - testWhnfE = testWhnf whnfE + testWhnfE = testWhnf (whnf defs) testNoStepE : String -> Elim Three d n -> Test - testNoStepE = testNoStep stepE + testNoStepE = testNoStep (whnf defs) testNoStepT : String -> Term Three d n -> Test - testNoStepT = testNoStep stepT + testNoStepT = testNoStep (whnf defs) tests = "whnf" :- [ @@ -70,6 +71,12 @@ tests = "whnf" :- [ (F "a") ], + "definitions" :- [ + testWhnfE "a (transparent)" + {defs = fromList [("a", mkDef Zero (TYPE 1) (TYPE 0))]} + (F "a") (TYPE 0 :# TYPE 1) + ], + "elim closure" :- [ testWhnfE "x{}" {n = 1} (CloE (BV 0) id)