mode eq mode into a reader
This commit is contained in:
parent
8443b2f6d8
commit
98fa8d9967
1 changed files with 118 additions and 102 deletions
|
|
@ -12,24 +12,31 @@ private %inline
|
||||||
ClashE : EqMode -> Elim d n -> Elim d n -> Error
|
ClashE : EqMode -> Elim d n -> Elim d n -> Error
|
||||||
ClashE mode = ClashT mode `on` E
|
ClashE mode = ClashT mode `on` E
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
CanEq : (Type -> Type) -> Type
|
record Env where
|
||||||
CanEq m = (MonadError Error m, MonadReader Definitions m)
|
constructor MakeEnv
|
||||||
|
defs : Definitions
|
||||||
|
mode : EqMode
|
||||||
|
|
||||||
|
|
||||||
parameters {auto _ : CanEq m}
|
parameters {auto _ : MonadError Error m} {auto _ : MonadReader Env m}
|
||||||
private %inline
|
private %inline
|
||||||
clashT : EqMode -> Term d n -> Term d n -> m a
|
mode : m EqMode
|
||||||
clashT mode = throwError .: ClashT mode
|
mode = asks mode
|
||||||
|
|
||||||
private %inline
|
private %inline
|
||||||
clashE : EqMode -> Elim d n -> Elim d n -> m a
|
clashT : Term d n -> Term d n -> m a
|
||||||
clashE mode = throwError .: ClashE mode
|
clashT s t = throwError $ ClashT !mode s t
|
||||||
|
|
||||||
|
private %inline
|
||||||
|
clashE : Elim d n -> Elim d n -> m a
|
||||||
|
clashE e f = throwError $ ClashE !mode e f
|
||||||
|
|
||||||
private %inline
|
private %inline
|
||||||
defE : Name -> m (Maybe (Elim d n))
|
defE : Name -> m (Maybe (Elim d n))
|
||||||
defE x = asks $ \defs => do
|
defE x = asks $ \env => do
|
||||||
g <- lookup x defs
|
g <- lookup x env.defs
|
||||||
pure $ (!g.term).def :# g.type.def
|
pure $ (!g.term).def :# g.type.def
|
||||||
|
|
||||||
private %inline
|
private %inline
|
||||||
|
|
@ -37,136 +44,145 @@ parameters {auto _ : CanEq m}
|
||||||
defT x = map E <$> defE x
|
defT x = map E <$> defE x
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
compareU' : EqMode -> Universe -> Universe -> Bool
|
compareU' : Universe -> Universe -> m Bool
|
||||||
compareU' = \case Equal => (==); Sub => (<=)
|
compareU' i j = pure $
|
||||||
|
case !mode of Equal => i == j; Sub => i <= j
|
||||||
|
|
||||||
export %inline
|
export %inline
|
||||||
compareU : EqMode -> Universe -> Universe -> m ()
|
compareU : Universe -> Universe -> m ()
|
||||||
compareU mode k l = unless (compareU' mode k l) $
|
compareU k l = unless !(compareU' k l) $
|
||||||
throwError $ ClashU mode k l
|
throwError $ ClashU !mode k l
|
||||||
|
|
||||||
mutual
|
mutual
|
||||||
private covering
|
private covering
|
||||||
compareTN' : EqMode ->
|
compareTN' : (s, t : Term 0 n) ->
|
||||||
(s, t : Term 0 n) ->
|
|
||||||
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
|
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
|
||||||
|
|
||||||
compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
|
compareTN' (E e) (E f) ps pt = compareE0 e f
|
||||||
-- if either term is a def, try to unfold it
|
-- if either term is a def, try to unfold it
|
||||||
compareTN' mode s@(E (F x)) t ps pt = do
|
compareTN' s@(E (F x)) t ps pt = do
|
||||||
Just s' <- defT x | Nothing => clashT mode s t
|
Just s' <- defT x | Nothing => clashT s t
|
||||||
compareT0 mode s' t
|
compareT0 s' t
|
||||||
compareTN' mode s t@(E (F y)) ps pt = do
|
compareTN' s t@(E (F y)) ps pt = do
|
||||||
Just t' <- defT y | Nothing => clashT mode s t
|
Just t' <- defT y | Nothing => clashT s t
|
||||||
compareT0 mode s t'
|
compareT0 s t'
|
||||||
compareTN' mode s@(E _) t _ _ = clashT mode s t
|
compareTN' s@(E _) t _ _ = clashT s t
|
||||||
|
|
||||||
compareTN' mode (TYPE k) (TYPE l) _ _ = compareU mode k l
|
compareTN' (TYPE k) (TYPE l) _ _ = compareU k l
|
||||||
compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
|
compareTN' s@(TYPE _) t _ _ = clashT s t
|
||||||
|
|
||||||
compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
|
compareTN' (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
|
||||||
unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
|
unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
|
||||||
compareT0 mode arg2 arg1 -- reversed for contravariant domain
|
compareT0 arg2 arg1 -- reversed for contravariant domain
|
||||||
compareTS0 mode res1 res2
|
compareTS0 res1 res2
|
||||||
compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
|
compareTN' s@(Pi {}) t _ _ = clashT s t
|
||||||
|
|
||||||
-- [todo] eta
|
-- [todo] eta
|
||||||
compareTN' _ (Lam _ body1) (Lam _ body2) _ _ =
|
compareTN' (Lam _ body1) (Lam _ body2) _ _ =
|
||||||
compareTS0 Equal body1 body2
|
local {mode := Equal} $ compareTS0 body1 body2
|
||||||
compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
|
compareTN' s@(Lam {}) t _ _ = clashT s t
|
||||||
|
|
||||||
compareTN' _ (CloT {}) _ ps _ = void $ ps IsCloT
|
compareTN' (CloT {}) _ ps _ = void $ ps IsCloT
|
||||||
compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
|
compareTN' (DCloT {}) _ ps _ = void $ ps IsDCloT
|
||||||
|
|
||||||
private covering
|
private covering
|
||||||
compareEN' : EqMode ->
|
compareEN' : (e, f : Elim 0 n) ->
|
||||||
(e, f : Elim 0 n) ->
|
|
||||||
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
|
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
|
||||||
|
|
||||||
compareEN' mode e@(F x) f@(F y) _ _ =
|
compareEN' e@(F x) f@(F y) _ _ =
|
||||||
if x == y then pure () else
|
if x == y then pure () else
|
||||||
case (!(defE x), !(defE y)) of
|
case (!(defE x), !(defE y)) of
|
||||||
(Nothing, Nothing) => clashE mode e f
|
(Nothing, Nothing) => clashE e f
|
||||||
(s', t') => compareE0 mode (fromMaybe e s') (fromMaybe f t')
|
(s', t') => compareE0 (fromMaybe e s') (fromMaybe f t')
|
||||||
compareEN' mode e@(F x) f _ _ = do
|
compareEN' e@(F x) f _ _ = do
|
||||||
Just e' <- defE x | Nothing => clashE mode e f
|
Just e' <- defE x | Nothing => clashE e f
|
||||||
compareE0 mode e' f
|
compareE0 e' f
|
||||||
compareEN' mode e f@(F y) _ _ = do
|
compareEN' e f@(F y) _ _ = do
|
||||||
Just f' <- defE y | Nothing => clashE mode e f
|
Just f' <- defE y | Nothing => clashE e f
|
||||||
compareE0 mode e f'
|
compareE0 e f'
|
||||||
|
|
||||||
compareEN' mode e@(B i) f@(B j) _ _ =
|
compareEN' e@(B i) f@(B j) _ _ =
|
||||||
unless (i == j) $ clashE mode e f
|
unless (i == j) $ clashE e f
|
||||||
compareEN' mode e@(B _) f _ _ = clashE mode e f
|
compareEN' e@(B _) f _ _ = clashE e f
|
||||||
|
|
||||||
-- [todo] tracking variance of functions? maybe???
|
-- [todo] tracking variance of functions? maybe???
|
||||||
-- probably not
|
-- probably not
|
||||||
compareEN' _ (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
|
compareEN' (fun1 :@ arg1) (fun2 :@ arg2) _ _ =
|
||||||
compareE0 Equal fun1 fun2
|
local {mode := Equal} $ do
|
||||||
compareT0 Equal arg1 arg2
|
compareE0 fun1 fun2
|
||||||
compareEN' mode e@(_ :@ _) f _ _ = clashE mode e f
|
compareT0 arg1 arg2
|
||||||
|
compareEN' e@(_ :@ _) f _ _ = clashE e f
|
||||||
|
|
||||||
-- [todo] is always checking the types are equal correct?
|
-- [todo] is always checking the types are equal correct?
|
||||||
compareEN' mode (tm1 :# ty1) (tm2 :# ty2) _ _ = do
|
compareEN' (tm1 :# ty1) (tm2 :# ty2) _ _ = do
|
||||||
compareT0 mode tm1 tm2
|
compareT0 tm1 tm2
|
||||||
compareT0 Equal ty1 ty2
|
local {mode := Equal} $ compareT0 ty1 ty2
|
||||||
compareEN' mode e@(_ :# _) f _ _ = clashE mode e f
|
compareEN' e@(_ :# _) f _ _ = clashE e f
|
||||||
|
|
||||||
compareEN' _ (CloE {}) _ pe _ = void $ pe IsCloE
|
compareEN' (CloE {}) _ pe _ = void $ pe IsCloE
|
||||||
compareEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
|
compareEN' (DCloE {}) _ pe _ = void $ pe IsDCloE
|
||||||
|
|
||||||
|
|
||||||
private covering %inline
|
private covering %inline
|
||||||
compareTN : EqMode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
|
compareTN : NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
|
||||||
compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd
|
compareTN s t = compareTN' s.fst t.fst s.snd t.snd
|
||||||
|
|
||||||
private covering %inline
|
private covering %inline
|
||||||
compareEN : EqMode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
|
compareEN : NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
|
||||||
compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
|
compareEN e f = compareEN' e.fst f.fst e.snd f.snd
|
||||||
|
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
compareT : EqMode -> DimEq d -> Term d n -> Term d n -> m ()
|
compareT : DimEq d -> Term d n -> Term d n -> m ()
|
||||||
compareT mode eqs s t =
|
compareT eqs s t =
|
||||||
for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
|
for_ (splits eqs) $ \th => compareT0 (s /// th) (t /// th)
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
compareE : EqMode -> DimEq d -> Elim d n -> Elim d n -> m ()
|
compareE : DimEq d -> Elim d n -> Elim d n -> m ()
|
||||||
compareE mode eqs e f =
|
compareE eqs e f =
|
||||||
for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
|
for_ (splits eqs) $ \th => compareE0 (e /// th) (f /// th)
|
||||||
|
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
compareT0 : EqMode -> Term 0 n -> Term 0 n -> m ()
|
compareT0 : Term 0 n -> Term 0 n -> m ()
|
||||||
compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
|
compareT0 s t = compareTN (whnfT s) (whnfT t)
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
compareE0 : EqMode -> Elim 0 n -> Elim 0 n -> m ()
|
compareE0 : Elim 0 n -> Elim 0 n -> m ()
|
||||||
compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
|
compareE0 e f = compareEN (whnfE e) (whnfE f)
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
compareTS0 : EqMode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
|
compareTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
|
||||||
compareTS0 mode (TUnused body1) (TUnused body2) =
|
compareTS0 (TUnused body1) (TUnused body2) =
|
||||||
compareT0 mode body1 body2
|
compareT0 body1 body2
|
||||||
compareTS0 mode body1 body2 =
|
compareTS0 body1 body2 =
|
||||||
compareT0 mode (fromScopeTerm body1) (fromScopeTerm body2)
|
compareT0 (fromScopeTerm body1) (fromScopeTerm body2)
|
||||||
|
|
||||||
|
|
||||||
|
parameters {auto _ : MonadError Error m} {auto _ : MonadReader Definitions m}
|
||||||
|
private %inline
|
||||||
|
into : EqMode ->
|
||||||
|
(forall n. MonadError Error n => MonadReader Env n =>
|
||||||
|
DimEq d -> a -> a -> n ()) ->
|
||||||
|
DimEq d -> a -> a -> m ()
|
||||||
|
into mode f eqs a b =
|
||||||
|
runReaderT {m} (MakeEnv {mode, defs = !ask}) $ f eqs a b
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
equalTWith : DimEq d -> Term d n -> Term d n -> m ()
|
equalTWith : DimEq d -> Term d n -> Term d n -> m ()
|
||||||
equalTWith = compareT Equal
|
equalTWith = into Equal compareT
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
|
equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
|
||||||
equalEWith = compareE Equal
|
equalEWith = into Equal compareE
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
subTWith : DimEq d -> Term d n -> Term d n -> m ()
|
subTWith : DimEq d -> Term d n -> Term d n -> m ()
|
||||||
subTWith = compareT Sub
|
subTWith = into Sub compareT
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
|
subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
|
||||||
subEWith = compareE Sub
|
subEWith = into Sub compareE
|
||||||
|
|
||||||
|
|
||||||
export covering %inline
|
export covering %inline
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue