module Agda.TypeChecking.Rules.LHS.Instantiate where
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views ( asView )
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S (Substitution)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.List
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "../../../undefined.h"
import Agda.Utils.Impossible
instantiateTel :: Substitution -> Telescope -> TCM (Telescope, Permutation, S.Substitution, [I.Dom Type])
instantiateTel s tel = liftTCM $ do
reportSDoc "tc.lhs.inst" 10 $ vcat
[ text "instantiateTel "
, nest 2 $ text "s =" <+> do
addCtxTel tel $
fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) s
, nest 2 $ text "tel =" <+> prettyTCM tel
]
let n = size s
deal (i, Nothing) = Left i
deal (i, Just _ ) = Right i
(is, isC) = mapEither deal $ zip [0..] $ reverse s
ps = Perm n is
psR = reverseP ps
psC = Perm n isC
reportSDoc "tc.lhs.inst" 10 $ vcat
[ nest 2 $ text $ "ps = " ++ show ps
, nest 2 $ text $ "psR = " ++ show psR
, nest 2 $ text $ "psC = " ++ show psC
]
let s' = renameP psR s
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
text "s' =" <+> fsep (punctuate comma $ map (maybe (text "_") prettyTCM) s')
let rho = mkSubst s'
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
text "rho = " <+> text (show rho)
let tel1 = flattenTel tel
names1 = teleNames tel
reportSDoc "tc.lhs.inst" 15 $ nest 2 $ vcat
[ text "tel1 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel1)
]
let tel2 = applySubst rho tel1
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
text "tel2 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel2)
tel3 <- instantiateFull $ permute ps tel2
let names3 = permute ps names1
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
text "tel3 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel3)
let failToReorder = inTopContext $ addContext names3 $ do
err <- sep [ text "Recursive telescope in left hand side:"
, fsep [ parens (text (argNameToString x) <+> text ":" <+> prettyTCM t)
| (x, t) <- zip names3 tel3 ]
]
typeError $ GenericError $ show err
tryNormalisedReorder = do
tel3 <- normalise tel3
reportSDoc "tc.lhs.inst" 30 $ text "failed to reorder unnormalised, trying again with" $$
nest 2 (text "norm =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel3))
p <- maybe failToReorder return . reorderTel =<< normalise tel3
return (p, tel3)
(p, tel3) <- maybe tryNormalisedReorder (\p -> return (p, tel3)) $ reorderTel tel3
reportSLn "tc.lhs.inst" 10 $ " p = " ++ show p
let rho' = renaming (reverseP p)
let tel4 = applySubst rho' (permute p tel3)
names4 = permute p names3
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
text "tel4 =" <+> brackets (fsep $ punctuate comma $ map prettyTCM tel4)
let tel5 = unflattenTel names4 tel4
reportSDoc "tc.lhs.inst" 15 $ nest 2 $
text "tel5 =" <+> prettyTCM tel5
let itypes = applySubst rho' $ permute psC tel2
return (tel5, composeP p ps, applySubst rho' rho, itypes)
where
mkSubst :: [Maybe Term] -> S.Substitution
mkSubst s = rho 0 s'
where s' = s
rho i (Nothing : s) = var i :# rho (i + 1) s
rho i (Just u : s) = u :# rho i s
rho i [] = raiseS i
nothingToSplitError :: Problem -> TCM a
nothingToSplitError (Problem ps _ tel pr) = splitError ps tel
where
splitError [] EmptyTel = do
if null $ restPats pr then __IMPOSSIBLE__ else do
typeError $ GenericError $ "Arguments left we cannot split on. TODO: better error message"
splitError (_:_) EmptyTel = __IMPOSSIBLE__
splitError [] ExtendTel{} = __IMPOSSIBLE__
splitError (p : ps) (ExtendTel a tel)
| isBad p = traceCall (CheckPattern (strip p) EmptyTel (unDom a)) $ case strip p of
A.DotP _ e -> typeError $ UninstantiatedDotPattern e
p -> typeError $ IlltypedPattern p (unDom a)
| otherwise = underAbstraction a tel $ \tel -> splitError ps tel
where
strip = snd . asView . namedArg
isBad p = case strip p of
A.DotP _ _ -> True
A.ConP _ _ _ -> True
A.LitP _ -> True
_ -> False