-- | Functions for abstracting terms over other terms.
module Agda.TypeChecking.Abstract where

import Control.Monad
import Control.Monad.Except

import Data.Function
import qualified Data.HashMap.Strict as HMap

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

import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin ( equalityUnview, primEqualityName )
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Telescope

import Agda.Utils.Functor
import Agda.Utils.List ( splitExactlyAt, dropEnd )
import Agda.Utils.Impossible

-- | @abstractType a v b[v] = b@ where @a : v@.
abstractType :: Type -> Term -> Type -> TCM Type
abstractType :: Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v (El Sort' Term
s Term
b) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Term -> Sort' Term -> Sort' Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
v Sort' Term
s) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> Term -> TCMT IO Term
abstractTerm Type
a Term
v (Sort' Term -> Type
sort Sort' Term
s) Term
b

-- | @piAbstractTerm NotHidden v a b[v] = (w : a) -> b[w]@
--   @piAbstractTerm Hidden    v a b[v] = {w : a} -> b[w]@
piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstractTerm ArgInfo
info Term
v Type
a Type
b = do
  Type
fun <- Dom (String, Type) -> Type -> Type
mkPi (ArgInfo -> Dom (String, Type) -> Dom (String, Type)
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom (String, Type) -> Dom (String, Type))
-> Dom (String, Type) -> Dom (String, Type)
forall a b. (a -> b) -> a -> b
$ (String, Type) -> Dom (String, Type)
forall a. a -> Dom a
defaultDom (String
"w", Type
a)) (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v Type
b
  String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"piAbstract" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a ]
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
b
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
fun ]
  String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"piAbstract" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Term -> String) -> Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> String
forall a. Show a => a -> String
show) Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
forall a. Show a => a -> String
show) Type
a ]
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"from" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
forall a. Show a => a -> String
show) Type
b
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
forall a. Show a => a -> String
show) Type
fun ]
  Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
fun

-- | @piAbstract (v, a) b[v] = (w : a) -> b[w]@
--
--   For the inspect idiom, it does something special:
--   @piAbstract (v, a) b[v] = (w : a) {w' : Eq a w v} -> b[w]
--
--   For @rewrite@, it does something special:
--   @piAbstract (prf, Eq a v v') b[v,prf] = (w : a) (w' : Eq a w v') -> b[w,w']@

piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
piAbstract (Arg ArgInfo
info (Term
v, OtherType Type
a)) Type
b = ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstractTerm ArgInfo
info Term
v Type
a Type
b
piAbstract (Arg ArgInfo
info (Term
v, IdiomType Type
a)) Type
b = do
  Type
b  <- Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise Nat
1 (Type -> Type) -> TCM Type -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v Type
b
  Type
eq <- (String, Dom Type) -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"w" :: String, Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
a) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
    -- manufacture the type @w ≡ v@
    QName
eqName <- TCM QName
primEqualityName
    Type
eqTy <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
eqName
    -- E.g. @eqTy = eqTel → Set a@ where @eqTel = {a : Level} {A : Set a} (x y : A)@.
    TelV Tele (Dom Type)
eqTel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
eqTy
    Args
tel  <- Tele (Dom Type) -> TCMT IO Args
forall (m :: * -> *).
MonadMetaSolver m =>
Tele (Dom Type) -> m Args
newTelMeta (ListTel -> Tele (Dom Type)
telFromList (ListTel -> Tele (Dom Type)) -> ListTel -> Tele (Dom Type)
forall a b. (a -> b) -> a -> b
$ Nat -> ListTel -> ListTel
forall a. Nat -> [a] -> [a]
dropEnd Nat
2 (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
eqTel)
    let eq :: Term
eq = QName -> [Elim] -> Term
Def QName
eqName ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply
                 (Args -> [Elim]) -> Args -> [Elim]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Arg Term) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) Args
tel
                 -- we write `v ≡ w` because this equality is typically used to
                 -- get `v` to unfold to whatever pattern was used to refine `w`
                 -- in a with-clause.
                 -- If we were to write `w ≡ v`, we would often need to take the
                 -- symmetric of the proof we get to make use of `rewrite`.
                 Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ [ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
v)
                    , Term -> Arg Term
