{-# LANGUAGE CPP #-}
{-# LANGUAGE Strict #-}
#if  __GLASGOW_HASKELL__ > 902
{-# OPTIONS_GHC -fworker-wrapper-cbv #-}
#endif
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wno-redundant-bang-patterns #-}

-- | 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.Monad
import Control.Monad.Trans      ( lift )

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import Agda.Utils.ExpandCase
import Agda.Utils.Maybe.Strict  qualified as Strict
import Agda.Utils.Monad         ( ifM )
import Agda.Utils.Unsafe        ( unsafeComparePointers )
import Agda.Utils.Tuple         ( (***) )
import Agda.Utils.StrictState


-- | 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 -> TCM a) ->
      (Type -> Type -> TCM a) ->
      TCM 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.
(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
env TCEnv -> Getting (Maybe Int) TCEnv (Maybe Int) -> Maybe Int
forall s a. s -> Getting a s a -> a
^. Getting (Maybe Int) TCEnv (Maybe Int)
Lens' TCEnv (Maybe Int)
eSyntacticEqualityFuel of
      Maybe Int
Strict.Nothing -> TCEnv
env
      Strict.Just Int
n  -> TCEnv
env TCEnv -> (TCEnv -> TCEnv) -> TCEnv
forall a b. a -> (a -> b) -> b
& (Maybe Int -> Identity (Maybe Int)) -> TCEnv -> Identity TCEnv
Lens' TCEnv (Maybe Int)
eSyntacticEqualityFuel ((Maybe Int -> Identity (Maybe Int)) -> TCEnv -> Identity TCEnv)
-> Maybe Int -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Int -> Maybe Int
forall a. a -> Maybe a
Strict.Just (Int -> Int
forall a. Enum a => a -> a
pred Int
n)

-- | Syntactic equality check for terms without checking remaining fuel.
checkSyntacticEquality'
  :: (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.
(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
  ((u, v), 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 (m :: * -> *) s a. Monad m => StateT s m a -> s -> m (a, s)
`runStateT` Bool
True
  if equal then s u v else f u v

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

syntacticEqualityFuelRemains :: MonadReduce m => m Bool
syntacticEqualityFuelRemains :: forall (m :: * -> *). MonadReduce m => m Bool
syntacticEqualityFuelRemains = do
  fuel <- Lens' TCEnv (Maybe Int) -> m (Maybe Int)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe Int -> f (Maybe Int)) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe Int)
eSyntacticEqualityFuel
  return $! case 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

-- Since List2 is only Applicative, not a monad, I cannot
-- define a List2T monad transformer, so we do it manually:
{-# INLINE (<$$>) #-}
(<$$>) :: Monad f => (a -> b) -> f (a, a) -> f (b, b)
a -> b
f <$$> :: forall (f :: * -> *) a b.
Monad f =>
(a -> b) -> f (a, a) -> f (b, b)
<$$> f (a, a)
aa = do
  (a, a') <- f (a, a)
aa
  let b  = a -> b
f a
a
  let b' = a -> b
f a
a'
  pure (b, b')

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)

{-# INLINE (<**>) #-}
(<**>) :: Monad f => f (a -> b, a -> b) -> f (a, a) -> f (b, b)
f (a -> b, a -> b)
ff <**> :: forall (f :: * -> *) a b.
Monad f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> f (a, a)
aa = do
  (f, f') <- f (a -> b, a -> b)
ff
  (a, a') <- aa
  let b = a -> b
f a
a
  let b' = a -> b
f' a
a'
  pure (b, b')

-- | Instantiate full as long as things are equal
class SynEq a where
  synEq  :: a -> a -> SynEqM (a, a)

  {-# INLINE synEq' #-}
  synEq' :: a -> a -> SynEqM (a, a)
  synEq' a
a a
a' = do
    eq <- StateT Bool ReduceM Bool
forall s (m :: * -> *). MonadState s m => m s
get
    expand \SynEqM (a, a) -> Result (SynEqM (a, a))
ret -> if Bool
eq then SynEqM (a, a) -> Result (SynEqM (a, a))
ret (SynEqM (a, a) -> Result (SynEqM (a, a)))
-> SynEqM (a, a) -> Result (SynEqM (a, a))
forall a b. (a -> b) -> a -> b
$ a -> a -> SynEqM (a, a)
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq a
a a
a'
                         else SynEqM (a, a) -> Result (SynEqM (a, a))
ret (SynEqM (a, a) -> Result (SynEqM (a, a)))
-> SynEqM (a, a) -> Result (SynEqM (a, a))
forall a b. (a -> b) -> a -> b
$ (a, a) -> SynEqM (a, a)
forall a. a -> SynEqM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
a, a
a')

instance SynEq Bool where
  synEq :: Bool -> Bool -> SynEqM (Bool, Bool)
synEq Bool
x Bool
y = ((SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool)))
 -> Result (SynEqM (Bool, Bool)))
-> SynEqM (Bool, Bool)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool))
ret -> if Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
y then SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool))
ret (SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool)))
-> SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool))
forall a b. (a -> b) -> a -> b
$ (Bool, Bool) -> SynEqM (Bool, Bool)
forall a. a -> SynEqM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
x, Bool
y) else SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool))
ret (SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool)))
-> SynEqM (Bool, Bool) -> Result (SynEqM (Bool, Bool))
forall a b. (a -> b) -> a -> b
$ (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' = ((SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
 -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret -> if Term -> Term -> Bool
forall a. a -> a -> Bool
unsafeComparePointers Term
v Term
v' then SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ (Term, Term) -> SynEqM (Term, Term)
forall a. a -> SynEqM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term
v, Term
v') else SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret do
    (v, 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')
    expand \SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret -> 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' -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ Int -> Elims -> Term
Var Int
i   (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Monad 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' -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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' -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f   (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Monad 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' -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term)
-> StateT Bool ReduceM (Elims, Elims) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Monad 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' -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ 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' )            -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> 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.
Monad 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.
Monad 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'    )            -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ Level -> Term
levelTm (Level -> Term)
-> StateT Bool ReduceM (Level, Level) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Monad 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'    )            -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort    (Sort -> Term)
-> StateT Bool ReduceM (Sort, Sort) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Monad 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' )            -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> 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.
Monad 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.
Monad 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' )            -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ Term -> Term
DontCare (Term -> Term) -> SynEqM (Term, Term) -> SynEqM (Term, Term)
forall (f :: * -> *) a b.
Monad 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{}     )            -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ (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)
_                                     -> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
ret (SynEqM (Term, Term) -> Result (SynEqM (Term, Term)))
-> SynEqM (Term, Term) -> Result (SynEqM (Term, Term))
forall a b. (a -> b) -> a -> b
$ (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 Level
l Level
l' = ((StateT Bool ReduceM (Level, Level)
  -> Result (StateT Bool ReduceM (Level, Level)))
 -> Result (StateT Bool ReduceM (Level, Level)))
-> StateT Bool ReduceM (Level, Level)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \StateT Bool ReduceM (Level, Level)
-> Result (StateT Bool ReduceM (Level, Level))
ret -> case (Level
l, Level
l') of
    (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'   -> StateT Bool ReduceM (Level, Level)
-> Result (StateT Bool ReduceM (Level, Level))
ret (StateT Bool ReduceM (Level, Level)
 -> Result (StateT Bool ReduceM (Level, Level)))
-> StateT Bool ReduceM (Level, Level)
-> Result (StateT Bool ReduceM (Level, Level))
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel] -> Level
levelMax Integer
n ([PlusLevel] -> Level)
-> StateT Bool ReduceM ([PlusLevel], [PlusLevel])
-> StateT Bool ReduceM (Level, Level)
forall (f :: * -> *) a b.
Monad 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 -> StateT Bool ReduceM (Level, Level)
-> Result (StateT Bool ReduceM (Level, Level))
ret (StateT Bool ReduceM (Level, Level)
 -> Result (StateT Bool ReduceM (Level, Level)))
-> StateT Bool ReduceM (Level, Level)
-> Result (StateT Bool ReduceM (Level, Level))
forall a b. (a -> b) -> a -> b
$ (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 PlusLevel
l PlusLevel
l' = ((SynEqM (PlusLevel, PlusLevel)
  -> Result (SynEqM (PlusLevel, PlusLevel)))
 -> Result (SynEqM (PlusLevel, PlusLevel)))
-> SynEqM (PlusLevel, PlusLevel)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (PlusLevel, PlusLevel)
-> Result (SynEqM (PlusLevel, PlusLevel))
ret -> case (PlusLevel
l, PlusLevel
l') of
    (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'   -> SynEqM (PlusLevel, PlusLevel)
-> Result (SynEqM (PlusLevel, PlusLevel))
ret (SynEqM (PlusLevel, PlusLevel)
 -> Result (SynEqM (PlusLevel, PlusLevel)))
-> SynEqM (PlusLevel, PlusLevel)
-> Result (SynEqM (PlusLevel, PlusLevel))
forall a b. (a -> b) -> a -> b
$ Integer -> Term -> PlusLevel
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel)
-> SynEqM (Term, Term) -> SynEqM (PlusLevel, PlusLevel)
forall (f :: * -> *) a b.
Monad 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 -> SynEqM (PlusLevel, PlusLevel)
-> Result (SynEqM (PlusLevel, PlusLevel))
ret (SynEqM (PlusLevel, PlusLevel)
 -> Result (SynEqM (PlusLevel, PlusLevel)))
-> SynEqM (PlusLevel, PlusLevel)
-> Result (SynEqM (PlusLevel, PlusLevel))
forall a b. (a -> b) -> a -> b
$ (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' = ((StateT Bool ReduceM (Sort, Sort)
  -> Result (StateT Bool ReduceM (Sort, Sort)))
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret -> if Sort -> Sort -> Bool
forall a. a -> a -> Bool
unsafeComparePointers Sort
s Sort
s' then StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ (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') else StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret do
    (s, 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')
    expand \StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret -> 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' -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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') -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ Dom' Term Term -> Sort -> Abs Sort -> Sort
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
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.
Monad 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.
Monad 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.
Monad 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') -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort -> Sort -> Sort)
-> StateT Bool ReduceM (Sort, Sort)
-> StateT Bool ReduceM (Sort -> Sort, Sort -> Sort)
forall (f :: * -> *) a b.
Monad 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.
Monad 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') -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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  ) -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
LockUniv, Sort
LockUniv  ) -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
LevelUniv, Sort
LevelUniv  ) -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ Sort -> StateT Bool ReduceM (Sort, Sort)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 Sort
s
      (Sort
IntervalUniv, Sort
IntervalUniv) -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ 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 -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ 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' -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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' -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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{}) -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ (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)
_ -> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
ret (StateT Bool ReduceM (Sort, Sort)
 -> Result (StateT Bool ReduceM (Sort, Sort)))
