-- | 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' Action (TCMT IO)
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 =
  (Term -> TCMT IO Term) -> Type -> TCM Type
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Action (TCMT IO) -> Type -> Term -> TCMT IO Term
reconstructParameters' Action (TCMT IO)
act (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Sort
forall a. LensSort a => a -> Sort
getSort Type
a)) Type
a

reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel Telescope
EmptyTel = Telescope -> TCM Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
forall a. Tele a
EmptyTel
reconstructParametersInTel (ExtendTel Dom Type
a Abs Telescope
tel) = do
  Type
ar <- Type -> TCM Type
reconstructParametersInType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
  ([Char], Dom Type) -> TCM Telescope -> TCM Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Abs Telescope -> [Char]
forall a. Abs a -> [Char]
absName Abs Telescope
tel, Dom Type
a) (TCM Telescope -> TCM Telescope) -> TCM Telescope -> TCM Telescope
forall a b. (a -> b) -> a -> b
$
    Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type
ar Type -> Dom Type -> Dom Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
a) (Abs Telescope -> Telescope)
-> TCMT IO (Abs Telescope) -> TCM Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Telescope -> TCM Telescope)
-> Abs Telescope -> TCMT IO (Abs Telescope)
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 (Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> TCMT IO (Arg Term)
-> TCMT IO (Arg Term -> Arg Term -> EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort Sort
s) Arg Term
a
                      TCMT IO (Arg Term -> Arg Term -> EqualityView)
-> TCMT IO (Arg Term) -> TCMT IO (Arg Term -> EqualityView)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Arg Term
u
                      TCMT IO (Arg Term -> EqualityView)
-> TCMT IO (Arg Term) -> TCM EqualityView
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> TCMT IO Term) -> Arg Term -> TCMT IO (Arg Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Type -> Term -> TCMT IO Term
reconstructParameters (Type -> Term -> TCMT IO Term) -> Type -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a) Arg Term
v
reconstructParametersInEqView (OtherType Type
a) = Type -> EqualityView
OtherType (Type -> EqualityView) -> TCM Type -> TCM EqualityView
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 (Type -> EqualityView) -> TCM Type -> TCM EqualityView
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 -> TCMT IO Term
reconstructParameters = Action (TCMT IO) -> Type -> Term -> TCMT IO Term
reconstructParameters' Action (TCMT IO)
forall (m :: * -> *). PureTCM m => Action m
defaultAction

reconstructParameters' :: Action TCM -> Type -> Term -> TCM Term
reconstructParameters' :: Action (TCMT IO) -> Type -> Term -> TCMT IO Term
reconstructParameters' Action (TCMT IO)
act Type
a Term
v = do
  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.with.reconstruct" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"reconstructing parameters in"
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
  Term
v <- Action (TCMT IO) -> Term -> Comparison -> Type -> TCMT IO Term
forall (m :: * -> *).
MonadCheckInternal m =>
Action m -> Term -> Comparison -> Type -> m Term
checkInternal' Action (TCMT IO)
reconstructAction Term
v Comparison
CmpLeq Type
a

  [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.with.reconstruct" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"-->" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  where
    reconstructAction :: Action (TCMT IO)
reconstructAction = Action (TCMT IO)
forall (m :: * -> *). PureTCM m => Action m
defaultAction{ postAction :: Type -> Term -> TCMT IO Term
postAction = Type -> Term -> TCMT IO Term
reconstruct }

    reconstruct :: Type -> Term -> TCMT IO Term
reconstruct Type
a Term
v = do
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.with.reconstruct" Int
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"reconstructing in"
        , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":", Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
      case Term -> Term
unSpine Term
v of
        Con ConHead
h ConInfo
ci [Elim]
vs -> do
          ConHead
hh <- (SigError -> ConHead) -> Either SigError ConHead -> ConHead
forall a b. (a -> b) -> Either a b -> b
fromRight SigError -> ConHead
forall a. HasCallStack => a
__IMPOSSIBLE__ (Either SigError ConHead -> ConHead)
-> TCM (Either SigError ConHead) -> TCM ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Either SigError ConHead)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError ConHead)
getConHead (ConHead -> QName
conName ConHead
h)
          TelV Telescope
tel Type
a <- Type -> TCM (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
          let under :: Int
under = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel  -- under-applied when under > 0
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
            [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"reconstructing"
                , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
                               , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a ] ]
          case (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) of
            Def QName
d [Elim]
es -> do
              Just Int
