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.List hiding (null)
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.Exception
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.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
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 = ExceptionT 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 " ++ show f ++ " with patterns:"
, nest 2 $ vcat $ map prCl cs
]
(splitTree, used, pss) <- cover f cs sc
reportSDoc "tc.cover.splittree" 10 $ vcat
[ text "generated split tree for" <+> prettyTCM f
, text $ show splitTree
]
unless (null pss) $
setCurrentRange cs $
typeError $ CoverageFailure f pss
let is = Set.toList $ Set.difference (Set.fromList [0..genericLength cs 1]) used
unless (null is) $ do
let unreached = map (cs !!) is
setCurrentRange unreached $
typeError $ UnreachableClauses f $ map namedClausePats unreached
return splitTree
isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool
isCovered f cs sc = do
(_, _, missing) <- cover f cs sc
return $ null missing
cover :: QName -> [Clause] -> SplitClause ->
TCM (SplitTree, Set Nat, [[NamedArg DeBruijnPattern]])
cover f cs sc@(SClause tel ps _ _ target) = do
reportSDoc "tc.cover.cover" 10 $ vcat
[ text "checking coverage of pattern:"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "ps =" <+> do addContext tel $ prettyTCMPatternList ps
]
exactSplitEnabled <- optExactSplit <$> pragmaOptions
cs' <- normaliseProjP cs
case match cs' ps of
Yes (i,(mps,ls0))
| not exactSplitEnabled || (clauseCatchall (cs !! i) || all isTrivialPattern mps)
-> do
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 (SplittingDone (size tel), Set.fromList is, [])
| otherwise -> do
reportSDoc "tc.cover.cover" 10 $ vcat
[ text $ "pattern covered by clause " ++ show i ++ " but case splitting was not exact. remaining mpats: "
, nest 2 $ vcat $ map (text . show) mps
]
setCurrentRange (cs !! i) $
typeError $ CoverageNoExactSplit f (cs !! i)
No -> do
reportSLn "tc.cover" 20 $ "pattern is not covered"
case fmap getHiding target of
Just h | h == Instance -> do
inferMissingClause f sc
return (SplittingDone (size tel), Set.empty, [])
_ -> return (SplittingDone (size tel), Set.empty, [ps])
Block res bs -> tryIf (getAny res) splitRes $ do
let done = return (SplittingDone (size tel), Set.empty, [ps])
if null bs then done else do
reportSLn "tc.cover.strategy" 20 $ "blocking vars = " ++ show bs
xs <- splitStrategy bs tel
r <- altM1 (split Inductive sc) xs
case r of
Left err -> case err of
CantSplit c tel us vs -> typeError $ CoverageCantSplitOn c tel us vs
NotADatatype a -> enterClosure a $ typeError . CoverageCantSplitType
IrrelevantDatatype a -> enterClosure a $ typeError . CoverageCantSplitIrrelevantType
CoinductiveDatatype a -> enterClosure a $ typeError . CoverageCantSplitType
GenericSplitError s -> fail $ "failed to split: " ++ s
Right (Covering n []) ->
return (SplittingDone (size tel), Set.empty, [])
Right (Covering n scs) -> do
(trees, useds, psss) <- unzip3 <$> mapM (cover f cs) (map snd scs)
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 (tree, Set.unions useds, concat psss)
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 (SplitTree, Set Nat, [[NamedArg DeBruijnPattern]]))
splitRes = do
reportSLn "tc.cover" 20 $ "blocked by projection pattern"
mcov <- splitResult f sc
Trav.forM mcov $ \ (Covering n scs) -> do
(projs, (trees, useds, psss)) <- mapSnd unzip3 . unzip <$> do
mapM (traverseF $ cover f cs <=< (snd <.> fixTarget)) scs
let tree = SplitAt n $ zip projs trees
return (tree, Set.unions useds, concat psss)
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__
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
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
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 { clauseRange = 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, MonadException SplitError tcm) =>
Induction -> Dom Type ->
tcm (QName, [Arg Term], [Arg Term], [QName])
isDatatype ind at = do
let t = unDom at
throw f = throwException . 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) = genericSplitAt 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 (setOrigin Inserted) $ 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')
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 $ 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 preserve (x, t@(El _ (Def d' _))) | d == d' = (n, t)
preserve (x, (El s (Shared p))) = preserve (x, El s $ derefPtr p)
preserve p = p
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{} -> do
debugCantSplit
throwException $ CantSplit (conName con) (delta1 `abstract` gamma) conIxs givenIxs
Unifies (delta1',rho0,_) -> do
debugSubst "rho0" rho0
let (rho1,rho2) = splitS (size gamma) rho0
let conp = ConP con noConPatternInfo $ applySubst rho2 $
map (setOrigin Inserted) $ 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
addContext tel $ debugPs ps
let ps' = applySubst rho ps
addContext delta' $ debugPlugged ps'
let mpsub' = applySubst (fromPatternSubstitution rho) mpsub
return $ Just $ SClause delta' ps' rho mpsub' 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 addContext tel $ prettyTCMPatternList ps
, text "d =" <+> prettyTCM d
, text "pars =" <+> prettyList (map prettyTCM pars)
, text "ixs =" <+> addContext delta1 (prettyList (map prettyTCM ixs))
, text "cixs =" <+> do addContext gamma $ prettyList (map prettyTCM cixs)
, text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> prettyTCM delta2
, text "gamma =" <+> 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 ps =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ nest 2 $ vcat
[ text "ps =" <+> prettyTCMPatternList ps
]
debugPlugged ps' =
liftTCM $ reportSDoc "tc.cover.split.con" 20 $ 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 $ runExceptionT $ do
debugInit tel x ps mpsub
(n, t, delta1, delta2) <- do
let (tel1, Dom info (n, t) : tel2) = genericSplitAt (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) ->
throwException . 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
]
throwException (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 $ do
reportSDoc "tc.cover.top" 10 $ vcat
[ text "TypeChecking.Coverage.split': split"
, nest 2 $ vcat
[ text "tel =" <+> prettyTCM tel
, text "x =" <+> text (show 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 =" <+> text (show 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 = " ++ show _r
, text "applied to parameters vs = " <+> (addContext tel $ prettyTCM vs)
, text $ "and have fields fs = " ++ show 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
]
]