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.Concrete (FieldAssignment'(..), nameFieldA)
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.Telescope
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Lens
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 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 "tel =" <+> prettyTCM tel
]
splitP ps 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 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
]
lift $ SplitRest argd <$> dType `piApplyM` (vs ++ [self])
_ -> __IMPOSSIBLE__
splitRest _ = mzero
splitP :: [NamedArg A.Pattern]
-> Telescope
-> ListT TCM SplitProblem
splitP [] _ = splitRest pr
splitP (_:_) EmptyTel = __IMPOSSIBLE__
splitP _ (ExtendTel _ NoAbs{}) = __IMPOSSIBLE__
splitP ps0@(p : ps) 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 tel0
keepGoing = consSplitProblem p x dom <$> do
underAbstraction dom xtel $ \ tel -> splitP ps 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 qs a
, splitRPats = Abs x $ Problem ps () tel __IMPOSSIBLE__
}
`mplus` keepGoing
(xs, p@(A.RecP _patInfo fs)) -> do
res <- lift $ tryRecordType a
case res of
Left Nothing -> keepGoing
Left (Just a') -> keepGoing
Right (d, vs, def) -> do
let np = recPars def
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)
]
let c = killRange $ conName $ recConHead def
let
axs = recordFieldNames def
args <- lift $ insertMissingFields d (const $ A.WildP A.patNoRange) fs axs
(return Split
{ splitLPats = empty
, splitAsNames = xs
, splitFocus = Arg ai $ Focus c ConPRec args (getRange p) qs d pars ixs 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 (piApply 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) qs 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 ()