forall a. a -> Arg a
defaultArg (Nat -> Term
var Nat
0)
                    ]
    Sort' Term
sort <- TCMT IO (Sort' Term)
forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
newSortMeta
    let ty :: Type
ty = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
sort Term
eq
    Type
ty Type -> TCMT IO () -> TCM Type
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type -> TCMT IO ()
forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
ty

  Type -> TCM Type
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi (Hiding -> Dom (String, Type) -> Dom (String, Type)
forall a. LensHiding a => Hiding -> a -> a
setHiding (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (Dom (String, Type) -> Dom (String, Type))
-> Dom (String, Type) -> Dom (String, Type)
forall a b. (a -> b) -> a -> b
$ (String, Type) -> Dom (String, Type)
forall a. a -> Dom a
defaultDom (String
"w", Type
a))
       (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi (Hiding -> Dom (String, Type) -> Dom (String, Type)
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden        (Dom (String, Type) -> Dom (String, Type))
-> Dom (String, Type) -> Dom (String, Type)
forall a b. (a -> b) -> a -> b
$ (String, Type) -> Dom (String, Type)
forall a. a -> Dom a
defaultDom (String
"eq", Type
eq))
       (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
b
piAbstract (Arg ArgInfo
info (Term
prf, EqualityViewType eqt :: EqualityTypeData
eqt@(EqualityTypeData Sort' Term
_ QName
_ Args
_ (Arg ArgInfo
_ Term
a) Arg Term
v Arg Term
_))) Type
b = do
  Sort' Term
s <- Term -> TCMT IO (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (Sort' Term)
sortOf Term
a
  let prfTy :: Type
      prfTy :: Type
prfTy = EqualityTypeData -> Type
forall a. EqualityUnview a => a -> Type
equalityUnview EqualityTypeData
eqt
      vTy :: Type
vTy   = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s Term
a
  Type
b <- Type -> Term -> Type -> TCM Type
abstractType Type
prfTy Term
prf Type
b
  Type
b <- (String, Dom Type) -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
"w" :: String, Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
prfTy) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
         Type -> Term -> Type -> TCM Type
abstractType (Nat -> Type -> Type
forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
vTy) (Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Nat -> Arg Term -> Arg Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 Arg Term
v) Type
b
  Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> (Type -> Type) -> Type -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type -> Type -> Type
funType String
"lhs" Type
vTy (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type -> Type -> Type
funType String
"equality" Type
eqTy' (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall a. TermSubst a => a -> a
swap01 (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type
b
  where
    funType :: String -> Type -> Type -> Type
funType String
str Type
a = Dom (String, Type) -> Type -> Type
mkPi (Dom (String, Type) -> Type -> Type)
-> Dom (String, Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Dom (String, Type) -> Dom (String, Type)
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom (String, Type) -> Dom (String, Type))
-> Dom (String, Type) -> Dom (String, Type)
forall a b. (a -> b) -> a -> b
$ (String, Type) -> Dom (String, Type)
forall a. a -> Dom a
defaultDom (String
str, Type
a)
    -- Abstract the lhs (@a@) of the equality only.
    eqt1 :: EqualityTypeData
    eqt1 :: EqualityTypeData
eqt1  = Nat -> EqualityTypeData -> EqualityTypeData
forall a. Subst a => Nat -> a -> a
raise Nat
1 EqualityTypeData
eqt
    eqTy' :: Type
    eqTy' :: Type
eqTy' = EqualityTypeData -> Type
forall a. EqualityUnview a => a -> Type
equalityUnview (EqualityTypeData -> Type) -> EqualityTypeData -> Type
forall a b. (a -> b) -> a -> b
$ EqualityTypeData
eqt1{ _eqtLhs :: Arg Term
_eqtLhs = EqualityTypeData -> Arg Term
_eqtLhs EqualityTypeData
eqt1 Arg Term -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Nat -> Term
var Nat
0 }


-- | @isPrefixOf u v = Just es@ if @v == u `applyE` es@.
class IsPrefixOf a where
  isPrefixOf :: a -> a -> Maybe Elims

instance IsPrefixOf Elims where
  isPrefixOf :: [Elim] -> [Elim] -> Maybe [Elim]
isPrefixOf [Elim]
us [Elim]
vs = do
    ([Elim]
vs1, [Elim]
vs2) <- Nat -> [Elim] -> Maybe ([Elim], [Elim])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt ([Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
us) [Elim]
vs
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
us [Elim]
vs1
    [Elim] -> Maybe [Elim]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Elim]
vs2

instance IsPrefixOf Args where
  isPrefixOf :: Args -> Args -> Maybe [Elim]
isPrefixOf Args
us Args
vs = do
    (Args
vs1, Args
vs2) <- Nat -> Args -> Maybe (Args, Args)
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
us) Args
vs
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Args -> Args -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Args
us Args
vs1
    [Elim] -> Maybe [Elim]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Elim] -> Maybe [Elim]) -> [Elim] -> Maybe [Elim]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs2

instance IsPrefixOf Term where
  isPrefixOf :: Term -> Term -> Maybe [Elim]
isPrefixOf Term
u Term
v =
    case (Term
u, Term
v) of
      (Var   Nat
i [Elim]
us, Var   Nat
j [Elim]
vs) | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j  -> [Elim]
us [Elim] -> [Elim] -> Maybe [Elim]
forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (Def   QName
f [Elim]
us, Def   QName
g [Elim]
vs) | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g  -> [Elim]
us [Elim] -> [Elim] -> Maybe [Elim]
forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (Con ConHead
c ConInfo
_ [Elim]
us, Con ConHead
d ConInfo
_ [Elim]
vs) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
d  -> [Elim]
us [Elim] -> [Elim] -> Maybe [Elim]
forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (MetaV MetaId
x [Elim]
us, MetaV MetaId
y [Elim]
vs) | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
y  -> [Elim]
us [Elim] -> [Elim] -> Maybe [Elim]
forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (Term
u, Term
v) -> Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term -> Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Term
u Term
v) Maybe () -> Maybe [Elim] -> Maybe [Elim]
forall a b. Maybe a -> Maybe b -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Elim] -> Maybe [Elim]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- Type-based abstraction. Needed if u is a constructor application (#745).
abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
abstractTerm :: Type -> Term -> Type -> Term -> TCMT IO Term
abstractTerm Type
a u :: Term
u@Con{} Type
b Term
v = do
  String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Abstracting"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a ]
        , TCMT IO Doc
"over"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
b ] ]
  String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Abstracting"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Term -> String) -> Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> String
forall a. Show a => a -> String
show) Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
forall a. Show a => a -> String
show) Type
a ]
        , TCMT IO Doc