-> StateT Bool ReduceM (Sort, Sort)
-> Result (StateT Bool ReduceM (Sort, Sort))
forall a b. (a -> b) -> a -> b
$ (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 Type
x Type
y = ((SynEqM (Type, Type) -> Result (SynEqM (Type, Type)))
 -> Result (SynEqM (Type, Type)))
-> SynEqM (Type, Type)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Type, Type) -> Result (SynEqM (Type, Type))
ret -> case (Type
x, Type
y) of
    (El Sort
s Term
t, El Sort
s' Term
t') -> SynEqM (Type, Type) -> Result (SynEqM (Type, Type))
ret (SynEqM (Type, Type) -> Result (SynEqM (Type, Type)))
-> SynEqM (Type, Type) -> Result (SynEqM (Type, Type))
forall a b. (a -> b) -> a -> b
$ (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 (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m 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' = ((SynEqM ([a], [a]) -> Result (SynEqM ([a], [a])))
 -> Result (SynEqM ([a], [a])))
-> SynEqM ([a], [a])
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
ret -> case ([a]
as, [a]
as') of
    ([], [])       -> SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
ret (SynEqM ([a], [a]) -> Result (SynEqM ([a], [a])))
-> SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
forall a b. (a -> b) -> a -> b
$ ([a], [a]) -> SynEqM ([a], [a])
forall a. a -> SynEqM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])
    (a
a:[a]
as, a
a':[a]
as') -> SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
ret (SynEqM ([a], [a]) -> Result (SynEqM ([a], [a])))
-> SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
forall a b. (a -> b) -> a -> b
$ (:) (a -> [a] -> [a])
-> StateT Bool ReduceM (a, a)
-> StateT Bool ReduceM ([a] -> [a], [a] -> [a])
forall (f :: * -> *) a b.
Monad 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 ([a] -> [a], [a] -> [a])
-> SynEqM ([a], [a]) -> SynEqM ([a], [a])
forall (f :: * -> *) a b.
Monad f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> [a] -> [a] -> SynEqM ([a], [a])
forall a. SynEq a => a -> a -> SynEqM (a, a)
synEq [a]
as [a]
as'
    ([a]
as, [a]
as')      -> SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
ret (SynEqM ([a], [a]) -> Result (SynEqM ([a], [a])))
-> SynEqM ([a], [a]) -> Result (SynEqM ([a], [a]))
forall a b. (a -> b) -> a -> b
$ ([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, b)
x (a, b)
y = ((SynEqM ((a, b), (a, b)) -> Result (SynEqM ((a, b), (a, b))))
 -> Result (SynEqM ((a, b), (a, b))))
-> SynEqM ((a, b), (a, b))
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM ((a, b), (a, b)) -> Result (SynEqM ((a, b), (a, b)))
ret -> case ((a, b)
x, (a, b)
y) of
    ((a
a,b
b), (a
a',b
b')) -> SynEqM ((a, b), (a, b)) -> Result (SynEqM ((a, b), (a, b)))
ret (SynEqM ((a, b), (a, b)) -> Result (SynEqM ((a, b), (a, b))))
-> SynEqM ((a, b), (a, b)) -> Result (SynEqM ((a, b), (a, b)))
forall a b. (a -> b) -> a -> b
$ (,) (a -> b -> (a, b))
-> StateT Bool ReduceM (a, a)
-> StateT Bool ReduceM (b -> (a, b), b -> (a, b))
forall (f :: * -> *) a b.
Monad 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.
Monad 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' = ((SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a)))
 -> Result (SynEqM (Elim' a, Elim' a)))
-> SynEqM (Elim' a, Elim' a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
ret ->
    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' -> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
ret (SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a)))
-> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
forall a b. (a -> b) -> a -> b
$ 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') -> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
ret (SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a)))
-> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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')
                          -> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
ret (SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a)))
-> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
forall a b. (a -> b) -> a -> b
$ (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 (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m 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)
_                   -> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
ret (SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a)))
-> SynEqM (Elim' a, Elim' a) -> Result (SynEqM (Elim' a, Elim' a))
forall a b. (a -> b) -> a -> b
$ (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' = ((SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a)))
 -> Result (SynEqM (Abs a, Abs a)))
