{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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
  , checkSyntacticEquality'
  , syntacticEqualityFuelRemains
  )
  where

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

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

import Agda.TypeChecking.Monad  ( ReduceM, MonadReduce(..), TCEnv(..), MonadTCEnv(..) )
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad (ifM)
import Agda.Utils.Unsafe (unsafeComparePointers)

-- | Syntactic equality check for terms. If syntactic equality
-- checking has fuel left, then 'checkSyntacticEquality' behaves as if
-- it were implemented in the following way (which does not match the
-- given type signature), only that @v@ and @v'@ are only fully
-- instantiated to the depth where they are equal (and the amount of
-- fuel is reduced by one unit in the failure branch):
--   @
--      checkSyntacticEquality v v' s f = do
--        (v, v') <- instantiateFull (v, v')
--        if v == v' then s v v' else f v v'
--   @
-- If syntactic equality checking does not have fuel left, then
-- 'checkSyntacticEquality' instantiates the two terms and takes the
-- failure branch.
--
-- Note that in either case the returned values @v@ and @v'@ cannot be
-- @MetaV@s that are instantiated.

{-# SPECIALIZE checkSyntacticEquality ::
      Term -> Term ->
      (Term -> Term -> ReduceM a) ->
      (Term -> Term -> ReduceM a) ->
      ReduceM a #-}
{-# SPECIALIZE checkSyntacticEquality ::
      Type -> Type ->
      (Type -> Type -> ReduceM a) ->
      (Type -> Type -> ReduceM a) ->
      ReduceM a #-}
checkSyntacticEquality
  :: (Instantiate a, SynEq a, MonadReduce m)
  => a
  -> a
  -> (a -> a -> m b)  -- ^ Continuation used upon success.
  -> (a -> a -> m b)  -- ^ Continuation used upon failure, or if
                      --   syntactic equality checking has been turned
                      --   off.
  -> m b
checkSyntacticEquality :: forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality a
u a
v a -> a -> m b
s a -> a -> m b
f =
  m Bool -> m b -> m b -> m b
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). MonadReduce m => m Bool
syntacticEqualityFuelRemains
  {-then-} (a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality' a
u a
v a -> a -> m b
s (\a
u a
v -> (TCEnv -> TCEnv) -> m b -> m b
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC TCEnv -> TCEnv
decreaseFuel (a -> a -> m b
f a
u a
v)))
  {-else-} ((a -> a -> m b) -> (a, a) -> m b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> m b
f ((a, a) -> m b) -> m (a, a) -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a, a) -> m (a, a)
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (a
u, a
v))
  where
  decreaseFuel :: TCEnv -> TCEnv
decreaseFuel TCEnv
env =
    case TCEnv -> Maybe Int
envSyntacticEqualityFuel TCEnv
env of
      Maybe Int
Strict.Nothing -> TCEnv
env
      Strict.Just Int
n  ->
        TCEnv
env { envSyntacticEqualityFuel = Strict.Just (pred n) }

-- | Syntactic equality check for terms without checking remaining fuel.

