{-# LANGUAGE CPP #-}
module Agda.TypeChecking.ReconstructParameters where
import Data.Traversable
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.TypeChecking.Monad
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Pretty
import Agda.Utils.Size
import Agda.Utils.Impossible
#include "undefined.h"
reconstructParametersInType :: Type -> TCM Type
reconstructParametersInType a =
traverse (reconstructParameters (sort $ getSort a)) a
reconstructParametersInTel :: Telescope -> TCM Telescope
reconstructParametersInTel EmptyTel = return EmptyTel
reconstructParametersInTel (ExtendTel a tel) = do
ar <- reconstructParametersInType (unDom a)
addContext (absName tel, a) $
ExtendTel (ar <$ a) <$> traverse reconstructParametersInTel tel
reconstructParametersInEqView :: EqualityView -> TCM EqualityView
reconstructParametersInEqView (EqualityType s eq l a u v) =
EqualityType s eq l <$> traverse (reconstructParameters $ sort s) a
<*> traverse (reconstructParameters $ El s $ unArg a) u
<*> traverse (reconstructParameters $ El s $ unArg a) v
reconstructParametersInEqView (OtherType a) = OtherType <$> reconstructParametersInType a
reconstructParameters :: Type -> Term -> TCM Term
reconstructParameters a v = do
reportSDoc "tc.with.reconstruct" 30 $
sep [ text "reconstructing parameters in"
, nest 2 $ sep [ prettyTCM v <+> text ":", nest 2 $ prettyTCM a ] ]
v <- checkInternal' (defaultAction{ postAction = reconstruct }) v a
reportSDoc "tc.with.reconstruct" 30 $
nest 2 $ text "-->" <+> prettyTCM v
return v
where
reconstruct a v = do
case v of
Con h ci vs -> do
TelV tel a <- telView a
let under = size tel
reportSDoc "tc.with.reconstruct" 50 $
sep [ text "reconstructing"
, nest 2 $ sep [ prettyTCM v <+> text ":"
, nest 2 $ prettyTCM a ] ]
case (unEl a) of
Def d es -> do
Just n <- defParameters <$> getConstInfo d
let ps = applySubst (strengthenS __IMPOSSIBLE__ under) . take n $ es
reportSLn "tc.with.reconstruct" 50 $ show n ++ " parameters"
return $ Con h ci (ps ++ vs)
_ -> __IMPOSSIBLE__
_ -> return v
dropParameters :: TermLike a => a -> TCM a
dropParameters = traverseTermM dropPars
where
dropPars v =
case v of
Con c ci vs -> do
Constructor{ conData = d } <- theDef <$> getConstInfo (conName c)
Just n <- defParameters <$> getConstInfo d
return $ Con c ci $ drop n vs
_ -> return v