-> SynEqM (Abs a, Abs a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
ret ->
    case (Abs a
a, Abs a
a') of
      (NoAbs ArgName
x a
b, NoAbs ArgName
x' a
b') -> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
ret (SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a)))
-> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
forall a b. (a -> b) -> 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 (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m 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') -> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
ret (SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a)))
-> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
forall a b. (a -> b) -> 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 (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m 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') -> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
ret (SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a)))
-> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
forall a b. (a -> b) -> 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.
Monad 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') -> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
ret (SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a)))
-> SynEqM (Abs a, Abs a) -> Result (SynEqM (Abs a, Abs a))
forall a b. (a -> b) -> 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.
Monad 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 a
x Arg a
y = ((SynEqM (Arg a, Arg a) -> Result (SynEqM (Arg a, Arg a)))
 -> Result (SynEqM (Arg a, Arg a)))
-> SynEqM (Arg a, Arg a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Arg a, Arg a) -> Result (SynEqM (Arg a, Arg a))
ret -> case (Arg a
x, Arg a
y) of
    ((Arg ArgInfo
ai a
a), (Arg ArgInfo
ai' a
a')) -> SynEqM (Arg a, Arg a) -> Result (SynEqM (Arg a, Arg a))
ret (SynEqM (Arg a, Arg a) -> Result (SynEqM (Arg a, Arg a)))
-> SynEqM (Arg a, Arg a) -> Result (SynEqM (Arg a, Arg a))
forall a b. (a -> b) -> a -> b
$ 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.
Monad 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.
Monad 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 and elaborated rewrite.
instance SynEq a => SynEq (Dom a) where
  synEq :: Dom a -> Dom a -> SynEqM (Dom a, Dom a)
synEq Dom a
d Dom a
d' = ((SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a)))
 -> Result (SynEqM (Dom a, Dom a)))
-> SynEqM (Dom a, Dom a)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a))
ret -> case (Dom a
d, Dom a
d') of
    (d :: Dom a
d@(Dom ArgInfo
ai Maybe NamedName
x Bool
f Maybe Term
t Maybe (RewDom' Term)
r a
a), d' :: Dom a
d'@(Dom ArgInfo
ai' Maybe NamedName
x' Bool
f' Maybe Term
_ Maybe (RewDom' Term)
r' a
a'))
      | Maybe NamedName
x Maybe NamedName -> Maybe NamedName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'   -> SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a))
ret (SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a)))
-> SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a))
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe Term
-> Maybe (RewDom' Term)
-> a
-> Dom a
forall t e.
ArgInfo
-> Maybe NamedName
-> Bool
-> Maybe t
-> Maybe (RewDom' t)
-> e
-> Dom' t e
Dom (ArgInfo
 -> Maybe NamedName
 -> Bool
 -> Maybe Term
 -> Maybe (RewDom' Term)
 -> a
 -> Dom a)
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> StateT
     Bool
     ReduceM
     (Maybe NamedName
      -> Bool -> Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a,
      Maybe NamedName
      -> Bool -> Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a)
forall (f :: * -> *) a b.
Monad 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 -> Maybe (RewDom' Term) -> a -> Dom a,
   Maybe NamedName
   -> Bool -> Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a)
-> StateT Bool ReduceM (Maybe NamedName, Maybe NamedName)
-> StateT
     Bool
     ReduceM
     (Bool -> Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a,
      Bool -> Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a)
forall (f :: * -> *) a b.
Monad 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 -> Maybe (RewDom' Term) -> a -> Dom a,
   Bool -> Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a)
-> SynEqM (Bool, Bool)
-> StateT
     Bool
     ReduceM
     (Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a,
      Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a)
forall (f :: * -> *) a b.
Monad 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 -> Maybe (RewDom' Term) -> a -> Dom a,
   Maybe Term -> Maybe (RewDom' Term) -> a -> Dom a)
-> StateT Bool ReduceM (Maybe Term, Maybe Term)
-> StateT
     Bool
     ReduceM
     (Maybe (RewDom' Term) -> a -> Dom a,
      Maybe (RewDom' Term) -> a -> Dom a)
forall (f :: * -> *) a b.
Monad 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
  (Maybe (RewDom' Term) -> a -> Dom a,
   Maybe (RewDom' Term) -> a -> Dom a)
-> StateT Bool ReduceM (Maybe (RewDom' Term), Maybe (RewDom' Term))
-> StateT Bool ReduceM (a -> Dom a, a -> Dom a)
forall (f :: * -> *) a b.
Monad f =>
f (a -> b, a -> b) -> f (a, a) -> f (b, b)
<**> (Maybe (RewDom' Term), Maybe (RewDom' Term))
-> StateT Bool ReduceM (Maybe (RewDom' Term), Maybe (RewDom' Term))
forall a. a -> SynEqM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (RewDom' Term)
r, Maybe (RewDom' Term)
r') StateT Bool ReduceM (a -> Dom a, a -> Dom a)
-> StateT Bool ReduceM (a, a) -> SynEqM (Dom a, Dom a)
forall (f :: * -> *) a b.
Monad 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 -> SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a))
ret (SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a)))
-> SynEqM (Dom a, Dom a) -> Result (SynEqM (Dom a, Dom a))
forall a b. (a -> b) -> a -> b
$ (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 ArgInfo
ai ArgInfo
ai' = ((StateT Bool ReduceM (ArgInfo, ArgInfo)
  -> Result (StateT Bool ReduceM (ArgInfo, ArgInfo)))
 -> Result (StateT Bool ReduceM (ArgInfo, ArgInfo)))
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall a. ExpandCase a => ((a -> Result a) -> Result a) -> a
expand \StateT Bool ReduceM (ArgInfo, ArgInfo)
-> Result (StateT Bool ReduceM (ArgInfo, ArgInfo))
ret -> case (ArgInfo
ai, ArgInfo
ai') of
    (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' -> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> Result (StateT Bool ReduceM (ArgInfo, ArgInfo))
ret (StateT Bool ReduceM (ArgInfo, ArgInfo)
 -> Result (StateT Bool ReduceM (ArgInfo, ArgInfo)))
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> Result (StateT Bool ReduceM (ArgInfo, ArgInfo))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall (f :: * -> *) a. Applicative f => a -> f (a, a)
pure2 ArgInfo
ai
      | Bool
otherwise                           -> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> Result (StateT Bool ReduceM (ArgInfo, ArgInfo))
ret (StateT Bool ReduceM (ArgInfo, ArgInfo)
 -> Result (StateT Bool ReduceM (ArgInfo, ArgInfo)))
-> StateT Bool ReduceM (ArgInfo, ArgInfo)
-> Result (StateT Bool ReduceM (ArgInfo, ArgInfo))
forall a b. (a -> b) -> a -> b
$ (ArgInfo, ArgInfo) -> StateT Bool ReduceM (ArgInfo, ArgInfo)
forall a. a -> SynEqM a
inequal (ArgInfo
ai, ArgInfo
ai')