{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Coverage
( SplitClause(..), clauseToSplitClause, insertTrailingArgs
, Covering(..), splitClauses
, coverageCheck
, isCovered
, splitClauseWithAbsurd
, splitLast
, splitResult
, normaliseProjP
) where
import Prelude hiding (null, (!!))
import Control.Monad
import Control.Monad.Trans ( lift )
import Data.Foldable (for_)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Translation.InternalToAbstract (NamedClause(..))
import Agda.TypeChecking.Names
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Primitive.Cubical (trFillTel)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Rules.LHS (checkSortOfSplitVar)
import Agda.TypeChecking.Rules.LHS.Problem (allFlexVars)
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.Term (unquoteTactic)
import Agda.TypeChecking.Coverage.Match
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Conversion (tryConversion, equalType)
import Agda.TypeChecking.Datatypes (getConForm)
import {-# SOURCE #-} Agda.TypeChecking.Empty ( checkEmptyTel, isEmptyTel, isEmptyType )
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Warnings
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Except
( ExceptT
, MonadError (throwError, catchError)
, 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.Singleton
import Agda.Utils.Size
import Agda.Utils.WithDefault
import Agda.Utils.Impossible
data SplitClause = SClause
{ scTel :: Telescope
, scPats :: [NamedArg SplitPattern]
, scSubst :: Substitution' SplitPattern
, scCheckpoints :: Map CheckpointId Substitution
, scTarget :: Maybe (Dom 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 = domFromArg <$> clauseType cl
}
type CoverM = ExceptT SplitError TCM
coverageCheck
:: QName
-> Type
-> [Clause]
-> TCM SplitTree
coverageCheck f t cs = do
reportSLn "tc.cover.top" 30 $ "entering coverageCheck for " ++ show f
reportSDoc "tc.cover.top" 75 $ " of type (raw): " <+> (text . prettyShow) t
reportSDoc "tc.cover.top" 45 $ " of type: " <+> prettyTCM t
TelV gamma a <- telViewUpTo (-1) t
reportSLn "tc.cover.top" 30 $ "coverageCheck: computed telView"
let
n = size gamma
xs = map (setOrigin Inserted) $ teleNamedArgs gamma
reportSLn "tc.cover.top" 30 $ "coverageCheck: getDefFreeVars"
fv <- getDefFreeVars f
reportSLn "tc.cover.top" 30 $ "coverageCheck: getting checkpoints"
checkpoints <- applySubst (raiseS (n - fv)) <$> viewTC eCheckpoints
let sc = SClause gamma xs idS checkpoints $ Just $ defaultDom 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 qss noex <- cover f cs sc
noex <- return $ List.filter (< length cs) $ IntSet.toList noex
reportSDoc "tc.cover.top" 10 $ vcat
[ "cover computed!"
, text $ "used clauses: " ++ show used
, text $ "non-exact clauses: " ++ show noex
]
reportSDoc "tc.cover.splittree" 10 $ vcat
[ "generated split tree for" <+> prettyTCM f
, text $ prettyShow splitTree
]
reportSDoc "tc.cover.covering" 10 $ vcat
[ text $ "covering patterns for " ++ prettyShow f
, nest 2 $ vcat $ map (\ cl -> addContext (clauseTel cl) $ prettyTCMPatternList $ namedClausePats cl) qss
]
whenM (optCubical <$> pragmaOptions) $ do
modifySignature $ updateDefinition f $ updateTheDef $ updateCovering $ const qss
pss <- flip filterM pss $ \(tel,ps) ->
caseEitherM (checkEmptyTel noRange tel) (\ _ -> return True) $ \ l -> do
let i = size tel - 1 - l
let sub = inplaceS i $ absurdP i
let cl = Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = applySubst sub ps
, clauseBody = Nothing
, clauseType = Nothing
, clauseCatchall = False
, clauseRecursive = Just False
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
reportSDoc "tc.cover.missing" 20 $ inTopContext $ do
sep [ "adding missing absurd clause"
, nest 2 $ prettyTCM $ QNamed f cl
]
reportSDoc "tc.cover.missing" 80 $ inTopContext $ vcat
[ "l = " <+> pretty l
, "i = " <+> pretty i
, "cl = " <+> pretty (QNamed f cl)
]
addClauses f [cl]
return False
unless (null pss) $ do
stLocalPartialDefs `modifyTCLens` Set.insert f
whenM ((YesCoverageCheck ==) <$> viewTC eCoverageCheck) $
setCurrentRange cs $ warning $ CoverageIssue f pss
let (is0, cs1) = unzip $ for (zip [0..] cs) $ \ (i, cl) ->
let unreachable = i `IntSet.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
let ranges = map clauseFullRange unreached
setCurrentRange ranges $ warning $ UnreachableClauses f ranges
unless (null noex) $ do
let noexclauses = map (indexWithDefault __IMPOSSIBLE__ cs1) noex
setCurrentRange (map clauseLHSRange noexclauses) $
warning $ CoverageNoExactSplit f $ noexclauses
return splitTree
isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool
isCovered f cs sc = do
reportSDoc "tc.cover.isCovered" 20 $ vcat
[ "isCovered"
, nest 2 $ vcat $
[ "f = " <+> prettyTCM f
, "cs = " <+> vcat (map (nest 2 . prettyTCM . NamedClause f True) cs)
, "sc = " <+> prettyTCM sc
]
]
(_ , sc') <- insertTrailingArgs sc
CoverResult { coverMissingClauses = missing } <- cover f cs sc'
return $ null missing
`catchError` \ _ -> return False
data CoverResult = CoverResult
{ coverSplitTree :: SplitTree
, coverUsedClauses :: IntSet
, coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
, coverPatterns :: [Clause]
, coverNoExactClauses :: IntSet
}
cover :: QName -> [Clause] -> SplitClause ->
TCM CoverResult
cover f cs sc@(SClause tel ps _ _ target) = updateRelevance $ do
reportSDoc "tc.cover.cover" 10 $ inTopContext $ vcat
[ "checking coverage of pattern:"
, nest 2 $ prettyTCM sc
, nest 2 $ "target sort =" <+> do addContext tel $ maybe (text "<none>") (prettyTCM . getSort . unDom) target
]
reportSLn "tc.cover.cover" 80 $ "raw target =\n" ++ show target
match cs ps >>= \case
Yes (i,mps) -> do
exact <- allM (map snd mps) isTrivialPattern
let cl0 = indexWithDefault __IMPOSSIBLE__ cs i
let noExactClause = if exact || clauseCatchall (indexWithDefault __IMPOSSIBLE__ cs i)
then empty
else singleton i
reportSLn "tc.cover.cover" 10 $ "pattern covered by clause " ++ show i
reportSDoc "tc.cover.cover" 20 $ text "with mps = " <+> do addContext tel $ pretty $ mps
cl <- applyCl sc cl0 mps
return $ CoverResult (SplittingDone (size tel)) (singleton i) [] [cl] noExactClause
No -> do
reportSLn "tc.cover" 20 $ "pattern is not covered"
let infer dom = isInstance dom || isJust (domTactic dom)
if maybe False infer target
then do
cl <- inferMissingClause f sc
return $ CoverResult (SplittingDone (size tel)) empty [] [cl] empty
else do
let ps' = fromSplitPatterns ps
return $ CoverResult (SplittingDone (size tel)) empty [(tel, ps')] [] empty
Block res bs -> trySplitRes res (null bs) splitError $ do
when (null bs) __IMPOSSIBLE__
reportSLn "tc.cover.strategy" 20 $ "blocking vars = " ++ prettyShow bs
xs <- splitStrategy bs tel
continue xs NoAllowPartialCover $ \ _err -> do
continue xs YesAllowPartialCover $ \ err -> do
splitError err
where
splitError :: SplitError -> TCM a
splitError = withRangeOfCandidateClauses . typeError . SplitError
withRangeOfCandidateClauses :: TCM a -> TCM a
withRangeOfCandidateClauses cont = do
cands <- mapMaybe (uncurry notNo) . zip cs <$> mapM (matchClause ps) cs
setCurrentRange cands cont
where
notNo :: Clause -> Match a -> Maybe Clause
notNo c = \case
Yes{} -> Just c
Block{} -> Just c
No{} -> Nothing
applyCl :: SplitClause -> Clause -> [(Nat, SplitPattern)] -> TCM Clause
applyCl SClause{scTel = tel, scPats = sps} cl mps = addContext tel $ do
let ps = namedClausePats cl
reportSDoc "tc.cover.applyCl" 40 $ "applyCl"
reportSDoc "tc.cover.applyCl" 40 $ "tel =" <+> prettyTCM tel
reportSDoc "tc.cover.applyCl" 40 $ "ps =" <+> pretty ps
reportSDoc "tc.cover.applyCl" 40 $ "mps =" <+> pretty mps
reportSDoc "tc.cover.applyCl" 40 $ "s =" <+> pretty s
reportSDoc "tc.cover.applyCl" 40 $ "ps[s] =" <+> pretty (s `applySubst` ps)
let extra = drop (length ps) $ fromSplitPatterns sps
n_extra = length extra
reportSDoc "tc.cover.applyCl" 40 $ "extra =" <+> pretty extra
mtv <- (traverse . traverse) (telViewUpToPath n_extra) $ clauseType cl
let ty = (fmap . fmap) ((parallelS (reverse $ map namedArg extra) `composeS` liftS n_extra s `applyPatSubst`) . theCore) mtv
reportSDoc "tc.cover.applyCl" 40 $ "new ty =" <+> pretty ty
return $
Clause { clauseLHSRange = clauseLHSRange cl
, clauseFullRange = clauseFullRange cl
, clauseTel = tel
, namedClausePats = (s `applySubst` ps) ++ extra
, clauseBody = (`applyE` patternsToElims extra) . (s `applyPatSubst`) <$> clauseBody cl
, clauseType = ty
, clauseCatchall = clauseCatchall cl
, clauseRecursive = clauseRecursive cl
, clauseUnreachable = clauseUnreachable cl
, clauseEllipsis = clauseEllipsis cl
}
where
(vs,qs) = unzip mps
mps' = zip vs $ map namedArg $ fromSplitPatterns $ map defaultNamedArg qs
s = parallelS (for [0..maximum (-1:vs)] $ (\ i -> fromMaybe (deBruijnVar i) (List.lookup i mps')))
updateRelevance :: TCM a -> TCM a
updateRelevance cont =
caseMaybe target cont $ \ b -> do
let m = getModality b
applyModalityToContext m cont
continue
:: [BlockingVar]
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue xs allowPartialCover handle = do
r <- altM1 (\ x -> fmap (,x) <$> split Inductive allowPartialCover sc x) xs
case r of
Left err -> handle err
Right (Covering n [], _) ->
do
let qs = []
return $ CoverResult (SplittingDone (size tel)) empty [] qs empty
Right (Covering n scs, x) -> do
cs <- do
let fallback = return cs
caseMaybeM (getPrimitiveName' builtinHComp) fallback $ \ comp -> do
let isComp = \case
SplitCon c -> comp == c
_ -> False
caseMaybe (List.find (isComp . fst) scs) fallback $ \ (_, newSc) -> do
snoc cs <$> createMissingHCompClause f n x sc newSc
results <- mapM (cover f cs) (map snd scs)
let trees = map coverSplitTree results
useds = map coverUsedClauses results
psss = map coverMissingClauses results
qsss = map coverPatterns results
noex = map coverNoExactClauses results
reportSDoc "tc.cover.split.eta" 60 $ vcat
[ "etaRecordSplits"
, nest 2 $ vcat
[ "n = " <+> text (show n)
, "scs = " <+> prettyTCM scs
, "ps = " <+> prettyTCMPatternList (fromSplitPatterns ps)
]
]
let trees' = zipWith (etaRecordSplits (unArg n) ps) scs trees
tree = SplitAt n StrictSplit trees'
return $ CoverResult tree (IntSet.unions useds) (concat psss) (concat qsss) (IntSet.unions noex)
trySplitRes
:: BlockedOnResult
-> Bool
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
-> TCM CoverResult
trySplitRes NotBlockedOnResult finalSplit splitError cont
| finalSplit = __IMPOSSIBLE__
| otherwise = cont
trySplitRes (BlockedOnApply IsApply) finalSplit splitError cont
| finalSplit = __IMPOSSIBLE__
| otherwise = cont
trySplitRes (BlockedOnApply IsIApply) finalSplit splitError cont
= do
caseMaybeM (splitResultPath f sc) fallback $ \ sc ->
cover f cs . snd =<< insertTrailingArgs sc
where
fallback | finalSplit = __IMPOSSIBLE__
| otherwise = cont
trySplitRes (BlockedOnProj True) finalSplit splitError cont
| finalSplit = splitError CosplitCatchall
| otherwise = cont
trySplitRes (BlockedOnProj False) finalSplit splitError cont = do
reportSLn "tc.cover" 20 $ "blocked by projection pattern"
mcov <- splitResultRecord f sc
case mcov of
Left err
| finalSplit -> splitError err
| otherwise -> cont
Right (Covering n scs) -> do
(projs, results) <- unzip <$> do
mapM (traverseF $ cover f cs <=< (snd <.> insertTrailingArgs)) scs
let trees = map coverSplitTree results
useds = map coverUsedClauses results
psss = map coverMissingClauses results
qsss = map coverPatterns results
noex = map coverNoExactClauses results
tree = SplitAt n StrictSplit $ zip projs trees
return $ CoverResult tree (IntSet.unions useds) (concat psss) (concat qsss) (IntSet.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__
IApplyP{} -> __IMPOSSIBLE__
DefP _ _ qs -> qs ++ gatherEtaSplits (-1) sc ps
| otherwise ->
updateNamedArg (\ _ -> p') p : gatherEtaSplits (n-1) sc ps
where p' = lookupS (scSubst sc) $ splitPatVarIndex x
IApplyP{} ->
updateNamedArg (applySubst (scSubst sc)) p : gatherEtaSplits (n-1) sc ps
DotP _ _ -> p : gatherEtaSplits (n-1) sc ps
ConP _ _ qs -> gatherEtaSplits n sc (qs ++ ps)
DefP _ _ 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) LazySplit [(SplitCon (conName c) , addEtaSplits k (qs ++ ps) t)]
LitP{} -> __IMPOSSIBLE__
ProjP{} -> __IMPOSSIBLE__
DefP{} -> __IMPOSSIBLE__
IApplyP{} -> addEtaSplits (k+1) ps t
etaRecordSplits :: Int -> [NamedArg SplitPattern] -> (SplitTag,SplitClause)
-> SplitTree -> (SplitTag,SplitTree)
etaRecordSplits n ps (q , sc) t =
(q , addEtaSplits 0 (gatherEtaSplits n sc ps) t)
createMissingHCompClause
:: QName
-> Arg Nat
-> BlockingVar
-> SplitClause
-> SplitClause
-> TCM Clause
createMissingHCompClause f n x old_sc (SClause tel ps _sigma' cps (Just t)) = setCurrentRange f $ do
reportSDoc "tc.cover.hcomp" 20 $ addContext tel $ text "Trying to create right-hand side of type" <+> prettyTCM t
reportSDoc "tc.cover.hcomp" 30 $ addContext tel $ text "ps = " <+> prettyTCMPatternList (fromSplitPatterns ps)
reportSDoc "tc.cover.hcomp" 30 $ text "tel = " <+> prettyTCM tel
io <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIOne
iz <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIZero
let
cannotCreate doc t = do
typeError . SplitError $ CannotCreateMissingClause f (tel,fromSplitPatterns ps) doc t
let old_ps = patternsToElims $ fromSplitPatterns $ scPats old_sc
old_t = fromJust $ scTarget old_sc
old_tel = scTel old_sc
getLevel t = do
s <- reduce $ getSort t
case s of
Type l -> pure (Level l)
s -> do
reportSDoc "tc.cover.hcomp" 20 $ text "getLevel, s = " <+> prettyTCM s
typeError . GenericDocError =<<
(text "The sort of" <+> prettyTCM t <+> text "should be of the form \"Set l\"")
(gamma,hdelta@(ExtendTel hdom delta)) = splitTelescopeAt (size old_tel - (blockingVarNo x + 1)) old_tel
(working_tel,_deltaEx) = splitTelescopeAt (size gamma + 3 + size delta) tel
rhoS = liftS (size hdelta) $ raiseS 3
vs = iApplyVars (scPats old_sc)
alphab <- forM vs $ \ i -> do
let
tm = Def f old_ps
(l,r) <- reduce (inplaceS i iz `applySubst` tm, inplaceS i io `applySubst` tm)
return $ (var i, (l, r))
cl <- do
(ty,rhs) <- addContext working_tel $ do
runNamesT [] $ do
tPOr <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinPOr
tIMax <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIMax
tIMin <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIMin
tINeg <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinINeg
tHComp <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinHComp
tTrans <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinTrans
extra_ps <- open $ patternsToElims $ fromSplitPatterns $ drop (length old_ps) ps
let
ineg j = pure tINeg <@> j
imax i j = pure tIMax <@> i <@> j
imin i j = pure tIMin <@> i <@> j
trFillTel' a b c d = do
m <- trFillTel <$> a <*> b <*> c <*> d
x <- lift $ runExceptT m
case x of
Left bad_t -> cannotCreate "Cannot transport with type family:" bad_t
Right args -> return args
comp <- do
let forward la bA r u = pure tTrans <#> (lam "i" $ \ i -> la <@> (i `imax` r))
<@> (lam "i" $ \ i -> bA <@> (i `imax` r))
<@> r
<@> u
return $ \ la bA phi u u0 ->
pure tHComp <#> (la <@> pure io) <#> (bA <@> pure io) <#> phi
<@> (lam "i" $ \ i -> ilam "o" $ \ o ->
forward la bA i (u <@> i <..> o))
<@> forward la bA (pure iz) u0
let
hcomp la bA phi u u0 = pure tHComp <#> la <#> bA
<#> phi
<@> u
<@> u0
hfill la bA phi u u0 i = hcomp la bA
(pure tIMax <@> phi <@> (pure tINeg <@> i))
(lam "j" $ \ j -> pure tPOr <#> la <@> phi <@> (pure tINeg <@> i) <#> (ilam "o" $ \ _ -> bA)
<@> (ilam "o" $ \ o -> u <@> (pure tIMin <@> i <@> j) <..> o)
<@> (ilam "o" $ \ _ -> u0)
)
u0
hcompS <- lift $ do
hdom <- pure $ raise 3 hdom
let
[phi,u,u0] = map (pure . var) [2,1,0]
htype = pure $ unEl . unDom $ hdom
lvl = getLevel $ unDom hdom
hc <- pure tHComp <#> lvl <#> htype
<#> phi
<@> u
<@> u0
return $ liftS (size delta) $ hc `consS` raiseS 3
hdom <- pure $ raise (3+size delta) hdom
htype <- open $ unEl . unDom $ hdom
lvl <- open =<< (lift . getLevel $ unDom hdom)
[phi,u,u0] <- mapM (open . raise (size delta) . var) [2,1,0]
g <- open $ raise (3+size delta) $ abstract hdelta (Def f old_ps)
old_t <- open $ raise (3+size delta) $ abstract hdelta (unDom old_t)
let bapp a x = lazyAbsApp <$> a <*> x
(delta_fill :: NamesT TCM (Abs Args)) <- (open =<<) $ do
delta <- open $ raise (3+size delta) delta
deltaf <- open =<< bind "i" (\ i ->
(delta `bapp` hfill lvl htype phi u u0 (ineg i)))
args <- (open =<<) $ teleArgs <$> (lazyAbsApp <$> deltaf <*> pure iz)
bind "i" $ \ i -> addContext ("i" :: String) $ do
trFillTel' deltaf (pure iz) args (ineg i)
let
apply_delta_fill i f = apply <$> f <*> (delta_fill `bapp` i)
call v i = apply_delta_fill i $ g <@> v
ty <- do
return $ \ i -> do
v <- hfill lvl htype phi u u0 i
hd <- old_t
args <- delta_fill `bapp` i
lift $ piApplyM hd $ [Arg (domInfo hdom) v] ++ args
ty_level <- do
t <- bind "i" ty
s <- reduce $ getSort (absBody t)
reportSDoc "tc.cover.hcomp" 20 $ text "ty_level, s = " <+> prettyTCM s
case s of
Type l -> open =<< (lam "i" $ \ _ -> pure $ Level l)
_ -> cannotCreate "Cannot compose with type family:" =<< (liftTCM $ buildClosure t)
let
pOr_ty i phi psi u0 u1 = pure tPOr <#> (ty_level <@> i)
<@> phi <@> psi
<#> (ilam "o" $ \ _ -> unEl <$> ty i) <@> u0 <@> u1
alpha <- do
vars <- mapM (open . applySubst hcompS . fst) alphab
return $ foldr imax (pure iz) $ map (\ v -> v `imax` ineg v) vars
b <- do
sides <- forM alphab $ \ (psi,(side0,side1)) -> do
psi <- open $ hcompS `applySubst` psi
[side0,side1] <- mapM (open . raise (3+size delta) . abstract hdelta) [side0,side1]
return $ (ineg psi `imax` psi, \ i -> pOr_ty i (ineg psi) psi (ilam "o" $ \ _ -> apply_delta_fill i $ side0 <@> hfill lvl htype phi u u0 i)
(ilam "o" $ \ _ -> apply_delta_fill i $ side1 <@> hfill lvl htype phi u u0 i))
let recurse [] i = __IMPOSSIBLE__
recurse [(psi,u)] i = u i
recurse ((psi,u):xs) i = pOr_ty i psi (foldr imax (pure iz) (map fst xs)) (u i) (recurse xs i)
return $ recurse sides
((,) <$> ty (pure io) <*>) $ do
comp ty_level
(lam "i" $ \ i -> unEl <$> ty i)
(phi `imax` alpha)
(lam "i" $ \ i ->
let rhs = (ilam "o" $ \ o -> call (u <@> i <..> o) i)
in if null alphab then rhs else
pOr_ty i phi alpha rhs (b i)
)
(call u0 (pure iz))
reportSDoc "tc.cover.hcomp" 20 $ text "old_tel =" <+> prettyTCM tel
let n = size tel - (size gamma + 3 + size delta)
reportSDoc "tc.cover.hcomp" 20 $ text "n =" <+> text (show n)
(TelV deltaEx t,bs) <- telViewUpToPathBoundary' n ty
rhs <- pure $ raise n rhs `applyE` teleElims deltaEx bs
cxt <- getContextTelescope
reportSDoc "tc.cover.hcomp" 30 $ text "cxt = " <+> prettyTCM cxt
reportSDoc "tc.cover.hcomp" 30 $ text "tel = " <+> prettyTCM tel
reportSDoc "tc.cover.hcomp" 20 $ addContext tel $ text "t = " <+> prettyTCM t
reportSDoc "tc.cover.hcomp" 20 $ addContext tel $ text "rhs = " <+> prettyTCM rhs
return $ Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = fromSplitPatterns ps
, clauseBody = Just $ rhs
, clauseType = Just $ defaultArg t
, clauseCatchall = False
, clauseRecursive = Nothing
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
addClauses f [cl]
return cl
createMissingHCompClause _ _ _ _ (SClause _ _ _ _ Nothing) = __IMPOSSIBLE__
inferMissingClause
:: QName
-> SplitClause
-> TCM Clause
inferMissingClause f (SClause tel ps _ cps (Just t)) = setCurrentRange f $ do
reportSDoc "tc.cover.infer" 20 $ addContext tel $ "Trying to infer right-hand side of type" <+> prettyTCM t
rhs <-
addContext tel
$ locallyTC eCheckpoints (const cps)
$ checkpoint IdS
$ case getHiding t of
_ | Just tac <- domTactic t -> do
reportSDoc "tc.cover.infer" 40 $ vcat
[ "@tactic rhs"
, nest 2 $ "target =" <+> pretty t ]
(_, v) <- newValueMeta DontRunMetaOccursCheck CmpLeq (unDom t)
v <$ unquoteTactic tac v (unDom t)
Instance{} -> snd <$> newInstanceMeta "" (unDom t)
Hidden -> __IMPOSSIBLE__
NotHidden -> __IMPOSSIBLE__
let cl = Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = fromSplitPatterns ps
, clauseBody = Just rhs
, clauseType = Just (argFromDom t)
, clauseCatchall = False
, clauseRecursive = Nothing
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
addClauses f [cl]
return cl
inferMissingClause _ (SClause _ _ _ _ Nothing) = __IMPOSSIBLE__
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy bs tel = return $ updateLast setBlockingVarOverlap xs
where
xs = strict ++ lazy
(lazy, strict) = List.partition blockingVarLazy bs
isDatatype :: (MonadTCM tcm, MonadError SplitError tcm) =>
Induction -> Dom Type ->
tcm (DataOrRecord, QName, [Arg Term], [Arg Term], [QName], Bool)
isDatatype ind at = do
let t = unDom at
throw f = throwError . f =<< do liftTCM $ buildClosure t
t' <- liftTCM $ reduce t
mInterval <- liftTCM $ getBuiltinName' builtinInterval
mIsOne <- liftTCM $ getBuiltinName' builtinIsOne
case unEl t' of
Def d [] | Just d == mInterval -> throw NotADatatype
Def d [Apply phi] | Just d == mIsOne -> do
xs <- liftTCM $ decomposeInterval =<< reduce (unArg phi)
if null xs
then return $ (IsData, d, [phi], [], [], False)
else throw NotADatatype
Def d es -> do
let ~(Just args) = allApplyElims es
def <- liftTCM $ theDef <$> getConstInfo d
case def of
Datatype{dataPars = np, dataCons = cs}
| otherwise -> do
let (ps, is) = splitAt np args
return (IsData, d, ps, is, cs, not $ null (dataPathCons def))
Record{recPars = np, recConHead = con, recInduction = i}
| i == Just CoInductive && ind /= CoInductive ->
throw CoinductiveDatatype
| otherwise ->
return (IsRecord, d, args, [], [conName con], False)
_ -> throw NotADatatype
_ -> throw NotADatatype
fixTargetType :: SplitClause -> Dom Type -> TCM SplitClause
fixTargetType sc@SClause{ scTel = sctel, scSubst = sigma } target = do
reportSDoc "tc.cover.target" 20 $ sep
[ "split clause telescope: " <+> prettyTCM sctel
]
reportSDoc "tc.cover.target" 60 $ sep
[ "substitution : " <+> prettyTCM sigma
]
reportSDoc "tc.cover.target" 60 $ sep
[ "target type before substitution:" <+> pretty target
, " after substitution:" <+> pretty (applySplitPSubst sigma target)
]
return $ sc { scTarget = Just $ applySplitPSubst sigma target }
insertTrailingArgs :: SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs sc@SClause{ scTel = sctel, scPats = ps, scSubst = sigma, scCheckpoints = cps, scTarget = target } =
caseMaybe target (return (empty,sc)) $ \ a -> do
(TelV tel b) <- telViewUpTo (-1) $ unDom a
reportSDoc "tc.cover.target" 15 $ sep
[ "target type telescope: " <+> do
addContext sctel $ prettyTCM tel
, "target type core : " <+> 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
[ "new split clause telescope : " <+> prettyTCM sctel'
]
reportSDoc "tc.cover.target" 30 $ sep
[ "new split clause patterns : " <+> do
addContext sctel' $ prettyTCMPatternList $ fromSplitPatterns ps'
]
reportSDoc "tc.cover.target" 60 $ sep
[ "new split clause substitution: " <+> prettyTCM (scSubst sc')
]
reportSDoc "tc.cover.target" 30 $ sep
[ "new split clause target : " <+> do
addContext sctel' $ prettyTCM $ fromJust newTarget
]
reportSDoc "tc.cover.target" 20 $ sep
[ "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
computeHCompSplit :: Telescope
-> PatVarName
-> Telescope
-> QName
-> Args
-> Args
-> Nat
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId Substitution
-> CoverM (Maybe (SplitTag,SplitClause))
computeHCompSplit delta1 n delta2 d pars ixs hix tel ps cps = do
dsort <- liftTCM $ (parallelS (reverse $ map unArg pars) `applySubst`) . dataSort . theDef <$> getConstInfo d
hCompName <- fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinHComp
theHCompT <- defType <$> getConstInfo hCompName
let
dlvl = Level . (\ (Type s) -> s) $ dsort
dterm = Def d [] `apply` (pars ++ ixs)
TelV gamma _ <- lift $ telView (theHCompT `piApply` [setHiding Hidden $ defaultArg $ dlvl , defaultArg $ dterm])
case (delta1 `abstract` gamma,IdS) of
(delta1',rho0) -> do
let (rho1,rho2) = splitS (size gamma) $ toSplitPSubst rho0
let
defp = DefP defaultPatternInfo hCompName . map (setOrigin Inserted) $
map (fmap unnamed) [setHiding Hidden $ defaultArg $ applySubst rho1 $ DotP defaultPatternInfo $ dlvl
,setHiding Hidden $ defaultArg $ applySubst rho1 $ DotP defaultPatternInfo $ dterm]
++ applySubst rho2 (teleNamedArgs gamma)
let rho3 = consS defp rho1
delta2' = applySplitPSubst rho3 delta2
delta' = delta1' `abstract` delta2'
rho = liftS (size delta2) rho3
let ps' = applySubst rho ps
let cps' = applySplitPSubst rho cps
return $ Just . (SplitCon hCompName,) $ SClause delta' ps' rho cps' Nothing
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, boundary) <- do
(TelV gamma0 (El _ d), boundary) <- liftTCM $ telViewPathBoundaryP (ctype `piApply` pars)
let Def _ es = d
Just cixs = allApplyElims es
return (gamma0, cixs, boundary)
let preserve (x, t@(El _ (Def d' _))) | d == d' = (n, t)
preserve (x, t) = (x, t)
gamma = telFromList . map (fmap preserve) . telToList $ gamma0
delta1Gamma = delta1 `abstract` gamma
debugInit con ctype d pars ixs cixs delta1 delta2 gamma tel ps hix
cforced <- defForced <$> getConstInfo c
let forced = replicate (size delta1) NotForced ++ cforced
flex = allFlexVars forced delta1Gamma
let conIxs = drop (size pars) cixs
givenIxs = raise (size gamma) ixs
dtype <- do
let (_, Dom{domInfo = info} : _) = splitAt (size tel - hix - 1) (telToList tel)
let updCoh = composeCohesion (getCohesion info)
TelV dtel dt <- telView dtype
return $ abstract (mapCohesion updCoh <$> dtel) dt
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 rho0' = toSplitPSubst rho0
let (rho1,rho2) = splitS (size gamma) $ rho0'
let cpi = noConPatternInfo{ conPInfo = PatternInfo PatOSplit [] , conPRecord = True }
conp = ConP con cpi $ applySubst rho0' $
map (mapArgInfo hiddenInserted) $ telePatterns' (tele2NamedArgs gamma0) gamma boundary
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 $ do
reportSDoc "tc.cover.split.con" 20 $ vcat
[ "computeNeighbourhood"
, nest 2 $ vcat
[ "context=" <+> (inTopContext . prettyTCM =<< getContextTelescope)
, "con =" <+> prettyTCM con
, "ctype =" <+> prettyTCM ctype
, "ps =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
, "d =" <+> prettyTCM d
, "pars =" <+> do prettyList $ map prettyTCM pars
, "ixs =" <+> do addContext delta1 $ prettyList $ map prettyTCM ixs
, "cixs =" <+> do addContext gamma $ prettyList $ map prettyTCM cixs
, "delta1 =" <+> do inTopContext $ prettyTCM delta1
, "delta2 =" <+> do inTopContext $ addContext delta1 $ addContext gamma $ prettyTCM delta2
, "gamma =" <+> do inTopContext $ addContext delta1 $ prettyTCM gamma
, "tel =" <+> do inTopContext $ prettyTCM tel
, "hix =" <+> text (show hix)
]
]
reportSDoc "tc.cover.split.con" 70 $ vcat
[ "computeNeighbourhood"
, nest 2 $ vcat
[ "context=" <+> (inTopContext . (text . show) =<< getContextTelescope)
, "con =" <+> (text . show) con
, "ctype =" <+> (text . show) ctype
, "ps =" <+> (text . show) ps
, "d =" <+> (text . show) d
, "pars =" <+> (text . show) pars
, "ixs =" <+> (text . show) ixs
, "cixs =" <+> (text . show) cixs
, "delta1 =" <+> (text . show) delta1
, "delta2 =" <+> (text . show) delta2
, "gamma =" <+> (text . show) gamma
, "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
[ "ps =" <+> prettyTCMPatternList (fromSplitPatterns ps)
]
debugPlugged delta' ps' = do
liftTCM $ reportSDoc "tc.cover.split.con" 20 $
inTopContext $ addContext delta' $ nest 2 $ vcat
[ "ps' =" <+> do prettyTCMPatternList $ fromSplitPatterns ps'
]
data InsertTrailing
= DoInsertTrailing
| DontInsertTrailing
deriving (Eq, Show)
data AllowPartialCover
= YesAllowPartialCover
| NoAllowPartialCover
deriving (Eq, Show)
splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd c x =
split' CheckEmpty Inductive NoAllowPartialCover DontInsertTrailing c (BlockingVar x [] [] True False)
splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)
splitLast ind tel ps = split ind NoAllowPartialCover sc (BlockingVar 0 [] [] True False)
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' NoCheckEmpty ind allowPartialCover DoInsertTrailing 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 = indexWithDefault __IMPOSSIBLE__ (telVars (size tel) tel) k
data CheckEmpty = CheckEmpty | NoCheckEmpty
split' :: CheckEmpty
-> Induction
-> AllowPartialCover
-> InsertTrailing
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' checkEmpty ind allowPartialCover inserttrailing
sc@(SClause tel ps _ cps target) (BlockingVar x pcons' plits overlap lazy) =
liftTCM $ runExceptT $ do
debugInit tel x ps cps
(n, t, delta1, delta2) <- do
let (tel1, dom : tel2) = splitAt (size tel - x - 1) $ telToList tel
return (fst $ unDom dom, snd <$> dom, telFromList tel1, telFromList tel2)
let computeNeighborhoods = do
(dr, d, pars, ixs, cons', isHIT) <- inContextOfT $ isDatatype ind t
cons <- case checkEmpty of
CheckEmpty -> ifM (liftTCM $ inContextOfT $ isEmptyType $ unDom t) (pure []) (pure cons')
NoCheckEmpty -> pure cons'
mns <- forM cons $ \ con -> fmap (SplitCon con,) <$>
computeNeighbourhood delta1 n delta2 d pars ixs x tel ps cps con
hcompsc <- if isHIT && inserttrailing == DoInsertTrailing
then computeHCompSplit delta1 n delta2 d pars ixs x tel ps cps
else return Nothing
return ( dr
, not (null ixs)
, catMaybes (mns ++ [hcompsc])
)
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 (PatternInfo 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 (IsData, False, ns ++ [ ca ])
(dr, isIndexed, ns) <- if null pcons' && not (null plits)
then computeLitNeighborhoods
else computeNeighborhoods
ns <- case target of
Just a -> forM ns $ \ (con, sc) -> lift $ (con,) <$> fixTargetType sc a
Nothing -> return ns
ns <- case inserttrailing of
DontInsertTrailing -> return ns
DoInsertTrailing -> lift $ forM ns $ \(con,sc) ->
(con,) . snd <$> insertTrailingArgs sc
propArrowRel <- isPropM t `and2M`
maybe (return True) (not <.> isPropM) target
mHCompName <- getPrimitiveName' builtinHComp
withoutK <- collapseDefault . optWithoutK <$> pragmaOptions
erased <- asksTC hasQuantity0
reportSLn "tc.cover.split" 60 $ "We are in erased context = " ++ show erased
let erasedError causedByWithoutK =
throwError . ErasedDatatype causedByWithoutK =<<
do liftTCM $ inContextOfT $ buildClosure (unDom t)
case ns of
[] -> do
let absurdp = VarP (PatternInfo 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
}
(_ : _) | dr == IsData && propArrowRel ->
throwError . IrrelevantDatatype =<< do liftTCM $ inContextOfT $ buildClosure (unDom t)
(_ : _ : _) | not erased && not (usableQuantity t) ->
erasedError False
[_] | not erased && not (usableQuantity t) &&
withoutK && isIndexed ->
erasedError True
_ -> do
let ptags = map (SplitCon . conName) pcons' ++ map SplitLit plits
let inferred_tags = maybe Set.empty (Set.singleton . SplitCon) mHCompName
let all_tags = Set.fromList ptags `Set.union` inferred_tags
when (allowPartialCover == NoAllowPartialCover && overlap == False) $
for_ ns $ \(tag, sc) -> do
when (not $ tag `Set.member` all_tags) $ do
isImpossibleClause <- liftTCM $ isEmptyTel $ scTel sc
unless isImpossibleClause $ do
liftTCM $ reportSDoc "tc.cover" 10 $ vcat
[ text "Missing case for" <+> prettyTCM tag
, nest 2 $ prettyTCM sc
]
throwError (GenericSplitError "precomputed set of constructors does not cover all cases")
liftTCM $ checkSortOfSplitVar dr (unDom t) target
return $ Right $ Covering (lookupPatternVar sc x) ns
where
inContextOfT, inContextOfDelta2 :: (MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) => tcm a -> tcm a
inContextOfT = addContext tel . escapeContext __IMPOSSIBLE__ (x + 1)
inContextOfDelta2 = addContext tel . escapeContext __IMPOSSIBLE__ x
debugInit tel x ps cps = liftTCM $ inTopContext $ do
reportSDoc "tc.cover.top" 10 $ vcat
[ "TypeChecking.Coverage.split': split"
, nest 2 $ vcat
[ "tel =" <+> prettyTCM tel
, "x =" <+> prettyTCM x
, "ps =" <+> do addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
, "cps =" <+> prettyTCM cps
]
]
reportSDoc "tc.cover.top" 60 $ vcat
[ "TypeChecking.Coverage.split': split"
, nest 2 $ vcat
[ "tel =" <+> (text . show) tel
, "x =" <+> (text . show) x
, "ps =" <+> (text . show) ps
, "cps =" <+> (text . show) cps
]
]
debugHoleAndType delta1 delta2 s ps t =
liftTCM $ reportSDoc "tc.cover.top" 10 $ nest 2 $ vcat $
[ "p =" <+> text (patVarNameToString s)
, "ps =" <+> prettyTCMPatternList ps
, "delta1 =" <+> prettyTCM delta1
, "delta2 =" <+> inContextOfDelta2 (prettyTCM delta2)
, "t =" <+> inContextOfT (prettyTCM t)
]
splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult f sc = do
caseMaybeM (splitResultPath f sc)
((fmap . fmap) splitClauses $ splitResultRecord f sc)
(return . Right . (:[]))
splitResultPath :: QName -> SplitClause -> TCM (Maybe SplitClause)
splitResultPath f sc@(SClause tel ps _ _ target) = do
caseMaybe target (return Nothing) $ \ t -> do
caseMaybeM (isPath (unDom t)) (return Nothing) $ \ _ -> do
(TelV i b, boundary) <- telViewUpToPathBoundary' 1 (unDom t)
let tel' = abstract tel i
rho = raiseS 1
ps' = applySubst rho (scPats sc) ++ telePatterns i boundary
cps' = applySubst rho (scCheckpoints sc)
target' = Just $ b <$ t
return . Just $ SClause tel' ps' idS cps' target'
splitResultRecord :: QName -> SplitClause -> TCM (Either SplitError Covering)
splitResultRecord f sc@(SClause tel ps _ _ target) = do
reportSDoc "tc.cover.split" 10 $ vcat
[ "splitting result:"
, nest 2 $ "f =" <+> prettyTCM f
, nest 2 $ "target =" <+> (addContext tel $ maybe empty prettyTCM target)
]
let failure = return . Left
caseMaybe target (failure CosplitNoTarget) $ \ t -> do
isR <- addContext tel $ isRecordType $ unDom 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 $ fromSplitPatterns ps
let self = defaultArg $ Def f [] `applyE` es
pargs = vs ++ [self]
fieldValues = for fs $ \ proj -> unArg self `applyE` [Proj ProjSystem (unDom proj)]
reportSDoc "tc.cover" 20 $ addContext tel $ sep
[ text "we are self =" <+> prettyTCM (unArg self)
, text " field values =" <+> prettyTCM fieldValues
]
let n = defaultArg $ permRange $ fromMaybe __IMPOSSIBLE__ $ dbPatPerm $ fromSplitPatterns ps
projOrigin <- ifM (optPostfixProjections <$> pragmaOptions) (return ProjPostfix) (return ProjPrefix)
Right . Covering n <$> do
forM (zip fs $ List.inits fieldValues) $ \ (proj, prevFields) -> do
dType <- defType <$> do getConstInfo $ unDom proj
let
fieldSub = reverse (map unArg vs ++ prevFields) ++# EmptyS __IMPOSSIBLE__
proj' = applySubst fieldSub proj
target' = Just $ proj' $> dType `piApply` pargs
projArg = fmap (Named Nothing . ProjP projOrigin) $ argFromDom $ setHiding NotHidden proj
sc' = sc { scPats = scPats sc ++ [projArg]
, scSubst = idS
, scTarget = target'
}
reportSDoc "tc.cover.copattern" 40 $ vcat
[ "fieldSub for" <+> prettyTCM (unDom proj)
, nest 2 $ pretty fieldSub ]
return (SplitCon (unDom proj), sc')
_ -> addContext tel $ do
buildClosure (unDom t) >>= failure . CosplitNoRecordType
instance PrettyTCM SplitClause where
prettyTCM (SClause tel pats sigma cps target) = sep
[ "SplitClause"
, nest 2 $ vcat
[ "tel =" <+> prettyTCM tel
, "pats =" <+> sep (map (prettyTCM . namedArg) pats)
, "subst =" <+> prettyTCM sigma
, "checkpoints =" <+> prettyTCM cps
, "target =" <+> do
caseMaybe target empty $ \ t -> do
addContext tel $ prettyTCM t
]
]