-- | A syntactic equality check that takes meta instantiations into account,
--   but does not reduce.  It replaces
--   @
--      (v, v') <- instantiateFull (v, v')
--      v == v'
--   @
--   by a more efficient routine which only traverses and instantiates the terms
--   as long as they are equal.

module Agda.TypeChecking.SyntacticEquality (SynEq, checkSyntacticEquality) where

import Control.Arrow            ( (***) )
import Control.Monad            ( zipWithM )
import Control.Monad.State      ( MonadState(..), StateT, runStateT )
import Control.Monad.Trans      ( lift )

import Agda.Interaction.Options ( optSyntacticEquality )

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad (ReduceM, MonadReduce(..), pragmaOptions, isInstantiatedMeta)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import Agda.Utils.Monad (ifM)


-- | Syntactic equality check for terms.
--   @
--      checkSyntacticEquality v v' = do
--        (v, v') <- instantiateFull (v, v')
--         return ((v, v'), v==v')
--   @
--   only that @v, v'@ are only fully instantiated to the depth
--   where they are equal.
--
--   This means in particular that the returned @v,v'@ cannot be @MetaV@s
--   that are instantiated.

{-# SPECIALIZE checkSyntacticEquality :: Term -> Term -> ReduceM ((Term, Term), Bool) #-}
{-# SPECIALIZE checkSyntacticEquality :: Type -> Type -> ReduceM ((Type, Type), Bool) #-}
checkSyntacticEquality :: (Instantiate a, SynEq a, MonadReduce m) => a -> a -> m ((a, a), Bool)
checkSyntacticEquality :: a -> a -> m ((a, a), Bool)
checkSyntacticEquality a
v a
v' = ReduceM ((a, a), Bool) -> m ((a, a), Bool)
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM ((a, a), Bool) -> m ((a, a), Bool))
-> ReduceM ((a, a), Bool) -> m ((a, a), Bool)
forall a b. (a -> b) -> a -> b
$ do
  ReduceM Bool
-> ReduceM ((a, a), Bool)
-> ReduceM ((a, a), Bool)
-> ReduceM ((a, a), Bool)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optSyntacticEquality (PragmaOptions -> Bool) -> ReduceM PragmaOptions -> ReduceM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
  {-then-} (a -> a -> SynEqM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
v a
v' SynEqM (a, a) -> Bool -> ReduceM ((a, a), Bool)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Bool
True)
  {-else-} ((,Bool
False) ((a, a) -> ((a, a), Bool))
-> ReduceM (a, a) -> ReduceM ((a, a), Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a, a) -> ReduceM (a, a)
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (a
v,a
v'))

-- | Monad for checking syntactic equality
type SynEqM = StateT Bool ReduceM

-- | Return, flagging inequalty.
inequal :: a -> SynEqM a
inequal :: a -> SynEqM a
inequal a
a = Bool -> StateT Bool ReduceM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False StateT Bool ReduceM () -> SynEqM a -> SynEqM a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> SynEqM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | If inequality is flagged, return, else continue.
ifEqual :: (a -> SynEqM a) -> (a -> SynEqM a)
ifEqual :: (a -> SynEqM a) -> a -> SynEqM a
ifEqual a -> SynEqM a
cont a
a = StateT Bool ReduceM Bool -> SynEqM a -> SynEqM a -> SynEqM a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM StateT Bool ReduceM Bool
forall s (m :: * -> *). MonadState s m => m s
get (a -> SynEqM a
cont a
a) (a -> SynEqM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)

-- Since List2 is only Applicative, not a monad, I cannot
-- define a List2T monad transformer, so we do it manually:

(<$$>) :: Functor f => (a -> b) -> f (a, a) -> f (b, b)
a -> b
f <$$> :: (a -> b) -> f (a, a) -> f (b, b)
<$$> f (a, a)
xx = (a -> b
f (a -> b) -> (a -> b) -> (a, a) -> (b, b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a -> b
f) ((a, a) -> (b, b)) -> f (a, a) -> f (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (a, a)
xx

pure2 :: Applicative f => a -> f (a, a)
pure2 :: a -> f (a, a)
pure2 a
a = (a, a) -> f (a, a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, a
a)

(<**>) :: Applicative f => f (a -> b, a -> b) -> f (a, a) -> f (b, b)
f (a -> b, a -> b)
ff <**> :: f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> f (a, a)
xx = (((a -> b) -> (a -> b) -> (a, a) -> (b, b))
-> (a -> b, a -> b) -> (a, a) -> (b, b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> b) -> (a -> b) -> (a, a) -> (b, b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
(***)) ((a -> b, a -> b) -> (a, a) -> (b, b))
-> f (a -> b, a -> b) -> f ((a, a) -> (b, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (a -> b, a -> b)
ff f ((a, a) -> (b, b)) -> f (a, a) -> f (b, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (a, a)
xx

-- | Instantiate full as long as things are equal
class SynEq a where
  synEq  :: a -> a -> SynEqM (a, a)
  synEq' :: a -> a -> SynEqM (a, a)
  synEq' a
a a
a' = ((a, a) -> SynEqM (a, a)) -> (a, a) -> SynEqM (a, a)
forall a. (a -> SynEqM a) -> a -> SynEqM a
ifEqual ((a -> a -> SynEqM (a, a)) -> (a, a) -> SynEqM (a, a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> SynEqM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq) (a
a, a
a')

instance SynEq Bool where
  synEq :: Bool -> Bool -> SynEqM (Bool, Bool)
synEq Bool
x Bool
y | Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y    = (Bool, Bool) -> SynEqM (Bool, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
x, Bool
y)
  synEq Bool
x Bool
y | Bool
otherwise = (Bool, Bool) -> SynEqM (Bool, Bool)
forall a. a -> SynEqM a
inequal (Bool
x, Bool
y)

-- | Syntactic term equality ignores 'DontCare' stuff.
instance SynEq Term where
  synEq :: Term -> Term -> SynEqM (Term, Term)
synEq Term
v Term
v' = do
    (Term
v, Term
v') <- ReduceM (Term, Term) -> SynEqM (Term, Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReduceM (Term, Term) -> SynEqM (Term, Term))
-> ReduceM (Term, Term) -> SynEqM (Term, Term)
forall a b. (a -> b) -> a -> b
$ (Term, Term) -> ReduceM (Term, Term)
forall t. Instantiate t => t -> ReduceM t
instantiate' (Term
v, Term
v')
    case (Term
v, Term
v') of
      (Var   Int
i Elims
vs, Var   Int
i' Elims
vs') | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' -> Int -> Elims -> Term
Var Int
i   (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
vs Elims
vs'
      (Con ConHead
c ConInfo
i Elims
vs, Con ConHead
c' ConInfo
i' Elims
vs') | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c (ConInfo -> ConInfo -> ConInfo
bestConInfo ConInfo
i ConInfo
i') (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
vs Elims
vs'
      (Def   QName
f Elims
vs, Def   QName
f' Elims
vs') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> QName -> Elims -> Term
Def QName
f   (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
vs Elims
vs'
      (MetaV MetaId
x Elims
vs, MetaV MetaId
x' Elims
vs') | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x' -> MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
vs Elims
vs'
      (Lit   Literal
l   , Lit   Literal
l'    ) | Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l' -> Term -> SynEqM (Term, Term)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 (Term -> SynEqM (Term, Term)) -> Term -> SynEqM (Term, Term)
forall a b. (a -> b) -> a -> b
$ Term
v
      (Lam   ArgInfo
h Abs Term
b , Lam   ArgInfo
h' Abs Term
b' )           -> ArgInfo -> Abs Term -> Term
Lam (ArgInfo -> Abs Term -> Term)
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> StateT Bool ReduceM (Abs Term -> Term, Abs Term -> Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq ArgInfo
h ArgInfo
h' StateT Bool ReduceM (Abs Term -> Term, Abs Term -> Term)
-> StateT Bool ReduceM (Abs Term, Abs Term) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Abs Term -> Abs Term -> StateT Bool ReduceM (Abs Term, Abs Term)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Abs Term
b Abs Term
b'
      (Level Level
l   , Level Level
l'    )           -> Level -> Term
levelTm (Level -> Term)
-> StateT Bool ReduceM (Level, Level) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Level
l Level
l'
      (Sort  Sort
s   , Sort  Sort
s'    )           -> Sort -> Term
Sort    (Sort -> Term)
-> StateT Bool ReduceM (Sort, Sort) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Sort
s Sort
s'
      (Pi    Dom Type
a Abs Type
b , Pi    Dom Type
a' Abs Type
b' )           -> Dom Type -> Abs Type -> Term
Pi      (Dom Type -> Abs Type -> Term)
-> StateT Bool ReduceM (Dom Type, Dom Type)
-> StateT Bool ReduceM (Abs Type -> Term, Abs Type -> Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Dom Type -> Dom Type -> StateT Bool ReduceM (Dom Type, Dom Type)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Dom Type
a Dom Type
a' StateT Bool ReduceM (Abs Type -> Term, Abs Type -> Term)
-> StateT Bool ReduceM (Abs Type, Abs Type) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Abs Type -> Abs Type -> StateT Bool ReduceM (Abs Type, Abs Type)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' Abs Type
b Abs Type
b'
      (DontCare Term
u, DontCare Term
u' )           -> Term -> Term
DontCare (Term -> Term) -> SynEqM (Term, Term) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Term -> Term -> SynEqM (Term, Term)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Term
u Term
u'
         -- Irrelevant things are not syntactically equal. ALT:
         -- pure (u, u')
         -- Jesper, 2019-10-21: considering irrelevant things to be
         -- syntactically equal causes implicit arguments to go
         -- unsolved, so it is better to go under the DontCare.
      (Dummy{}   , Dummy{}     )           -> (Term, Term) -> SynEqM (Term, Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term
v, Term
v')
      (Term, Term)
_                                    -> (Term, Term) -> SynEqM (Term, Term)
forall a. a -> SynEqM a
inequal (Term
v, Term
v')

instance SynEq Level where
  synEq :: Level -> Level -> StateT Bool ReduceM (Level, Level)
synEq l :: Level
l@(Max Integer
n [PlusLevel' Term]
vs) l' :: Level
l'@(Max Integer
n' [PlusLevel' Term]
vs')
    | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n'   = Integer -> [PlusLevel' Term] -> Level
levelMax Integer
n ([PlusLevel' Term] -> Level)
-> StateT Bool ReduceM ([PlusLevel' Term], [PlusLevel' Term])
-> StateT Bool ReduceM (Level, Level)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> [PlusLevel' Term]
-> [PlusLevel' Term]
-> StateT Bool ReduceM ([PlusLevel' Term], [PlusLevel' Term])
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq [PlusLevel' Term]
vs [PlusLevel' Term]
vs'
    | Bool
otherwise = (Level, Level) -> StateT Bool ReduceM (Level, Level)
forall a. a -> SynEqM a
inequal (Level
l, Level
l')

instance SynEq PlusLevel where
  synEq :: PlusLevel' Term
-> PlusLevel' Term -> SynEqM (PlusLevel' Term, PlusLevel' Term)
synEq l :: PlusLevel' Term
l@(Plus Integer
n Term
v) l' :: PlusLevel' Term
l'@(Plus Integer
n' Term
v')
    | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n'   = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel' Term)
-> SynEqM (Term, Term) -> SynEqM (PlusLevel' Term, PlusLevel' Term)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Term -> Term -> SynEqM (Term, Term)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Term
v Term
v'
    | Bool
otherwise = (PlusLevel' Term, PlusLevel' Term)
-> SynEqM (PlusLevel' Term, PlusLevel' Term)
forall a. a -> SynEqM a
inequal (PlusLevel' Term
l, PlusLevel' Term
l')

instance SynEq Sort where
  synEq :: Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
synEq Sort
s Sort
s' = do
    (Sort
s, Sort
s') <- ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort))
-> ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
forall a b. (a -> b) -> a -> b
$ (Sort, Sort) -> ReduceM (Sort, Sort)
forall t. Instantiate t => t -> ReduceM t
instantiate' (Sort
s, Sort
s')
    case (Sort
s, Sort
s') of
      (Type Level
l  , Type Level
l'   ) -> Level -> Sort
forall t. Level' t -> Sort' t
Type (Level -> Sort)
-> StateT Bool ReduceM (Level, Level)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Level
l Level
l'
      (PiSort Dom' Term Term
a Sort
b Abs Sort
c, PiSort Dom' Term Term
a' Sort
b' Abs Sort
c') -> Dom' Term Term -> Sort -> Abs Sort -> Sort
piSort (Dom' Term Term -> Sort -> Abs Sort -> Sort)
-> StateT Bool ReduceM (Dom' Term Term, Dom' Term Term)
-> StateT
     Bool ReduceM (Sort -> Abs Sort -> Sort, Sort -> Abs Sort -> Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Dom' Term Term
-> Dom' Term Term
-> StateT Bool ReduceM (Dom' Term Term, Dom' Term Term)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Dom' Term Term
a Dom' Term Term
a' StateT
  Bool ReduceM (Sort -> Abs Sort -> Sort, Sort -> Abs Sort -> Sort)
-> StateT Bool ReduceM (Sort, Sort)
-> StateT Bool ReduceM (Abs Sort -> Sort, Abs Sort -> Sort)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' Sort
b Sort
b' StateT Bool ReduceM (Abs Sort -> Sort, Abs Sort -> Sort)
-> StateT Bool ReduceM (Abs Sort, Abs Sort)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Abs Sort -> Abs Sort -> StateT Bool ReduceM (Abs Sort, Abs Sort)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' Abs Sort
c Abs Sort
c'
      (FunSort Sort
a Sort
b, FunSort Sort
a' Sort
b') -> Sort -> Sort -> Sort
funSort (Sort -> Sort -> Sort)
-> StateT Bool ReduceM (Sort, Sort)
-> StateT Bool ReduceM (Sort -> Sort, Sort -> Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Sort
a Sort
a' StateT Bool ReduceM (Sort -> Sort, Sort -> Sort)
-> StateT Bool ReduceM (Sort, Sort)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' Sort
b Sort
b'
      (UnivSort Sort
a, UnivSort Sort
a') -> Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort (Sort -> Sort)
-> StateT Bool ReduceM (Sort, Sort)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Sort
a Sort
a'
      (Sort
SizeUniv, Sort
SizeUniv  ) -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
LockUniv, Sort
LockUniv  ) -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Prop Level
l  , Prop Level
l'   ) -> Level -> Sort
forall t. Level' t -> Sort' t
Prop (Level -> Sort)
-> StateT Bool ReduceM (Level, Level)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Level
l Level
l'
      (Inf IsFibrant
f Integer
m , Inf IsFibrant
f' Integer
n) | IsFibrant
f IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
f', Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (SSet Level
l  , SSet Level
l'   ) -> Level -> Sort
forall t. Level' t -> Sort' t
SSet (Level -> Sort)
-> StateT Bool ReduceM (Level, Level)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Level -> Level -> StateT Bool ReduceM (Level, Level)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Level
l Level
l'
      (MetaS MetaId
x Elims
es , MetaS MetaId
x' Elims
es') | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x' -> MetaId -> Elims -> Sort
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort)
-> StateT Bool ReduceM (Elims, Elims)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
es Elims
es'
      (DefS  QName
d Elims
es , DefS  QName
d' Elims
es') | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' -> QName -> Elims -> Sort
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d  (Elims -> Sort)
-> StateT Bool ReduceM (Elims, Elims)
-> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Elims -> Elims -> StateT Bool ReduceM (Elims, Elims)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Elims
es Elims
es'
      (DummyS{}, DummyS{}) -> (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort
s, Sort
s')
      (Sort, Sort)
_ -> (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
forall a. a -> SynEqM a
inequal (Sort
s, Sort
s')

-- | Syntactic equality ignores sorts.
instance SynEq Type where
  synEq :: Type -> Type -> SynEqM (Type, Type)
synEq (El Sort
s Term
t) (El Sort
s' Term
t') = (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> (Term -> Type) -> (Term, Term) -> (Type, Type)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s') ((Term, Term) -> (Type, Type))
-> SynEqM (Term, Term) -> SynEqM (Type, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Term -> SynEqM (Term, Term)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Term
t Term
t'

instance SynEq a => SynEq [a] where
  synEq :: [a] -> [a] -> SynEqM ([a], [a])
synEq [a]
as [a]
as'
    | [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as' = [(a, a)] -> ([a], [a])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(a, a)] -> ([a], [a]))
-> StateT Bool ReduceM [(a, a)] -> SynEqM ([a], [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> a -> StateT Bool ReduceM (a, a))
-> [a] -> [a] -> StateT Bool ReduceM [(a, a)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq' [a]
as [a]
as'
    | Bool
otherwise               = ([a], [a]) -> SynEqM ([a], [a])
forall a. a -> SynEqM a
inequal ([a]
as, [a]
as')

instance (SynEq a, SynEq b) => SynEq (a,b) where
  synEq :: (a, b) -> (a, b) -> SynEqM ((a, b), (a, b))
synEq (a
a,b
b) (a
a',b
b') = (,) (a -> b -> (a, b))
-> StateT Bool ReduceM (a, a)
-> StateT Bool ReduceM (b -> (a, b), b -> (a, b))
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
a a
a' StateT Bool ReduceM (b -> (a, b), b -> (a, b))
-> StateT Bool ReduceM (b, b) -> SynEqM ((a, b), (a, b))
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> b -> b -> StateT Bool ReduceM (b, b)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq b
b b
b'

instance SynEq a => SynEq (Elim' a) where
  synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)
synEq Elim' a
e Elim' a
e' =
    case (Elim' a
e, Elim' a
e') of
      (Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> Elim' a -> SynEqM (Elim' a, Elim' a)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Elim' a
e
      (Apply Arg a
a, Apply Arg a
a') -> Arg a -> Elim' a
forall a. Arg a -> Elim' a
Apply (Arg a -> Elim' a)
-> StateT Bool ReduceM (Arg a, Arg a) -> SynEqM (Elim' a, Elim' a)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> Arg a -> Arg a -> StateT Bool ReduceM (Arg a, Arg a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Arg a
a Arg a
a'
      (IApply a
u a
v a
r, IApply a
u' a
v' a
r')
                          -> (a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
u a
v (a -> Elim' a) -> (a -> Elim' a) -> (a, a) -> (Elim' a, Elim' a)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** a -> a -> a -> Elim' a
forall a. a -> a -> a -> Elim' a
IApply a
u' a
v') ((a, a) -> (Elim' a, Elim' a))
-> StateT Bool ReduceM (a, a) -> SynEqM (Elim' a, Elim' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
r a
r'
      (Elim' a, Elim' a)
_                   -> (Elim' a, Elim' a) -> SynEqM (Elim' a, Elim' a)
forall a. a -> SynEqM a
inequal (Elim' a
e, Elim' a
e')

instance (Subst a, SynEq a) => SynEq (Abs a) where
  synEq :: Abs a -> Abs a -> SynEqM (Abs a, Abs a)
synEq Abs a
a Abs a
a' =
    case (Abs a
a, Abs a
a') of
      (NoAbs ArgName
x a
b, NoAbs ArgName
x' a
b') -> (ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x (a -> Abs a) -> (a -> Abs a) -> (a, a) -> (Abs a, Abs a)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs ArgName
x') ((a, a) -> (Abs a, Abs a))
-> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
b a
b'
      (Abs   ArgName
x a
b, Abs   ArgName
x' a
b') -> (ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x (a -> Abs a) -> (a -> Abs a) -> (a, a) -> (Abs a, Abs a)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x') ((a, a) -> (Abs a, Abs a))
-> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
b a
b'
      (Abs   ArgName
x a
b, NoAbs ArgName
x' a
b') -> ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x  (a -> Abs a) -> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
b (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
1 a
b')  -- TODO: mkAbs?
      (NoAbs ArgName
x a
b, Abs   ArgName
x' a
b') -> ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs ArgName
x' (a -> Abs a) -> StateT Bool ReduceM (a, a) -> SynEqM (Abs a, Abs a)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
1 a
b) a
b'

-- NOTE: Do not ignore 'ArgInfo', or test/fail/UnequalHiding will pass.
instance SynEq a => SynEq (Arg a) where
  synEq :: Arg a -> Arg a -> SynEqM (Arg a, Arg a)
synEq (Arg ArgInfo
ai a
a) (Arg ArgInfo
ai' a
a') = ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> a -> Arg a)
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> StateT Bool ReduceM (a -> Arg a, a -> Arg a)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq ArgInfo
ai ArgInfo
ai' StateT Bool ReduceM (a -> Arg a, a -> Arg a)
-> StateT Bool ReduceM (a, a) -> SynEqM (Arg a, Arg a)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
a a
a'

-- Ignore the tactic.
instance SynEq a => SynEq (Dom a) where
  synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
synEq d :: Dom a
d@(Dom ArgInfo
ai Bool
b Maybe NamedName
x Maybe Term
t a
a) d' :: Dom a
d'@(Dom ArgInfo
ai' Bool
b' Maybe NamedName
x' Maybe Term
_ a
a')
    | Maybe NamedName
x Maybe NamedName -> Maybe NamedName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'   = ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Bool -> Maybe NamedName -> Maybe t -> e -> Dom' t e
Dom (ArgInfo -> Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> StateT
     Bool
     ReduceM
     (Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a,
      Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq ArgInfo
ai ArgInfo
ai' StateT
  Bool
  ReduceM
  (Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a,
   Bool -> Maybe NamedName -> Maybe Term -> a -> Dom a)
-> SynEqM (Bool, Bool)
-> StateT
     Bool
     ReduceM
     (Maybe NamedName -> Maybe Term -> a -> Dom a,
      Maybe NamedName -> Maybe Term -> a -> Dom a)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Bool -> Bool -> SynEqM (Bool, Bool)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Bool
b Bool
b' StateT
  Bool
  ReduceM
  (Maybe NamedName -> Maybe Term -> a -> Dom a,
   Maybe NamedName -> Maybe Term -> a -> Dom a)
-> StateT Bool ReduceM (Maybe NamedName, Maybe NamedName)
-> StateT
     Bool ReduceM (Maybe Term -> a -> Dom a, Maybe Term -> a -> Dom a)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Maybe NamedName
-> StateT Bool ReduceM (Maybe NamedName, Maybe NamedName)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Maybe NamedName
x StateT
  Bool ReduceM (Maybe Term -> a -> Dom a, Maybe Term -> a -> Dom a)
-> StateT Bool ReduceM (Maybe Term, Maybe Term)
-> StateT Bool ReduceM (a -> Dom a, a -> Dom a)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> Maybe Term -> StateT Bool ReduceM (Maybe Term, Maybe Term)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Maybe Term
t StateT Bool ReduceM (a -> Dom a, a -> Dom a)
-> StateT Bool ReduceM (a, a) -> SynEqM (Dom a, Dom a)
forall (f :: * -> *) a b.
Applicative f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> a -> a -> StateT Bool ReduceM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
a a
a'
    | Bool
otherwise = (Dom a, Dom a) -> SynEqM (Dom a, Dom a)
forall a. a -> SynEqM a
inequal (Dom a
d, Dom a
d')

instance SynEq ArgInfo where
  synEq :: ArgInfo -> ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
synEq ai :: ArgInfo
ai@(ArgInfo Hiding
h Modality
r Origin
o FreeVariables
_ Annotation
a) ai' :: ArgInfo
ai'@(ArgInfo Hiding
h' Modality
r' Origin
o' FreeVariables
_ Annotation
a')
    | Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
h', Modality -> Modality -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality Modality
r Modality
r', Annotation
a Annotation -> Annotation -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation
a' = ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 ArgInfo
ai
    | Bool
otherwise        = (ArgInfo, ArgInfo) -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall a. a -> SynEqM a
inequal (ArgInfo
ai, ArgInfo
ai')