"over"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Term -> String) -> Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> String
forall a. Show a => a -> String
show) Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> (Type -> String) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String
forall a. Show a => a -> String
show) Type
b ] ]

  QName
hole <- ModuleName -> Name -> QName
qualify (ModuleName -> Name -> QName)
-> TCMT IO ModuleName -> TCMT IO (Name -> QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule TCMT IO (Name -> QName) -> TCMT IO Name -> TCM QName
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *). MonadFresh NameId m => String -> m Name
freshName_ (String
"hole" :: String)
  TCMT IO () -> TCMT IO ()
forall a. TCM a -> TCM a
noMutualBlock (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
hole ArgInfo
defaultArgInfo QName
hole Type
a Defn
defaultAxiom

  [Elim]
args <- (Arg Term -> Elim) -> Args -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Args -> [Elim]) -> TCMT IO Args -> TCMT IO [Elim]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  let n :: Nat
n = [Elim] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
args

  let abstr :: Type -> Term -> TCMT IO Term
abstr Type
b Term
v = do
        Nat
m <- TCMT IO Nat
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
        let (Type
a', Term
u') = Nat -> (Type, Term) -> (Type, Term)
forall a. Subst a => Nat -> a -> a
raise (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n) (Type
a, Term
u)
        case Term
u' Term -> Term -> Maybe [Elim]
forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` Term
v of
          Maybe [Elim]
Nothing -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          Just [Elim]
es -> do -- Check that the types match.
            TCState
s <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
            do  TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCMT IO ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a' Type
b
                TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
                Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
hole (Nat -> [Elim] -> [Elim]
forall a. Subst a => Nat -> a -> a
raise (Nat
m Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n) [Elim]
args [Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++ [Elim]
es)
              TCMT IO Term -> (TCErr -> TCMT IO Term) -> TCMT IO Term
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> do
                String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract.ill-typed" Nat
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
                  [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Skipping ill-typed abstraction"
                      , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
b ] ]
                Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

  -- #2763: This can fail if the user is with-abstracting incorrectly (for
  -- instance, abstracting over a first component of a sigma without also
  -- abstracting the second component). In this case we skip abstraction
  -- altogether and let the type check of the final with-function type produce
  -- the error message.
  Term
res <- TCMT IO Term -> (TCErr -> TCMT IO Term) -> TCMT IO Term
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
catchError_ (Action (TCMT IO) -> Term -> Comparison -> Type -> TCMT IO Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' (Action (TCMT IO)
forall (m :: * -> *). PureTCM m => Action m
defaultAction { preAction :: Type -> Term -> TCMT IO Term
preAction = Type -> Term -> TCMT IO Term
abstr }) Term
v Comparison
CmpLeq Type
b) ((TCErr -> TCMT IO Term) -> TCMT IO Term)
-> (TCErr -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ TCErr
err -> do
        String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract.ill-typed" Nat
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Skipping typed abstraction over ill-typed term" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
b))
        Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  String -> Nat -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Resulting abstraction" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
res
  (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCMT IO ())
-> (Signature -> Signature) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions ((Definitions -> Definitions) -> Signature -> Signature)
-> (Definitions -> Definitions) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ QName -> Definitions -> Definitions
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HMap.delete QName
hole
  Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm (QName -> [Elim] -> Term
Def QName
hole [Elim]
args) Term
res

abstractTerm Type
_ Term
u Type
_ Term
v = Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v -- Non-constructors can use untyped abstraction

class AbsTerm a where
  -- | @subst u . absTerm u == id@
  absTerm :: Term -> a -> a

instance AbsTerm Term where
  absTerm :: Term -> Term -> Term
absTerm Term
u Term
v | Just [Elim]
es <- Term
u Term -> Term -> Maybe [Elim]
forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` Term
v = Nat -> [Elim] -> Term
Var Nat
0 ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absT [Elim]
es
              | Bool
otherwise                   =
    case Term
v of
-- Andreas, 2013-10-20: the original impl. works only at base types
--    v | u == v  -> Var 0 []  -- incomplete see succeed/WithOfFunctionType
      Var Nat
i [Elim]
vs    -> Nat -> [Elim] -> Term
Var (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absT [Elim]
vs
      Lam ArgInfo
h Abs Term
b     -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ Abs Term -> Abs Term
forall b. AbsTerm b => b -> b
absT Abs Term
b
      Def QName
c [Elim]
vs    -> QName -> [Elim] -> Term
Def QName
c ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absT [Elim]
vs
      Con ConHead
c ConInfo
ci [Elim]
vs -> ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absT [Elim]
vs
      Pi Dom Type
a Abs Type
b      -> (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi ((Dom Type, Abs Type) -> Term) -> (Dom Type, Abs Type) -> Term
forall a b. (a -> b) -> a -> b
$ (Dom Type, Abs Type) -> (Dom Type, Abs Type)
forall b. AbsTerm b => b -> b
absT (Dom Type
a, Abs Type
b)
      Lit Literal
l       -> Literal -> Term
Lit Literal
l
      Level Level
l     -> Level -> Term
Level (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall b. AbsTerm b => b -> b
absT Level
l
      Sort Sort' Term
s      -> Sort' Term -> Term
Sort (Sort' Term -> Term) -> Sort' Term -> Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Sort' Term
forall b. AbsTerm b => b -> b
absT Sort' Term
s
      MetaV MetaId
m [Elim]
vs  -> MetaId -> [Elim] -> Term
MetaV MetaId
m ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absT [Elim]
vs
      DontCare Term
mv -> Term -> Term
DontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall b. AbsTerm b => b -> b
absT Term
mv
      Dummy String
s [Elim]
es   -> String -> [Elim] -> Term
Dummy String
s ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absT [Elim]
es
      where
        absT :: AbsTerm b => b -> b
        absT :: forall b. AbsTerm b => b -> b
absT b
x = Term -> b -> b
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u b
x

instance AbsTerm Type where
  absTerm :: Term -> Type -> Type
absTerm Term
u (El Sort' Term
s Term
v) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Term -> Sort' Term -> Sort' Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Sort' Term
s) (Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v)

instance AbsTerm Sort where
  absTerm :: Term -> Sort' Term -> Sort' Term
absTerm Term
u = \case
    Type Level
n     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall b. AbsTerm b => b -> b
absS Level
n
    Prop Level
n     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Prop (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall b. AbsTerm b => b -> b
absS Level
n
    s :: Sort' Term
s@(Inf IsFibrant
f Integer
n)-> Sort' Term
s
    SSet Level
n     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall b. AbsTerm b => b -> b
absS Level
n
    Sort' Term
SizeUniv   -> Sort' Term
forall t. Sort' t
SizeUniv
    Sort' Term
LockUniv   -> Sort' Term
forall t. Sort' t
LockUniv
    Sort' Term
IntervalUniv -> Sort' Term
forall t. Sort' t
LockUniv
    PiSort Dom' Term Term
a Sort' Term
s1 Abs (Sort' Term)
s2 -> Dom' Term Term -> Sort' Term -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (Dom' Term Term -> Dom' Term Term
forall b. AbsTerm b => b -> b
absS Dom' Term Term
a) (Sort' Term -> Sort' Term
forall b. AbsTerm b => b -> b
absS Sort' Term
s1) (Abs (Sort' Term) -> Abs (Sort' Term)
forall b. AbsTerm b => b -> b
absS Abs (Sort' Term)
s2)
    FunSort Sort' Term
s1 Sort' Term
s2 -> Sort' Term -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t -> Sort' t
FunSort (Sort' Term -> Sort' Term
forall b. AbsTerm b => b -> b
absS Sort' Term
s1) (Sort' Term -> Sort' Term
forall b. AbsTerm b => b -> b
absS Sort' Term
s2)
    UnivSort Sort' Term
s -> Sort' Term -> Sort' Term
forall t. Sort' t -> Sort' t
UnivSort (Sort' Term -> Sort' Term) -> Sort' Term -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Sort' Term
forall b. AbsTerm b => b -> b
absS Sort' Term
s
    MetaS MetaId
x [Elim]
es -> MetaId -> [Elim] -> Sort' Term
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x ([Elim] -> Sort' Term) -> [Elim] -> Sort' Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absS [Elim]
es
    DefS QName
d [Elim]
es  -> QName -> [Elim] -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d ([Elim] -> Sort' Term) -> [Elim] -> Sort' Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> [Elim]
forall b. AbsTerm b => b -> b
absS [Elim]
es
    s :: Sort' Term
s@DummyS{} -> Sort' Term
s
    where
      absS :: AbsTerm b => b -> b
      absS :: forall b. AbsTerm b => b -> b
absS b
x = Term -> b -> b
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u b
x

instance AbsTerm Level where
  absTerm :: Term -> Level -> Level
absTerm Term
u (Max Integer
n [PlusLevel' Term]
as) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n ([PlusLevel' Term] -> Level) -> [PlusLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u [PlusLevel' Term]
as

instance AbsTerm PlusLevel where
  absTerm :: Term -> PlusLevel' Term -> PlusLevel' Term
absTerm Term
u (Plus Integer
n Term
l) = Integer -> Term -> PlusLevel' Term
forall t. Integer -> t -> PlusLevel' t
Plus Integer
n (Term -> PlusLevel' Term) -> Term -> PlusLevel' Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
l

instance AbsTerm a => AbsTerm (Elim' a) where
  absTerm :: Term -> Elim' a -> Elim' a
absTerm = (a -> a) -> Elim' a -> Elim' a
forall a b. (a -> b) -> Elim' a -> Elim' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Elim' a -> Elim' a)
-> (Term -> a -> a) -> Term -> Elim' a -> Elim' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm

instance AbsTerm a => AbsTerm (Arg a) where
  absTerm :: Term -> Arg a -> Arg a
absTerm = (a -> a) -> Arg a -> Arg a
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Arg a -> Arg a)
-> (Term -> a -> a) -> Term -> Arg a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm

instance AbsTerm a => AbsTerm (Dom a) where
  absTerm :: Term -> Dom a -> Dom a
absTerm = (a -> a) -> Dom a -> Dom a
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Dom a -> Dom a)
-> (Term -> a -> a) -> Term -> Dom a -> Dom a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm

instance AbsTerm a => AbsTerm [a] where
  absTerm :: Term -> [a] -> [a]
absTerm = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> [a] -> [a]) -> (Term -> a -> a) -> Term -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm

instance AbsTerm a => AbsTerm (Maybe a) where
  absTerm :: Term -> Maybe a -> Maybe a
absTerm = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> Maybe a -> Maybe a)
-> (Term -> a -> a) -> Term -> Maybe a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm

instance (TermSubst a, AbsTerm a) => AbsTerm (Abs a) where
  absTerm :: Term -> Abs a -> Abs a
absTerm Term
u (NoAbs String
x a
v) = String -> a -> Abs a
forall a. String -> a -> Abs a
NoAbs String
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
v
  absTerm Term
u (Abs   String
x a
v) = String -> a -> Abs a
forall a. String -> a -> Abs a
Abs String
x (a -> Abs a) -> a -> Abs a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. TermSubst a => a -> a
swap01 (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm (Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
u) a
v

instance (AbsTerm a, AbsTerm b) => AbsTerm (a, b) where
  absTerm :: Term -> (a, b) -> (a, b)
absTerm Term
u (a
x, b
y) = (Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
x, Term -> b -> b
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u b
y)

-- | This swaps @var 0@ and @var 1@.
swap01 :: TermSubst a => a -> a
swap01 :: forall a. TermSubst a => a -> a
swap01 = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' (SubstArg a) -> a -> a)
-> Substitution' (SubstArg a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
1 Term -> Substitution' Term -> Substitution' Term
forall a. a -> Substitution' a -> Substitution' a
:# Nat -> Substitution' Term -> Substitution' Term
forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (Nat -> Substitution' Term
forall a. Nat -> Substitution' a
raiseS Nat
1)


-- ** Equality of terms for the sake of with-abstraction.

-- The following could be parameterized by a record of flags
-- what parts of the syntax tree should be ignored.
-- For now, there is a fixed strategy.

class EqualSy a where
  equalSy :: a -> a -> Bool

instance EqualSy a => EqualSy [a] where
  equalSy :: [a] -> [a] -> Bool
equalSy [a]
us [a]
vs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ ([a] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
us Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
vs) Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (a -> a -> Bool) -> [a] -> [a] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [a]
us [a]
vs

instance EqualSy Term where
  equalSy :: Term -> Term -> Bool
equalSy = ((Term, Term) -> Bool) -> Term -> Term -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Term, Term) -> Bool) -> Term -> Term -> Bool)
-> ((Term, Term) -> Bool) -> Term -> Term -> Bool
forall a b. (a -> b) -> a -> b
$ \case
    (Var Nat
i   [Elim]
vs, Var Nat
i'   [Elim]
vs') -> Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
i' Bool -> Bool -> Bool
&& [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
vs [Elim]
vs'
    (Con ConHead
c ConInfo
_ [Elim]
es, Con ConHead
c' ConInfo
_ [Elim]
es') -> ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' Bool -> Bool -> Bool
&& [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
    (Def   QName
f [Elim]
es, Def   QName
f' [Elim]
es') -> QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' Bool -> Bool -> Bool
&& [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
    (MetaV MetaId
x [Elim]
es, MetaV MetaId
x' [Elim]
es') -> MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
    (Lit   Literal
l   , Lit   Literal
l'    ) -> Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
    (Lam   ArgInfo
ai Abs Term
b, Lam   ArgInfo
ai' Abs Term
b') -> ArgInfo -> ArgInfo -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy ArgInfo
ai ArgInfo
ai' Bool -> Bool -> Bool
&& Abs Term -> Abs Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Abs Term
b Abs Term
b'
    (Level Level
l   , Level Level
l'    ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Sort  Sort' Term
s   , Sort  Sort' Term
s'    ) -> Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
s Sort' Term
s'
    (Pi    Dom Type
a Abs Type
b , Pi    Dom Type
a' Abs Type
b' ) -> Dom Type -> Dom Type -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Dom Type
a Dom Type
a' Bool -> Bool -> Bool
&& Abs Type -> Abs Type -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Abs Type
b Abs Type
b'
    (DontCare Term
_, DontCare Term
_  ) -> Bool
True
       -- Irrelevant things are syntactically equal.
    (Dummy{}   , Term
_           ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Term
_         , Dummy{}     ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Term, Term)
_ -> Bool
False

instance EqualSy Level where
  equalSy :: Level -> Level -> Bool
equalSy (Max Integer
n [PlusLevel' Term]
vs) (Max Integer
n' [PlusLevel' Term]
vs') = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> Bool
&& [PlusLevel' Term] -> [PlusLevel' Term] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [PlusLevel' Term]
vs [PlusLevel' Term]
vs'

instance EqualSy PlusLevel where
  equalSy :: PlusLevel' Term -> PlusLevel' Term -> Bool
equalSy (Plus Integer
n Term
v) (Plus Integer
n' Term
v') = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> Bool
&& Term -> Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Term
v Term
v'

instance EqualSy Sort where
  equalSy :: Sort' Term -> Sort' Term -> Bool
equalSy = ((Sort' Term, Sort' Term) -> Bool)
-> Sort' Term -> Sort' Term -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Sort' Term, Sort' Term) -> Bool)
 -> Sort' Term -> Sort' Term -> Bool)
-> ((Sort' Term, Sort' Term) -> Bool)
-> Sort' Term
-> Sort' Term
-> Bool
forall a b. (a -> b) -> a -> b
$ \case
    (Type Level
l    , Type Level
l'     ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Prop Level
l    , Prop Level
l'     ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy 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' Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n
    (SSet Level
l    , SSet Level
l'     ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Sort' Term
SizeUniv  , Sort' Term
SizeUniv    ) -> Bool
True
    (PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c, PiSort Dom' Term Term
a' Sort' Term
b' Abs (Sort' Term)
c') -> Dom' Term Term -> Dom' Term Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Dom' Term Term
a Dom' Term Term
a' Bool -> Bool -> Bool
&& Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
b Sort' Term
b' Bool -> Bool -> Bool
&& Abs (Sort' Term) -> Abs (Sort' Term) -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Abs (Sort' Term)
c Abs (Sort' Term)
c'
    (FunSort Sort' Term
a Sort' Term
b, FunSort Sort' Term
a' Sort' Term
b') -> Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
a Sort' Term
a' Bool -> Bool -> Bool
&& Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
b Sort' Term
b'
    (UnivSort Sort' Term
a, UnivSort Sort' Term
a' ) -> Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
a Sort' Term
a'
    (MetaS MetaId
x [Elim]
es, MetaS MetaId
x' [Elim]
es') -> MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
    (DefS  QName
d [Elim]
es, DefS  QName
d' [Elim]
es') -> QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' Bool -> Bool -> Bool
&& [Elim] -> [Elim] -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
    (DummyS{}  , Sort' Term
_           ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Sort' Term
_         , DummyS{}    ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Sort' Term, Sort' Term)
_ -> Bool
False

-- | Ignores sorts.
instance EqualSy Type where
  equalSy :: Type -> Type -> Bool
equalSy = Term -> Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy (Term -> Term -> Bool) -> (Type -> Term) -> Type -> Type -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Type -> Term
forall t a. Type'' t a -> a
unEl

instance EqualSy a => EqualSy (Elim' a) where
  equalSy :: Elim' a -> Elim' a -> Bool
equalSy = ((Elim' a, Elim' a) -> Bool) -> Elim' a -> Elim' a -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Elim' a, Elim' a) -> Bool) -> Elim' a -> Elim' a -> Bool)
-> ((Elim' a, Elim' a) -> Bool) -> Elim' a -> Elim' a -> Bool
forall a b. (a -> b) -> a -> b
$ \case
    (Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') -> QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'
    (Apply Arg a
a, Apply Arg a
a') -> Arg a -> Arg a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Arg a
a Arg a
a'
    (IApply a
u a
v a
r, IApply a
u' a
v' a
r') ->
           a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
u a
u'
        Bool -> Bool -> Bool
&& a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
v a
v'
        Bool -> Bool -> Bool
&& a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
r a
r'
    (Elim' a, Elim' a)
_ -> Bool
False

-- | Ignores 'absName'.
instance (Subst a, EqualSy a) => EqualSy (Abs a) where
  equalSy :: Abs a -> Abs a -> Bool
equalSy = ((Abs a, Abs a) -> Bool) -> Abs a -> Abs a -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Abs a, Abs a) -> Bool) -> Abs a -> Abs a -> Bool)
-> ((Abs a, Abs a) -> Bool) -> Abs a -> Abs a -> Bool
forall a b. (a -> b) -> a -> b
$ \case
    (NoAbs String
_x a
b, NoAbs String
_x' a
b') -> a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
b a
b' -- no need to raise if both are NoAbs
    (Abs a
a         , Abs a
a'          ) -> a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy (Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a) (Abs a -> a
forall a. Subst a => Abs a -> a
absBody Abs a
a')

-- | Ignore origin and free variables.
instance EqualSy ArgInfo where
  equalSy :: ArgInfo -> ArgInfo -> Bool
equalSy (ArgInfo Hiding
h Modality
m Origin
_o FreeVariables
_fv Annotation
a) (ArgInfo Hiding
h' Modality
m' Origin
_o' FreeVariables
_fv' Annotation
a') =
    Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
h' Bool -> Bool -> Bool
&& Modality
m Modality -> Modality -> Bool
forall a. Eq a => a -> a -> Bool
== Modality
m' Bool -> Bool -> Bool
&& Annotation
a Annotation -> Annotation -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation
a'

-- | Ignore the tactic.
instance EqualSy a => EqualSy (Dom a) where
  equalSy :: Dom a -> Dom a -> Bool
equalSy d :: Dom a
d@(Dom ArgInfo
ai Maybe NamedName
x Bool
f Maybe Term
_tac a
a) d' :: Dom a
d'@(Dom ArgInfo
ai' Maybe NamedName
x' Bool
f' Maybe Term
_tac' a
a') = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    [ Maybe NamedName
x Maybe NamedName -> Maybe NamedName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'
    , Bool
f Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
f'
    , ArgInfo -> ArgInfo -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy ArgInfo
ai ArgInfo
ai'
    , a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
a a
a'
    ]

-- | Ignores irrelevant arguments and modality.
--   (And, of course, origin and free variables).
instance EqualSy a => EqualSy (Arg a) where
  equalSy :: Arg a -> Arg a -> Bool
equalSy (Arg (ArgInfo Hiding
h Modality
m Origin
_o FreeVariables
_fv Annotation
a) a
v) (Arg (ArgInfo Hiding
h' Modality
m' Origin
_o' FreeVariables
_fv' Annotation
a') a
v') =
    Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
h' Bool -> Bool -> Bool
&& (Modality -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
m Bool -> Bool -> Bool
|| Modality -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
m' Bool -> Bool -> Bool
|| a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
v a
v')
    -- Andreas, 2017-10-04, issue #2775,
    -- ignore irrelevant arguments during with-abstraction.
    -- 2019-07-05, issue #3889, don't ignore quantity during caching
    -- this is why we let equalSy replace (==).