module Agda.TypeChecking.Rules.LHS.Split where
import Control.Applicative
import Control.Monad.Error
import Data.Maybe (fromMaybe)
import Data.Monoid (mempty, mappend)
import Data.List
import Data.Traversable hiding (mapM, sequence)
import Agda.Interaction.Options
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 hiding (SplitError)
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.Maybe
import Agda.Utils.Monad
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
-> TCM (Either SplitError SplitProblem)
splitProblem mf (Problem ps (perm, qs) tel pr) = 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
]
runErrorT $
splitP ps (permute perm $ zip [0..] $ allHoles qs) tel
where
splitRest :: ProblemRest -> ErrorT SplitError TCM SplitProblem
splitRest (ProblemRest (p : ps) b) | Just f <- mf = do
let failure = lift $ typeError $ CannotEliminateWithPattern p $ unArg b
notProjP = lift $ typeError $ NotAProjectionPattern p
notRecord = failure
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 $ \p -> case p of
Projection{projProper = Nothing} -> __IMPOSSIBLE__
Projection{projProper = Just d, projFromType = _, projIndex = n} -> do
unless (n > 0) notProjP
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 _ = throwError $ NothingToSplit
stripLambdas :: Term -> TCM Term
stripLambdas v = case ignoreSharing v of
Lam _ b -> addContext (absName b) $ stripLambdas (absBody b)
v -> return v
splitP :: [A.NamedArg A.Pattern] -> [(Int, OneHolePatterns)] -> Telescope -> ErrorT SplitError TCM SplitProblem
splitP _ [] (ExtendTel _ _) = __IMPOSSIBLE__
splitP _ (_:_) EmptyTel = __IMPOSSIBLE__
splitP [] _ _ = splitRest pr
splitP ps [] EmptyTel = __IMPOSSIBLE__
splitP (p : ps) ((i, q) : qs) tel0@(ExtendTel a tel) = do
liftTCM $ reportSDoc "tc.lhs.split" 30 $ sep
[ text "splitP looking at pattern"
, nest 2 $ text "p =" <+> prettyA p
, nest 2 $ text "a =" <+> prettyTCM a
]
let tryAgain = splitP (p : ps) ((i, q) : qs) tel0
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 a) $
typeError $ SplitOnIrrelevant p a
b <- lift $ litType lit
ok <- lift $ do
noConstraints (equalType (unDom a) b)
return True
`catchError` \_ -> return False
if ok
then return $
Split mempty
xs
(argFromDom $ fmap (LitFocus lit q i) a)
(fmap (\ tel -> Problem ps () tel __IMPOSSIBLE__) tel)
else 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)
(True <$ noConstraints (equalType a' (El s $ Def d $ map Apply vs)))
`catchError` \_ -> return False
if ok then tryAgain else keepGoing
| otherwise = keepGoing
ifBlockedType (unDom 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 a) $ do
allowed <- liftTCM $ optExperimentalIrrelevance <$> pragmaOptions
unless allowed $ typeError $ SplitOnIrrelevant p a
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
liftTCM $ traceCall (CheckPattern p EmptyTel (unDom a)) $ do
c <- 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] -> return c
[] -> typeError $ ConstructorPatternInWrongDatatype (head cs) d
cs ->
typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d cs
let (pars, ixs) = genericSplitAt np vs
reportSDoc "tc.lhs.split" 10 $
vcat [ sep [ text "splitting on"
, nest 2 $ fsep [ prettyA p, text ":", prettyTCM a ]
]
, 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 mempty
xs
(argFromDom $ fmap (Focus c (A.patImplicit ci) args (getRange p) q i d pars ixs) a)
(fmap (\ tel -> Problem ps () tel __IMPOSSIBLE__) tel)
_ -> keepGoing
p -> keepGoing
where
keepGoing = do
r <- underAbstraction a tel $ \tel -> splitP ps qs tel
case r of
SplitRest{} -> return r
Split p1 xs foc p2 -> do
let p0 = Problem [p] () (ExtendTel a (EmptyTel <$ tel)) mempty
return $ Split (mappend p0 p1) xs foc p2
checkParsIfUnambiguous :: [QName] -> QName -> Args -> TCM ()
checkParsIfUnambiguous [c] d pars = 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 ()
wellFormedIndices :: Type -> TCM ()
wellFormedIndices t = do
t <- reduce t
reportSDoc "tc.lhs.split.well-formed" 10 $
fsep [ text "Checking if indices are well-formed:"
, nest 2 $ prettyTCM t
]
(pars, ixs) <- normalise =<< case ignoreSharing $ unEl t of
Def d es -> do
let args = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
def <- getConstInfo d
typedArgs <- args `withTypesFrom` defType def
let (noPars, smallPars, nonLinPars) = case theDef def of
Datatype { dataPars = n, dataSmallPars = Perm _ sps, dataNonLinPars = nl }
-> (n, sps, permPicks $ doDrop nl)
Record { recPars = n } -> (n, [0..n1], [])
_ -> __IMPOSSIBLE__
(pars0, ixs0) = genericSplitAt noPars typedArgs
pars = map (pars0 !!) (smallPars \\ nonLinPars)
ixs = map (pars0 !!) nonLinPars ++ ixs0
return (map fst pars, ixs)
_ -> __IMPOSSIBLE__
mvs <- constructorApplications ixs
vs <- case mvs of
Nothing -> typeError $
IndicesNotConstructorApplications (map fst ixs)
Just vs -> return vs
unless (fastDistinct vs) $
typeError $ IndexVariablesNotDistinct vs (map fst ixs)
case map fst $ filter snd $ zip vs (map (`freeIn` pars) vs) of
[] -> return ()
vs ->
typeError $ IndicesFreeInParameters vs (map fst ixs) pars
where
constructorApplication :: Term
-> Type
-> TCM (Maybe [Nat])
constructorApplication (Var x []) _ = return (Just [x])
constructorApplication (Lit {}) _ = return (Just [])
constructorApplication (Shared p) t = constructorApplication (derefPtr p) t
constructorApplication (Con c conArgs) (El _ (Def d es)) = do
let dataArgs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
conDef <- getConInfo c
dataDef <- getConstInfo d
let (noPars, smallPars) = case theDef dataDef of
Datatype { dataPars = n, dataSmallPars = Perm _ is }
-> (n, is)
Record { recPars = n } -> (n, [0..n1])
_ -> __IMPOSSIBLE__
dataPars = take noPars dataArgs
allArgs <- (dataPars ++ conArgs) `withTypesFrom` defType conDef
let ixs = drop noPars allArgs
pars = map (allArgs !!) smallPars
reportSDoc "tc.lhs.split.well-formed" 20 $
fsep [ text "Reconstructed parameters:"
, nest 2 $
prettyTCM (Con c []) <+>
text "(:" <+> prettyTCM (defType conDef) <> text ")" <+>
text "<<" <+> prettyTCM (map fst pars) <+> text ">>" <+>
prettyTCM conArgs
]
constructorApplications $ pars ++ ixs
constructorApplication _ _ = return Nothing
constructorApplications :: [(I.Arg Term, I.Dom Type)] -> TCM (Maybe [Nat])
constructorApplications args = do
xs <- mapM (\(e, t) -> do
t <- reduce (unDom t)
constructorApplication (unArg e) (ignoreSharingType t))
args
return (concat <$> sequence xs)
withTypesFrom :: Args -> Type -> TCM [(I.Arg Term, I.Dom Type)]
[] `withTypesFrom` _ = return []
(arg : args) `withTypesFrom` t = do
t <- reduce t
case ignoreSharing $ unEl t of
Pi a b -> ((arg, a) :) <$>
args `withTypesFrom` absApp b (unArg arg)
_ -> __IMPOSSIBLE__