{-# LANGUAGE UndecidableInstances #-}
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 :: Type -> Term -> Type -> TCM Type
abstractType :: Type -> Term -> Type -> TCM Type
abstractType a :: Type
a v :: Term
v (El s :: Sort' Term
s b :: 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 :: Hiding -> Term -> Type -> Type -> TCM Type
piAbstractTerm :: Hiding -> Term -> Type -> Type -> TCM Type
piAbstractTerm h :: Hiding
h v :: Term
v a :: Type
a b :: 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 ("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 "tc.abstract" 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 [ "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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "-->" 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 "tc.abstract" 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 [ "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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "-->" 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 :: WithHiding (Term, EqualityView) -> Type -> TCM Type
piAbstract :: WithHiding (Term, EqualityView) -> Type -> TCM Type
piAbstract (WithHiding h :: Hiding
h (v :: Term
v, OtherType a :: Type
a)) b :: Type
b = Hiding -> Term -> Type -> Type -> TCM Type
piAbstractTerm Hiding
h Term
v Type
a Type
b
piAbstract (WithHiding h :: Hiding
h (prf :: Term
prf, eqt :: EqualityView
eqt@(EqualityType _ _ _ (Arg _ a :: Term
a) v :: Arg Term
v _))) b :: 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 ("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 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 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 "lhs" Type
vTy (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Type -> Type -> Type
funType "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 str :: ArgName
str a :: 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)
eqt1 :: EqualityView
eqt1 = VerboseLevel -> EqualityView -> EqualityView
forall t a. Subst t a => VerboseLevel -> a -> a
raise 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 0 }
class IsPrefixOf a where
isPrefixOf :: a -> a -> Maybe Elims
instance IsPrefixOf Elims where
isPrefixOf :: Elims -> Elims -> Maybe Elims
isPrefixOf us :: Elims
us vs :: Elims
vs = do
(vs1 :: Elims
vs1, vs2 :: 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 :: Args -> Args -> Maybe Elims
isPrefixOf us :: Args
us vs :: Args
vs = do
(vs1 :: Args
vs1, vs2 :: Args
vs2) <- VerboseLevel -> Args -> Maybe (Args, Args)
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (Args -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
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
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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
vs2
instance IsPrefixOf Term where
isPrefixOf :: Term -> Term -> Maybe Elims
isPrefixOf u :: Term
u v :: Term
v =
case (Term
u, Term
v) of
(Var i :: VerboseLevel
i us :: Elims
us, Var j :: VerboseLevel
j vs :: 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 f :: QName
f us :: Elims
us, Def g :: QName
g vs :: 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 c :: ConHead
c _ us :: Elims
us, Con d :: ConHead
d _ vs :: 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 x :: MetaId
x us :: Elims
us, MetaV y :: MetaId
y vs :: 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
(u :: Term
u, v :: 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 []
abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
abstractTerm :: Type -> Term -> Type -> Term -> TCMT IO Term
abstractTerm a :: Type
a u :: Term
u@Con{} b :: Type
b v :: Term
v = do
ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.abstract" 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 [ "Abstracting"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 ]
, "over"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 "tc.abstract" 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 [ "Abstracting"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 ]
, "over"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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_ ("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) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Args -> Elims) -> TCMT IO Args -> TCMT IO Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
let n :: VerboseLevel
n = Elims -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Elims
args
let abstr :: Type -> Term -> m Term
abstr b :: Type
b v :: Term
v = do
VerboseLevel
m <- m VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
let (a' :: Type
a', u' :: 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
Nothing -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
Just es :: Elims
es -> do
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` \ _ -> do
ArgName -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.abstract.ill-typed" 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 [ "Skipping ill-typed abstraction"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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
<+> ":", VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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
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
$ \ err :: TCErr
err -> do
ArgName -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.abstract.ill-typed" 40 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
"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
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 "tc.abstract" 50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "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 _ u :: Term
u _ v :: 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
class AbsTerm a where
absTerm :: Term -> a -> a
instance AbsTerm Term where
absTerm :: Term -> Term -> Term
absTerm u :: Term
u v :: Term
v | Just es :: Elims
es <- Term
u Term -> Term -> Maybe Elims
forall a. IsPrefixOf a => a -> a -> Maybe Elims
`isPrefixOf` Term
v = VerboseLevel -> Elims -> Term
Var 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
Var i :: VerboseLevel
i vs :: Elims
vs -> VerboseLevel -> Elims -> Term
Var (VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ 1) (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ Elims -> Elims
forall a. AbsTerm a => a -> a
absT Elims
vs
Lam h :: ArgInfo
h b :: 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 c :: QName
c vs :: 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 c :: ConHead
c ci :: ConInfo
ci vs :: 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 a :: Dom Type
a b :: 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 l :: Literal
l -> Literal -> Term
Lit Literal
l
Level l :: 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 s :: 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 m :: MetaId
m vs :: 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 mv :: 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 s :: ArgName
s es :: 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 x :: 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 u :: Term
u (El s :: Sort' Term
s v :: 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 u :: Term
u s :: Sort' Term
s = case Sort' Term
s of
Type n :: 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 n :: 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
Inf -> Sort' Term
forall t. Sort' t
Inf
SizeUniv -> Sort' Term
forall t. Sort' t
SizeUniv
PiSort a :: Dom Type
a s :: 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 s1 :: Sort' Term
s1 s2 :: 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 s :: 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 x :: MetaId
x es :: 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 d :: QName
d es :: 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 x :: 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 u :: Term
u (Max n :: Integer
n as :: [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 u :: Term
u (Plus n :: Integer
n l :: 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 u :: Term
u l :: LevelAtom' Term
l = case LevelAtom' Term
l of
MetaLevel m :: MetaId
m vs :: 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 r :: NotBlocked
r v :: 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 _ v :: 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
UnreducedLevel v :: 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 u :: Term
u (NoAbs x :: ArgName
x v :: 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 u :: Term
u (Abs x :: ArgName
x v :: 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 1 Term
u) a
v
instance (AbsTerm a, AbsTerm b) => AbsTerm (a, b) where
absTerm :: Term -> (a, b) -> (a, b)
absTerm u :: Term
u (x :: a
x, y :: 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)
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 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 1 (VerboseLevel -> Substitution' Term
forall a. VerboseLevel -> Substitution' a
raiseS 1)
class EqualSy a where
equalSy :: a -> a -> Bool
instance EqualSy a => EqualSy [a] where
equalSy :: [a] -> [a] -> Bool
equalSy us :: [a]
us vs :: [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 i :: VerboseLevel
i vs :: Elims
vs, Var i' :: VerboseLevel
i' vs' :: 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 c :: ConHead
c _ es :: Elims
es, Con c' :: ConHead
c' _ es' :: 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 f :: QName
f es :: Elims
es, Def f' :: QName
f' es' :: 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 x :: MetaId
x es :: Elims
es, MetaV x' :: MetaId
x' es' :: 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 l :: Literal
l , Lit l' :: Literal
l' ) -> Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
(Lam ai :: ArgInfo
ai b :: Abs Term
b, Lam ai' :: ArgInfo
ai' b' :: 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 l :: Level
l , Level l' :: Level
l' ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
(Sort s :: Sort' Term
s , Sort s' :: Sort' Term
s' ) -> Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
s Sort' Term
s'
(Pi a :: Dom Type
a b :: Abs Type
b , Pi a' :: Dom Type
a' b' :: 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 _, DontCare _ ) -> Bool
True
(Dummy{} , _ ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , Dummy{} ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> Bool
False
instance EqualSy Level where
equalSy :: Level -> Level -> Bool
equalSy (Max n :: Integer
n vs :: [PlusLevel' Term]
vs) (Max n' :: Integer
n' vs' :: [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 n :: Integer
n v :: LevelAtom' Term
v) (Plus n' :: Integer
n' v' :: 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 l :: Level
l , Type l' :: Level
l' ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
(Prop l :: Level
l , Prop l' :: Level
l' ) -> Level -> Level -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
(Inf , Inf ) -> Bool
True
(SizeUniv , SizeUniv ) -> Bool
True
(PiSort a :: Dom Type
a b :: Abs (Sort' Term)
b, PiSort a' :: Dom Type
a' b' :: 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 a :: Sort' Term
a b :: Sort' Term
b, FunSort a' :: Sort' Term
a' b' :: 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 a :: Sort' Term
a, UnivSort a' :: Sort' Term
a' ) -> Sort' Term -> Sort' Term -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
a Sort' Term
a'
(MetaS x :: MetaId
x es :: Elims
es, MetaS x' :: MetaId
x' es' :: 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 d :: QName
d es :: Elims
es, DefS d' :: QName
d' es' :: 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{} , _ ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , DummyS{} ) -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> Bool
False
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 _ f :: QName
f, Proj _ f' :: QName
f') -> QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f'
(Apply a :: Arg a
a , Apply a' :: Arg a
a' ) -> Arg a -> Arg a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy Arg a
a Arg a
a'
(IApply u :: a
u v :: a
v r :: a
r, IApply u' :: a
u' v' :: a
v' r' :: 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'
]
_ -> Bool
False
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 _x :: ArgName
_x b :: a
b, NoAbs _x' :: ArgName
_x' b' :: a
b') -> a -> a -> Bool
forall a. EqualSy a => a -> a -> Bool
equalSy a
b a
b'
(a :: Abs a
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')
instance EqualSy ArgInfo where
equalSy :: ArgInfo -> ArgInfo -> Bool
equalSy (ArgInfo h :: Hiding
h m :: Modality
m _o :: Origin
_o _fv :: FreeVariables
_fv) (ArgInfo h' :: Hiding
h' m' :: Modality
m' _o' :: Origin
_o' _fv' :: 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'
instance EqualSy a => EqualSy (Dom a) where
equalSy :: Dom a -> Dom a -> Bool
equalSy d :: Dom a
d@(Dom ai :: ArgInfo
ai b :: Bool
b x :: Maybe NamedName
x _tac :: Maybe Term
_tac a :: a
a) d' :: Dom a
d'@(Dom ai' :: ArgInfo
ai' b' :: Bool
b' x' :: Maybe NamedName
x' _tac' :: Maybe Term
_tac' a' :: 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'
]
instance EqualSy a => EqualSy (Arg a) where
equalSy :: Arg a -> Arg a -> Bool
equalSy (Arg (ArgInfo h :: Hiding
h m :: Modality
m _o :: Origin
_o _fv :: FreeVariables
_fv) v :: a
v) (Arg (ArgInfo h' :: Hiding
h' m' :: Modality
m' _o' :: Origin
_o' _fv' :: FreeVariables
_fv') v' :: 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')