-- | Reconstruct dropped parameters from constructors.  Used by
--   with-abstraction to avoid ill-typed abstractions (#745). Note that the
--   term is invalid after parameter reconstruction. Parameters need to be
--   dropped again before using it.

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  -- under-applied when under > 0
          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 ty f vs@ where @ty@ is the type of @f []@ and vs are valid
    -- arguments to something of type @ty@
    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
    -- We duplicate @f@ because we don't want the parameters to be reconstructed in
    -- type, since it would cause type-checking error when running @checkInternal'@.
    -- The first one @fTe@ is for term, the other one @fTy@ for type.
    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