module Agda.TypeChecking.Rules.LHS.Split
( splitProblem
) where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad.Trans ( lift )
import Control.Monad.Trans.Maybe
import Data.Maybe (fromMaybe)
import Data.List hiding (null)
import Data.Traversable hiding (mapM, sequence)
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate (storeDisambiguatedName)
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView)
import qualified Agda.Syntax.Info as A
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.Functor ((<.>))
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Tuple
import qualified Agda.Utils.Pretty as P
#include "undefined.h"
import Agda.Utils.Impossible
splitProblem ::
Maybe QName
-> Problem
-> ListT TCM SplitProblem
splitProblem mf (Problem ps (perm, qs) tel pr) = do
lift $ do
reportSLn "tc.lhs.split" 20 $ "initiating splitting"
++ maybe "" ((" for definition " ++) . show) mf
reportSDoc "tc.lhs.split" 30 $ sep
[ nest 2 $ text "ps =" <+> sep (map (P.parens <.> prettyA) ps)
, nest 2 $ text "qs =" <+> sep (map (P.parens <.> prettyTCM . namedArg) qs)
, nest 2 $ text "perm =" <+> prettyTCM perm
, nest 2 $ text "tel =" <+> prettyTCM tel
]
splitP ps (permute perm $ zip [0..] $ allHoles qs) tel
where
splitRest :: ProblemRest -> ListT TCM SplitProblem
splitRest (ProblemRest (p : ps) b) | Just f <- mf = do
let failure = typeError $ CannotEliminateWithPattern p $ unArg b
notProjP = typeError $ NotAProjectionPattern p
notRecord = failure
wrongHiding :: MonadTCM tcm => QName -> tcm a
wrongHiding d = typeError . GenericDocError =<< do
liftTCM $ text "Wrong hiding used for projection " <+> prettyTCM d
lift $ reportSDoc "tc.lhs.split" 20 $ sep
[ text "splitting problem rest"
, nest 2 $ text "pattern p =" <+> prettyA p
, nest 2 $ text "eliminates type b =" <+> prettyTCM b
]
caseMaybe (isProjP p) failure $ \ d -> do
caseMaybeM (lift $ isProjection d) notProjP $ \ proj -> case proj of
Projection{projProper = Nothing} -> notProjP
Projection{projProper = Just d, projIndex = n, projArgInfo = ai} -> do
unless (n > 0) notProjP
unless (getHiding p == getHiding ai) $ wrongHiding d
lift $ reportSLn "tc.lhs.split" 90 "we are a projection pattern"
caseMaybeM (lift $ isRecordType $ unArg b) notRecord $ \(r, vs, def) -> case def of
Record{ recFields = fs } -> do
lift $ reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "we are of record type r = " ++ show r
, text "applied to parameters vs = " <+> prettyTCM vs
, text $ "and have fields fs = " ++ show fs
, text $ "original proj d = " ++ show d
]
argd <- maybe failure return $ find ((d ==) . unArg) fs
let es = patternsToElims perm qs
fvs <- lift $ freeVarsToApply f
let self = defaultArg $ Def f (map Apply fvs) `applyE` es
dType <- lift $ defType <$> getConstInfo d
lift $ reportSDoc "tc.lhs.split" 20 $ sep
[ text "we are self = " <+> prettyTCM (unArg self)
, text "being projected by dType = " <+> prettyTCM dType
]
return $ SplitRest argd $ dType `apply` (vs ++ [self])
_ -> __IMPOSSIBLE__
splitRest _ = mzero
splitP :: [A.NamedArg A.Pattern]
-> [(Int, OneHolePatterns)]
-> Telescope
-> ListT TCM SplitProblem
splitP _ [] (ExtendTel _ _) = __IMPOSSIBLE__
splitP _ (_:_) EmptyTel = __IMPOSSIBLE__
splitP [] _ _ = splitRest pr
splitP ps [] EmptyTel = __IMPOSSIBLE__
splitP _ _ (ExtendTel _ NoAbs{}) = __IMPOSSIBLE__
splitP ps0@(p : ps) qs0@((i, q) : qs) tel0@(ExtendTel dom@(Dom ai a) xtel@(Abs x tel)) = do
liftTCM $ reportSDoc "tc.lhs.split" 30 $ sep
[ text "splitP looking at pattern"
, nest 2 $ text "p =" <+> prettyA p
, nest 2 $ text "dom =" <+> prettyTCM dom
]
let
tryAgain = splitP ps0 qs0 tel0
keepGoing = consSplitProblem p x dom <$> do
underAbstraction dom xtel $ \ tel -> splitP ps qs tel
p <- lift $ expandLitPattern p
case asView $ namedArg p of
(_, A.DefP _ d ps) -> typeError $
if null ps
then CannotEliminateWithPattern p (telePi tel0 $ unArg $ restType pr)
else IllformedProjectionPattern $ namedArg p
(xs, p@(A.LitP lit)) -> do
when (unusableRelevance $ getRelevance ai) $
typeError $ SplitOnIrrelevant p dom
ifNotM (lift $ tryConversion $ equalType a =<< litType lit)
keepGoing $
return Split
{ splitLPats = empty
, splitAsNames = xs
, splitFocus = Arg ai $ LitFocus lit q i a
, splitRPats = Abs x $ Problem ps () tel __IMPOSSIBLE__
}
`mplus` keepGoing
(xs, p@(A.ConP ci (A.AmbQ cs) args)) -> do
let tryInstantiate a'
| [c] <- cs = do
ok <- lift $ do
Constructor{ conData = d } <- theDef <$> getConstInfo c
dt <- defType <$> getConstInfo d
vs <- newArgsMeta dt
Sort s <- ignoreSharing . unEl <$> reduce (apply dt vs)
tryConversion $ equalType a' (El s $ Def d $ map Apply vs)
if ok then tryAgain else keepGoing
| otherwise = keepGoing
ifBlockedType a (const tryInstantiate) $ \ a' -> do
case ignoreSharing $ unEl a' of
Def d es -> do
def <- liftTCM $ theDef <$> getConstInfo d
unless (defIsRecord def) $
when (unusableRelevance $ getRelevance ai) $
unlessM (liftTCM $ optExperimentalIrrelevance <$> pragmaOptions) $
typeError $ SplitOnIrrelevant p dom
let mp = case def of
Datatype{dataPars = np} -> Just np
Record{recPars = np} -> Just np
_ -> Nothing
case mp of
Nothing -> keepGoing
Just np -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
traceCall (CheckPattern p EmptyTel a) $ do
c <- lift $ do
cs' <- mapM canonicalName cs
d' <- canonicalName d
let cons def = case theDef def of
Datatype{dataCons = cs} -> cs
Record{recConHead = c} -> [conName c]
_ -> __IMPOSSIBLE__
cs0 <- cons <$> getConstInfo d'
case [ c | (c, c') <- zip cs cs', elem c' cs0 ] of
[c] -> do
when (length cs >= 2) $ storeDisambiguatedName c
return c
[] -> typeError $ ConstructorPatternInWrongDatatype (head cs) d
cs ->
typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d cs
let (pars, ixs) = genericSplitAt np vs
lift $ reportSDoc "tc.lhs.split" 10 $ vcat
[ sep [ text "splitting on"
, nest 2 $ fsep [ prettyA p, text ":", prettyTCM dom ]
]
, nest 2 $ text "pars =" <+> fsep (punctuate comma $ map prettyTCM pars)
, nest 2 $ text "ixs =" <+> fsep (punctuate comma $ map prettyTCM ixs)
]
checkParsIfUnambiguous cs d pars
(return Split
{ splitLPats = empty
, splitAsNames = xs
, splitFocus = Arg ai $ Focus c (A.patOrigin ci) args (getRange p) q i d pars ixs a
, splitRPats = Abs x $ Problem ps () tel __IMPOSSIBLE__
}) `mplus` keepGoing
_ -> keepGoing
_ -> keepGoing
checkParsIfUnambiguous :: MonadTCM tcm => [QName] -> QName -> Args -> tcm ()
checkParsIfUnambiguous [c] d pars = liftTCM $ do
dc <- getConstructorData c
a <- reduce (Def dc [])
case ignoreSharing a of
Def d0 es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
reportSDoc "tc.lhs.split" 40 $
vcat [ nest 2 $ text "d =" <+> prettyTCM d
, nest 2 $ text "d0 (should be == d) =" <+> prettyTCM d0
, nest 2 $ text "dc =" <+> prettyTCM dc
]
t <- typeOfConst d
compareArgs [] t (Def d []) vs (take (length vs) pars)
_ -> __IMPOSSIBLE__
checkParsIfUnambiguous _ _ _ = return ()