{-# SPECIALIZE checkSyntacticEquality' ::
      Term -> Term ->
      (Term -> Term -> ReduceM a) ->
      (Term -> Term -> ReduceM a) ->
      ReduceM a #-}
{-# SPECIALIZE checkSyntacticEquality' ::
      Type -> Type ->
      (Type -> Type -> ReduceM a) ->
      (Type -> Type -> ReduceM a) ->
      ReduceM a #-}
checkSyntacticEquality'
  :: (Instantiate a, SynEq a, MonadReduce m)
  => a
  -> a
  -> (a -> a -> m b)  -- ^ Continuation used upon success.
  -> (a -> a -> m b)  -- ^ Continuation used upon failure.
  -> m b
checkSyntacticEquality' :: forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
checkSyntacticEquality' a
u a
v a -> a -> m b
s a -> a -> m b
f = do
  ((a
u, a
v), Bool
equal) <- ReduceM ((a, a), Bool) -> m ((a, a), Bool)
forall a. ReduceM a -> m a
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
$ a -> a -> SynEqM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
u 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
  if Bool
equal then a -> a -> m b
s a
u a
v else a -> a -> m b
f a
u a
v

-- | Does the syntactic equality check have any remaining fuel?

syntacticEqualityFuelRemains :: MonadReduce m => m Bool
syntacticEqualityFuelRemains :: forall (m :: * -> *). MonadReduce m => m Bool
syntacticEqualityFuelRemains = do
  Maybe Int
fuel <- TCEnv -> Maybe Int
envSyntacticEqualityFuel (TCEnv -> Maybe Int) -> m TCEnv -> m (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
  Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ case Maybe Int
fuel of
    Maybe Int
Strict.Nothing -> Bool
True
    Strict.Just Int
n  -> Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0

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

-- | Return, flagging inequalty.
inequal :: a -> SynEqM a
inequal :: forall a. a -> SynEqM a
inequal a
a = Bool -> StateT Bool ReduceM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False StateT Bool ReduceM ()
-> StateT Bool ReduceM a -> StateT Bool ReduceM a
forall a b.
StateT Bool ReduceM a
-> StateT Bool ReduceM b -> StateT Bool ReduceM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> StateT Bool ReduceM a
forall a. 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 :: forall a. (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 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 <$$> :: forall (f :: * -> *) a b.
Functor 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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 :: forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 a
a = (a, a) -> f (a, a)
forall a. a -> f 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 <**> :: forall (f :: * -> *) a b.
Applicative f =>
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 a b. f (a -> b) -> f a -> f 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 a. a -> SynEqM a
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' = if Term -> Term -> Bool
forall a. a -> a -> Bool
unsafeComparePointers Term
v Term
v' then (Term, Term) -> SynEqM (Term, Term)
forall a. a -> SynEqM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Term
v') else do
    (Term
v, Term
v') <- ReduceM (Term, Term) -> SynEqM (Term, Term)
forall (m :: * -> *) a. Monad m => m a -> StateT Bool m a
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 a. a -> SynEqM a
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]
vs) l' :: Level
l'@(Max Integer
n' [PlusLevel]
vs')
    | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n'   = Integer -> [PlusLevel] -> Level
levelMax Integer
n ([PlusLevel] -> Level)
-> StateT Bool ReduceM ([PlusLevel], [PlusLevel])
-> StateT Bool ReduceM (Level, Level)
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> [PlusLevel]
-> [PlusLevel] -> StateT Bool ReduceM ([PlusLevel], [PlusLevel])
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq [PlusLevel]
vs [PlusLevel]
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 -> PlusLevel -> SynEqM (PlusLevel, PlusLevel)
synEq l :: PlusLevel
l@(Plus Integer
n Term
v) l' :: PlusLevel
l'@(Plus Integer
n' Term
v')
    | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n'   = Integer -> Term -> PlusLevel
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel)
-> SynEqM (Term, Term) -> SynEqM (PlusLevel, PlusLevel)
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, PlusLevel) -> SynEqM (PlusLevel, PlusLevel)
forall a. a -> SynEqM a
inequal (PlusLevel
l, PlusLevel
l')

instance SynEq Sort where
  synEq :: Sort -> Sort -> StateT Bool ReduceM (Sort, Sort)
synEq Sort
s Sort
s' = if Sort -> Sort -> Bool
forall a. a -> a -> Bool
unsafeComparePointers Sort
s Sort
s' then (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
forall a. a -> SynEqM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort
s, Sort
s') else do
    (Sort
s, Sort
s') <- ReduceM (Sort, Sort) -> StateT Bool ReduceM (Sort, Sort)
forall (m :: * -> *) a. Monad m => m a -> StateT Bool m a
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
      (Univ Univ
u Level
l, Univ Univ
u' Level
l') | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' -> Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (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
a Sort
b Abs Sort
c, PiSort Dom Term
a' Sort
b' Abs Sort
c') -> Dom Term -> Sort -> Abs Sort -> Sort
piSort (Dom Term -> Sort -> Abs Sort -> Sort)
-> StateT Bool ReduceM (Dom Term, Dom 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 -> Dom Term -> StateT Bool ReduceM (Dom Term, Dom Term)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Dom Term
a Dom 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
      (Sort
LevelUniv, Sort
LevelUniv  ) -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
IntervalUniv, Sort
IntervalUniv) -> Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Inf Univ
u Integer
m , Inf Univ
u' Integer
n) | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u', 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
      (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 a. a -> SynEqM a
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 a. [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 a. [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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
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 Maybe NamedName
x Bool
f Maybe Term
t a
a) d' :: Dom a
d'@(Dom ArgInfo
ai' Maybe NamedName
x' Bool
f' Maybe Term
_ a
a')
    | Maybe NamedName
x Maybe NamedName -> Maybe NamedName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'   = ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a
forall t e.
ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e
Dom (ArgInfo -> Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> StateT
     Bool
     ReduceM
     (Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a,
      Maybe NamedName -> Bool -> 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
  (Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a,
   Maybe NamedName -> Bool -> Maybe Term -> a -> Dom a)
-> StateT Bool ReduceM (Maybe NamedName, Maybe NamedName)
-> StateT
     Bool
     ReduceM
     (Bool -> Maybe Term -> a -> Dom a,
      Bool -> 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
  (Bool -> Maybe Term -> a -> Dom a,
   Bool -> Maybe Term -> a -> Dom a)
-> SynEqM (Bool, Bool)
-> 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)
<**> Bool -> Bool -> SynEqM (Bool, Bool)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq Bool
f Bool
f' 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')