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 )
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative hiding (empty)
#endif
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.Rules.LHS.Problem (allFlexVars)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Coverage.Match
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes (getConForm)
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.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 DeBruijnPattern]
, scSubst :: PatternSubstitution
, scModuleParameterSub :: ModuleParamDict
, scTarget :: Maybe (Arg Type)
}
data Covering = Covering
{ covSplitArg :: Arg Nat
, covSplitClauses :: [(QName, SplitClause)]
}
splitClauses :: Covering -> [SplitClause]
splitClauses (Covering _ qcs) = map snd qcs
clauseToSplitClause :: Clause -> SplitClause
clauseToSplitClause cl = SClause
{ scTel = clauseTel cl
, scPats = namedClausePats cl
, scSubst = idS
, scModuleParameterSub = 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
moduleParams <- raise (n fv) <$> use stModuleParameters
let sc = SClause gamma xs idS moduleParams $ 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.splittree" 10 $ vcat
[ text "generated split tree for" <+> prettyTCM f
, text $ prettyShow splitTree
]
unless (null pss) $
setCurrentRange cs $
warning $ CoverageIssue f pss
let is = filter (`Set.notMember` used) [0..length cs 1]
unless (null is) $ do
let unreached = map (cs !!) is
setCurrentRange (map clauseFullRange unreached) $
warning $ UnreachableClauses f $ map namedClausePats unreached
unless (null noex) $ do
let noexclauses = map (cs !!) (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 ps
]
cs' <- normaliseProjP cs
case match cs' ps of
Yes (i,(mps,ls0)) -> 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
let lsis = mapMaybe (\(j,c) -> (,j) <$> matchLits c ps) $ zip [0..i1] cs
reportSLn "tc.cover.cover" 10 $ "literal matches: " ++ show lsis
let is = Map.elems $ Map.fromListWith min $ (ls0,i) : lsis
return $ CoverResult (SplittingDone (size tel)) (Set.fromList is) [] 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
_ -> return $ CoverResult (SplittingDone (size tel)) Set.empty [(tel, ps)] Set.empty
Block res bs -> tryIf (getAny res) splitRes $ do
let 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
r <- altM1 (split Inductive sc) xs
case r of
Left err -> typeError $ SplitError 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)
where
tryIf :: Monad m => Bool -> m (Maybe a) -> m a -> m a
tryIf True me m = fromMaybeM m me
tryIf False me m = m
splitRes :: TCM (Maybe 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 DeBruijnPattern] -> [NamedArg DeBruijnPattern]
gatherEtaSplits n sc []
| n >= 0 = __IMPOSSIBLE__
| otherwise = []
gatherEtaSplits n sc (p:ps) = case namedArg p of
VarP x
| n == 0 -> case p' of
VarP _ -> __IMPOSSIBLE__
DotP _ -> __IMPOSSIBLE__
AbsurdP _ -> __IMPOSSIBLE__
ConP _ _ qs -> qs ++ gatherEtaSplits (1) sc ps
LitP _ -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
| otherwise ->
updateNamedArg (\ _ -> p') p : gatherEtaSplits (n1) sc ps
where p' = lookupS (scSubst sc) $ dbPatVarIndex x
DotP _ -> p : gatherEtaSplits (n1) sc ps
AbsurdP _ -> p : gatherEtaSplits (n1) sc ps
ConP _ _ qs -> gatherEtaSplits n sc (qs ++ ps)
LitP _ -> gatherEtaSplits n sc ps
ProjP{} -> gatherEtaSplits n sc ps
addEtaSplits :: Int -> [NamedArg DeBruijnPattern] -> 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
AbsurdP _ -> addEtaSplits (k+1) ps t
ConP c cpi qs -> SplitAt (p $> k) [(conName c , addEtaSplits k (qs ++ ps) t)]
LitP _ -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
etaRecordSplits :: Int -> [NamedArg DeBruijnPattern] -> (QName,SplitClause)
-> SplitTree -> (QName,SplitTree)
etaRecordSplits n ps (q , sc) t =
(q , addEtaSplits 0 (gatherEtaSplits n sc ps) t)
inferMissingClause :: QName -> SplitClause -> TCM ()
inferMissingClause f (SClause tel ps _ mpsub (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 $ withModuleParameters mpsub $ do
(x, rhs) <- case getHiding t of
Instance{} -> newIFSMeta "" (unArg t)
Hidden -> __IMPOSSIBLE__
NotHidden -> __IMPOSSIBLE__
return $ Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = ps
, clauseBody = Just rhs
, clauseType = Just t
, clauseCatchall = False }
addClauses f [cl]
inferMissingClause _ (SClause _ _ _ _ Nothing) = __IMPOSSIBLE__
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy bs tel = return $ updateLast clearBlockingVarCons 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 ignoreSharing $ 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, scModuleParameterSub = mpsub, 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 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 $ applyPatSubst 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
, scModuleParameterSub = applySubst (raiseS n) mpsub
, 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 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 DeBruijnPattern]
-> ModuleParamDict
-> QName
-> CoverM (Maybe SplitClause)
computeNeighbourhood delta1 n delta2 d pars ixs hix tel ps mpsub 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 = ignoreSharing d
Just cixs = allApplyElims es
return (gamma0, cixs)
let maybeUserWritten arg | getOrigin arg == UserWritten = Just $ unArg arg
| otherwise = Nothing
(userNames0 :: [ArgName]) = mapMaybe maybeUserWritten $ teleArgNames tel
(userNames :: [PatVarName]) = map dbPatVarName $ lefts $
mapMaybe maybeUserWritten $ patternVars ps
avoidNames = userNames List.\\ [n, "_", "()"]
avoidUserName :: ArgName -> ArgName
avoidUserName = nameVariant (`elem` avoidNames)
debugNames userNames0 userNames avoidNames
let preserve (x, t@(El _ (Def d' _))) | d == d' = (n, t)
preserve (x, (El s (Shared p))) = preserve (x, El s $ derefPtr p)
preserve (x, t) = (avoidUserName 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) rho0
let conp = ConP con noConPatternInfo $ applySubst rho2 $
map (mapArgInfo hiddenInserted) $ tele2NamedArgs gamma0 gamma
let rho3 = consS conp rho1
delta2' = applyPatSubst 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 mpsub' = applySubst (fromPatternSubstitution rho) mpsub
return $ Just $ SClause delta' ps' rho mpsub' Nothing
where
debugNames userNames0 userNames avoidNames =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ vcat
[ text " user written names in pat.tel =" <+> sep (map text userNames0)
, text " user written names in patterns =" <+> sep (map text userNames)
, text " names to be avoided by split =" <+> sep (map text avoidNames)
]
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 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 ps
]
debugPlugged delta' ps' =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $
inTopContext $ addContext delta' $ nest 2 $ vcat
[ text "ps' =" <+> do prettyTCMPatternList ps'
]
splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd c x = split' Inductive False c (BlockingVar x Nothing)
splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)
splitLast ind tel ps = split ind sc (BlockingVar 0 Nothing)
where sc = SClause tel ps empty empty Nothing
split :: Induction
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
split ind sc x = fmap blendInAbsurdClause <$> split' ind True 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 pats
k = size tel x 1
arg = telVars (size tel) tel !! k
split' :: Induction
-> Bool
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' ind fixtarget sc@(SClause tel ps _ mpsub target) (BlockingVar x mcons) = liftTCM $ runExceptT $ do
debugInit tel x ps mpsub
(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)
(d, pars, ixs, cons) <- inContextOfT $ isDatatype ind t
ns <- catMaybes <$> do
forM cons $ \ con ->
fmap (con,) <$> do
msc <- computeNeighbourhood delta1 n delta2 d pars ixs x tel ps mpsub con
if not fixtarget then return msc else do
Trav.forM msc $ \ sc -> lift $ snd <$> fixTarget sc{ scTarget = target }
case ns of
[] -> do
let ps' = (fmap . fmap . fmap . fmap)
(\(DBPatVar name y) -> if (x==y)
then DBPatVar absurdPatternName y
else DBPatVar name y)
ps
return $ Left $ SClause
{ scTel = telFromList $ telToList delta1 ++
[fmap ((,) "()") t] ++
telToList delta2
, scPats = ps
, scSubst = idS
, scModuleParameterSub = __IMPOSSIBLE__
, scTarget = Nothing
}
(_ : _ : _) | unusableRelevance (getRelevance t) ->
throwError . IrrelevantDatatype =<< do liftTCM $ buildClosure (unDom t)
_ | Just pcons' <- mcons,
let pcons = map conName pcons',
let cons = (map fst ns),
let diff = Set.fromList cons Set.\\ Set.fromList pcons,
not (Set.null diff) -> do
liftTCM $ reportSDoc "tc.cover.precomputed" 10 $ vcat
[ hsep $ text "pcons =" : map prettyTCM pcons
, hsep $ text "cons =" : map prettyTCM cons
]
throwError (GenericSplitError "precomputed set of constructors does not cover all cases")
_ -> return $ Right $ Covering (lookupPatternVar sc x) ns
where
inContextOfT :: MonadTCM tcm => tcm a -> tcm a
inContextOfT = addContext tel . escapeContext (x + 1)
inContextOfDelta2 :: MonadTCM tcm => tcm a -> tcm a
inContextOfDelta2 = addContext tel . escapeContext x
debugInit tel x ps mpsub = 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 ps
, text "mpsub =" <+> prettyTCM mpsub
]
]
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)
]
splitResult :: QName -> SplitClause -> TCM (Maybe 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 done = return Nothing
caseMaybe target done $ \ 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
]
let es = patternsToElims 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 ps
projOrigin <- ifM (optPostfixProjections <$> pragmaOptions) (return ProjPostfix) (return ProjPrefix)
Just . 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 (unArg proj, sc')
_ -> done
instance PrettyTCM SplitClause where
prettyTCM (SClause tel pats sigma mpsub target) = sep
[ text "SplitClause"
, nest 2 $ vcat
[ text "tel =" <+> prettyTCM tel
, text "pats =" <+> sep (map (prettyTCM . namedArg) pats)
, text "subst =" <+> (text . show) sigma
, text "mpsub =" <+> prettyTCM mpsub
, text "target =" <+> do
caseMaybe target empty $ \ t -> do
addContext tel $ prettyTCM t
]
]