{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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 Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic

import Agda.TypeChecking.Monad
import Agda.TypeChecking.CheckInternal
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.Either
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Size

import Agda.Utils.Impossible

reconstructParametersInType :: Type -> TCM Type
reconstructParametersInType :: Type'' Term Term -> TCM (Type'' Term Term)
reconstructParametersInType = Action -> Type'' Term Term -> TCM (Type'' Term Term)
reconstructParametersInType' Action
defaultAction

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

reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel :: Tele (Dom (Type'' Term Term))
-> TCM (Tele (Dom (Type'' Term Term)))
reconstructParametersInTel Tele (Dom (Type'' Term Term))
EmptyTel = Tele (Dom (Type'' Term Term))
-> TCM (Tele (Dom (Type'' Term Term)))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom (Type'' Term Term))
forall a. Tele a
EmptyTel
reconstructParametersInTel (ExtendTel Dom (Type'' Term Term)
a Abs (Tele (Dom (Type'' Term Term)))
tel) = do
  ar <- Type'' Term Term -> TCM (Type'' Term Term)
reconstructParametersInType (Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom (Type'' Term Term)
a)
  addContext (absName tel, a) $
    ExtendTel (ar <$ a) <$> traverse reconstructParametersInTel tel

reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView (EqualityType Range
r Sort
s QName
eq [Arg Term]
l Arg Term
a Arg Term
u Arg Term
v) =
  Range
-> Sort
-> QName
-> [Arg Term]
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Range
r 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (Type'' Term Term -> Term -> TCMT IO Term
reconstructParameters (Type'' Term Term -> Term -> TCMT IO Term)
-> Type'' Term Term -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Type'' Term Term
sort Sort
s) Arg Term
a
                      TCMT IO (Arg Term -> Arg Term -> EqualityView)
-> TCMT IO (Arg Term) -> TCMT IO (Arg Term -> EqualityView)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (Type'' Term Term -> Term -> TCMT IO Term
reconstructParameters (Type'' Term Term -> Term -> TCMT IO Term)
-> Type'' Term Term -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type'' Term Term) -> Term -> Type'' Term Term
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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse (Type'' Term Term -> Term -> TCMT IO Term
reconstructParameters (Type'' Term Term -> Term -> TCMT IO Term)
-> Type'' Term Term -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type'' Term Term) -> Term -> Type'' Term Term
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'' Term Term
a) = Type'' Term Term -> EqualityView
OtherType (Type'' Term Term -> EqualityView)
-> TCM (Type'' Term Term) -> TCM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> TCM (Type'' Term Term)
reconstructParametersInType Type'' Term Term
a
reconstructParametersInEqView (IdiomType Type'' Term Term
a) = Type'' Term Term -> EqualityView
IdiomType (Type'' Term Term -> EqualityView)
-> TCM (Type'' Term Term) -> TCM EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> TCM (Type'' Term Term)
reconstructParametersInType Type'' Term Term
a

reconstructParameters :: Type -> Term -> TCM Term
reconstructParameters :: Type'' Term Term -> Term -> TCMT IO Term
reconstructParameters = Action -> Type'' Term Term -> Term -> TCMT IO Term
reconstructParameters' Action
defaultAction

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

  reportSDoc "tc.reconstruct" 30 $
    nest 2 $ "-->" <+> prettyTCM v
  return v

reconstructAction :: Action
reconstructAction :: Action
reconstructAction = Action -> Action
reconstructAction' Action
defaultAction

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

reconstruct :: Type -> Term -> TCM Term
reconstruct :: Type'' Term Term -> Term -> TCMT IO Term
reconstruct Type'' Term Term
ty Term
v = do
    [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"reconstructing in"
      , VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":", VerboseLevel -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
ty ] ]
    case Term
v of
      Con ConHead
h ConInfo
ci [Elim]
vs -> do
        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)
-> TCMT IO (Either SigError ConHead) -> TCMT IO ConHead
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Either SigError ConHead)
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Either SigError ConHead)
getConHead (ConHead -> QName
conName ConHead
h)
        TelV tel dataTy <- telView ty
        reportSDoc "tc.reconstruct" 50 $
          sep [ "reconstructing"
              , nest 2 $ sep [ prettyTCM v <+> ":"
                             , nest 2 $ prettyTCM dataTy ] ]
        pars <- addContext tel $ extractParameters (conName h) dataTy
        -- If the constructor is underapplied, we need to escape from the telescope.
        let escape = Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term])
-> Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Impossible -> VerboseLevel -> Substitution' (SubstArg [Arg Term])
forall a. Impossible -> VerboseLevel -> Substitution' a
strengthenS Impossible
forall a. HasCallStack => a
__IMPOSSIBLE__ (VerboseLevel -> Substitution' (SubstArg [Arg Term]))
-> VerboseLevel -> Substitution' (SubstArg [Arg Term])
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Tele (Dom (Type'' Term Term))
tel
        return $ Con hh ci $ map Apply (escape pars) ++ vs
      Def QName
f [Elim]
es -> Term -> TCMT IO ProjectionView
forall (m :: * -> *). HasConstInfo m => Term -> m ProjectionView
projView Term
v TCMT IO ProjectionView
-> (ProjectionView -> TCMT IO Term) -> TCMT IO Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        ProjectionView QName
_f Arg Term
a [Elim]
es -> do
          recTy <- Term -> TCM (Type'' Term Term)
infer (Term -> TCM (Type'' Term Term))
-> TCMT IO Term -> TCM (Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a. TermLike a => a -> TCM a
dropParameters (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
          pars <- extractParameters f recTy
          loop ty (Def f . (map Apply pars ++) . (Apply a:)) es
        LoneProjectionLike QName
_f ArgInfo
i -> Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
ty) TCMT IO Term -> (Term -> TCMT IO Term) -> TCMT IO Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Pi Dom (Type'' Term Term)
recTy Abs (Type'' Term Term)
_ -> do
            pars <- QName -> Type'' Term Term -> TCMT IO [Arg Term]
extractParameters QName
f (Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom (Type'' Term Term)
recTy)
            return $ Def f $ map Apply pars
          Term
_ -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
        NoProjection{} -> do
          ty <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
          loop ty (Def f) es
      Var VerboseLevel
i [Elim]
es -> do
        ty <- VerboseLevel -> TCM (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
VerboseLevel -> m (Type'' Term Term)
typeOfBV VerboseLevel
i
        loop ty (Var i) es
      MetaV MetaId
m [Elim]
es -> do
        ty <- MetaId -> TCM (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
getMetaType MetaId
m
        loop ty (MetaV m) es
      Term
_ -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
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'' Term Term -> ([Elim] -> Term) -> [Elim] -> TCMT IO Term
loop Type'' Term Term
ty [Elim] -> Term
f []           = do
      [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Loop ended" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Elim] -> Term
f [])
      Term -> TCMT IO Term
forall a. a -> TCMT IO a
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
f []
    loop Type'' Term Term
ty [Elim] -> Term
f (Apply Arg Term
u:[Elim]
es) = do
      [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The type before app is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type'' Term Term
ty
      [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The term before app is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM ([Elim] -> Term
f [])
      uu <- Arg Term -> TCMT IO (Arg Term)
forall a. TermLike a => a -> TCM a
dropParameters Arg Term
u
      reportSDoc "tc.reconstruct" 50 $ "The app is:" <+> pretty uu
      ty' <- piApplyM ty uu
      reportSDoc "tc.reconstruct" 50 $ "The type after app is:" <+> pretty ty'
      loop ty' (f . (Apply u :)) es
    loop Type'' Term Term
ty [Elim] -> Term
f (Proj ProjOrigin
o QName
p:[Elim]
es) = do
      [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The type is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type'' Term Term
ty
      [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The term is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([Elim] -> Term
f [])
      [Char] -> VerboseLevel -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" VerboseLevel
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"The proj is:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
p
      pars <- QName -> Type'' Term Term -> TCMT IO [Arg Term]
extractParameters QName
p Type'' Term Term
ty
      ~(Just (El _ (Pi _ b))) <- getDefType p =<< reduce ty
      let fTm = [Elim] -> Term
f []
      fe <- dropParameters fTm
      loop (absApp b fe) (Def p . (map Apply pars ++) . (Apply (defaultArg fTm) :)) es
    loop Type'' Term Term
ty [Elim] -> Term
_ (IApply {}:[Elim]
vs) = TCMT IO Term
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'' Term Term -> TCMT IO [Arg Term]
extractParameters QName
q Type'' Term Term
ty = Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
ty) TCMT IO Term -> (Term -> TCMT IO [Arg Term]) -> TCMT IO [Arg Term]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
d [Elim]
prePs -> do
    dt <- Definition -> Type'' Term Term
defType (Definition -> Type'' Term Term)
-> TCMT IO Definition -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
    reportSDoc "tc.reconstruct" 50 $ "Start traversing parameters: " <+> pretty prePs
    postPs <- checkInternal' reconstructAction prePs CmpEq (dt , Def d)
    reportSDoc "tc.reconstruct" 50 $ "Traversed parameters:" <+> pretty postPs
    info <- getConstInfo q
    let mkParam b
erasure =
            b -> (Arg a -> Arg a) -> Arg a -> Arg a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen b
erasure (Quantity -> Arg a -> Arg a
forall a. LensQuantity a => Quantity -> a -> a
applyQuantity Quantity
zeroQuantity)
          (Arg a -> Arg a) -> (Elim' a -> Arg a) -> Elim' a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> Arg a
forall a. (LensHiding a, LensRelevance a) => a -> a
hideAndRelParams
          (Arg a -> Arg a) -> (Elim' a -> Arg a) -> Elim' a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Empty -> Elim' a -> Arg a
forall a. Empty -> Elim' a -> Arg a
isApplyElim' Empty
forall a. HasCallStack => a
__IMPOSSIBLE__
    if -- Case: data or record constructor
       | Constructor{ conPars = n, conErasure = e } <- theDef info ->
           return $ map (mkParam e) $ take n postPs
       -- Case: regular projection
       | isProperProjection (theDef info) ->
         case theDef info of
           d :: Defn
d@Function{} ->
             [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term] -> TCMT IO [Arg Term])
-> [Arg Term] -> TCMT IO [Arg Term]
forall a b. (a -> b) -> a -> b
$ (Elim -> Arg Term) -> [Elim] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Elim -> Arg Term
forall {b} {a}. IsBool b => b -> Elim' a -> Arg a
mkParam (Defn
d Defn -> Getting Bool Defn Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Defn Bool
Lens' Defn Bool
funErasure)) [Elim]
postPs
           Defn
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
       -- Case: projection-like function
       | otherwise -> do
           TelV tel _ <- telViewUpTo (size postPs) $ defType info
           return $ zipWith ($>) (teleArgs tel :: Args) $ map (unArg . isApplyElim' __IMPOSSIBLE__) postPs
  Term
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__

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
forall (m :: * -> *). 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 = d } <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
          Just n <- defParameters <$> getConstInfo d
          return $ Con c ci $ drop n 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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Maybe Projection
Nothing -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
            Just Projection
pr -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v