{-# LANGUAGE UndecidableInstances #-}

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

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

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (equalityUnview)
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Pretty

import Agda.Utils.Functor
import Agda.Utils.List (splitExactlyAt)
import Agda.Utils.Except

import Agda.Utils.Impossible

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

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

-- | @piAbstract (v, a) b[v] = (w : a) -> 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 :: WithHiding (Term, EqualityView) -> Type -> TCM Type
piAbstract :: WithHiding (Term, EqualityView) -> Type -> TCM Type
piAbstract (WithHiding Hiding
h (Term
v, OtherType Type
a))                              Type
b = Hiding -> Term -> Type -> Type -> TCM Type
piAbstractTerm Hiding
h Term
v Type
a Type
b
piAbstract (WithHiding Hiding
h (Term
prf, eqt :: EqualityView
eqt@(EqualityType Sort' Term
_ QName
_ [Arg Term]
_ (Arg ArgInfo
_ Term
a) Arg Term
v Arg Term
_))) Type
b = do
  Sort' Term
s <- Term -> TCMT IO (Sort' Term)
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> m (Sort' Term)
inferSort Term
a
  let prfTy :: Type
prfTy = EqualityView -> Type
equalityUnview EqualityView
eqt
      vTy :: Type
vTy   = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s Term
a
  Type
b <- Type -> Term -> Type -> TCM Type
abstractType Type
prfTy Term
prf Type
b
  Type
b <- (ArgName, Dom Type) -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (ArgName
"w" :: String, Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
prfTy) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
         Type -> Term -> Type -> TCM Type
abstractType (VerboseLevel -> Type -> Type
forall t a. Subst t a => VerboseLevel -> a -> a
raise VerboseLevel
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
$ VerboseLevel -> Arg Term -> Arg Term
forall t a. Subst t a => VerboseLevel -> a -> a
raise VerboseLevel
1 Arg Term
v) Type
b
  Type -> TCM Type
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
. ArgName -> Type -> Type -> Type
funType ArgName
"lhs" Type
vTy (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Type -> Type -> Type
funType ArgName
"equality" Type
eqTy' (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
forall a. Subst Term a => a -> a
swap01 (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type
b
  where
    funType :: ArgName -> Type -> Type -> Type
funType ArgName
str Type
a = Dom (ArgName, Type) -> Type -> Type
mkPi (Dom (ArgName, Type) -> Type -> Type)
-> Dom (ArgName, Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Hiding -> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (Dom (ArgName, Type) -> Dom (ArgName, Type))
-> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall a b. (a -> b) -> a -> b
$ (ArgName, Type) -> Dom (ArgName, Type)
forall a. a -> Dom a
defaultDom (ArgName
str, Type
a)
    -- Abstract the lhs (@a@) of the equality only.
    eqt1 :: EqualityView
eqt1  = VerboseLevel -> EqualityView -> EqualityView
forall t a. Subst t a => VerboseLevel -> a -> a
raise VerboseLevel
1 EqualityView
eqt
    eqTy' :: Type
eqTy' = EqualityView -> Type
equalityUnview (EqualityView -> Type) -> EqualityView -> Type
forall a b. (a -> b) -> a -> b
$ EqualityView
eqt1 { eqtLhs :: Arg Term
eqtLhs = EqualityView -> Arg Term
eqtLhs EqualityView
eqt1 Arg Term -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel -> Term
var VerboseLevel
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 :: Elims -> Elims -> Maybe Elims
isPrefixOf Elims
us Elims
vs = do
    (Elims
vs1, Elims
vs2) <- VerboseLevel -> Elims -> Maybe (Elims, Elims)
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
us) Elims
vs
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
us Elims
vs1
    Elims -> Maybe Elims
forall (m :: * -> *) a. Monad m => a -> m a
return Elims
vs2

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

instance IsPrefixOf Term where
  isPrefixOf :: Term -> Term -> Maybe Elims
isPrefixOf Term
u Term
v =
    case (Term
u, Term
v) of
      (Var   VerboseLevel
i Elims
us, Var   VerboseLevel
j Elims
vs) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j  -> Elims
us Elims -> Elims -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
`isPrefixOf` Elims
vs
      (Def   QName
f Elims
us, Def   QName
g Elims
vs) | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g  -> Elims
us Elims -> Elims -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
`isPrefixOf` Elims
vs
      (Con ConHead
c ConInfo
_ Elims
us, Con ConHead
d ConInfo
_ Elims
vs) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
d  -> Elims
us Elims -> Elims -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
`isPrefixOf` Elims
vs
      (MetaV MetaId
x Elims
us, MetaV MetaId
y Elims
vs) | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
y  -> Elims
us Elims -> Elims -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
`isPrefixOf` Elims
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 Elims -> Maybe Elims
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Elims -> Maybe Elims
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
  ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.abstract" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"Abstracting"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
        , TCM Doc
"over"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b ] ]
  ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.abstract" VerboseLevel
70 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"Abstracting"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ (ArgName -> TCM Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Term -> ArgName) -> Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ArgName
forall a. Show a => a -> ArgName
show) Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (ArgName -> TCM Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Type -> ArgName) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ArgName
forall a. Show a => a -> ArgName
show) Type
a ]
        , TCM Doc
"over"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ (ArgName -> TCM Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Term -> ArgName) -> Term -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> ArgName
forall a. Show a => a -> ArgName
show) Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (ArgName -> TCM Doc
forall (m :: * -> *). Monad m => ArgName -> m Doc
text (ArgName -> TCM Doc) -> (Type -> ArgName) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ArgName
forall a. Show a => a -> ArgName
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 -> TCMT IO QName
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ArgName -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (ArgName
"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 -> Definition -> TCMT IO ()
addConstant QName
hole (Definition -> TCMT IO ()) -> Definition -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
hole Type
a Defn
Axiom

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

  let abstr :: Type -> Term -> m Term
abstr Type
b Term
v = do
        VerboseLevel
m <- m VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
        let (Type
a', Term
u') = VerboseLevel -> (Type, Term) -> (Type, Term)
forall t a. Subst t a => VerboseLevel -> a -> a
raise (VerboseLevel
m VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n) (Type
a, Term
u)
        case Term -> Term -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
isPrefixOf Term
u' Term
v of
          Maybe Elims
Nothing -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
          Just Elims
es -> do -- Check that the types match.
            TCState
s <- m TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
            do  m () -> m ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> m ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a' Type
b
                TCState -> m ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
                Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
hole (VerboseLevel -> Elims -> Elims
forall t a. Subst t a => VerboseLevel -> a -> a
raise (VerboseLevel
m VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n) Elims
args Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ Elims
es)
              m Term -> (TCErr -> m Term) -> m Term
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> do
                ArgName -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.abstract.ill-typed" VerboseLevel
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
                  [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"Skipping ill-typed abstraction"
                      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b ] ]
                Term -> m Term
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. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ (Action (TCMT IO) -> Term -> Comparison -> Type -> TCMT IO Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' (Action (TCMT IO)
forall (m :: * -> *). Monad m => Action m
defaultAction { preAction :: Type -> Term -> TCMT IO Term
preAction = Type -> Term -> TCMT IO Term
forall (m :: * -> *).
(MonadStatistics m, MonadMetaSolver m, MonadTCState m,
 MonadWarning m, MonadFresh VerboseLevel m,
 MonadFresh ProblemId m) =>
Type -> Term -> m Term
abstr }) Term
v Comparison
CmpLeq Type
b) ((TCErr -> TCMT IO Term) -> TCMT IO Term)
-> (TCErr -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ TCErr
err -> do
        ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.abstract.ill-typed" VerboseLevel
40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
          TCM Doc
"Skipping typed abstraction over ill-typed term" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b))
        Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc ArgName