n <- Definition -> Maybe Int
defParameters (Definition -> Maybe Int) -> TCM Definition -> TCM (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
              let prePs :: [Elim]
prePs = Substitution' (SubstArg [Elim]) -> [Elim] -> [Elim]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> Int -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible Int
under) ([Elim] -> [Elim]) -> ([Elim] -> [Elim]) -> [Elim] -> [Elim]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Elim] -> [Elim]
forall a. Int -> [a] -> [a]
take Int
n ([Elim] -> [Elim]) -> [Elim] -> [Elim]
forall a b. (a -> b) -> a -> b
$ [Elim]
es
              let hiddenPs :: [Elim]
hiddenPs = (Arg Term -> Elim) -> [Arg Term] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Arg Term -> Arg Term) -> Arg Term -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Arg Term
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams) ([Arg Term] -> [Elim]) -> [Arg Term] -> [Elim]
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$
                               [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
prePs
              [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The hiddenPs are" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Elim] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Elim]
hiddenPs
              Type
tyCon <- Definition -> Type
defType (Definition -> Type) -> TCM Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
hh)
              [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Here we start infering spine"
              ((Term
_,Con ConHead
hh ConInfo
ci [Elim]
psAfterAct),Type
_) <- Action (TCMT IO)
-> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), 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
_) <- Action (TCMT IO)
-> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), 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
              [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The spine has been inferred:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
conWithPars
              Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> [Elim] -> Term
applyWithoutReversing Term
conWithPars [Elim]
vs
            Term
_ -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
        Term
_  -> do
          Term
vv <- ProjEliminator -> Term -> TCMT IO Term
forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
EvenLone Term
v
          Type -> Term -> TCMT IO Term
unSpineAndReconstruct Type
a Term
vv
    unSpineAndReconstruct :: Type -> Term -> TCM Term
    unSpineAndReconstruct :: Type -> Term -> TCMT IO Term
unSpineAndReconstruct Type
a Term
v =
      case Term
v of
        Var Int
i [Elim]
vs -> do
          Type
ty <- Int -> TCM Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
          Telescope
ctx <- TCM Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ([Char] -> TCM Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"Var case "[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++(Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++[Char]
" with context")) TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
ctx
          Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
loop Type
ty (Int -> [Elim] -> Term
Var Int
i) [Elim]
vs
        Def QName
nam [Elim]
vs -> do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Def case"
          Type
ty <- Definition -> Type
defType (Definition -> Type) -> TCM Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
nam
          Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
loop Type
ty (QName -> [Elim] -> Term
Def QName
nam) [Elim]
vs
        MetaV MetaId
id [Elim]
vs -> do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"MetaVar case"
          Type
ty <- MetaId -> TCM Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
id
          Type -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
loop Type
ty (MetaId -> [Elim] -> Term
MetaV MetaId
id) [Elim]
vs
        Term
_ -> do
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Another case" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
          Term -> TCMT IO Term
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] -> TCMT IO Term
loop Type
ty [Elim] -> Term
f = Type
-> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO 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] -> TCMT IO Term
loop' Type
ty [Elim] -> Term
fTe [Elim] -> Term
_   []           = do
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Loop ended" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Term -> TCM Doc) -> Term -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
fTe [])
      Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
fTe []
    loop' Type
ty [Elim] -> Term
fTe [Elim] -> Term
fTy (Apply Arg Term
u:[Elim]
es) = do
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The type before app is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The term before app is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Elim] -> Term
fTe [])
      Arg Term
uu <- Arg Term -> TCMT IO (Arg Term)
forall a. TermLike a => a -> TCM a
dropParameters Arg Term
u
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The app is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
uu
      Type
ty' <- Type -> Arg Term -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
ty Arg Term
uu
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The type after app is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty'
      Type
-> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
loop' Type
ty' ([Elim] -> Term
fTe ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
u Elim -> [Elim] -> [Elim]
forall a. a -> [a] -> [a]
:)) ([Elim] -> Term
fTy ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
uu Elim -> [Elim] -> [Elim]
forall a. a -> [a] -> [a]
:)) [Elim]
es
    loop' Type
ty [Elim] -> Term
fTe [Elim] -> Term
fTy (Proj ProjOrigin
o QName
p:[Elim]
es) = do
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The type is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The term is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Elim] -> Term
fTe [])
      [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The proj is:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
p
      Type
ty' <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
ty
      case Type -> Term
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))) <- QName -> Type -> TCMT IO (Maybe Type)
forall (m :: * -> *). PureTCM m => QName -> Type -> m (Maybe Type)
getDefType QName
p Type
ty'
          Type
