{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Coverage
( SplitClause(..), clauseToSplitClause, fixTarget
, Covering(..), splitClauses
, coverageCheck
, isCovered
, splitClauseWithAbsurd
, splitLast
, splitResult
, normaliseProjP
) where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.Trans ( lift )
import Data.Either (lefts)
import qualified Data.List as List
import Data.Monoid (Any(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Traversable as Trav
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (litType)
import Agda.TypeChecking.Rules.LHS (checkSortOfSplitVar)
import Agda.TypeChecking.Rules.LHS.Problem (allFlexVars)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Coverage.Match
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Conversion (tryConversion, equalType)
import Agda.TypeChecking.Datatypes (getConForm)
import Agda.TypeChecking.Patterns.Internal (dotPatternsToPatterns)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Warnings
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Except
( ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Suffix (nameVariant)
import Agda.Utils.Tuple
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
data SplitClause = SClause
{ scTel :: Telescope
, scPats :: [NamedArg SplitPattern]
, scSubst :: Substitution' SplitPattern
, scCheckpoints :: Map CheckpointId Substitution
, scTarget :: Maybe (Arg Type)
}
data Covering = Covering
{ covSplitArg :: Arg Nat
, covSplitClauses :: [(SplitTag, SplitClause)]
}
splitClauses :: Covering -> [SplitClause]
splitClauses (Covering _ qcs) = map snd qcs
clauseToSplitClause :: Clause -> SplitClause
clauseToSplitClause cl = SClause
{ scTel = clauseTel cl
, scPats = toSplitPatterns $ namedClausePats cl
, scSubst = idS
, scCheckpoints = Map.empty
, scTarget = clauseType cl
}
type CoverM = ExceptT SplitError TCM
coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
coverageCheck f t cs = do
TelV gamma a <- telView t
let
n = size gamma
xs = map (setOrigin Inserted) $ teleNamedArgs gamma
fv <- getDefFreeVars f
checkpoints <- applySubst (raiseS (n - fv)) <$> view eCheckpoints
let sc = SClause gamma xs idS checkpoints $ Just $ defaultArg a
reportSDoc "tc.cover.top" 10 $ do
let prCl cl = addContext (clauseTel cl) $
prettyTCMPatternList $ namedClausePats cl
vcat
[ text $ "Coverage checking " ++ prettyShow f ++ " with patterns:"
, nest 2 $ vcat $ map prCl cs
]
CoverResult splitTree used pss noex <- cover f cs sc
reportSDoc "tc.cover.top" 10 $ vcat
[ text "cover computed!"
, text $ "used clauses: " ++ show used
, text $ "non-exact clauses: " ++ show noex
]
reportSDoc "tc.cover.splittree" 10 $ vcat
[ text "generated split tree for" <+> prettyTCM f
, text $ prettyShow splitTree
]
unless (null pss) $
setCurrentRange cs $
warning $ CoverageIssue f pss
let (is0, cs1) = unzip $ for (zip [0..] cs) $ \ (i, cl) ->
let unreachable = i `Set.notMember` used in
(boolToMaybe unreachable i, cl { clauseUnreachable = Just unreachable })
let is = catMaybes is0
reportSDoc "tc.cover.top" 10 $ vcat
[ text $ "unreachable clauses: " ++ if null is then "(none)" else show is
]
modifyFunClauses f $ \ cs0 -> cs1 ++ drop (length cs1) cs0
unless (null is) $ do
let unreached = filter ((Just True ==) . clauseUnreachable) cs1
setCurrentRange (map clauseFullRange unreached) $
warning $ UnreachableClauses f $ map namedClausePats unreached
unless (null noex) $ do
let noexclauses = map (cs1 !!) $ Set.toList noex
setCurrentRange (map clauseLHSRange noexclauses) $
warning $ CoverageNoExactSplit f $ noexclauses
return splitTree
isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool
isCovered f cs sc = do
CoverResult { coverMissingClauses = missing } <- cover f cs sc
return $ null missing
data CoverResult = CoverResult
{ coverSplitTree :: SplitTree
, coverUsedClauses :: Set Nat
, coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
, coverNoExactClauses :: Set Nat
}
cover :: QName -> [Clause] -> SplitClause ->
TCM CoverResult
cover f cs sc@(SClause tel ps _ _ target) = do
reportSDoc "tc.cover.cover" 10 $ inTopContext $ vcat
[ text "checking coverage of pattern:"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "ps =" <+> do addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
]
reportSDoc "tc.cover.cover" 60 $ vcat
[ nest 2 $ text "ps =" <+> pretty ps
]
cs' <- normaliseProjP cs
ps <- (traverse . traverse . traverse) dotPatternsToPatterns ps
case match cs' ps of
Yes (i,mps) -> do
exact <- allM mps isTrivialPattern
let noExactClause = if exact || clauseCatchall (cs !! i)
then Set.empty
else Set.singleton i
reportSLn "tc.cover.cover" 10 $ "pattern covered by clause " ++ show i
return $ CoverResult (SplittingDone (size tel)) (Set.singleton i) [] noExactClause
No -> do
reportSLn "tc.cover" 20 $ "pattern is not covered"
case fmap getHiding target of
Just h | isInstance h -> do
inferMissingClause f sc
return $ CoverResult (SplittingDone (size tel)) Set.empty [] Set.empty
_ -> do
let ps' = fromSplitPatterns ps
return $ CoverResult (SplittingDone (size tel)) Set.empty [(tel, ps')] Set.empty
Block res bs -> tryIf res splitRes $ do
let ps' = fromSplitPatterns ps
done = return $ CoverResult (SplittingDone (size tel)) Set.empty [(tel, ps')] Set.empty
if null bs then done else do
reportSLn "tc.cover.strategy" 20 $ "blocking vars = " ++ prettyShow bs
xs <- splitStrategy bs tel
continue xs NoAllowPartialCover $ \ _err -> do
continue xs YesAllowPartialCover $ \ err -> do
typeError $ SplitError err
where
continue
:: [BlockingVar]
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue xs allowPartialCover handle = do
r <- altM1 (split Inductive allowPartialCover sc) xs
case r of
Left err -> handle err
Right (Covering n []) ->
return $ CoverResult (SplittingDone (size tel)) Set.empty [] Set.empty
Right (Covering n scs) -> do
results <- mapM (cover f cs) (map snd scs)
let trees = map coverSplitTree results
useds = map coverUsedClauses results
psss = map coverMissingClauses results
noex = map coverNoExactClauses results
reportSDoc "tc.cover.split.eta" 60 $ vcat
[ text "etaRecordSplits"
, nest 2 $ vcat
[ text "n = " <+> text (show n)
, text "scs = " <+> prettyTCM scs
, text "ps = " <+> text (show ps)
]
]
let trees' = zipWith (etaRecordSplits (unArg n) ps) scs trees
tree = SplitAt n trees'
return $ CoverResult tree (Set.unions useds) (concat psss) (Set.unions noex)
tryIf :: Monad m => Bool -> m (Either err a) -> m a -> m a
tryIf True me m = fromRightM (const m) me
tryIf False me m = m
splitRes :: TCM (Either CosplitError CoverResult)
splitRes = do
reportSLn "tc.cover" 20 $ "blocked by projection pattern"
mcov <- splitResult f sc
Trav.forM mcov $ \ (Covering n scs) -> do
(projs, results) <- unzip <$> do
mapM (traverseF $ cover f cs <=< (snd <.> fixTarget)) scs
let trees = map coverSplitTree results
useds = map coverUsedClauses results
psss = map coverMissingClauses results
noex = map coverNoExactClauses results
tree = SplitAt n $ zip projs trees
return $ CoverResult tree (Set.unions useds) (concat psss) (Set.unions noex)
gatherEtaSplits :: Int -> SplitClause
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
gatherEtaSplits n sc []
| n >= 0 = __IMPOSSIBLE__
| otherwise = []
gatherEtaSplits n sc (p:ps) = case namedArg p of
VarP _ x
| n == 0 -> case p' of
VarP _ _ -> p : gatherEtaSplits (-1) sc ps
DotP _ _ -> __IMPOSSIBLE__
ConP _ _ qs -> qs ++ gatherEtaSplits (-1) sc ps
LitP _ -> gatherEtaSplits (-1) sc ps
ProjP{} -> __IMPOSSIBLE__
| otherwise ->
updateNamedArg (\ _ -> p') p : gatherEtaSplits (n-1) sc ps
where p' = lookupS (scSubst sc) $ splitPatVarIndex x
DotP _ _ -> p : gatherEtaSplits (n-1) sc ps
ConP _ _ qs -> gatherEtaSplits n sc (qs ++ ps)
LitP _ -> gatherEtaSplits n sc ps
ProjP{} -> gatherEtaSplits n sc ps
addEtaSplits :: Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits k [] t = t
addEtaSplits k (p:ps) t = case namedArg p of
VarP _ _ -> addEtaSplits (k+1) ps t
DotP _ _ -> addEtaSplits (k+1) ps t
ConP c cpi qs -> SplitAt (p $> k) [(SplitCon (conName c) , addEtaSplits k (qs ++ ps) t)]
LitP _ -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
etaRecordSplits :: Int -> [NamedArg SplitPattern] -> (SplitTag,SplitClause)
-> SplitTree -> (SplitTag,SplitTree)
etaRecordSplits n ps (q , sc) t =
(q , addEtaSplits 0 (gatherEtaSplits n sc ps) t)
inferMissingClause
:: QName
-> SplitClause
-> TCM ()
inferMissingClause f (SClause tel ps _ cps (Just t)) = setCurrentRange f $ do
reportSDoc "tc.cover.infer" 20 $ addContext tel $ text "Trying to infer right-hand side of type" <+> prettyTCM t
cl <- addContext tel
$ locally eCheckpoints (const cps)
$ checkpoint IdS $ do
(_x, rhs) <- case getHiding t of
Instance{} -> newIFSMeta "" (unArg t)
Hidden -> __IMPOSSIBLE__
NotHidden -> __IMPOSSIBLE__
return $ Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = fromSplitPatterns ps
, clauseBody = Just rhs
, clauseType = Just t
, clauseCatchall = False
, clauseUnreachable = Just False
}
addClauses f [cl]
inferMissingClause _ (SClause _ _ _ _ Nothing) = __IMPOSSIBLE__
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy bs tel = return $ updateLast setBlockingVarOverlap xs
where
xs = bs
isDatatype :: (MonadTCM tcm, MonadError SplitError tcm) =>
Induction -> Dom Type ->
tcm (QName, [Arg Term], [Arg Term], [QName])
isDatatype ind at = do
let t = unDom at
throw f = throwError . f =<< do liftTCM $ buildClosure t
t' <- liftTCM $ reduce t
case unEl t' of
Def d es -> do
let ~(Just args) = allApplyElims es
def <- liftTCM $ theDef <$> getConstInfo d
splitOnIrrelevantDataAllowed <- liftTCM $ optExperimentalIrrelevance <$> pragmaOptions
case def of
Datatype{dataPars = np, dataCons = cs, dataInduction = i}
| i == CoInductive && ind /= CoInductive ->
throw CoinductiveDatatype
| isIrrelevant at && not splitOnIrrelevantDataAllowed ->
throw IrrelevantDatatype
| otherwise -> do
let (ps, is) = splitAt np args
return (d, ps, is, cs)
Record{recPars = np, recConHead = con, recInduction = i}
| i == Just CoInductive && ind /= CoInductive ->
throw CoinductiveDatatype
| otherwise ->
return (d, args, [], [conName con])
_ -> throw NotADatatype
_ -> throw NotADatatype
fixTarget :: SplitClause -> TCM (Telescope, SplitClause)
fixTarget sc@SClause{ scTel = sctel, scPats = ps, scSubst = sigma, scCheckpoints = cps, scTarget = target } =
caseMaybe target (return (empty, sc)) $ \ a -> do
reportSDoc "tc.cover.target" 20 $ sep
[ text "split clause telescope: " <+> prettyTCM sctel
, text "old patterns : " <+> do
addContext sctel $ prettyTCMPatternList $ fromSplitPatterns ps
]
reportSDoc "tc.cover.target" 60 $ sep
[ text "substitution : " <+> text (show sigma)
]
reportSDoc "tc.cover.target" 30 $ sep
[ text "target type before substitution (variables may be wrong): " <+> do
addContext sctel $ prettyTCM a
]
TelV tel b <- telView $ applySplitPSubst sigma $ unArg a
reportSDoc "tc.cover.target" 15 $ sep
[ text "target type telescope (after substitution): " <+> do
addContext sctel $ prettyTCM tel
, text "target type core (after substitution): " <+> do
addContext sctel $ addContext tel $ prettyTCM b
]
let n = size tel
xs = map (mapArgInfo hiddenInserted) $ teleNamedArgs tel
sctel' = telFromList $ telToList (raise n sctel) ++ telToList tel
ps' = applySubst (raiseS n) ps ++ xs
newTarget = Just $ a $> b
sc' = SClause
{ scTel = sctel'
, scPats = ps'
, scSubst = wkS n $ sigma
, scCheckpoints = applySubst (raiseS n) cps
, scTarget = newTarget
}
reportSDoc "tc.cover.target" 30 $ sep
[ text "new split clause telescope : " <+> prettyTCM sctel'
]
reportSDoc "tc.cover.target" 30 $ sep
[ text "new split clause patterns : " <+> do
addContext sctel' $ prettyTCMPatternList $ fromSplitPatterns ps'
]
reportSDoc "tc.cover.target" 60 $ sep
[ text "new split clause substitution: " <+> text (show $ scSubst sc')
]
reportSDoc "tc.cover.target" 30 $ sep
[ text "new split clause target : " <+> do
addContext sctel' $ prettyTCM $ fromJust newTarget
]
reportSDoc "tc.cover.target" 20 $ sep
[ text "new split clause"
, prettyTCM sc'
]
return $ if n == 0 then (empty, sc { scTarget = newTarget }) else (tel, sc')
hiddenInserted :: ArgInfo -> ArgInfo
hiddenInserted ai
| visible ai = setOrigin UserWritten ai
| otherwise = setOrigin Inserted ai
computeNeighbourhood
:: Telescope
-> PatVarName
-> Telescope
-> QName
-> Args
-> Args
-> Nat
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId Substitution
-> QName
-> CoverM (Maybe SplitClause)
computeNeighbourhood delta1 n delta2 d pars ixs hix tel ps cps c = do
dtype <- liftTCM $ (`piApply` pars) . defType <$> getConstInfo d
con <- liftTCM $ fromRight __IMPOSSIBLE__ <$> getConForm c
con <- return $ con { conName = c }
ctype <- liftTCM $ defType <$> getConInfo con
(gamma0, cixs) <- do
TelV gamma0 (El _ d) <- liftTCM $ telView (ctype `piApply` pars)
let Def _ es = d
Just cixs = allApplyElims es
return (gamma0, cixs)
let preserve (x, t@(El _ (Def d' _))) | d == d' = (n, t)
preserve (x, t) = (x, t)
gammal = map (fmap preserve) . telToList $ gamma0
gamma = telFromList gammal
delta1Gamma = delta1 `abstract` gamma
debugInit con ctype d pars ixs cixs delta1 delta2 gamma tel ps hix
let flex = allFlexVars delta1Gamma
let conIxs = drop (size pars) cixs
givenIxs = raise (size gamma) ixs
r <- unifyIndices
delta1Gamma
flex
(raise (size gamma) dtype)
conIxs
givenIxs
case r of
NoUnify {} -> debugNoUnify $> Nothing
DontKnow errs -> do
debugCantSplit
throwError $ UnificationStuck (conName con) (delta1 `abstract` gamma) conIxs givenIxs errs
Unifies (delta1',rho0,_) -> do
debugSubst "rho0" rho0
let (rho1,rho2) = splitS (size gamma) $ toSplitPSubst rho0
let cpi = noConPatternInfo{ conPRecord = Just PatOSplit }
conp = ConP con cpi $ applySubst rho2 $
map (mapArgInfo hiddenInserted) $ tele2NamedArgs gamma0 gamma
let rho3 = consS conp rho1
delta2' = applySplitPSubst rho3 delta2
delta' = delta1' `abstract` delta2'
rho = liftS (size delta2) rho3
debugTel "delta'" delta'
debugSubst "rho" rho
debugPs tel ps
let ps' = applySubst rho ps
debugPlugged delta' ps'
let cps' = applySplitPSubst rho cps
return $ Just $ SClause delta' ps' rho cps' Nothing
where
debugInit con ctype d pars ixs cixs delta1 delta2 gamma tel ps hix =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ vcat
[ text "computeNeighbourhood"
, nest 2 $ vcat
[ text "context=" <+> (inTopContext . prettyTCM =<< getContextTelescope)
, text "con =" <+> prettyTCM con
, text "ctype =" <+> prettyTCM ctype
, text "ps =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
, text "d =" <+> prettyTCM d
, text "pars =" <+> do prettyList $ map prettyTCM pars
, text "ixs =" <+> do addContext delta1 $ prettyList $ map prettyTCM ixs
, text "cixs =" <+> do addContext gamma $ prettyList $ map prettyTCM cixs
, text "delta1 =" <+> do inTopContext $ prettyTCM delta1
, text "delta2 =" <+> do inTopContext $ addContext delta1 $ addContext gamma $ prettyTCM delta2
, text "gamma =" <+> do inTopContext $ addContext delta1 $ prettyTCM gamma
, text "hix =" <+> text (show hix)
]
]
debugNoUnify =
liftTCM $ reportSLn "tc.cover.split.con" 20 " Constructor impossible!"
debugCantSplit =
liftTCM $ reportSLn "tc.cover.split.con" 20 " Bad split!"
debugSubst s sub =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text (s ++ " =") <+> prettyTCM sub
]
debugTel s tel =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text (s ++ " =") <+> prettyTCM tel
]
debugPs tel ps =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $
inTopContext $ addContext tel $ nest 2 $ vcat
[ text "ps =" <+> prettyTCMPatternList (fromSplitPatterns ps)
]
debugPlugged delta' ps' =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $
inTopContext $ addContext delta' $ nest 2 $ vcat
[ text "ps' =" <+> do prettyTCMPatternList $ fromSplitPatterns ps'
]
data FixTarget
= YesFixTarget
| NoFixTarget
deriving (Show)
data AllowPartialCover
= YesAllowPartialCover
| NoAllowPartialCover
deriving (Eq, Show)
splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd c x = split' Inductive NoAllowPartialCover NoFixTarget c (BlockingVar x [] [] True)
splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)
splitLast ind tel ps = split ind NoAllowPartialCover sc (BlockingVar 0 [] [] True)
where sc = SClause tel (toSplitPatterns ps) empty empty Nothing
split :: Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
split ind allowPartialCover sc x =
fmap blendInAbsurdClause <$> split' ind allowPartialCover YesFixTarget sc x
where
n = lookupPatternVar sc $ blockingVarNo x
blendInAbsurdClause :: Either SplitClause Covering -> Covering
blendInAbsurdClause = fromRight (const $ Covering n [])
lookupPatternVar :: SplitClause -> Int -> Arg Nat
lookupPatternVar SClause{ scTel = tel, scPats = pats } x = arg $>
if n < 0 then __IMPOSSIBLE__ else n
where n = if k < 0
then __IMPOSSIBLE__
else fromMaybe __IMPOSSIBLE__ $ permPicks perm !!! k
perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm $ fromSplitPatterns pats
k = size tel - x - 1
arg = telVars (size tel) tel !! k
split' :: Induction
-> AllowPartialCover
-> FixTarget
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' ind allowPartialCover fixtarget sc@(SClause tel ps _ cps target) (BlockingVar x pcons' plits overlap) =
liftTCM $ runExceptT $ do
debugInit tel x ps cps
(n, t, delta1, delta2) <- do
let (tel1, Dom info (n, t) : tel2) = splitAt (size tel - x - 1) $ telToList tel
return (n, Dom info t, telFromList tel1, telFromList tel2)
let computeNeighborhoods = do
(d, pars, ixs, cons) <- inContextOfT $ isDatatype ind t
mns <- forM cons $ \ con -> fmap (SplitCon con,) <$>
computeNeighbourhood delta1 n delta2 d pars ixs x tel ps cps con
return $ catMaybes mns
computeLitNeighborhoods = do
typeOk <- liftTCM $ do
t' <- litType $ headWithDefault __IMPOSSIBLE__ plits
liftTCM $ dontAssignMetas $ tryConversion $ equalType (unDom t) t'
unless typeOk $ throwError . NotADatatype =<< do liftTCM $ buildClosure (unDom t)
ns <- forM plits $ \lit -> do
let delta2' = subst 0 (Lit lit) delta2
delta' = delta1 `abstract` delta2'
rho = liftS x $ consS (LitP lit) idS
ps' = applySubst rho ps
cps' = applySplitPSubst rho cps
return (SplitLit lit , SClause delta' ps' rho cps' Nothing)
ca <- do
let delta' = tel
varp = VarP PatOSplit $ SplitPatVar
{ splitPatVarName = underscore
, splitPatVarIndex = 0
, splitExcludedLits = plits
}
rho = liftS x $ consS varp $ raiseS 1
ps' = applySubst rho ps
return (SplitCatchall , SClause delta' ps' rho cps Nothing)
return $ ns ++ [ ca ]
ns <- if null pcons' && not (null plits)
then computeLitNeighborhoods
else computeNeighborhoods
ns <- case fixtarget of
NoFixTarget -> return ns
YesFixTarget -> lift $ forM ns $ \(con,sc) ->
(con,) . snd <$> fixTarget sc{ scTarget = target }
case ns of
[] -> do
let absurdp = VarP PatOAbsurd $ SplitPatVar underscore 0 []
rho = liftS x $ consS absurdp $ raiseS 1
ps' = applySubst rho ps
return $ Left $ SClause
{ scTel = tel
, scPats = ps'
, scSubst = __IMPOSSIBLE__
, scCheckpoints = __IMPOSSIBLE__
, scTarget = Nothing
}
(_ : _ : _) | unusableRelevance (getRelevance t) ->
throwError . IrrelevantDatatype =<< do liftTCM $ buildClosure (unDom t)
_ | allowPartialCover == NoAllowPartialCover,
overlap == False,
let ptags = map (SplitCon . conName) pcons' ++ map SplitLit plits,
let tags = map fst ns,
let diff = Set.fromList tags Set.\\ Set.fromList ptags,
not (Set.null diff) -> do
liftTCM $ reportSDoc "tc.cover.precomputed" 10 $ vcat
[ hsep $ text "ptags =" : map prettyTCM ptags
, hsep $ text "tags =" : map prettyTCM tags
]
throwError (GenericSplitError "precomputed set of constructors does not cover all cases")
_ -> do
liftTCM $ checkSortOfSplitVar $ unDom t
return $ Right $ Covering (lookupPatternVar sc x) ns
where
inContextOfT, inContextOfDelta2 :: (MonadTCM tcm, MonadDebug tcm) => tcm a -> tcm a
inContextOfT = addContext tel . escapeContext (x + 1)
inContextOfDelta2 = addContext tel . escapeContext x
debugInit tel x ps cps = liftTCM $ inTopContext $ do
reportSDoc "tc.cover.top" 10 $ vcat
[ text "TypeChecking.Coverage.split': split"
, nest 2 $ vcat
[ text "tel =" <+> prettyTCM tel
, text "x =" <+> prettyTCM x
, text "ps =" <+> do addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
, text "cps =" <+> prettyTCM cps
]
]
debugHoleAndType delta1 delta2 s ps t =
liftTCM $ reportSDoc "tc.cover.top" 10 $ nest 2 $ vcat $
[ text "p =" <+> text (patVarNameToString s)
, text "ps =" <+> text (show ps)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> inContextOfDelta2 (prettyTCM delta2)
, text "t =" <+> inContextOfT (prettyTCM t)
]
data CosplitError
= CosplitNoTarget
| CosplitNoRecordType Telescope Type
| CosplitIrrelevantProjections
instance PrettyTCM CosplitError where
prettyTCM = \case
CosplitNoTarget ->
text "target type is unknown"
CosplitIrrelevantProjections ->
text "record has irrelevant fields, but no corresponding projections"
CosplitNoRecordType tel t -> addContext tel $ do
text "target type " <+> prettyTCM t <+> text " is not a record type"
splitResult :: QName -> SplitClause -> TCM (Either CosplitError Covering)
splitResult f sc@(SClause tel ps _ _ target) = do
reportSDoc "tc.cover.split" 10 $ vcat
[ text "splitting result:"
, nest 2 $ text "f =" <+> prettyTCM f
, nest 2 $ text "target =" <+> (addContext tel $ maybe empty prettyTCM target)
]
let failure = return . Left
caseMaybe target (failure CosplitNoTarget) $ \ t -> do
isR <- addContext tel $ isRecordType $ unArg t
case isR of
Just (_r, vs, Record{ recFields = fs }) -> do
reportSDoc "tc.cover" 20 $ sep
[ text $ "we are of record type _r = " ++ prettyShow _r
, text "applied to parameters vs = " <+> (addContext tel $ prettyTCM vs)
, text $ "and have fields fs = " ++ prettyShow fs
]
ifNotM (strongRecord fs) (failure CosplitIrrelevantProjections) $ do
let es = patternsToElims $ fromSplitPatterns ps
let self = defaultArg $ Def f [] `applyE` es
pargs = vs ++ [self]
reportSDoc "tc.cover" 20 $ sep
[ text "we are self = " <+> (addContext tel $ prettyTCM $ unArg self)
]
let n = defaultArg $ permRange $ fromMaybe __IMPOSSIBLE__ $ dbPatPerm $ fromSplitPatterns ps
projOrigin <- ifM (optPostfixProjections <$> pragmaOptions) (return ProjPostfix) (return ProjPrefix)
Right . Covering n <$> do
forM fs $ \ proj -> do
dType <- defType <$> do getConstInfo $ unArg proj
let
target' = Just $ proj $> dType `piApply` pargs
projArg = fmap (Named Nothing . ProjP projOrigin) $ setHiding NotHidden proj
sc' = sc { scPats = scPats sc ++ [projArg]
, scSubst = idS
, scTarget = target'
}
return (SplitCon (unArg proj), sc')
_ -> failure $ CosplitNoRecordType tel $ unArg t
where
strongRecord :: [Arg QName] -> TCM Bool
strongRecord fs = (optIrrelevantProjections <$> pragmaOptions) `or2M`
(return $ not $ any isIrrelevant fs)
instance PrettyTCM SplitClause where
prettyTCM (SClause tel pats sigma cps target) = sep
[ text "SplitClause"
, nest 2 $ vcat
[ text "tel =" <+> prettyTCM tel
, text "pats =" <+> sep (map (prettyTCM . namedArg) pats)
, text "subst =" <+> (text . show) sigma
, text "checkpoints =" <+> prettyTCM cps
, text "target =" <+> do
caseMaybe target empty $ \ t -> do
addContext tel $ prettyTCM t
]
]