{-# 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.Arrow (second)
import Control.Monad
import Control.Monad.Reader
import Control.Monad.Trans ( lift )
import Data.Either (lefts)
import Data.Foldable (for_)
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.Names
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Primitive.Cubical
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.Coverage.Match
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Conversion (tryConversion, equalType, equalTermOnFace)
import Agda.TypeChecking.Datatypes (getConForm)
import {-# SOURCE #-} Agda.TypeChecking.Empty ( checkEmptyTel, isEmptyTel, isEmptyType )
import Agda.TypeChecking.Free
import Agda.TypeChecking.Irrelevance
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.Telescope.Path
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.Function
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.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
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 $ 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 qss noex <- cover f cs sc
noex <- return $ List.filter (< length cs) $ Set.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 -> enterClosure cl $ \ 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
, clauseUnreachable = Just False
}
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) $
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 (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
CoverResult { coverMissingClauses = missing } <- cover f cs sc
return $ null missing
data CoverResult = CoverResult
{ coverSplitTree :: SplitTree
, coverUsedClauses :: Set Nat
, coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
, coverPatterns :: [Closure Clause]
, coverNoExactClauses :: Set Nat
}
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 $ "tel =" <+> prettyTCM tel
, nest 2 $ "ps =" <+> do addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
, nest 2 $ "target =" <+> do addContext tel $ maybe (text "<none>") prettyTCM target
, nest 2 $ "target sort =" <+> do addContext tel $ maybe (text "<none>") (prettyTCM . getSort . unArg) 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 Set.empty
else Set.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)) (Set.singleton i) [] [cl] noExactClause
No -> do
reportSLn "tc.cover" 20 $ "pattern is not covered"
case fmap getHiding target of
Just h | isInstance h -> do
cl <- inferMissingClause f sc
return $ CoverResult (SplittingDone (size tel)) Set.empty [] [cl] Set.empty
_ -> do
let ps' = fromSplitPatterns ps
return $ CoverResult (SplittingDone (size tel)) Set.empty [(tel, ps')] [] Set.empty
Block res bs -> trySplitRes res (null bs) $ 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
typeError $ SplitError err
where
applyCl :: SplitClause -> Clause -> [(Nat, SplitPattern)] -> TCM (Closure Clause)
applyCl SClause{scTel = tel, scCheckpoints = cps} cl mps
= addContext tel
$ locallyTC eCheckpoints (const cps)
$ checkpoint IdS $ do
reportSDoc "tc.cover.applyCl" 40 $ "applyCl"
reportSDoc "tc.cover.applyCl" 40 $ "tel =" <+> prettyTCM tel
reportSDoc "tc.cover.applyCl" 40 $ "ps =" <+> pretty (namedClausePats cl)
reportSDoc "tc.cover.applyCl" 40 $ "mps =" <+> pretty mps
reportSDoc "tc.cover.applyCl" 40 $ "s =" <+> pretty s
reportSDoc "tc.cover.applyCl" 40 $ "new ps =" <+> pretty (s `applySubst` namedClausePats cl)
buildClosure $
Clause { clauseLHSRange = clauseLHSRange cl
, clauseFullRange = clauseFullRange cl
, clauseTel = tel
, namedClausePats = s `applySubst` namedClausePats cl
, clauseBody = (s `applyPatSubst`) <$> clauseBody cl
, clauseType = (s `applyPatSubst`) <$> clauseType cl
, clauseCatchall = clauseCatchall cl
, clauseUnreachable = clauseUnreachable 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)) Set.empty [] qs Set.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 trees'
return $ CoverResult tree (Set.unions useds) (concat psss) (concat qsss) (Set.unions noex)
trySplitRes
:: BlockedOnResult
-> Bool
-> TCM CoverResult
-> TCM CoverResult
trySplitRes NotBlockedOnResult finalSplit cont
| finalSplit = __IMPOSSIBLE__
| otherwise = cont
trySplitRes (BlockedOnApply IsApply) finalSplit cont
| finalSplit = __IMPOSSIBLE__
| otherwise = cont
trySplitRes (BlockedOnApply IsIApply) finalSplit cont
= do
caseMaybeM (splitResultPath f sc) fallback $ \ sc ->
cover f cs . snd =<< fixTarget sc
where
fallback | finalSplit = __IMPOSSIBLE__
| otherwise = cont
trySplitRes (BlockedOnProj True) finalSplit cont
| finalSplit = typeError $ SplitError CosplitCatchall
| otherwise = cont
trySplitRes (BlockedOnProj False) finalSplit cont = do
reportSLn "tc.cover" 20 $ "blocked by projection pattern"
mcov <- splitResultRecord f sc
case mcov of
Left err
| finalSplit -> typeError $ SplitError err
| otherwise -> cont
Right (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
qsss = map coverPatterns results
noex = map coverNoExactClauses results
tree = SplitAt n $ zip projs trees
return $ CoverResult tree (Set.unions useds) (concat psss) (concat qsss) (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__
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) [(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 (unArg 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
, clauseUnreachable = Just False
}
addClauses f [cl]
return cl
createMissingHCompClause _ _ _ _ (SClause _ _ _ _ Nothing) = __IMPOSSIBLE__
inferMissingClause
:: QName
-> SplitClause
-> TCM (Closure 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
cl <- addContext tel
$ locallyTC eCheckpoints (const cps)
$ checkpoint IdS $ do
(_x, rhs) <- case getHiding t of
Instance{} -> newInstanceMeta "" (unArg t)
Hidden -> __IMPOSSIBLE__
NotHidden -> __IMPOSSIBLE__
buildClosure $
Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
, namedClausePats = fromSplitPatterns ps
, clauseBody = Just rhs
, clauseType = Just t
, clauseCatchall = False
, clauseUnreachable = Just False
}
addClauses f [clValue cl]
return 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 (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, dataInduction = i}
| i == CoInductive && ind /= CoInductive ->
throw CoinductiveDatatype
| 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
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
[ "split clause telescope: " <+> prettyTCM sctel
, "old patterns : " <+> do
addContext sctel $ prettyTCMPatternList $ fromSplitPatterns ps
]
reportSDoc "tc.cover.target" 60 $ sep
[ "substitution : " <+> prettyTCM sigma
]
reportSDoc "tc.cover.target" 30 $ sep
[ "target type before substitution (variables may be wrong): " <+> do
addContext sctel $ prettyTCM a
]
(TelV tel b) <- telViewUpTo (-1) $ applySplitPSubst sigma $ unArg a
reportSDoc "tc.cover.target" 15 $ sep
[ "target type telescope (after substitution): " <+> do
addContext sctel $ prettyTCM tel
, "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
[ "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 PatOSystem hCompName . map (setOrigin Inserted) $
map (fmap unnamed) [setHiding Hidden $ defaultArg $ applySubst rho1 $ DotP PatOSystem $ dlvl
,setHiding Hidden $ defaultArg $ applySubst rho1 $ DotP PatOSystem $ 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)
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 rho0' = toSplitPSubst rho0
let (rho1,rho2) = splitS (size gamma) $ rho0'
let cpi = noConPatternInfo{ conPRecord = Just PatOSplit }
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 $ 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
, "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 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' CheckEmpty 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' NoCheckEmpty 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 = indexWithDefault __IMPOSSIBLE__ (telVars (size tel) tel) k
data CheckEmpty = CheckEmpty | NoCheckEmpty
split' :: CheckEmpty
-> Induction
-> AllowPartialCover
-> FixTarget
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' checkEmpty 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 : 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 then case fixtarget of YesFixTarget -> computeHCompSplit delta1 n delta2 d pars ixs x tel ps cps; _ -> return Nothing
else return Nothing
return $ (dr, 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 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 , ns ++ [ ca ])
(dr, 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 }
propArrowRel <- isPropM t `and2M`
maybe (return True) (not <.> isPropM) target
mHCompName <- getPrimitiveName' builtinHComp
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
}
(_ : _) | dr == IsData && propArrowRel ->
throwError . IrrelevantDatatype =<< do liftTCM $ inContextOfT $ buildClosure (unDom t)
(_ : _ : _) | not (usableQuantity t) ->
throwError . ErasedDatatype =<< do liftTCM $ inContextOfT $ buildClosure (unDom t)
_ -> 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, 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
[ "TypeChecking.Coverage.split': split"
, nest 2 $ vcat
[ "tel =" <+> prettyTCM tel
, "x =" <+> prettyTCM x
, "ps =" <+> do addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
, "cps =" <+> prettyTCM 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 (unArg t)) (return Nothing) $ \ _ -> do
(TelV i b, boundary) <- telViewUpToPathBoundary' 1 (unArg 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 $ 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 $ 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')
_ -> addContext tel $ do
buildClosure (unArg 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
]
]