"tc.abstract" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Resulting abstraction" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
res
  (Signature -> Signature) -> TCMT IO ()
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 (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm (QName -> Elims -> Term
Def QName
hole Elims
args) Term
res

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

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

instance AbsTerm Term where
  absTerm :: Term -> Term -> Term
absTerm Term
u Term
v | Just Elims
es <- Term
u Term -> Term -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
`isPrefixOf` Term
v = VerboseLevel -> Elims -> Term
Var VerboseLevel
0 (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
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 VerboseLevel
i Elims
vs    -> VerboseLevel -> Elims -> Term
Var (VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
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 a. AbsTerm a => a -> a
absT Abs Term
b
      Def QName
c Elims
vs    -> QName -> Elims -> Term
Def QName
c (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
vs
      Con ConHead
c ConInfo
ci Elims
vs -> ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
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 a. AbsTerm a => a -> a
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 a. AbsTerm a => a -> a
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 a. AbsTerm a => a -> a
absT Sort' Term
s
      MetaV MetaId
m Elims
vs  -> MetaId -> Elims -> Term
MetaV MetaId
m (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
vs
      DontCare Term
mv -> Term -> Term
DontCare (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall a. AbsTerm a => a -> a
absT Term
mv
      Dummy ArgName
s Elims
es   -> ArgName -> Elims -> Term
Dummy ArgName
s (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
es
      where
        absT :: a -> a
absT a
x = Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
x

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

instance AbsTerm Sort where
  absTerm :: Term -> Sort' Term -> Sort' Term
absTerm Term
u Sort' Term
s = case Sort' Term
s of
    Type Level
n     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall a. AbsTerm a => a -> a
absS Level
n
    Prop Level
n     -> Level -> Sort' Term
forall t. Level' t -> Sort' t
Prop (Level -> Sort' Term) -> Level -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Level -> Level
forall a. AbsTerm a => a -> a
absS Level
n
    Sort' Term
Inf        -> Sort' Term
forall t. Sort' t
Inf
    Sort' Term
SizeUniv   -> Sort' Term
forall t. Sort' t
SizeUniv
    PiSort Dom Type
a Abs (Sort' Term)
s -> Dom Type -> Abs (Sort' Term) -> Sort' Term
forall t. Dom' t (Type'' t t) -> Abs (Sort' t) -> Sort' t
PiSort (Dom Type -> Dom Type
forall a. AbsTerm a => a -> a
absS Dom Type
a) (Abs (Sort' Term) -> Abs (Sort' Term)
forall a. AbsTerm a => a -> a
absS Abs (Sort' Term)
s)
    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 a. AbsTerm a => a -> a
absS Sort' Term
s1) (Sort' Term -> Sort' Term
forall a. AbsTerm a => a -> a
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 a. AbsTerm a => a -> a
absS Sort' Term
s
    MetaS MetaId
x Elims
es -> MetaId -> Elims -> Sort' Term
forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x (Elims -> Sort' Term) -> Elims -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absS Elims
es
    DefS QName
d Elims
es  -> QName -> Elims -> Sort' Term
forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d (Elims -> Sort' Term) -> Elims -> Sort' Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absS Elims
es
    DummyS{}   -> Sort' Term
s
    where absS :: a -> a
absS a
x = Term -> a -> a
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
x

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

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

instance AbsTerm LevelAtom where
  absTerm :: Term -> LevelAtom' Term -> LevelAtom' Term
absTerm Term
u LevelAtom' Term
l = case LevelAtom' Term
l of
    MetaLevel MetaId
m Elims
vs   -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u (MetaId -> Elims -> Term
MetaV MetaId
m Elims
vs)
    NeutralLevel NotBlocked
r Term
v -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
r (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v
    BlockedLevel MetaId
_ Term
v -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v -- abstracting might remove the blockage
    UnreducedLevel Term
v -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v

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

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

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

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

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

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

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

-- | This swaps @var 0@ and @var 1@.
swap01 :: (Subst Term a) => a -> a
swap01 :: a -> a
swap01 = Substitution' Term -> a -> a
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Substitution' Term -> a -> a) -> Substitution' Term -> a -> a
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
1 Term -> Substitution' Term -> Substitution' Term
forall a. a -> Substitution' a -> Substitution' a
:# VerboseLevel -> Substitution' Term -> Substitution' Term
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS VerboseLevel
1 (VerboseLevel -> Substitution' Term
forall a. VerboseLevel -> Substitution' a
raiseS VerboseLevel
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] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [a]
us VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
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 VerboseLevel
i   Elims
vs, Var VerboseLevel
i'   Elims
vs') -> VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
i' Bool -> Bool -> Bool
&& Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
vs Elims
vs'
    (Con ConHead
c ConInfo
_ Elims
es, Con ConHead
c' ConInfo
_ Elims
es') -> ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' Bool -> Bool -> Bool
&& Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
es Elims
es'
    (Def   QName
f Elims
es, Def   QName
f' Elims
es') -> QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' Bool -> Bool -> Bool
&& Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
es Elims
es'
    (MetaV MetaId
x Elims
es, MetaV MetaId
x' Elims
es') -> MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
es Elims
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 LevelAtom' Term
v) (Plus Integer
n' LevelAtom' Term
v') = Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> Bool
&& LevelAtom' Term -> LevelAtom' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy LevelAtom' Term
v LevelAtom' Term
v'

instance EqualSy LevelAtom where
  equalSy :: LevelAtom' Term -> LevelAtom' Term -> Bool
equalSy = Term -> Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy (Term -> Term -> Bool)
-> (LevelAtom' Term -> Term)
-> LevelAtom' Term
-> LevelAtom' Term
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LevelAtom' Term -> Term
unLevelAtom

instance EqualSy Sort where
  equalSy :: Sort' Term -> Sort' Term -> Bool
equalSy = ((Sort' Term, Sort' Term) -> Bool)
-> Sort' Term -> Sort' Term -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Sort' Term, Sort' Term) -> Bool)
 -> Sort' Term -> Sort' Term -> Bool)
-> ((Sort' Term, Sort' Term) -> Bool)
-> Sort' Term
-> Sort' Term
-> Bool
forall a b. (a -> b) -> a -> b
$ \case
    (Type Level
l    , Type Level
l'     ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Prop Level
l    , Prop Level
l'     ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
    (Sort' Term
Inf       , Sort' Term
Inf         ) -> Bool
True
    (Sort' Term
SizeUniv  , Sort' Term
SizeUniv    ) -> Bool
True
    (PiSort Dom Type
a Abs (Sort' Term)
b, PiSort Dom Type
a' Abs (Sort' Term)
b') -> Dom Type -> Dom Type -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Dom Type
a Dom Type
a' Bool -> Bool -> Bool
&& Abs (Sort' Term) -> Abs (Sort' Term) -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Abs (Sort' Term)
b Abs (Sort' Term)
b'
    (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 Elims
es, MetaS MetaId
x' Elims
es') -> MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
es Elims
es'
    (DefS  QName
d Elims
es, DefS  QName
d' Elims
es') -> QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' Bool -> Bool -> Bool
&& Elims -> Elims -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Elims
es Elims
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') -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
u a
u'
      , a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
v a
v'
      , 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 t 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 ArgName
_x a
b, NoAbs ArgName
_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 t a. Subst t a => Abs a -> a
absBody Abs a
a) (Abs a -> a
forall t a. Subst t 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) (ArgInfo Hiding
h' Modality
m' Origin
_o' FreeVariables
_fv') =
    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'

-- | Ignore the tactic.
instance EqualSy a => EqualSy (Dom a) where
  equalSy :: Dom a -> Dom a -> Bool
equalSy d :: Dom a
d@(Dom ArgInfo
ai Bool
b Maybe NamedName
x Maybe Term
_tac a
a) d' :: Dom a
d'@(Dom ArgInfo
ai' Bool
b' Maybe NamedName
x' 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
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b'
    , 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) a
v) (Arg (ArgInfo Hiding
h' Modality
m' Origin
_o' FreeVariables
_fv') 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 (==).