{-# OPTIONS_GHC -Wunused-imports #-}

-- | Functions for abstracting terms over other terms.

module Agda.TypeChecking.Abstract where

import Prelude hiding ( null )

import Control.Monad
import Control.Monad.Except

import Data.Function ( on )
import qualified Data.HashMap.Strict as HMap

import Agda.Syntax.Common
import Agda.Syntax.Position ( Range )
import Agda.Syntax.Internal

import Agda.TypeChecking.Free ( freeIn )
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
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.TypeChecking.Warnings ( warning )

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

import Agda.Utils.Impossible

-- | @abstractType r a v b[v] = b@ where @a : v@.
abstractType ::
     Range     -- ^ Range of the @rewrite@ expression, if any, otherwise empty.
  -> Type      -- ^ Type of the term to abstract.
  -> Term      -- ^ Term to abstract.
  -> Type      -- ^ Type to abstract in.
  -> TCM Type  -- ^ Type with hole (de Bruijn index 0) for the abstracted term.
abstractType :: Range -> Type -> Term -> Type -> TCM Type
abstractType Range
r Type
a Term
v (El Sort' Term
s Term
b) = do

  Type
c <- Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Nat -> Term -> Sort' Term -> Sort' Term
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
0 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
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Range -> Bool
forall a. Null a => a -> Bool
null Range
r Bool -> Bool -> Bool
|| Nat
0 Nat -> Type -> Bool
forall a. Free a => Nat -> a -> Bool
`freeIn` Type
c) do
    -- Andreas, 2025-07-03, issue #7973
    -- If with abstraction did not abstract anything, warn the user.
    Range -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
RewritesNothing
  Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
c

-- | @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
<$> Range -> Type -> Term -> Type -> TCM Type
abstractType Range
forall a. Null a => a
empty 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
<$> Range -> Type -> Term -> Type -> TCM Type
abstractType Range
forall a. Null a => a
empty 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
3 (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]
++ [ Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Nat -> Term -> Term
forall a. Subst a => Nat -> a -> a
raise Nat
1 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
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)
                    ]
    -- Since the result of this function will be type-checked in
    -- `withFunctionType`, we can be a little lazy here and put
    -- a meta for the sort.
    Sort' Term
sort <- TCMT IO (Sort' Term)
forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
newSortMeta
    Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
sort Term
eq

  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 Range
r 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, MonadConstraint 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
  -- Andreas, 2025-07-03, issue #7973
  -- We alert the user when the lhs of the equality proof could not be abstracted
  -- but not when the equality proof itself could not be abstracted.
  -- Only the former means that the rewrite did not fire.
  Type
b <- Range -> Type -> Term -> Type -> TCM Type
abstractType Range
forall a. Null a => a
empty Type
prfTy Term
prf Type
b  -- @empty@ means do not warn
  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
$
         -- Passing range @r@ here means warn if abstraction failed to abstract anything.
         Range -> Type -> Term -> Type -> TCM Type
abstractType Range
r (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 = _eqtLhs eqt1 $> var 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 -> Type -> Defn -> TCMT IO ()
addConstant' QName
hole ArgInfo
defaultArgInfo 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 :: * -> *). 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 :: * -> *). 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 -> TypeOf Term -> TCMT IO Term
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> TypeOf Term -> m Term
checkInternal' (Action (TCMT IO)
forall (m :: * -> *). PureTCM m => Action m
defaultAction { preAction = abstr }) Term
v Comparison
CmpLeq TypeOf Term
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
$ Nat -> Term -> Term -> Term
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
0 (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
$ Nat -> Term -> Term -> Term
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
0 Term
u Term
v -- Non-constructors can use untyped abstraction

class AbsTerm a where
  -- | @subst j u . absTerm j u == id@
  absTerm ::
       Nat   -- ^ De Bruijn index that should be the placeholder for the abstracted term.
    -> Term  -- ^ Term to abstract.
    -> a     -- ^ Where to abstract.
    -> a     -- ^ If the given de Bruijn index is free in the result, abstraction actually happened.

instance AbsTerm Term where
  absTerm :: Nat -> Term -> Term -> Term
absTerm Nat
j 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
j ([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 j []  -- incomplete see succeed/WithOfFunctionType
      Var Nat
i [Elim]
vs    -> Nat -> [Elim] -> Term
Var (if Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
j then Nat
i else 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 = Nat -> Term -> b -> b
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j Term
u b
x

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

instance AbsTerm Sort where
  absTerm :: Nat -> Term -> Sort' Term -> Sort' Term
absTerm Nat
j Term
u = \case
    Univ Univ
u Level
n   -> Univ -> Level -> Sort' Term
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (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{}    -> Sort' Term
s
    Sort' Term
SizeUniv   -> Sort' Term
forall t. Sort' t
SizeUniv
    Sort' Term
LockUniv   -> Sort' Term
forall t. Sort' t
LockUniv
    Sort' Term
LevelUniv  -> Sort' Term
forall t. Sort' t
LevelUniv
    Sort' Term
IntervalUniv -> Sort' Term
forall t. Sort' t
IntervalUniv
    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 = Nat -> Term -> b -> b
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j Term
u b
x

instance AbsTerm Level where
  absTerm :: Nat -> Term -> Level -> Level
absTerm Nat
j 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
$ Nat -> Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j Term
u [PlusLevel' Term]
as

instance AbsTerm PlusLevel where
  absTerm :: Nat -> Term -> PlusLevel' Term -> PlusLevel' Term
absTerm Nat
j 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
$ Nat -> Term -> Term -> Term
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j Term
u Term
l

instance AbsTerm a => AbsTerm (Elim' a) where
  absTerm :: Nat -> Term -> Elim' a -> Elim' a
absTerm Nat
j = (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
. Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j

instance AbsTerm a => AbsTerm (Arg a) where
  absTerm :: Nat -> Term -> Arg a -> Arg a
absTerm Nat
j = (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
. Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j

instance AbsTerm a => AbsTerm (Dom a) where
  absTerm :: Nat -> Term -> Dom a -> Dom a
absTerm Nat
j = (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
. Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j

instance AbsTerm a => AbsTerm [a] where
  absTerm :: Nat -> Term -> [a] -> [a]
absTerm Nat
j = (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
. Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j

instance AbsTerm a => AbsTerm (Maybe a) where
  absTerm :: Nat -> Term -> Maybe a -> Maybe a
absTerm Nat
j = (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
. Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j

instance (TermSubst a, AbsTerm a) => AbsTerm (Abs a) where
  absTerm :: Nat -> Term -> Abs a -> Abs a
absTerm Nat
j 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
$ Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j Term
u a
v
  absTerm Nat
j 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
$ Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm (Nat
j Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) (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 :: Nat -> Term -> (a, b) -> (a, b)
absTerm Nat
j Term
u (a
x, b
y) = (Nat -> Term -> a -> a
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j Term
u a
x, Nat -> Term -> b -> b
forall a. AbsTerm a => Nat -> Term -> a -> a
absTerm Nat
j 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
    (Univ Univ
u Level
l  , Univ Univ
u' Level
l'  ) -> Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Inf Univ
u Integer
m   , Inf Univ
u' Integer
n    ) -> Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n
    (Sort' Term
SizeUniv  , Sort' Term
SizeUniv    ) -> Bool
True
    (Sort' Term
LevelUniv , Sort' Term
LevelUniv   ) -> 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 (==).