{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.Abstract where
import Control.Monad
import Control.Monad.Except
import Data.Function (on)
import qualified Data.HashMap.Strict as HMap
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Telescope
import Agda.Utils.Functor
import Agda.Utils.List ( splitExactlyAt, dropEnd )
import Agda.Utils.Impossible
abstractType :: Type -> Term -> Type -> TCM Type
abstractType :: Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v (El Sort' Term
s Term
b) = forall t a. Sort' t -> a -> Type'' t a
El (forall a. AbsTerm a => Term -> a -> a
absTerm Term
v Sort' Term
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> Term -> TCM Term
abstractTerm Type
a Term
v (Sort' Term -> Type
sort Sort' Term
s) Term
b
piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstractTerm ArgInfo
info Term
v Type
a Type
b = do
Type
fun <- Dom (String, Type) -> Type -> Type
mkPi (forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
"w", Type
a)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v Type
b
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"piAbstract" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
fun ]
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
70 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"piAbstract" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
a ]
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"from" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
b
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"-->" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
fun ]
forall (m :: * -> *) a. Monad m => a -> m a
return Type
fun
piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
piAbstract (Arg ArgInfo
info (Term
v, OtherType Type
a)) Type
b = ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstractTerm ArgInfo
info Term
v Type
a Type
b
piAbstract (Arg ArgInfo
info (Term
v, IdiomType Type
a)) Type
b = do
Type
b <- forall a. Subst a => Nat -> a -> a
raise Nat
1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> Type -> TCM Type
abstractType Type
a Term
v Type
b
Type
eq <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"w" :: String, forall a. a -> Dom a
defaultDom Type
a) forall a b. (a -> b) -> a -> b
$ do
QName
eqName <- TCM QName
primEqualityName
Type
eqTy <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
eqName
TelV Tele (Dom Type)
eqTel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
eqTy
Args
tel <- forall (m :: * -> *).
MonadMetaSolver m =>
Tele (Dom Type) -> m Args
newTelMeta (ListTel -> Tele (Dom Type)
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Nat -> [a] -> [a]
dropEnd Nat
2 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
eqTel)
let eq :: Term
eq = QName -> [Elim] -> Term
Def QName
eqName forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply
forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) Args
tel
forall a. [a] -> [a] -> [a]
++ [ forall a. a -> Arg a
defaultArg (forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
v)
, forall a. a -> Arg a
defaultArg (Nat -> Term
var Nat
0)
]
Sort' Term
sort <- forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
newSortMeta
let ty :: Type
ty = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
sort Term
eq
Type
ty forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *). MonadCheckInternal m => Type -> m ()
checkType Type
ty
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi (forall a. LensHiding a => Hiding -> a -> a
setHiding (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
"w", Type
a))
forall a b. (a -> b) -> a -> b
$ Dom (String, Type) -> Type -> Type
mkPi (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
"eq", Type
eq))
forall a b. (a -> b) -> a -> b
$ Type
b
piAbstract (Arg ArgInfo
info (Term
prf, EqualityViewType eqt :: EqualityTypeData
eqt@(EqualityTypeData Sort' Term
_ QName
_ Args
_ (Arg ArgInfo
_ Term
a) Arg Term
v Arg Term
_))) Type
b = do
Sort' Term
s <- forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m (Sort' Term)
sortOf Term
a
let prfTy :: Type
prfTy :: Type
prfTy = forall a. EqualityUnview a => a -> Type
equalityUnview EqualityTypeData
eqt
vTy :: Type
vTy = forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s Term
a
Type
b <- Type -> Term -> Type -> TCM Type
abstractType Type
prfTy Term
prf Type
b
Type
b <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"w" :: String, forall a. a -> Dom a
defaultDom Type
prfTy) forall a b. (a -> b) -> a -> b
$
Type -> Term -> Type -> TCM Type
abstractType (forall a. Subst a => Nat -> a -> a
raise Nat
1 Type
vTy) (forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
1 Arg Term
v) Type
b
forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type -> Type -> Type
funType String
"lhs" Type
vTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Type -> Type -> Type
funType String
"equality" Type
eqTy' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermSubst a => a -> a
swap01 forall a b. (a -> b) -> a -> b
$ Type
b
where
funType :: String -> Type -> Type -> Type
funType String
str Type
a = Dom (String, Type) -> Type -> Type
mkPi forall a b. (a -> b) -> a -> b
$ forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom (String
str, Type
a)
eqt1 :: EqualityTypeData
eqt1 :: EqualityTypeData
eqt1 = forall a. Subst a => Nat -> a -> a
raise Nat
1 EqualityTypeData
eqt
eqTy' :: Type
eqTy' :: Type
eqTy' = forall a. EqualityUnview a => a -> Type
equalityUnview forall a b. (a -> b) -> a -> b
$ EqualityTypeData
eqt1{ _eqtLhs :: Arg Term
_eqtLhs = EqualityTypeData -> Arg Term
_eqtLhs EqualityTypeData
eqt1 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Nat -> Term
var Nat
0 }
class IsPrefixOf a where
isPrefixOf :: a -> a -> Maybe Elims
instance IsPrefixOf Elims where
isPrefixOf :: [Elim] -> [Elim] -> Maybe [Elim]
isPrefixOf [Elim]
us [Elim]
vs = do
([Elim]
vs1, [Elim]
vs2) <- forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
us) [Elim]
vs
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
us [Elim]
vs1
forall (m :: * -> *) a. Monad m => a -> m a
return [Elim]
vs2
instance IsPrefixOf Args where
isPrefixOf :: Args -> Args -> Maybe [Elim]
isPrefixOf Args
us Args
vs = do
(Args
vs1, Args
vs2) <- forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt (forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
us) Args
vs
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. EqualSy a => a -> a -> Bool
equalSy Args
us Args
vs1
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
vs2
instance IsPrefixOf Term where
isPrefixOf :: Term -> Term -> Maybe [Elim]
isPrefixOf Term
u Term
v =
case (Term
u, Term
v) of
(Var Nat
i [Elim]
us, Var Nat
j [Elim]
vs) | Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
(Def QName
f [Elim]
us, Def QName
g [Elim]
vs) | QName
f forall a. Eq a => a -> a -> Bool
== QName
g -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
(Con ConHead
c ConInfo
_ [Elim]
us, Con ConHead
d ConInfo
_ [Elim]
vs) | ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
d -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
(MetaV MetaId
x [Elim]
us, MetaV MetaId
y [Elim]
vs) | MetaId
x forall a. Eq a => a -> a -> Bool
== MetaId
y -> [Elim]
us forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` [Elim]
vs
(Term
u, Term
v) -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. EqualSy a => a -> a -> Bool
equalSy Term
u Term
v) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return []
abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
abstractTerm Type
a u :: Term
u@Con{} Type
b Term
v = do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Abstracting"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ]
, TCMT IO Doc
"over"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b ] ]
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
70 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Abstracting"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
a ]
, TCMT IO Doc
"over"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Type
b ] ]
QName
hole <- ModuleName -> Name -> QName
qualify forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (String
"hole" :: String)
forall a. TCM a -> TCM a
noMutualBlock forall a b. (a -> b) -> a -> b
$ QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
hole ArgInfo
defaultArgInfo QName
hole Type
a Defn
defaultAxiom
[Elim]
args <- forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
let n :: Nat
n = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Elim]
args
let abstr :: Type -> Term -> TCM Term
abstr Type
b Term
v = do
Nat
m <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Nat
getContextSize
let (Type
a', Term
u') = forall a. Subst a => Nat -> a -> a
raise (Nat
m forall a. Num a => a -> a -> a
- Nat
n) (Type
a, Term
u)
case Term
u' forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` Term
v of
Maybe [Elim]
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
Just [Elim]
es -> do
TCState
s <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
do forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType Type
a' Type
b
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
hole (forall a. Subst a => Nat -> a -> a
raise (Nat
m forall a. Num a => a -> a -> a
- Nat
n) [Elim]
args forall a. [a] -> [a] -> [a]
++ [Elim]
es)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract.ill-typed" Nat
50 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Skipping ill-typed abstraction"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b ] ]
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
Term
res <- forall a. TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ (forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
Action m -> a -> Comparison -> TypeOf a -> m a
checkInternal' (forall (m :: * -> *). PureTCM m => Action m
defaultAction { preAction :: Type -> Term -> TCM Term
preAction = Type -> Term -> TCM Term
abstr }) Term
v Comparison
CmpLeq Type
b) forall a b. (a -> b) -> a -> b
$ \ TCErr
err -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract.ill-typed" Nat
40 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Skipping typed abstraction over ill-typed term" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b))
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
forall (m :: * -> *).
MonadDebug m =>
String -> Nat -> TCMT IO Doc -> m ()
reportSDoc String
"tc.abstract" Nat
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Resulting abstraction" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
res
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
HMap.delete QName
hole
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm (QName -> [Elim] -> Term
Def QName
hole [Elim]
args) Term
res
abstractTerm Type
_ Term
u Type
_ Term
v = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v
class AbsTerm a where
absTerm :: Term -> a -> a
instance AbsTerm Term where
absTerm :: Term -> Term -> Term
absTerm Term
u Term
v | Just [Elim]
es <- Term
u forall a. IsPrefixOf a => a -> a -> Maybe [Elim]
`isPrefixOf` Term
v = Nat -> [Elim] -> Term
Var Nat
0 forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
es
| Bool
otherwise =
case Term
v of
Var Nat
i [Elim]
vs -> Nat -> [Elim] -> Term
Var (Nat
i forall a. Num a => a -> a -> a
+ Nat
1) forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
Lam ArgInfo
h Abs Term
b -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
h forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Abs Term
b
Def QName
c [Elim]
vs -> QName -> [Elim] -> Term
Def QName
c forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
Con ConHead
c ConInfo
ci [Elim]
vs -> ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
Pi Dom Type
a Abs Type
b -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT (Dom Type
a, Abs Type
b)
Lit Literal
l -> Literal -> Term
Lit Literal
l
Level Level
l -> Level -> Term
Level forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Level
l
Sort Sort' Term
s -> Sort' Term -> Term
Sort forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Sort' Term
s
MetaV MetaId
m [Elim]
vs -> MetaId -> [Elim] -> Term
MetaV MetaId
m forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
vs
DontCare Term
mv -> Term -> Term
DontCare forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT Term
mv
Dummy String
s [Elim]
es -> String -> [Elim] -> Term
Dummy String
s forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absT [Elim]
es
where
absT :: AbsTerm b => b -> b
absT :: forall b. AbsTerm b => b -> b
absT b
x = forall a. AbsTerm a => Term -> a -> a
absTerm Term
u b
x
instance AbsTerm Type where
absTerm :: Term -> Type -> Type
absTerm Term
u (El Sort' Term
s Term
v) = forall t a. Sort' t -> a -> Type'' t a
El (forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Sort' Term
s) (forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
v)
instance AbsTerm Sort where
absTerm :: Term -> Sort' Term -> Sort' Term
absTerm Term
u = \case
Univ Univ
u Level
n -> forall t. Univ -> Level' t -> Sort' t
Univ Univ
u forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS Level
n
s :: Sort' Term
s@Inf{} -> Sort' Term
s
Sort' Term
SizeUniv -> forall t. Sort' t
SizeUniv
Sort' Term
LockUniv -> forall t. Sort' t
LockUniv
Sort' Term
LevelUniv -> forall t. Sort' t
LevelUniv
Sort' Term
IntervalUniv -> forall t. Sort' t
IntervalUniv
PiSort Dom' Term Term
a Sort' Term
s1 Abs (Sort' Term)
s2 -> forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort (forall b. AbsTerm b => b -> b
absS Dom' Term Term
a) (forall b. AbsTerm b => b -> b
absS Sort' Term
s1) (forall b. AbsTerm b => b -> b
absS Abs (Sort' Term)
s2)
FunSort Sort' Term
s1 Sort' Term
s2 -> forall t. Sort' t -> Sort' t -> Sort' t
FunSort (forall b. AbsTerm b => b -> b
absS Sort' Term
s1) (forall b. AbsTerm b => b -> b
absS Sort' Term
s2)
UnivSort Sort' Term
s -> forall t. Sort' t -> Sort' t
UnivSort forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS Sort' Term
s
MetaS MetaId
x [Elim]
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS [Elim]
es
DefS QName
d [Elim]
es -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
d forall a b. (a -> b) -> a -> b
$ forall b. AbsTerm b => b -> b
absS [Elim]
es
s :: Sort' Term
s@DummyS{} -> Sort' Term
s
where
absS :: AbsTerm b => b -> b
absS :: forall b. AbsTerm b => b -> b
absS b
x = forall a. AbsTerm a => Term -> a -> a
absTerm Term
u b
x
instance AbsTerm Level where
absTerm :: Term -> Level -> Level
absTerm Term
u (Max Integer
n [PlusLevel' Term]
as) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm Term
u [PlusLevel' Term]
as
instance AbsTerm PlusLevel where
absTerm :: Term -> PlusLevel' Term -> PlusLevel' Term
absTerm Term
u (Plus Integer
n Term
l) = forall t. Integer -> t -> PlusLevel' t
Plus Integer
n forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm Term
u Term
l
instance AbsTerm a => AbsTerm (Elim' a) where
absTerm :: Term -> Elim' a -> Elim' a
absTerm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AbsTerm a => Term -> a -> a
absTerm
instance AbsTerm a => AbsTerm (Arg a) where
absTerm :: Term -> Arg a -> Arg a
absTerm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AbsTerm a => Term -> a -> a
absTerm
instance AbsTerm a => AbsTerm (Dom a) where
absTerm :: Term -> Dom a -> Dom a
absTerm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AbsTerm a => Term -> a -> a
absTerm
instance AbsTerm a => AbsTerm [a] where
absTerm :: Term -> [a] -> [a]
absTerm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AbsTerm a => Term -> a -> a
absTerm
instance AbsTerm a => AbsTerm (Maybe a) where
absTerm :: Term -> Maybe a -> Maybe a
absTerm = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. AbsTerm a => Term -> a -> a
absTerm
instance (TermSubst a, AbsTerm a) => AbsTerm (Abs a) where
absTerm :: Term -> Abs a -> Abs a
absTerm Term
u (NoAbs String
x a
v) = forall a. String -> a -> Abs a
NoAbs String
x forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
v
absTerm Term
u (Abs String
x a
v) = forall a. String -> a -> Abs a
Abs String
x forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => a -> a
swap01 forall a b. (a -> b) -> a -> b
$ forall a. AbsTerm a => Term -> a -> a
absTerm (forall a. Subst a => Nat -> a -> a
raise Nat
1 Term
u) a
v
instance (AbsTerm a, AbsTerm b) => AbsTerm (a, b) where
absTerm :: Term -> (a, b) -> (a, b)
absTerm Term
u (a
x, b
y) = (forall a. AbsTerm a => Term -> a -> a
absTerm Term
u a
x, forall a. AbsTerm a => Term -> a -> a
absTerm Term
u b
y)
swap01 :: TermSubst a => a -> a
swap01 :: forall a. TermSubst a => a -> a
swap01 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst forall a b. (a -> b) -> a -> b
$ Nat -> Term
var Nat
1 forall a. a -> Substitution' a -> Substitution' a
:# forall a. Nat -> Substitution' a -> Substitution' a
liftS Nat
1 (forall a. Nat -> Substitution' a
raiseS Nat
1)
class EqualSy a where
equalSy :: a -> a -> Bool
instance EqualSy a => EqualSy [a] where
equalSy :: [a] -> [a] -> Bool
equalSy [a]
us [a]
vs = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
us forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length [a]
vs) forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. EqualSy a => a -> a -> Bool
equalSy [a]
us [a]
vs
instance EqualSy Term where
equalSy :: Term -> Term -> Bool
equalSy = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(Var Nat
i [Elim]
vs, Var Nat
i' [Elim]
vs') -> Nat
i forall a. Eq a => a -> a -> Bool
== Nat
i' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
vs [Elim]
vs'
(Con ConHead
c ConInfo
_ [Elim]
es, Con ConHead
c' ConInfo
_ [Elim]
es') -> ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
c' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
(Def QName
f [Elim]
es, Def QName
f' [Elim]
es') -> QName
f forall a. Eq a => a -> a -> Bool
== QName
f' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
(MetaV MetaId
x [Elim]
es, MetaV MetaId
x' [Elim]
es') -> MetaId
x forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
(Lit Literal
l , Lit Literal
l' ) -> Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l'
(Lam ArgInfo
ai Abs Term
b, Lam ArgInfo
ai' Abs Term
b') -> forall a. EqualSy a => a -> a -> Bool
equalSy ArgInfo
ai ArgInfo
ai' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Abs Term
b Abs Term
b'
(Level Level
l , Level Level
l' ) -> forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
(Sort Sort' Term
s , Sort Sort' Term
s' ) -> forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
s Sort' Term
s'
(Pi Dom Type
a Abs Type
b , Pi Dom Type
a' Abs Type
b' ) -> forall a. EqualSy a => a -> a -> Bool
equalSy Dom Type
a Dom Type
a' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Abs Type
b Abs Type
b'
(DontCare Term
_, DontCare Term
_ ) -> Bool
True
(Dummy{} , Term
_ ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
(Term
_ , Dummy{} ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
(Term, Term)
_ -> Bool
False
instance EqualSy Level where
equalSy :: Level -> Level -> Bool
equalSy (Max Integer
n [PlusLevel' Term]
vs) (Max Integer
n' [PlusLevel' Term]
vs') = Integer
n forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [PlusLevel' Term]
vs [PlusLevel' Term]
vs'
instance EqualSy PlusLevel where
equalSy :: PlusLevel' Term -> PlusLevel' Term -> Bool
equalSy (Plus Integer
n Term
v) (Plus Integer
n' Term
v') = Integer
n forall a. Eq a => a -> a -> Bool
== Integer
n' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Term
v Term
v'
instance EqualSy Sort where
equalSy :: Sort' Term -> Sort' Term -> Bool
equalSy = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(Univ Univ
u Level
l , Univ Univ
u' Level
l' ) -> Univ
u forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Level
l Level
l'
(Inf Univ
u Integer
m , Inf Univ
u' Integer
n ) -> Univ
u forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& Integer
m forall a. Eq a => a -> a -> Bool
== Integer
n
(Sort' Term
SizeUniv , Sort' Term
SizeUniv ) -> Bool
True
(Sort' Term
LevelUniv , Sort' Term
LevelUniv ) -> Bool
True
(PiSort Dom' Term Term
a Sort' Term
b Abs (Sort' Term)
c, PiSort Dom' Term Term
a' Sort' Term
b' Abs (Sort' Term)
c') -> forall a. EqualSy a => a -> a -> Bool
equalSy Dom' Term Term
a Dom' Term Term
a' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
b Sort' Term
b' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Abs (Sort' Term)
c Abs (Sort' Term)
c'
(FunSort Sort' Term
a Sort' Term
b, FunSort Sort' Term
a' Sort' Term
b') -> forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
a Sort' Term
a' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
b Sort' Term
b'
(UnivSort Sort' Term
a, UnivSort Sort' Term
a' ) -> forall a. EqualSy a => a -> a -> Bool
equalSy Sort' Term
a Sort' Term
a'
(MetaS MetaId
x [Elim]
es, MetaS MetaId
x' [Elim]
es') -> MetaId
x forall a. Eq a => a -> a -> Bool
== MetaId
x' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
(DefS QName
d [Elim]
es, DefS QName
d' [Elim]
es') -> QName
d forall a. Eq a => a -> a -> Bool
== QName
d' Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy [Elim]
es [Elim]
es'
(DummyS{} , Sort' Term
_ ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
(Sort' Term
_ , DummyS{} ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
(Sort' Term, Sort' Term)
_ -> Bool
False
instance EqualSy Type where
equalSy :: Type -> Type -> Bool
equalSy = forall a. EqualSy a => a -> a -> Bool
equalSy forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall t a. Type'' t a -> a
unEl
instance EqualSy a => EqualSy (Elim' a) where
equalSy :: Elim' a -> Elim' a -> Bool
equalSy = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(Proj ProjOrigin
_ QName
f, Proj ProjOrigin
_ QName
f') -> QName
f forall a. Eq a => a -> a -> Bool
== QName
f'
(Apply Arg a
a, Apply Arg a
a') -> forall a. EqualSy a => a -> a -> Bool
equalSy Arg a
a Arg a
a'
(IApply a
u a
v a
r, IApply a
u' a
v' a
r') ->
forall a. EqualSy a => a -> a -> Bool
equalSy a
u a
u'
Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy a
v a
v'
Bool -> Bool -> Bool
&& forall a. EqualSy a => a -> a -> Bool
equalSy a
r a
r'
(Elim' a, Elim' a)
_ -> Bool
False
instance (Subst a, EqualSy a) => EqualSy (Abs a) where
equalSy :: Abs a -> Abs a -> Bool
equalSy = forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall a b. (a -> b) -> a -> b
$ \case
(NoAbs String
_x a
b, NoAbs String
_x' a
b') -> forall a. EqualSy a => a -> a -> Bool
equalSy a
b a
b'
(Abs a
a , Abs a
a' ) -> forall a. EqualSy a => a -> a -> Bool
equalSy (forall a. Subst a => Abs a -> a
absBody Abs a
a) (forall a. Subst a => Abs a -> a
absBody Abs a
a')
instance EqualSy ArgInfo where
equalSy :: ArgInfo -> ArgInfo -> Bool
equalSy (ArgInfo Hiding
h Modality
m Origin
_o FreeVariables
_fv Annotation
a) (ArgInfo Hiding
h' Modality
m' Origin
_o' FreeVariables
_fv' Annotation
a') =
Hiding
h forall a. Eq a => a -> a -> Bool
== Hiding
h' Bool -> Bool -> Bool
&& Modality
m forall a. Eq a => a -> a -> Bool
== Modality
m' Bool -> Bool -> Bool
&& Annotation
a forall a. Eq a => a -> a -> Bool
== Annotation
a'
instance EqualSy a => EqualSy (Dom a) where
equalSy :: Dom a -> Dom a -> Bool
equalSy d :: Dom a
d@(Dom ArgInfo
ai Maybe NamedName
x Bool
f Maybe Term
_tac a
a) d' :: Dom a
d'@(Dom ArgInfo
ai' Maybe NamedName
x' Bool
f' Maybe Term
_tac' a
a') = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ Maybe NamedName
x forall a. Eq a => a -> a -> Bool
== Maybe NamedName
x'
, Bool
f forall a. Eq a => a -> a -> Bool
== Bool
f'
, forall a. EqualSy a => a -> a -> Bool
equalSy ArgInfo
ai ArgInfo
ai'
, forall a. EqualSy a => a -> a -> Bool
equalSy a
a a
a'
]
instance EqualSy a => EqualSy (Arg a) where
equalSy :: Arg a -> Arg a -> Bool
equalSy (Arg (ArgInfo Hiding
h Modality
m Origin
_o FreeVariables
_fv Annotation
a) a
v) (Arg (ArgInfo Hiding
h' Modality
m' Origin
_o' FreeVariables
_fv' Annotation
a') a
v') =
Hiding
h forall a. Eq a => a -> a -> Bool
== Hiding
h' Bool -> Bool -> Bool
&& (forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
m Bool -> Bool -> Bool
|| forall a. LensRelevance a => a -> Bool
isIrrelevant Modality
m' Bool -> Bool -> Bool
|| forall a. EqualSy a => a -> a -> Bool
equalSy a
v a
v')