-- | 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.Functor ( ($>) )
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 :: Tele (Dom Type) -> TCM (Tele (Dom Type))
reconstructParametersInTel Tele (Dom Type)
EmptyTel = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Tele a
EmptyTel
reconstructParametersInTel (ExtendTel Dom Type
a Abs (Tele (Dom Type))
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 -> ArgName
absName Abs (Tele (Dom Type))
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 Tele (Dom Type) -> TCM (Tele (Dom Type))
reconstructParametersInTel Abs (Tele (Dom Type))
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 =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.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) -> Action (TCMT IO)
reconstructAction' Action (TCMT IO)
act) Term
v Comparison
CmpLeq Type
a

  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.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

reconstructAction :: Action TCM
reconstructAction :: Action (TCMT IO)
reconstructAction = Action (TCMT IO) -> Action (TCMT IO)
reconstructAction' forall (m :: * -> *). PureTCM m => Action m
defaultAction

reconstructAction' :: Action TCM -> Action TCM
reconstructAction' :: Action (TCMT IO) -> Action (TCMT IO)
reconstructAction' Action (TCMT IO)
act = Action (TCMT IO)
act{ postAction :: Type -> Term -> TCM Term
postAction = \Type
ty Term
tm -> forall (m :: * -> *). Action m -> Type -> Term -> m Term
postAction Action (TCMT IO)
act Type
ty Term
tm forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> Term -> TCM Term
reconstruct Type
ty }

reconstruct :: Type -> Term -> TCM Term
reconstruct :: Type -> Term -> TCM Term
reconstruct Type
ty Term
v = do
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.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
ty ] ]
    case Term
v of
      Con ConHead
h ConInfo
ci Elims
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 Tele (Dom Type)
tel Type
dataTy <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
ty
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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
dataTy ] ]
        [Arg Term]
pars <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Tele (Dom Type)
tel forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCMT IO [Arg Term]
extractParameters (ConHead -> QName
conName ConHead
h) Type
dataTy
        -- If the constructor is underapplied, we need to escape from the telescope.
        let escape :: [Arg Term] -> [Arg Term]
escape = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst forall a b. (a -> b) -> a -> b
$ forall a. Impossible -> Int -> Substitution' a
strengthenS forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
hh ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply ([Arg Term] -> [Arg Term]
escape [Arg Term]
pars) forall a. [a] -> [a] -> [a]
++ Elims
vs
      Def QName
f Elims
es -> forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        ProjectionView QName
_f Arg Term
a Elims
es -> do
          Type
recTy <- forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. TermLike a => a -> TCM a
dropParameters (forall e. Arg e -> e
unArg Arg Term
a)
          [Arg Term]
pars <- QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
f Type
recTy
          Type -> (Elims -> Term) -> Elims -> TCM Term
loop Type
ty (QName -> Elims -> Term
Def QName
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
pars forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Arg a -> Elim' a
Apply Arg Term
aforall a. a -> [a] -> [a]
:)) Elims
es
        LoneProjectionLike QName
_f ArgInfo
i -> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
ty) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Pi Dom Type
recTy Abs Type
_ -> do
            [Arg Term]
pars <- QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
f (forall t e. Dom' t e -> e
unDom Dom Type
recTy)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
pars
          Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
        NoProjection{} -> do
          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
f
          Type -> (Elims -> Term) -> Elims -> TCM Term
loop Type
ty (QName -> Elims -> Term
Def QName
f) Elims
es
      Var Int
i Elims
es -> do
        Type
ty <- forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
        Type -> (Elims -> Term) -> Elims -> TCM Term
loop Type
ty (Int -> Elims -> Term
Var Int
i) Elims
es
      MetaV MetaId
m Elims
es -> do
        Type
ty <- forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m
        Type -> (Elims -> Term) -> Elims -> TCM Term
loop Type
ty (MetaId -> Elims -> Term
MetaV MetaId
m) Elims
es
      Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

  where
    -- @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 -> (Elims -> Term) -> Elims -> TCM Term
loop Type
ty Elims -> Term
f []           = do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 (Elims -> Term
f [])
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Elims -> Term
f []
    loop Type
ty Elims -> Term
f (Apply Arg Term
u:Elims
es) = do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 (Elims -> Term
f [])
      Arg Term
uu <- forall a. TermLike a => a -> TCM a
dropParameters Arg Term
u
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 -> (Elims -> Term) -> Elims -> TCM Term
loop Type
ty' (Elims -> Term
f 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]
:)) Elims
es
    loop Type
ty Elims -> Term
f (Proj ProjOrigin
o QName
p:Elims
es) = do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 (Elims -> Term
f [])
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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
      [Arg Term]
pars <- QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
p Type
ty
      ~(Just (El Sort
_ (Pi Dom Type
_ Abs Type
b))) <- forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty
      let fTm :: Term
fTm = Elims -> Term
f []
      Term
fe <- forall a. TermLike a => a -> TCM a
dropParameters Term
fTm
      Type -> (Elims -> Term) -> Elims -> TCM Term
loop (forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b Term
fe) (QName -> Elims -> Term
Def QName
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
pars forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Arg a -> Elim' a
Apply (forall a. a -> Arg a
defaultArg Term
fTm) forall a. a -> [a] -> [a]
:)) Elims
es
    loop Type
ty Elims -> Term
_ (IApply {}:Elims
vs) = forall a. HasCallStack => a
__IMPOSSIBLE__

-- Extract the parameters from the type of a constructor
-- application or the type of the principal argument of a
-- projection.
extractParameters :: QName -> Type -> TCM Args
extractParameters :: QName -> Type -> TCMT IO [Arg Term]
extractParameters QName
q Type
ty = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
ty) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
d Elims
prePs -> do
    Type
dt <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Here we start infering spine"
    ((Term
_,Def QName
_ Elims
postPs),Type
_) <- forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
inferSpine' Action (TCMT IO)
reconstructAction Type
dt (QName -> Elims -> Term
Def QName
d []) (QName -> Elims -> Term
Def QName
d []) Elims
prePs
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCM Doc -> m ()
reportSDoc ArgName
"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 Elims
postPs
    Definition
info <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
    let mkParam :: Elim' a -> Arg a
mkParam = forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Empty -> Elim' a -> Arg a
isApplyElim' forall a. HasCallStack => a
__IMPOSSIBLE__
    if -- Case: data or record constructor
       | Constructor{ conPars :: Defn -> Int
conPars = Int
n } <- Definition -> Defn
theDef Definition
info ->
           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}. Elim' a -> Arg a
mkParam forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
n Elims
postPs
       -- Case: regular projection
       | Defn -> Bool
isProperProjection (Definition -> Defn
theDef Definition
info) ->
           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}. Elim' a -> Arg a
mkParam Elims
postPs
       -- Case: projection-like function
       | Bool
otherwise -> do
           TelV Tele (Dom Type)
tel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo (forall a. Sized a => a -> Int
size Elims
postPs) forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
info
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall (f :: * -> *) a b. Functor f => f a -> b -> f b
($>) (forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel :: Args) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Empty -> Elim' a -> Arg a
isApplyElim' forall a. HasCallStack => a
__IMPOSSIBLE__) Elims
postPs
  Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

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 Elims
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 -> Elims -> Term
Con ConHead
c ConInfo
ci forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n Elims
vs
        v :: Term
v@(Def QName
f Elims
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 -> Elims -> t
applyE (Projection -> ProjOrigin -> Term
projDropPars Projection
pr ProjOrigin
ProjSystem) Elims
vs
        Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v