whnf actually reduces to whnf now (probably)
This commit is contained in:
parent
f097e1c091
commit
92617a2e4a
11 changed files with 693 additions and 679 deletions
|
|
@ -64,4 +64,4 @@ main : IO Unit
|
|||
main = do
|
||||
putStrLn $ banner defPrettyOpts
|
||||
prettyTermDef tm
|
||||
prettyTermDef $ pushSubstsT tm
|
||||
prettyTermDef $ pushSubsts tm
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
||||
parameters {0 isGlobal : _} (defs : Definitions' q isGlobal)
|
||||
mutual
|
||||
private covering
|
||||
compareTN' : CanEqual' q _ m => Eq q =>
|
||||
namespace Term
|
||||
export covering
|
||||
compareN' : CanEqual q m => Eq q =>
|
||||
(s, t : Term q 0 n) ->
|
||||
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
|
||||
(0 _ : NotRedex defs s) -> (0 _ : NotRedex defs 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
|
||||
compareN' (TYPE k) (TYPE l) _ _ = compareU k l
|
||||
compareN' s@(TYPE _) t _ _ = clashT s t
|
||||
|
||||
compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
|
||||
compareTN' s@(TYPE _) t _ _ = clashT s t
|
||||
|
||||
compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
|
||||
compareN' (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
|
||||
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
|
||||
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
|
||||
compareN' (Eq _ ty1 l1 r1) (Eq _ ty2 l2 r2) _ _ = do
|
||||
compare0 ty1 ty2
|
||||
local {mode := Equal} $ do
|
||||
compareT0 l1 l2
|
||||
compareT0 r1 r2
|
||||
compareTN' s@(Eq {}) t _ _ = clashT s t
|
||||
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 =>
|
||||
namespace Elim
|
||||
export covering
|
||||
compareN' : CanEqual q m => Eq q =>
|
||||
(e, f : Elim q 0 n) ->
|
||||
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
|
||||
(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) _ _ =
|
||||
compareN' e@(B i) f@(B j) _ _ =
|
||||
unless (i == j) $ clashE e f
|
||||
compareEN' e@(B _) f _ _ = clashE e f
|
||||
compareN' e@(B _) f _ _ = clashE e f
|
||||
|
||||
-- [todo] tracking variance of functions? maybe???
|
||||
-- probably not
|
||||
compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
|
||||
compareN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
|
||||
local {mode := Equal} $ do
|
||||
compareE0 fun1 fun2
|
||||
compareT0 arg1 arg2
|
||||
compareEN' e@(_ :@ _) f _ _ = clashE e f
|
||||
compare0 fun1 fun2
|
||||
compare0 arg1 arg2
|
||||
compareN' e@(_ :@ _) f _ _ = clashE e f
|
||||
|
||||
compareEN' (fun1 :% dim1) (fun2 :% dim2) _ _ = do
|
||||
compareE0 fun1 fun2
|
||||
-- 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
|
||||
compareEN' e@(_ :% _) f _ _ = clashE e f
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
export covering %inline
|
||||
compareT : CanEqual' q _ m => Eq q =>
|
||||
compare : 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)
|
||||
compare eqs s t =
|
||||
for_ (splits eqs) $ \th => compare0 (s /// th) (t /// th)
|
||||
|
||||
export covering %inline
|
||||
compareE : CanEqual' q _ m => Eq q =>
|
||||
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 ()
|
||||
compareE eqs e f =
|
||||
for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
|
||||
|
||||
compare eqs e f =
|
||||
for_ (splits eqs) $ \th => compare0 (e /// th) (f /// th)
|
||||
|
||||
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)
|
||||
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
|
||||
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 =>
|
||||
compare0 : 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
|
||||
compare0 (TUnused body0) (TUnused body1) = compare0 body0 body1
|
||||
compare0 body0 body1 = compare0 body0.term body1.term
|
||||
|
||||
namespace DScopeTerm
|
||||
export covering %inline
|
||||
compareDST0 : CanEqual' q _ m => Eq q =>
|
||||
compare0 : 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
|
||||
compare0 (DUnused body0) (DUnused body1) = compare0 body0 body1
|
||||
compare0 body0 body1 = do
|
||||
compare0 body0.zero body1.zero
|
||||
compare0 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
|
||||
|
||||
namespace Term
|
||||
export covering %inline
|
||||
equalTWith : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
equal : HasErr q m => Eq q =>
|
||||
DimEq d -> Term q d n -> Term q d n -> m ()
|
||||
equalTWith = into compareT Equal
|
||||
equal eqs s t {m} = runReaderT {m} (MakeEnv Equal) $ compare eqs s t
|
||||
|
||||
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 =>
|
||||
sub : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
DimEq d -> Term q d n -> Term q d n -> m ()
|
||||
subTWith = into compareT Sub
|
||||
sub eqs s t {m} = runReaderT {m} (MakeEnv Sub) $ compare eqs s t
|
||||
|
||||
namespace Elim
|
||||
export covering %inline
|
||||
subEWith : HasErr q m => HasDefs' q _ m => Eq q =>
|
||||
equal : HasErr q m => Eq q =>
|
||||
DimEq d -> Elim q d n -> Elim q d n -> m ()
|
||||
subEWith = into compareE Sub
|
||||
|
||||
equal eqs e f {m} = runReaderT {m} (MakeEnv Equal) $ compare eqs e f
|
||||
|
||||
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
|
||||
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
|
||||
|
|
|
|||
54
lib/Quox/No.idr
Normal file
54
lib/Quox/No.idr
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
||| 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 NotClo : Pred $ Term {}
|
||||
NotClo = No . isClo
|
||||
|
||||
||| 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 NonCloElim : TermLike
|
||||
NonCloElim q d n = Subset (Elim q d n) NotClo
|
||||
|
||||
public export
|
||||
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
|
||||
namespace Term
|
||||
||| 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
|
||||
pushSubsts : Term q d n -> NonCloTerm q d n
|
||||
pushSubsts s = pushSubstsWith id id s
|
||||
|
||||
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
|
||||
|
||||
namespace Elim
|
||||
||| 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
|
||||
pushSubsts : Elim q d n -> NonCloElim q d n
|
||||
pushSubsts e = pushSubstsWith id id e
|
||||
|
||||
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
|
||||
|
||||
export
|
||||
pushSubstsEWith : DSubst dfrom dto -> TSubst q dto from to ->
|
||||
pushSubstsWith : DSubst dfrom dto -> TSubst q dto from to ->
|
||||
Elim q dfrom from -> NonCloElim q dto to
|
||||
pushSubstsEWith th ph (F x) =
|
||||
pushSubstsWith th ph (F x) =
|
||||
ncloE $ F x
|
||||
pushSubstsEWith th ph (B i) =
|
||||
pushSubstsWith 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) =
|
||||
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
|
||||
pushSubstsEWith th ph (f :% d) =
|
||||
pushSubstsWith th ph (f :% d) =
|
||||
ncloE $ subs f th ph :% (d // th)
|
||||
pushSubstsEWith th ph (s :# a) =
|
||||
pushSubstsWith 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
|
||||
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
|
||||
pushSubstsTWith' : Term q dfrom from -> Term q dto to
|
||||
pushSubstsTWith' s = (pushSubstsTWith th ph s).fst
|
||||
pushSubstsWith' : Term q dfrom from -> Term q dto to
|
||||
pushSubstsWith' s = (pushSubstsWith th ph s).fst
|
||||
|
||||
namespace Elim
|
||||
public export %inline
|
||||
pushSubstsEWith' : Elim q dfrom from -> Elim q dto to
|
||||
pushSubstsEWith' e = (pushSubstsEWith th ph e).fst
|
||||
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
|
||||
|
||||
|
||||
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
|
||||
isLamHead _ = False
|
||||
|
||||
public export %inline
|
||||
isDLamHead : Elim {} -> Bool
|
||||
isDLamHead (DLam {} :# Eq {}) = True
|
||||
isDLamHead _ = False
|
||||
|
||||
public export %inline
|
||||
isE : Term {} -> Bool
|
||||
isE (E _) = True
|
||||
isE _ = False
|
||||
|
||||
public export %inline
|
||||
isAnn : Elim {} -> Bool
|
||||
isAnn (_ :# _) = True
|
||||
isAnn _ = False
|
||||
|
||||
parameters (g : Lookup q d n)
|
||||
mutual
|
||||
namespace Elim
|
||||
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
|
||||
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
|
||||
|
||||
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
|
||||
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 %inline
|
||||
NotRedexT : Term q d n -> Type
|
||||
NotRedexT = Not . IsRedexT
|
||||
|
||||
public export %inline
|
||||
NotRedexE : Elim q d n -> Type
|
||||
NotRedexE = Not . IsRedexE
|
||||
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 (g : Lookup q d n)
|
||||
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
|
||||
|
||||
|
||||
public export %inline
|
||||
RedexTerm : Type -> Nat -> Nat -> Type
|
||||
RedexTerm q d n = Subset (Term q d n) IsRedexT
|
||||
|
||||
public export %inline
|
||||
NonRedexTerm : Type -> Nat -> Nat -> Type
|
||||
NonRedexTerm q d n = Subset (Term q d n) NotRedexT
|
||||
|
||||
public export %inline
|
||||
RedexElim : Type -> Nat -> Nat -> Type
|
||||
RedexElim q d n = Subset (Elim q d n) IsRedexE
|
||||
|
||||
public export %inline
|
||||
NonRedexElim : Type -> Nat -> Nat -> Type
|
||||
NonRedexElim q d n = Subset (Elim q d n) NotRedexE
|
||||
|
||||
|
||||
||| 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)
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
namespace Elim
|
||||
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 : 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
|
||||
|
||||
whnf (B i) = Element (B i) Ah
|
||||
|
||||
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 (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
|
||||
|
||||
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
|
||||
|
||||
whnf (CloE el th) = whnf $ pushSubstsWith' id th el
|
||||
whnf (DCloE el th) = whnf $ pushSubstsWith' th id el
|
||||
|
||||
namespace Term
|
||||
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
|
||||
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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
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
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ depends = base, contrib, elab-util, sop, snocvect
|
|||
modules =
|
||||
Quox.NatExtra,
|
||||
Quox.Decidable,
|
||||
Quox.No,
|
||||
-- Quox.Unicode,
|
||||
-- Quox.OPE,
|
||||
Quox.Pretty,
|
||||
|
|
|
|||
|
|
@ -55,26 +55,26 @@ 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" :- [
|
||||
note #""0=1 ⊢ 𝒥" means that 𝒥 holds in an inconsistent dim context"#,
|
||||
|
||||
"universes" :- [
|
||||
testEq "★₀ ≡ ★₀" $
|
||||
equalT (TYPE 0) (TYPE 0),
|
||||
|
|
@ -91,14 +91,19 @@ tests = "equality & subtyping" :- [
|
|||
],
|
||||
|
||||
"pi" :- [
|
||||
-- ⊸ for →₁, ⇾ for →₀
|
||||
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" $
|
||||
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,
|
||||
|
|
@ -166,16 +171,17 @@ tests = "equality & subtyping" :- [
|
|||
],
|
||||
|
||||
"term closure" :- [
|
||||
testEq "[x]{} ≡ [x]" $
|
||||
note "𝑖, 𝑗 for bound variables pointing outside of the current expr",
|
||||
testEq "[𝑖]{} ≡ [𝑖]" $
|
||||
equalT (CloT (BVT 0) id) (BVT 0) {n = 1},
|
||||
testEq "[x]{a/x} ≡ [a]" $
|
||||
testEq "[𝑖]{a/𝑖} ≡ [a]" $
|
||||
equalT (CloT (BVT 0) (F "a" ::: id)) (FT "a"),
|
||||
testEq "[x]{a/x,b/y} ≡ [a]" $
|
||||
testEq "[𝑖]{a/𝑖,b/𝑗} ≡ [a]" $
|
||||
equalT (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"),
|
||||
testEq "(λy. [x]){y/y, a/x} ≡ λy. [a] (TUnused)" $
|
||||
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. [x]){y/y, a/x} ≡ λy. [a] (TUsed)" $
|
||||
testEq "(λy. [𝑖]){y/y, a/𝑖} ≡ λy. [a] (TUsed)" $
|
||||
equalT (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id))
|
||||
(Lam "y" $ TUsed $ FT "a")
|
||||
],
|
||||
|
|
@ -194,6 +200,10 @@ tests = "equality & subtyping" :- [
|
|||
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} $
|
||||
|
|
@ -201,14 +211,27 @@ tests = "equality & subtyping" :- [
|
|||
testEq "A <: A" $
|
||||
subE (F "A") (F "A"),
|
||||
testNeq "A ≮: B" $
|
||||
subE (F "A") (F "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}
|
||||
],
|
||||
|
||||
"bound var" :- [
|
||||
testEq "#0 ≡ #0" $
|
||||
note "𝑖, 𝑗 for distinct bound variables",
|
||||
testEq "𝑖 ≡ 𝑖" $
|
||||
equalE (BV 0) (BV 0) {n = 1},
|
||||
testNeq "#0 ≢ #1" $
|
||||
equalE (BV 0) (BV 1) {n = 2}
|
||||
testNeq "𝑖 ≢ 𝑗" $
|
||||
equalE (BV 0) (BV 1) {n = 2},
|
||||
testEq "0=1 ⊢ 𝑖 ≡ 𝑗" $
|
||||
equalE {n = 2, eqs = ZeroIsOne} (BV 0) (BV 1)
|
||||
],
|
||||
|
||||
"application" :- [
|
||||
|
|
@ -235,7 +258,12 @@ tests = "equality & subtyping" :- [
|
|||
subE
|
||||
((Lam "x" (TUsed (BVT 0)) :# (Arr One (FT "A") (FT "A")))
|
||||
:@ FT "a")
|
||||
(F "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 "annotation",
|
||||
|
|
@ -247,6 +275,8 @@ tests = "equality & subtyping" :- [
|
|||
"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"
|
||||
]
|
||||
]
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Reference in a new issue