-- | 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) = forall t a. Sort' t -> a -> Type'' t a
El (forall a. AbsTerm a => Term -> a -> a
absTerm Term
v Sort' Term
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> Term -> TCM 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 (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
"w", Type
a)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v Type
b
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"piAbstract" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fun ]
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
70 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"piAbstract" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
a ]
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
b
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
fun ]
  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  <- forall a. Subst a => Nat -> a -> a
raise Nat
1 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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"w" :: String, forall a. a -> Dom a
defaultDom Type
a) forall a b. (a -> b) -> a -> b
$ do
    -- manufacture the type @w ≡ v@
    QName
eqName <- TCM QName
primEqualityName
    Type
eqTy <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
eqTy
    Args
tel  <- forall (m :: * -> *).
MonadMetaSolver m =>
Tele (Dom Type) -> m Args
newTelMeta (ListTel -> Tele (Dom Type)
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
dropEnd Nat
2 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
eqTel)
    let eq :: Term
eq = QName -> [Elim] -> Term
Def QName
eqName forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply
                 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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`.
                 forall a. [a] -> [a] -> [a]
++ [ forall a. a -> Arg a
defaultArg (forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
v)
                    , forall a. a -> Arg a
defaultArg (Nat -> Term
var Nat
0)
                    ]
    Sort' Term
sort <- forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
newSortMeta
    let ty :: Type
ty = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
sort Term
eq
    Type
ty forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
ty

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi (forall a. LensHiding a => Hiding -> a -> a
setHiding (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
"w", Type
a))
       forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden        forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
"eq", Type
eq))
       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 <- forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (Sort' Term)
sortOf Term
a
  let prfTy :: Type
      prfTy :: Type
prfTy = forall a. EqualityUnview a => a -> Type
equalityUnview EqualityTypeData
eqt
      vTy :: Type
vTy   = 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 <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"w" :: String, forall a. a -> Dom a
defaultDom Type
prfTy) forall a b. (a -> b) -> a -> b
$
         Type -> Term -> Type -> TCM Type
abstractType (forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
vTy) (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
1 Arg Term
v) Type
b
  forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type -> Type -> Type
funType String
"lhs" Type
vTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type -> Type -> Type
funType String
"equality" Type
eqTy' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermSubst a => a -> a
swap01 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 forall a b. (a -> b) -> a -> b
$ forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
str, Type
a)
    -- Abstract the lhs (@a@) of the equality only.
    eqt1 :: EqualityTypeData
    eqt1 :: EqualityTypeData
eqt1  = forall a. Subst a => Nat -> a -> a
raise Nat
1 EqualityTypeData
eqt
    eqTy' :: Type
    eqTy' :: Type
eqTy' = forall a. EqualityUnview a => a -> Type
equalityUnview forall a b. (a -> b) -> a -> b
$ EqualityTypeData
eqt1{ _eqtLhs :: Arg Term
_eqtLhs = EqualityTypeData -> Arg Term
_eqtLhs EqualityTypeData
eqt1 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) <- forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
us) [Elim]
vs
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
us [Elim]
vs1
    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) <- forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
us) Args
vs
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. EqualSy a => a -> a -> Bool
equalSy Args
us Args
vs1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 forall a. Eq a => a -> a -> Bool
== Nat
j  -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (Def   QName
f [Elim]
us, Def   QName
g [Elim]
vs) | QName
f forall a. Eq a => a -> a -> Bool
== QName
g  -> [Elim]
us 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 forall a. Eq a => a -> a -> Bool
== ConHead
d  -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (MetaV MetaId
x [Elim]
us, MetaV MetaId
y [Elim]
vs) | MetaId
x forall a. Eq a => a -> a -> Bool
== MetaId
y  -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
      (Term
u, Term
v) -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. EqualSy a => a -> a -> Bool
equalSy Term
u Term
v) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 -> TCM Term
abstractTerm Type
a u :: Term
u@Con{} Type
b Term
v = do
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Abstracting"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
        , TCMT IO Doc
"over"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b ] ]
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
70 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Abstracting"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
a ]
        , TCMT IO Doc
"over"
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
b ] ]

  QName
hole <- ModuleName -> Name -> QName
qualify forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"hole" :: String)
  forall a. TCM a -> TCM a
noMutualBlock 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 <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  let n :: Nat
n = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
args

  let abstr :: Type -> Term -> TCM Term
abstr Type
b Term
v = do
        Nat
m <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
        let (Type
a', Term
u') = forall a. Subst a => Nat -> a -> a
raise (Nat
m forall a. Num a => a -> a -> a
- Nat
n) (Type
a, Term
u)
        case Term
u' forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` Term
v of
          Maybe [Elim]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          Just [Elim]
es -> do -- Check that the types match.
            TCState
s <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
            do  forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a' Type
b
                forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
hole (forall a. Subst a => Nat -> a -> a
raise (Nat
m forall a. Num a => a -> a -> a
- Nat
n) [Elim]
args forall a. [a] -> [a] -> [a]
++ [Elim]
es)
              forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> do
                forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract.ill-typed" Nat
50 forall a b. (a -> b) -> a -> b
$
                  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Skipping ill-typed abstraction"
                      , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b ] ]
                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 <- forall a. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ (forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' (forall (m :: * -> *). PureTCM m => Action m
defaultAction { preAction :: Type -> Term -> TCM Term
preAction = Type -> Term -> TCM Term
abstr }) Term
v Comparison
CmpLeq Type
b) forall a b. (a -> b) -> a -> b
$ \ TCErr
err -> do
        forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract.ill-typed" Nat
40 forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"Skipping typed abstraction over ill-typed term" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b))
        forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Resulting abstraction" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
res
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HMap.delete QName
hole
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` Term
v = Nat -> [Elim] -> Term
Var Nat
0 forall a b. (a -> b) -> a -> b
$ 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 forall a. Num a => a -> a -> a
+ Nat
1) forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
      Lam ArgInfo
h Abs Term
b     -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Abs Term
b
      Def QName
c [Elim]
vs    -> QName -> [Elim] -> Term
Def QName
c forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
      Pi Dom Type
a Abs Type
b      -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Level
l
      Sort Sort' Term
s      -> Sort' Term -> Term
Sort forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Sort' Term
s
      MetaV MetaId
m [Elim]
vs  -> MetaId -> [Elim] -> Term
MetaV MetaId
m forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
      DontCare Term
mv -> Term -> Term
DontCare forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Term
mv
      Dummy String
s [Elim]
es   -> String -> [Elim] -> Term
Dummy String
s forall a b. (a -> b) -> a -> b
$ 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 = 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) = forall t a. Sort' t -> a -> Type'' t a
El (forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Sort' Term
s) (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     -> forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS Level
n
    Prop Level
n     -> forall t. Level' t -> Sort' t
Prop forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS Level
n
    s :: Sort' Term
s@(Inf IsFibrant
f Integer
n)-> Sort' Term
s
    SSet Level
n     -> forall t. Level' t -> Sort' t
SSet forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS Level
n
    Sort' Term
SizeUniv   -> forall t. Sort' t
SizeUniv
    Sort' Term
LockUniv   -> forall t. Sort' t
LockUniv
    Sort' Term
IntervalUniv -> forall t. Sort' t
LockUniv
    PiSort Dom' Term Term
a Sort' Term
s1 Abs (Sort' Term)
s2 -> forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (forall b. AbsTerm b => b -> b
absS Dom' Term Term
a) (forall b. AbsTerm b => b -> b
absS Sort' Term
s1) (forall b. AbsTerm b => b -> b
absS Abs (Sort' Term)
s2)
    FunSort Sort' Term
s1 Sort' Term
s2 -> forall t. Sort' t -> Sort' t -> Sort' t
FunSort (forall b. AbsTerm b => b -> b
absS Sort' Term
s1) (forall b. AbsTerm b => b -> b
absS Sort' Term
s2)
    UnivSort Sort' Term
s -> forall t. Sort' t -> Sort' t
UnivSort forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS Sort' Term
s
    MetaS MetaId
x [Elim]
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS [Elim]
es
    DefS QName
d [Elim]
es  -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d forall a b. (a -> b) -> a -> b
$ 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 = 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) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n forall a b. (a -> b) -> a -> b
$ 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) = forall t. Integer -> t -> PlusLevel' t
Plus Integer
n forall a b. (a -> b) -> a -> b
$ 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AbsTerm a => Term -> a -> a
absTerm

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

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

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

instance AbsTerm a => AbsTerm (Maybe a) where
  absTerm :: Term -> Maybe a -> Maybe a
absTerm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. String -> a -> Abs a
NoAbs String
x forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
v
  absTerm Term
u (Abs   String
x a
v) = forall a. String -> a -> Abs a
Abs String
x forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => a -> a
swap01 forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm (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) = (forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
x, 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 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
1 forall a. a -> Substitution' a -> Substitution' a
:# forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
us forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
vs) forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. EqualSy a => a -> a -> Bool
equalSy [a]
us [a]
vs

instance EqualSy Term where
  equalSy :: Term -> Term -> Bool
equalSy = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
    (Var Nat
i   [Elim]
vs, Var Nat
i'   [Elim]
vs') -> Nat
i forall a. Eq a => a -> a -> Bool
== Nat
i' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== ConHead
c' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== QName
f' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
    (Lit   Literal
l   , Lit   Literal
l'    ) -> Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l'
    (Lam   ArgInfo
ai Abs Term
b, Lam   ArgInfo
ai' Abs Term
b') -> forall a. EqualSy a => a -> a -> Bool
equalSy ArgInfo
ai ArgInfo
ai' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Abs Term
b Abs Term
b'
    (Level Level
l   , Level Level
l'    ) -> forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Sort  Sort' Term
s   , Sort  Sort' Term
s'    ) -> 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' ) -> forall a. EqualSy a => a -> a -> Bool
equalSy Dom Type
a Dom Type
a' Bool -> Bool -> 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
_           ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (Term
_         , Dummy{}     ) -> 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 forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> 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 forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Term
v Term
v'

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

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

instance EqualSy a => EqualSy (Elim' a) where
  equalSy :: Elim' a -> Elim' a -> Bool
equalSy = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
    (Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') -> QName
f forall a. Eq a => a -> a -> Bool
== QName
f'
    (Apply Arg a
a, Apply Arg a
a') -> 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') ->
           forall a. EqualSy a => a -> a -> Bool
equalSy a
u a
u'
        Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy a
v a
v'
        Bool -> Bool -> 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 = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
    (NoAbs String
_x a
b, NoAbs String
_x' a
b') -> 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'          ) -> forall a. EqualSy a => a -> a -> Bool
equalSy (forall a. Subst a => Abs a -> a
absBody 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 forall a. Eq a => a -> a -> Bool
== Hiding
h' Bool -> Bool -> Bool
&& Modality
m forall a. Eq a => a -> a -> Bool
== Modality
m' Bool -> Bool -> Bool
&& Annotation
a 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') = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    [ Maybe NamedName
x forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'
    , Bool
f forall a. Eq a => a -> a -> Bool
== Bool
f'
    , forall a. EqualSy a => a -> a -> Bool
equalSy ArgInfo
ai ArgInfo
ai'
    , 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 forall a. Eq a => a -> a -> Bool
== Hiding
h' Bool -> Bool -> Bool
&& (forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
m Bool -> Bool -> Bool
|| forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
m' Bool -> Bool -> 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 (==).