quox/lib/Quox/Equal.idr

186 lines
5.8 KiB
Idris

module Quox.Equal
import public Quox.Syntax
import public Quox.Definition
import public Quox.Typing
import public Control.Monad.Either
import public Control.Monad.Reader
import Data.Maybe
private %inline
ClashE : EqMode -> Elim d n -> Elim d n -> Error
ClashE mode = ClashT mode `on` E
public export
CanEq : (Type -> Type) -> Type
CanEq m = (MonadError Error m, MonadReader Definitions m)
parameters {auto _ : CanEq m}
private %inline
clashT : EqMode -> Term d n -> Term d n -> m a
clashT mode = throwError .: ClashT mode
private %inline
clashE : EqMode -> Elim d n -> Elim d n -> m a
clashE mode = throwError .: ClashE mode
private %inline
defE : Name -> m (Maybe (Elim d n))
defE x = asks $ \defs => do
g <- lookup x defs
pure $ (!g.term).def :# g.type.def
private %inline
defT : Name -> m (Maybe (Term d n))
defT x = map E <$> defE x
export %inline
compareU' : EqMode -> Universe -> Universe -> Bool
compareU' = \case Equal => (==); Sub => (<=)
export %inline
compareU : EqMode -> Universe -> Universe -> m ()
compareU mode k l = unless (compareU' mode k l) $
throwError $ ClashU mode k l
mutual
private covering
compareTN' : EqMode ->
(s, t : Term 0 n) ->
(0 _ : NotRedexT s) -> (0 _ : NotRedexT t) -> m ()
compareTN' mode (E e) (E f) ps pt = compareE0 mode e f
-- if either term is a def, try to unfold it
compareTN' mode s@(E (F x)) t ps pt = do
Just s' <- defT x | Nothing => clashT mode s t
compareT0 mode s' t
compareTN' mode s t@(E (F y)) ps pt = do
Just t' <- defT y | Nothing => clashT mode s t
compareT0 mode s t'
compareTN' mode s@(E _) t _ _ = clashT mode s t
compareTN' mode (TYPE k) (TYPE l) _ _ = compareU mode k l
compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
unless (qty1 == qty2) $ throwError $ ClashQ qty1 qty2
compareT0 mode arg2 arg1 -- reversed for contravariant domain
compareTS0 mode res1 res2
compareTN' mode s@(Pi {}) t _ _ = clashT mode s t
-- [todo] eta
compareTN' _ (Lam _ body1) (Lam _ body2) _ _ =
compareTS0 Equal body1 body2
compareTN' mode s@(Lam {}) t _ _ = clashT mode s t
compareTN' _ (CloT {}) _ ps _ = void $ ps IsCloT
compareTN' _ (DCloT {}) _ ps _ = void $ ps IsDCloT
private covering
compareEN' : EqMode ->
(e, f : Elim 0 n) ->
(0 _ : NotRedexE e) -> (0 _ : NotRedexE f) -> m ()
compareEN' mode e@(F x) f@(F y) _ _ =
if x == y then pure () else
case (!(defE x), !(defE y)) of
(Nothing, Nothing) => clashE mode e f
(s', t') => compareE0 mode (fromMaybe e s') (fromMaybe f t')
compareEN' mode e@(F x) f _ _ = do
Just e' <- defE x | Nothing => clashE mode e f
compareE0 mode e' f
compareEN' mode e f@(F y) _ _ = do
Just f' <- defE y | Nothing => clashE mode e f
compareE0 mode e f'
compareEN' mode e@(B i) f@(B j) _ _ =
unless (i == j) $ clashE mode e f
compareEN' mode e@(B _) f _ _ = clashE mode e f
-- [todo] tracking variance of functions? maybe???
-- probably not
compareEN' _ (fun1 :@ arg1) (fun2 :@ arg2) _ _ = do
compareE0 Equal fun1 fun2
compareT0 Equal arg1 arg2
compareEN' mode e@(_ :@ _) f _ _ = clashE mode e f
-- [todo] is always checking the types are equal correct?
compareEN' mode (tm1 :# ty1) (tm2 :# ty2) _ _ = do
compareT0 mode tm1 tm2
compareT0 Equal ty1 ty2
compareEN' mode e@(_ :# _) f _ _ = clashE mode e f
compareEN' _ (CloE {}) _ pe _ = void $ pe IsCloE
compareEN' _ (DCloE {}) _ pe _ = void $ pe IsDCloE
private covering %inline
compareTN : EqMode -> NonRedexTerm 0 n -> NonRedexTerm 0 n -> m ()
compareTN mode s t = compareTN' mode s.fst t.fst s.snd t.snd
private covering %inline
compareEN : EqMode -> NonRedexElim 0 n -> NonRedexElim 0 n -> m ()
compareEN mode e f = compareEN' mode e.fst f.fst e.snd f.snd
export covering %inline
compareT : EqMode -> DimEq d -> Term d n -> Term d n -> m ()
compareT mode eqs s t =
for_ (splits eqs) $ \th => compareT0 mode (s /// th) (t /// th)
export covering %inline
compareE : EqMode -> DimEq d -> Elim d n -> Elim d n -> m ()
compareE mode eqs e f =
for_ (splits eqs) $ \th => compareE0 mode (e /// th) (f /// th)
export covering %inline
compareT0 : EqMode -> Term 0 n -> Term 0 n -> m ()
compareT0 mode s t = compareTN mode (whnfT s) (whnfT t)
export covering %inline
compareE0 : EqMode -> Elim 0 n -> Elim 0 n -> m ()
compareE0 mode e f = compareEN mode (whnfE e) (whnfE f)
export covering %inline
compareTS0 : EqMode -> ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
compareTS0 mode (TUnused body1) (TUnused body2) =
compareT0 mode body1 body2
compareTS0 mode body1 body2 =
compareT0 mode (fromScopeTerm body1) (fromScopeTerm body2)
export covering %inline
equalTWith : DimEq d -> Term d n -> Term d n -> m ()
equalTWith = compareT Equal
export covering %inline
equalEWith : DimEq d -> Elim d n -> Elim d n -> m ()
equalEWith = compareE Equal
export covering %inline
subTWith : DimEq d -> Term d n -> Term d n -> m ()
subTWith = compareT Sub
export covering %inline
subEWith : DimEq d -> Elim d n -> Elim d n -> m ()
subEWith = compareE Sub
export covering %inline
equalT : {d : Nat} -> Term d n -> Term d n -> m ()
equalT = equalTWith DimEq.new
export covering %inline
equalE : {d : Nat} -> Elim d n -> Elim d n -> m ()
equalE = equalEWith DimEq.new
export covering %inline
subT : {d : Nat} -> Term d n -> Term d n -> m ()
subT = subTWith DimEq.new
export covering %inline
subE : {d : Nat} -> Elim d n -> Elim d n -> m ()
subE = subEWith DimEq.new