module Agda.TypeChecking.ReconstructParameters where
import Data.Maybe
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.TypeChecking.Monad
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Datatypes
import Agda.Utils.Size
import Agda.Utils.Either
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Impossible
reconstructParametersInType :: Type -> TCM Type
reconstructParametersInType :: Type -> TCM Type
reconstructParametersInType = Action (TCMT IO) -> Type -> TCM Type
reconstructParametersInType' forall (m :: * -> *). PureTCM m => Action m
defaultAction
reconstructParametersInType' :: Action TCM -> Type -> TCM Type
reconstructParametersInType' :: Action (TCMT IO) -> Type -> TCM Type
reconstructParametersInType' Action (TCMT IO)
act Type
a =
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Action (TCMT IO) -> Type -> Term -> TCM Term
reconstructParameters' Action (TCMT IO)
act (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
a)) Type
a
reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel Telescope
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Tele a
EmptyTel
reconstructParametersInTel (ExtendTel Dom Type
a Abs Telescope
tel) = do
Type
ar <- Type -> TCM Type
reconstructParametersInType (forall t e. Dom' t e -> e
unDom Dom Type
a)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (forall a. Abs a -> [Char]
absName Abs Telescope
tel, Dom Type
a) forall a b. (a -> b) -> a -> b
$
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
ar forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Telescope -> TCM Telescope
reconstructParametersInTel Abs Telescope
tel
reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView (EqualityType Sort
s QName
eq [Arg Term]
l Arg Term
a Arg Term
u Arg Term
v) =
Sort
-> QName
-> [Arg Term]
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Sort
s QName
eq [Arg Term]
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCM Term
reconstructParameters forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
s) Arg Term
a
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCM Term
reconstructParameters forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a) Arg Term
u
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCM Term
reconstructParameters forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a) Arg Term
v
reconstructParametersInEqView (OtherType Type
a) = Type -> EqualityView
OtherType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Type
reconstructParametersInType Type
a
reconstructParametersInEqView (IdiomType Type
a) = Type -> EqualityView
IdiomType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Type
reconstructParametersInType Type
a
reconstructParameters :: Type -> Term -> TCM Term
reconstructParameters :: Type -> Term -> TCM Term
reconstructParameters = Action (TCMT IO) -> Type -> Term -> TCM Term
reconstructParameters' forall (m :: * -> *). PureTCM m => Action m
defaultAction
reconstructParameters' :: Action TCM -> Type -> Term -> TCM Term
reconstructParameters' :: Action (TCMT IO) -> Type -> Term -> TCM Term
reconstructParameters' Action (TCMT IO)
act Type
a Term
v = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.with.reconstruct" Int
30 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"reconstructing parameters in"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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
<+> TCM Doc
":", forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
Term
v <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action (TCMT IO)
reconstructAction Term
v Comparison
CmpLeq Type
a
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.with.reconstruct" Int
30 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCM Doc
"-->" 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 :: * -> *) a. Monad m => a -> m a
return Term
v
where
reconstructAction :: Action (TCMT IO)
reconstructAction = forall (m :: * -> *). PureTCM m => Action m
defaultAction{ postAction :: Type -> Term -> TCM Term
postAction = Type -> Term -> TCM Term
reconstruct }
reconstruct :: Type -> Term -> TCM Term
reconstruct Type
a Term
v = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.with.reconstruct" Int
30 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"reconstructing in"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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
<+> TCM Doc
":", forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
case Term -> Term
unSpine Term
v of
Con ConHead
h ConInfo
ci [Elim]
vs -> do
ConHead
hh <- forall a b. (a -> b) -> Either a b -> b
fromRight forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead (ConHead -> QName
conName ConHead
h)
TelV Telescope
tel Type
a <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
let under :: Int
under = forall a. Sized a => a -> Int
size Telescope
tel
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"reconstructing"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
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
<+> TCM Doc
":"
, forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
case (forall t a. Type'' t a -> a
unEl Type
a) of
Def QName
d [Elim]
es -> do
Just Int
n <- Definition -> Maybe Int
defParameters forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
let prePs :: [Elim]
prePs = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Impossible -> Int -> Substitution' a
strengthenS HasCallStack => Impossible
impossible Int
under) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
n forall a b. (a -> b) -> a -> b
$ [Elim]
es
let hiddenPs :: [Elim]
hiddenPs = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
prePs
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The hiddenPs are" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Elim]
hiddenPs
Type
tyCon <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
hh)
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Here we start infering spine"
((Term
_,Con ConHead
hh ConInfo
ci [Elim]
psAfterAct),Type
_) <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
inferSpine' Action (TCMT IO)
act Type
tyCon (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
hh ConInfo
ci []) (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
hh ConInfo
ci []) [Elim]
hiddenPs
((Term
_,Term
conWithPars),Type
_) <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
inferSpine' Action (TCMT IO)
reconstructAction Type
tyCon (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
hh ConInfo
ci []) (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
hh ConInfo
ci []) [Elim]
psAfterAct
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The spine has been inferred:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
conWithPars
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> [Elim] -> Term
applyWithoutReversing Term
conWithPars [Elim]
vs
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Term
_ -> do
Term
vv <- forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone Term
v
Type -> Term -> TCM Term
unSpineAndReconstruct Type
a Term
vv
unSpineAndReconstruct :: Type -> Term -> TCM Term
unSpineAndReconstruct :: Type -> Term -> TCM Term
unSpineAndReconstruct Type
a Term
v =
case Term
v of
Var Int
i [Elim]
vs -> do
Type
ty <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
Telescope
ctx <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Var case "forall a. [a] -> [a] -> [a]
++(forall a. Show a => a -> [Char]
show Int
i)forall a. [a] -> [a] -> [a]
++[Char]
" with context")) forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ctx
Type -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop Type
ty (Int -> [Elim] -> Term
Var Int
i) [Elim]
vs
Def QName
nam [Elim]
vs -> do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Def case"
Type
ty <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
nam
Type -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop Type
ty (QName -> [Elim] -> Term
Def QName
nam) [Elim]
vs
MetaV MetaId
id [Elim]
vs -> do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"MetaVar case"
Type
ty <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
id
Type -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop Type
ty (MetaId -> [Elim] -> Term
MetaV MetaId
id) [Elim]
vs
Term
_ -> do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Another case" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
loop :: Type -> (Elims -> Term) -> Elims -> TCM Term
loop :: Type -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop Type
ty [Elim] -> Term
f = Type -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop' Type
ty [Elim] -> Term
f [Elim] -> Term
f
loop' :: Type -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop' Type
ty [Elim] -> Term
fTe [Elim] -> Term
_ [] = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Loop ended" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
fTe [])
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
fTe []
loop' Type
ty [Elim] -> Term
fTe [Elim] -> Term
fTy (Apply Arg Term
u:[Elim]
es) = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The type before app is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The term before app is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Elim] -> Term
fTe [])
Arg Term
uu <- forall a. TermLike a => a -> TCM a
dropParameters Arg Term
u
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The app is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
uu
Type
ty' <- forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
ty Arg Term
uu
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The type after app is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty'
Type -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop' Type
ty' ([Elim] -> Term
fTe forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Arg a -> Elim' a
Apply Arg Term
u forall a. a -> [a] -> [a]
:)) ([Elim] -> Term
fTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Arg a -> Elim' a
Apply Arg Term
uu forall a. a -> [a] -> [a]
:)) [Elim]
es
loop' Type
ty [Elim] -> Term
fTe [Elim] -> Term
fTy (Proj ProjOrigin
o QName
p:[Elim]
es) = do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The type is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The term is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Elim] -> Term
fTe [])
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The proj is:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
p
Type
ty' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty
case forall t a. Type'' t a -> a
unEl Type
ty' of
Def QName
r [Elim]
pars -> do
~(Just (El Sort
_ (Pi Dom Type
_ Abs Type
b))) <- forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
p Type
ty'
Type
tyProj <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p
let reconstructWithoutPostFixing :: Action (TCMT IO)
reconstructWithoutPostFixing = Action (TCMT IO)
reconstructAction { elimViewAction :: Term -> TCM Term
elimViewAction = forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
NoPostfix }
let hiddenPs :: [Elim]
hiddenPs = forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall {a}. (LensHiding a, LensRelevance a) => Type -> [a] -> [a]
mapHide Type
tyProj forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
pars
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"The params are" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Elim]
hiddenPs
((Term
_,Def QName
p [Elim]
psAfterAct),Type
_) <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
inferSpine' Action (TCMT IO)
act Type
tyProj (QName -> [Elim] -> Term
Def QName
p []) (QName -> [Elim] -> Term
Def QName
p []) [Elim]
hiddenPs
((Term
_,Term
projWithPars),Type
_) <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m
-> Type -> Term -> Term -> [Elim] -> m ((Term, Term), Type)
inferSpine' Action (TCMT IO)
reconstructWithoutPostFixing Type
tyProj (QName -> [Elim] -> Term
Def QName
p []) (QName -> [Elim] -> Term
Def QName
p []) [Elim]
psAfterAct
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Spine infered" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
projWithPars
let fTe' :: [Elim] -> Term
fTe' [Elim]
x = Term -> [Elim] -> Term
applyWithoutReversing Term
projWithPars ((forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
fTe [])forall a. a -> [a] -> [a]
:[Elim]
x)
Type -> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCM Term
loop' (forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b ([Elim] -> Term
fTy [])) [Elim] -> Term
fTe' ([Elim] -> Term
fTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
pforall a. a -> [a] -> [a]
:)) [Elim]
es
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
loop' Type
ty [Elim] -> Term
_ [Elim] -> Term
_ (IApply {}:[Elim]
vs) = forall a. HasCallStack => a
__IMPOSSIBLE__
applyWithoutReversing :: Term -> Elims -> Term
applyWithoutReversing :: Term -> [Elim] -> Term
applyWithoutReversing (Var Int
i [Elim]
es) [Elim]
ess = Int -> [Elim] -> Term
Var Int
i ([Elim]
esforall a. [a] -> [a] -> [a]
++[Elim]
ess)
applyWithoutReversing (Def QName
n [Elim]
es) [Elim]
ess = QName -> [Elim] -> Term
Def QName
n ([Elim]
esforall a. [a] -> [a] -> [a]
++[Elim]
ess)
applyWithoutReversing (Con ConHead
h ConInfo
i [Elim]
es) [Elim]
ess = ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
h ConInfo
i ([Elim]
esforall a. [a] -> [a] -> [a]
++[Elim]
ess)
applyWithoutReversing (MetaV MetaId
i [Elim]
es) [Elim]
ess = MetaId -> [Elim] -> Term
MetaV MetaId
i ([Elim]
esforall a. [a] -> [a] -> [a]
++[Elim]
ess)
applyWithoutReversing (Dummy [Char]
s [Elim]
es) [Elim]
ess = [Char] -> [Elim] -> Term
Dummy [Char]
s ([Elim]
esforall a. [a] -> [a] -> [a]
++[Elim]
ess)
applyWithoutReversing Term
_ [Elim]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
mapHide :: Type -> [a] -> [a]
mapHide (El Sort
_ (Pi Dom Type
a Abs Type
b)) (a
p:[a]
tl) =
forall a. Bool -> (a -> a) -> a -> a
applyWhen (forall a. LensHiding a => a -> Hiding
getHiding Dom Type
a forall a. Eq a => a -> a -> Bool
== Hiding
Hidden) forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams a
p forall a. a -> [a] -> [a]
: Type -> [a] -> [a]
mapHide (forall a. Abs a -> a
unAbs Abs Type
b) [a]
tl
mapHide Type
t [a]
l = [a]
l
dropParameters :: TermLike a => a -> TCM a
dropParameters :: forall a. TermLike a => a -> TCM a
dropParameters = forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM forall a b. (a -> b) -> a -> b
$
\case
Con ConHead
c ConInfo
ci [Elim]
vs -> do
Constructor{ conData :: Defn -> QName
conData = QName
d } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
Just Int
n <- Definition -> Maybe Int
defParameters forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n [Elim]
vs
v :: Term
v@(Def QName
f [Elim]
vs) -> do
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe Projection
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
Just Projection
pr -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Apply t => t -> [Elim] -> t
applyE (Projection -> ProjOrigin -> Term
projDropPars Projection
pr ProjOrigin
ProjSystem) [Elim]
vs
Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v