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 Data.Foldable (msum)
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(..), MaybePostfixProjP(..))
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.Except (catchError)
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
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
]
lift $ reportSDoc "tc.lhs.split" 80 $ sep
[ nest 2 $ text $ "pattern (raw) p = " ++ show p
]
caseMaybe (maybePostfixProjP p) failure $ \ (o, AmbQ ds) -> do
projs <- lift $ mapMaybeM (\ d -> fmap (d,) <$> isProjection d) ds
when (null projs) notProjP
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
]
let es = patternsToElims qs
let self = defaultArg $ Def f [] `applyE` es
ai = getArgInfo p
msum $ map (tryProj o ai self fs vs (length projs >= 2)) projs
_ -> __IMPOSSIBLE__
where
failure = lift $ typeError $ CannotEliminateWithPattern p $ unArg b
notProjP = lift $ 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
tryProj :: ProjOrigin -> ArgInfo -> Arg Term -> [Arg QName] -> Args -> Bool -> (QName, Projection) -> ListT TCM SplitProblem
tryProj o ai self fs vs amb (d0, proj) = do
let ambErr err = if amb then mzero else err
case proj of
Projection{projProper = False} -> ambErr notProjP
Projection{projProper = True, projOrig = d, projLams = lams} -> do
let ai = projArgInfo proj
when (null lams) $ ambErr notProjP
lift $ reportSLn "tc.lhs.split" 90 "we are a projection pattern"
lift $ reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "proj d0 = " ++ show d0
, text $ "original proj d = " ++ show d
]
argd <- maybe (ambErr failure) return $ find ((d ==) . unArg) fs
let ai' = setRelevance (getRelevance argd) ai
unless (getHiding p == getHiding ai) $ wrongHiding d
lift $ storeDisambiguatedName d0
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 (Arg ai' d0) o <$> dType `piApplyM` (vs ++ [self])
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
]
unless (getHiding p == getHiding ai) $ typeError WrongHidingInLHS
let
tryAgain = splitP ps0 tel0
keepGoing = consSplitProblem p x dom <$> do
underAbstraction dom xtel $ \ tel -> splitP ps tel
p <- lift $ expandLitPattern p
case snd $ asView $ namedArg p of
A.ProjP{} -> typeError $
CannotEliminateWithPattern p (telePi tel0 $ unArg $ restType pr)
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
, splitFocus = Arg ai $ LitFocus lit qs a
, splitRPats = Abs x $ Problem ps () tel __IMPOSSIBLE__
}
`mplus` keepGoing
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
, splitFocus = Arg ai $ Focus c ConORec args (getRange p) qs d pars ixs a
, splitRPats = Abs x $ Problem ps () tel __IMPOSSIBLE__
}) `mplus` keepGoing
p@(A.ConP ci (A.AmbQ cs) args) -> do
let tryInstantiate a'
| [c] <- cs = do
lift $ reportSDoc "tc.lhs.split" 30 $
text "split ConP: type is blocked"
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 = do
lift $ reportSDoc "tc.lhs.split" 30 $
text "split ConP: type is blocked and constructor is ambiguous"
keepGoing
ifBlockedType a (const tryInstantiate) $ \ a' -> do
lift $ reportSDoc "tc.lhs.split" 30 $ text "split ConP: type is " <+> prettyTCM a'
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
, 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 ()