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.Either
import Data.Maybe (fromMaybe)
import qualified Data.List as List
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.Errors (dropTopLevelModule)
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.Either
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.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Tuple
#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 " ++) . prettyShow) 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
]
reportSDoc "tc.lhs.split" 60 $ sep
[ nest 2 $ text "ps (raw) =" <+> sep (map (P.parens <.> text . show) ps)
, nest 2 $ text "qs (raw) =" <+> sep (map (P.parens <.> text . show . namedArg) qs)
, nest 2 $ text "tel (raw) =" <+> (text . show) 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 = " ++ prettyShow r
, text "applied to parameters vs = " <+> prettyTCM vs
, text $ "and have fields fs = " ++ prettyShow fs
]
let es = patternsToElims qs
let self = defaultArg $ Def f [] `applyE` es
ai = getArgInfo p
msum $ mapAwareLast (tryProj o ai self fs r vs $ length ds >= 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
wrongProj :: MonadTCM tcm => QName -> Bool -> tcm a
wrongProj d amb = typeError . GenericDocError =<< do
liftTCM $ sep
[ text "Cannot eliminate type "
, prettyTCM (unArg b)
, text " with projection "
, if amb then text . prettyShow =<< dropTopLevelModule d else prettyTCM d
]
mapAwareLast :: forall a b. (Bool -> a -> b) -> [a] -> [b]
mapAwareLast f [] = []
mapAwareLast f [a] = [f False a]
mapAwareLast f (a:as) = f True a : mapAwareLast f as
tryProj
:: ProjOrigin
-> ArgInfo
-> Arg Term
-> [Arg QName]
-> QName
-> Args
-> Bool
-> Bool
-> (QName, Projection)
-> ListT TCM SplitProblem
tryProj o ai self fs r vs amb soft (d0, proj) = do
let ambErr err = if soft then mzero else err
ambTry m
| soft = unlessM (liftTCM $ tryConversion m) mzero
| otherwise = liftTCM $ noConstraints m
case proj of
Projection{projProper = Nothing} -> ambErr notProjP
Projection{projProper = Just qr, 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 = " ++ prettyShow d0
, text $ "original proj d = " ++ prettyShow d
]
argd <- maybe (ambErr $ wrongProj d amb) return $ List.find ((d ==) . unArg) fs
let ai' = setRelevance (getRelevance argd) ai
unless (sameHiding p ai) $ ambErr $ wrongHiding d
ambTry $ checkParameters qr r vs
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 (sameHiding p 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) = splitAt 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.AbsurdP info) -> do
lift $ reportSDoc "tc.lhs.split.absurd" 30 $ text "split AbsurdP: type is " <+> prettyTCM a
let i = size tel
(return Split
{ splitLPats = empty
, splitFocus = Arg ai $ AbsurdFocus info i $ raise (i+1) 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
lift $ reportSLn "tc.lhs.split" 30 $ "split ConP: relevance is " ++ show ai
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
(cs1, cs') <- unzip . snd . partitionEithers <$> do
forM cs $ \ c -> mapRight ((c,) . conName) <$> getConHead c
when (null cs1) $ typeError $ AbstractConstructorNotInScope $ head cs
d' <- canonicalName d
cs0 <- (theDef <$> getConstInfo d') <&> \case
Datatype{dataCons = cs0} -> cs0
Record{recConHead = c0} -> [conName c0]
_ -> __IMPOSSIBLE__
case [ c | (c, c') <- zip cs1 cs', elem c' cs0 ] of
[c] -> do
when (length cs >= 2) $ storeDisambiguatedName c
return c
[] -> typeError $ ConstructorPatternInWrongDatatype (head cs1) d
cs3 ->
typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d cs3
let (pars, ixs) = splitAt 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)
]
checkConstructorParameters c 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
checkConstructorParameters :: MonadTCM tcm => QName -> QName -> Args -> tcm ()
checkConstructorParameters c d pars = do
dc <- liftTCM $ getConstructorData c
checkParameters dc d pars
checkParameters
:: MonadTCM tcm
=> QName
-> QName
-> Args
-> tcm ()
checkParameters dc d pars = liftTCM $ do
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 =" <+> (text . prettyShow) d
, nest 2 $ text "d0 (should be == d) =" <+> (text . prettyShow) d0
, nest 2 $ text "dc =" <+> (text . prettyShow) dc
, nest 2 $ text "vs =" <+> prettyTCM vs
]
t <- typeOfConst d
compareArgs [] t (Def d []) vs (take (length vs) pars)
_ -> __IMPOSSIBLE__