tyProj <- Definition -> Type
defType (Definition -> Type) -> TCM Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p
          let reconstructWithoutPostFixing :: Action (TCMT IO)
reconstructWithoutPostFixing = Action (TCMT IO)
reconstructAction { elimViewAction :: Term -> TCMT IO Term
elimViewAction = ProjEliminator -> Term -> TCMT IO Term
forall (m :: * -> *). PureTCM m => ProjEliminator -> Term -> m Term
elimView ProjEliminator
NoPostfix }
          let hiddenPs :: [Elim]
hiddenPs = (Arg Term -> Elim) -> [Arg Term] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> [Elim]) -> [Arg Term] -> [Elim]
forall a b. (a -> b) -> a -> b
$ Type -> [Arg Term] -> [Arg Term]
forall {a}. (LensHiding a, LensRelevance a) => Type -> [a] -> [a]
mapHide Type
tyProj ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$
                               [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
pars
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"The params are" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Elim] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Elim]
hiddenPs
          ((Term
_,Def QName
p [Elim]
psAfterAct),Type
_) <- Action (TCMT IO)
-> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), 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
_) <- Action (TCMT IO)
-> Type -> Term -> Term -> [Elim] -> TCM ((Term, Term), 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
          [Char] -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCM Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Spine infered" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM 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 ((Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
fTe [])Elim -> [Elim] -> [Elim]
forall a. a -> [a] -> [a]
:[Elim]
x)
          Type
-> ([Elim] -> Term) -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
loop' (Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Type
b ([Elim] -> Term
fTy [])) [Elim] -> Term
fTe' ([Elim] -> Term
fTy ([Elim] -> Term) -> ([Elim] -> [Elim]) -> [Elim] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
o QName
pElim -> [Elim] -> [Elim]
forall a. a -> [a] -> [a]
:)) [Elim]
es
        Term
_ -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    loop' Type
ty [Elim] -> Term
_   [Elim] -> Term
_   (IApply {}:[Elim]
vs) = TCMT IO Term
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]
es[Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++[Elim]
ess)
    applyWithoutReversing (Def QName
n [Elim]
es)   [Elim]
ess = QName -> [Elim] -> Term
Def QName
n ([Elim]
es[Elim] -> [Elim] -> [Elim]
forall 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]
es[Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++[Elim]
ess)
    applyWithoutReversing (MetaV MetaId
i [Elim]
es) [Elim]
ess = MetaId -> [Elim] -> Term
MetaV MetaId
i ([Elim]
es[Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++[Elim]
ess)
    applyWithoutReversing (Dummy [Char]
s [Elim]
es) [Elim]
ess = [Char] -> [Elim] -> Term
Dummy [Char]
s ([Elim]
es[Elim] -> [Elim] -> [Elim]
forall a. [a] -> [a] -> [a]
++[Elim]
ess)
    applyWithoutReversing Term
_            [Elim]
_   = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

    mapHide :: Type -> [a] -> [a]
mapHide (El Sort
_ (Pi Dom Type
a Abs Type
b)) (a
p:[a]
tl) =
      Bool -> (a -> a) -> a -> a
forall a. Bool -> (a -> a) -> a -> a
applyWhen (Dom Type -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Dom Type
a Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
Hidden) a -> a
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams a
p a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Type -> [a] -> [a]
mapHide (Abs Type -> Type
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 = (Term -> TCMT IO Term) -> a -> TCMT IO a
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM ((Term -> TCMT IO Term) -> a -> TCMT IO a)
-> (Term -> TCMT IO Term) -> a -> TCMT IO a
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 (Definition -> Defn) -> TCM Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
          Just Int
n <- Definition -> Maybe Int
defParameters (Definition -> Maybe Int) -> TCM Definition -> TCM (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
          Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c ConInfo
ci ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ Int -> [Elim] -> [Elim]
forall a. Int -> [a] -> [a]
drop Int
n [Elim]
vs
        v :: Term
v@(Def QName
f [Elim]
vs) -> do
          QName -> TCMT IO (Maybe Projection)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe Projection)
isRelevantProjection QName
f TCMT IO (Maybe Projection)
-> (Maybe Projection -> TCMT IO Term) -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe Projection
Nothing -> Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
            Just Projection
pr -> Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
applyE (Projection -> ProjOrigin -> Term
projDropPars Projection
pr ProjOrigin
ProjSystem) [Elim]
vs
        Term
v -> Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v