{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeApplications #-}
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.Except
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 qualified Data.Set as Set
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Agda.Benchmarking as Bench
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal hiding (DataOrRecord)
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Translation.InternalToAbstract (NamedClause(..))
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Rules.LHS (DataOrRecord, 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.Coverage.SplitClause
import Agda.TypeChecking.Coverage.Cubical
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.MetaVars
import Agda.TypeChecking.Warnings
import Agda.Interaction.Options
import Agda.Utils.Either
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.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Control.Monad.State
type CoverM = ExceptT SplitError TCM
coverageCheck
:: QName
-> Type
-> [Clause]
-> TCM SplitTree
coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
coverageCheck QName
f Type
t [Clause]
cs = do
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.top" Int
30 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"entering coverageCheck for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
f
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
75 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" of type (raw): " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) Type
t
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
45 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" of type: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
TelV gamma a <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo (-Int
1) Type
t
reportSLn "tc.cover.top" 30 $ "coverageCheck: computed telView"
let
n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma
xs = (NamedArg SplitPattern -> NamedArg SplitPattern)
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> NamedArg SplitPattern -> NamedArg SplitPattern
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) ([NamedArg SplitPattern] -> [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg SplitPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
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 = Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
gamma [NamedArg SplitPattern]
xs Substitution' SplitPattern
forall a. Substitution' a
idS Map CheckpointId (Substitution' Term)
checkpoints (Maybe (Dom Type) -> SplitClause)
-> Maybe (Dom Type) -> SplitClause
forall a b. (a -> b) -> a -> b
$ Dom Type -> Maybe (Dom Type)
forall a. a -> Maybe a
Just (Dom Type -> Maybe (Dom Type)) -> Dom Type -> Maybe (Dom Type)
forall a b. (a -> b) -> a -> b
$ Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
a
reportSDoc "tc.cover.top" 10 $ do
let prCl Clause
cl = Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
cl) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
NAPs -> m Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList (NAPs -> m Doc) -> NAPs -> m Doc
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
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 (\ Clause
cl -> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
cl) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList (NAPs -> TCMT IO Doc) -> NAPs -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl) qss
]
opts <- pragmaOptions
when (isJust (optCubical opts) || optKeepCoveringClauses opts) $
modifySignature $ updateDefinition f $ updateTheDef $ updateCovering $ const qss
pss <- ifNotM (optInferAbsurdClauses <$> pragmaOptions) (pure pss) $
flip filterM pss $ \(Telescope
tel,NAPs
ps) ->
TCMT IO (Either ErrorNonEmpty Int)
-> (ErrorNonEmpty -> TCMT IO Bool)
-> (Int -> TCMT IO Bool)
-> TCMT IO Bool
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (Range -> Telescope -> TCMT IO (Either ErrorNonEmpty Int)
checkEmptyTel Range
forall a. Range' a
noRange Telescope
tel) (\ ErrorNonEmpty
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) ((Int -> TCMT IO Bool) -> TCMT IO Bool)
-> (Int -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \ Int
l -> do
let i :: Int
i = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
l
let sub :: PatternSubstitution
sub = Int -> DeBruijnPattern -> PatternSubstitution
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i (DeBruijnPattern -> PatternSubstitution)
-> DeBruijnPattern -> PatternSubstitution
forall a b. (a -> b) -> a -> b
$ Int -> DeBruijnPattern
absurdP Int
i
let cl :: Clause
cl = Clause { clauseLHSRange :: Range
clauseLHSRange = Range
forall a. Range' a
noRange
, clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
, clauseTel :: Telescope
clauseTel = Telescope
tel
, namedClausePats :: NAPs
namedClausePats = Substitution' (SubstArg NAPs) -> NAPs -> NAPs
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
Substitution' (SubstArg NAPs)
sub NAPs
ps
, clauseBody :: Maybe Term
clauseBody = Maybe Term
forall a. Maybe a
Nothing
, clauseType :: Maybe (Arg Type)
clauseType = Maybe (Arg Type)
forall a. Maybe a
Nothing
, clauseCatchall :: Bool
clauseCatchall = Bool
True
, clauseExact :: Maybe Bool
clauseExact = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseRecursive :: Maybe Bool
clauseRecursive = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
}
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.missing" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"adding missing absurd clause"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ QNamed Clause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QNamed Clause -> m Doc
prettyTCM (QNamed Clause -> TCMT IO Doc) -> QNamed Clause -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
f Clause
cl
]
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.missing" Int
80 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"l = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
l
, TCMT IO Doc
"i = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
i
, TCMT IO Doc
"cl = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QNamed Clause -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
f Clause
cl)
]
QName -> [Clause] -> TCMT IO ()
forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
f [Clause
cl]
Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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) $ \ (Int
i, Clause
cl) -> let
unreachable :: Bool
unreachable = Int
i Int -> IntSet -> Bool
`IntSet.notMember` IntSet
used
exact :: Bool
exact = Int
i Int -> IntSet -> Bool
`IntSet.notMember` ([Int] -> IntSet
IntSet.fromList [Int]
noex)
in (Bool -> Int -> Maybe Int
forall a. Bool -> a -> Maybe a
boolToMaybe Bool
unreachable Int
i, Clause
cl
{ clauseUnreachable = Just unreachable
, clauseExact = Just exact
})
let is = [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
is0
reportSDoc "tc.cover.top" 10 $ vcat
[ text $ "unreachable clauses: " ++ if null is then "(none)" else show is
]
modifyFunClauses f $ \ [Clause]
cs0 -> [Clause]
cs1 [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ Int -> [Clause] -> [Clause]
forall a. Int -> [a] -> [a]
drop ([Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cs1) [Clause]
cs0
unless (null is) $ do
let unreached = (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseUnreachable) [Clause]
cs1
let ranges = (Clause -> Range) -> [Clause] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Range
clauseFullRange [Clause]
unreached
setCurrentRange ranges $ warning $ UnreachableClauses f ranges
let noexclauses = [Int] -> (Int -> Maybe Clause) -> [Clause]
forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [Int]
noex ((Int -> Maybe Clause) -> [Clause])
-> (Int -> Maybe Clause) -> [Clause]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
let cl :: Clause
cl = Clause -> [Clause] -> Int -> Clause
forall a. a -> [a] -> Int -> a
indexWithDefault Clause
forall a. HasCallStack => a
__IMPOSSIBLE__ [Clause]
cs1 Int
i
if Clause -> Bool
clauseCatchall Clause
cl then Maybe Clause
forall a. Maybe a
Nothing else Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
cl
unless (null noexclauses) $ do
setCurrentRange (map clauseLHSRange noexclauses) $
warning $ CoverageNoExactSplit f $ noexclauses
return splitTree
isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool
isCovered :: QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause]
cs SplitClause
sc = do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.isCovered" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"isCovered"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"f = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
, TCMT IO Doc
"cs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (Clause -> TCMT IO Doc) -> Clause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedClause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> TCMT IO Doc)
-> (Clause -> NamedClause) -> Clause -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True) [Clause]
cs)
, TCMT IO Doc
"sc = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> SplitClause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => SplitClause -> m Doc
prettyTCM SplitClause
sc
]
]
(_ , sc') <- Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
True SplitClause
sc
CoverResult { coverMissingClauses = missing } <- cover f cs sc'
return $ null missing
TCMT IO Bool -> (TCErr -> TCMT IO Bool) -> TCMT IO Bool
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
cover :: QName -> [Clause] -> SplitClause ->
TCM CoverResult
cover :: QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs sc :: SplitClause
sc@(SClause Telescope
tel [NamedArg SplitPattern]
ps Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
_ Maybe (Dom Type)
target) = TCM CoverResult -> TCM CoverResult
forall a. TCM a -> TCM a
updateRelevance (TCM CoverResult -> TCM CoverResult)
-> TCM CoverResult -> TCM CoverResult
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.cover" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checking coverage of pattern:"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ SplitClause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => SplitClause -> m Doc
prettyTCM SplitClause
sc
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target sort =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
-> (Dom Type -> TCMT IO Doc) -> Maybe (Dom Type) -> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"<none>") (Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM (Sort -> TCMT IO Doc)
-> (Dom Type -> Sort) -> Dom Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Sort
forall a. LensSort a => a -> Sort
getSort (Type -> Sort) -> (Dom Type -> Type) -> Dom Type -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Type
forall t e. Dom' t e -> e
unDom) Maybe (Dom Type)
target
]
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.cover" Int
80 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"raw target =\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe (Dom Type) -> [Char]
forall a. Show a => a -> [Char]
show Maybe (Dom Type)
target
[Char] -> Int -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.cover.matching" Int
20 (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.matching" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"clauses when matching:"
[Clause] -> (Clause -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Clause]
cs ((Clause -> TCMT IO ()) -> TCMT IO ())
-> (Clause -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ Clause
c -> do
let gamma :: Telescope
gamma = Clause -> Telescope
clauseTel Clause
c
ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
c
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.matching" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"ps :" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [DeBruijnPattern] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [DeBruijnPattern] -> m Doc
prettyTCM ((Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NAPs
ps)
[Clause]
-> [NamedArg SplitPattern]
-> TCMT IO (Match (Int, [(Int, SplitPattern)]))
forall (m :: * -> *).
PureTCM m =>
[Clause]
-> [NamedArg SplitPattern]
-> m (Match (Int, [(Int, SplitPattern)]))
match [Clause]
cs [NamedArg SplitPattern]
ps TCMT IO (Match (Int, [(Int, SplitPattern)]))
-> (Match (Int, [(Int, SplitPattern)]) -> TCM CoverResult)
-> TCM CoverResult
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Yes (Int
i,[(Int, SplitPattern)]
mps) -> do
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.cover" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"pattern covered by clause " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.cover" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"with mps = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [(Int, SplitPattern)] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, SplitPattern)]
mps
exact <- [(Int, SplitPattern)]
-> ((Int, SplitPattern) -> TCMT IO Bool) -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM [(Int, SplitPattern)]
mps (((Int, SplitPattern) -> TCMT IO Bool) -> TCMT IO Bool)
-> ((Int, SplitPattern) -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ SplitPattern -> TCMT IO Bool
forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern (SplitPattern -> TCMT IO Bool)
-> ((Int, SplitPattern) -> SplitPattern)
-> (Int, SplitPattern)
-> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, SplitPattern) -> SplitPattern
forall a b. (a, b) -> b
snd
let cl0 = Clause -> [Clause] -> Int -> Clause
forall a. a -> [a] -> Int -> a
indexWithDefault Clause
forall a. HasCallStack => a
__IMPOSSIBLE__ [Clause]
cs Int
i
cl <- applyCl sc cl0 mps
return $ CoverResult
{ coverSplitTree = SplittingDone (size tel)
, coverUsedClauses = singleton i
, coverMissingClauses = []
, coverPatterns = [cl]
, coverNoExactClauses = if exact then empty else singleton i
}
Match (Int, [(Int, SplitPattern)])
No -> do
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"pattern is not covered"
let infer :: Dom' a e -> Bool
infer Dom' a e
dom = Dom' a e -> Bool
forall a. LensHiding a => a -> Bool
isInstance Dom' a e
dom Bool -> Bool -> Bool
|| Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Dom' a e -> Maybe a
forall t e. Dom' t e -> Maybe t
domTactic Dom' a e
dom)
if Bool -> (Dom Type -> Bool) -> Maybe (Dom Type) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Dom Type -> Bool
forall {a} {e}. Dom' a e -> Bool
infer Maybe (Dom Type)
target
then do
cl <- QName -> SplitClause -> TCM Clause
inferMissingClause QName
f SplitClause
sc
return $ CoverResult (SplittingDone (size tel)) empty [] [cl] empty
else do
let ps' :: NAPs
ps' = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
CoverResult -> TCM CoverResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoverResult -> TCM CoverResult) -> CoverResult -> TCM CoverResult
forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult (Int -> SplitTree
forall a. Int -> SplitTree' a
SplittingDone (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel)) IntSet
forall a. Null a => a
empty [(Telescope
tel, NAPs
ps')] [] IntSet
forall a. Null a => a
empty
Block BlockedOnResult
res BlockingVars
bs -> BlockedOnResult
-> Bool
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
-> TCM CoverResult
trySplitRes BlockedOnResult
res (BlockingVars -> Bool
forall a. Null a => a -> Bool
null BlockingVars
bs) SplitError -> TCM CoverResult
forall a. SplitError -> TCM a
splitError (TCM CoverResult -> TCM CoverResult)
-> TCM CoverResult -> TCM CoverResult
forall a b. (a -> b) -> a -> b
$ do
Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BlockingVars -> Bool
forall a. Null a => a -> Bool
null BlockingVars
bs) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.strategy" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"blocking vars = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ BlockingVars -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow BlockingVars
bs
xs <- BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy BlockingVars
bs Telescope
tel
continue xs NoAllowPartialCover $ \ SplitError
_err -> do
BlockingVars
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue BlockingVars
xs AllowPartialCover
YesAllowPartialCover ((SplitError -> TCM CoverResult) -> TCM CoverResult)
-> (SplitError -> TCM CoverResult) -> TCM CoverResult
forall a b. (a -> b) -> a -> b
$ \ SplitError
err -> do
SplitError -> TCM CoverResult
forall a. SplitError -> TCM a
splitError SplitError
err
where
splitError :: SplitError -> TCM a
splitError :: forall a. SplitError -> TCM a
splitError = TCM a -> TCM a
forall a. TCM a -> TCM a
withRangeOfCandidateClauses (TCM a -> TCM a) -> (SplitError -> TCM a) -> SplitError -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM a)
-> (SplitError -> TypeError) -> SplitError -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitError -> TypeError
SplitError
withRangeOfCandidateClauses :: TCM a -> TCM a
withRangeOfCandidateClauses :: forall a. TCM a -> TCM a
withRangeOfCandidateClauses TCM a
cont = do
cands <- ((Clause, Match (DList (Int, SplitPattern))) -> Maybe Clause)
-> [(Clause, Match (DList (Int, SplitPattern)))] -> [Clause]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Clause -> Match (DList (Int, SplitPattern)) -> Maybe Clause)
-> (Clause, Match (DList (Int, SplitPattern))) -> Maybe Clause
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Clause -> Match (DList (Int, SplitPattern)) -> Maybe Clause
forall a. Clause -> Match a -> Maybe Clause
notNo) ([(Clause, Match (DList (Int, SplitPattern)))] -> [Clause])
-> ([Match (DList (Int, SplitPattern))]
-> [(Clause, Match (DList (Int, SplitPattern)))])
-> [Match (DList (Int, SplitPattern))]
-> [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Clause]
-> [Match (DList (Int, SplitPattern))]
-> [(Clause, Match (DList (Int, SplitPattern)))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Clause]
cs ([Match (DList (Int, SplitPattern))] -> [Clause])
-> TCMT IO [Match (DList (Int, SplitPattern))] -> TCMT IO [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Clause -> TCMT IO (Match (DList (Int, SplitPattern))))
-> [Clause] -> TCMT IO [Match (DList (Int, SplitPattern))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([NamedArg SplitPattern]
-> Clause -> TCMT IO (Match (DList (Int, SplitPattern)))
forall (m :: * -> *).
PureTCM m =>
[NamedArg SplitPattern]
-> Clause -> m (Match (DList (Int, SplitPattern)))
matchClause [NamedArg SplitPattern]
ps) [Clause]
cs
setCurrentRange cands cont
where
notNo :: Clause -> Match a -> Maybe Clause
notNo :: forall a. Clause -> Match a -> Maybe Clause
notNo Clause
c = \case
Yes{} -> Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
c
Block{} -> Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
c
No{} -> Maybe Clause
forall a. Maybe a
Nothing
renTeleFromNap :: SplitClause -> Clause -> Telescope
renTeleFromNap :: SplitClause -> Clause -> Telescope
renTeleFromNap SClause{scTel :: SplitClause -> Telescope
scTel = Telescope
tel, scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
sps} Clause
clause =
ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ State Int ListTel -> Int -> ListTel
forall s a. State s a -> s -> a
evalState ((Dom ([Char], Type) -> StateT Int Identity (Dom ([Char], Type)))
-> ListTel -> State Int ListTel
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Dom ([Char], Type) -> StateT Int Identity (Dom ([Char], Type))
upd (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel)) (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
offset)
where
ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
clause
offset :: Int
offset = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NAPs -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
sps) Int -> Int -> Int
forall a. Num a => a -> a -> a
- NAPs -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
ps
nameSuggest :: DeBruijnPattern -> IntMap ArgName
nameSuggest :: DeBruijnPattern -> IntMap [Char]
nameSuggest DeBruijnPattern
ps = ((DeBruijnPattern -> IntMap [Char])
-> DeBruijnPattern -> IntMap [Char])
-> DeBruijnPattern
-> (DeBruijnPattern -> IntMap [Char])
-> IntMap [Char]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DeBruijnPattern -> IntMap [Char])
-> DeBruijnPattern -> IntMap [Char]
forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern DeBruijnPattern
ps ((DeBruijnPattern -> IntMap [Char]) -> IntMap [Char])
-> (DeBruijnPattern -> IntMap [Char]) -> IntMap [Char]
forall a b. (a -> b) -> a -> b
$ \case
VarP PatternInfo
_ DBPatVar
i | DBPatVar -> [Char]
dbPatVarName DBPatVar
i [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ->
Int -> [Char] -> IntMap [Char]
forall a. Int -> a -> IntMap a
IntMap.singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
i) (DBPatVar -> [Char]
dbPatVarName DBPatVar
i)
IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
i | DBPatVar -> [Char]
dbPatVarName DBPatVar
i [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ->
Int -> [Char] -> IntMap [Char]
forall a. Int -> a -> IntMap a
IntMap.singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
i) (DBPatVar -> [Char]
dbPatVarName DBPatVar
i)
DeBruijnPattern
_ -> IntMap [Char]
forall a. Monoid a => a
mempty
suggestions :: IntMap [Char]
suggestions = (Arg (Named_ DeBruijnPattern) -> IntMap [Char])
-> NAPs -> IntMap [Char]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (DeBruijnPattern -> IntMap [Char]
nameSuggest (DeBruijnPattern -> IntMap [Char])
-> (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> IntMap [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named_ DeBruijnPattern -> DeBruijnPattern)
-> (Arg (Named_ DeBruijnPattern) -> Named_ DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern)
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ DeBruijnPattern) -> Named_ DeBruijnPattern
forall e. Arg e -> e
unArg) NAPs
ps
size :: Int
size = ListTel -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel)
upd :: Dom (ArgName , Type) -> State Int (Dom (ArgName , Type))
upd :: Dom ([Char], Type) -> StateT Int Identity (Dom ([Char], Type))
upd Dom ([Char], Type)
dom = (Int -> (Dom ([Char], Type), Int))
-> StateT Int Identity (Dom ([Char], Type))
forall a. (Int -> (a, Int)) -> StateT Int Identity a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state ((Int -> (Dom ([Char], Type), Int))
-> StateT Int Identity (Dom ([Char], Type)))
-> (Int -> (Dom ([Char], Type), Int))
-> StateT Int Identity (Dom ([Char], Type))
forall a b. (a -> b) -> a -> b
$ \Int
s -> do
case Int -> IntMap [Char] -> Maybe [Char]
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
s IntMap [Char]
suggestions of
Just [Char]
nm' -> ( Dom ([Char], Type)
dom{ domName = Just (WithOrigin CaseSplit (unranged nm'))
, unDom = (nm' , snd (unDom dom))
} , Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
Maybe [Char]
Nothing -> (Dom ([Char], Type)
dom , Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
applyCl :: SplitClause -> Clause -> [(Nat, SplitPattern)] -> TCM Clause
applyCl :: SplitClause -> Clause -> [(Int, SplitPattern)] -> TCM Clause
applyCl sc :: SplitClause
sc@SClause{scTel :: SplitClause -> Telescope
scTel = Telescope
pretel, scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
sps} Clause
cl [(Int, SplitPattern)]
mps
| Telescope
tel <- SplitClause -> Clause -> Telescope
renTeleFromNap SplitClause
sc Clause
cl = Telescope -> TCM Clause -> TCM Clause
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$ do
let ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
cl
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"applyCl"
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"pretel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
pretel
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
tel
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NAPs -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NAPs
ps
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Int, SplitPattern)] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, SplitPattern)]
mps
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"s =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> PatternSubstitution -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PatternSubstitution
s
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps[s] =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NAPs -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (PatternSubstitution
Substitution' (SubstArg NAPs)
s Substitution' (SubstArg NAPs) -> NAPs -> NAPs
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` NAPs
ps)
let extra :: NAPs
extra = Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
drop (NAPs -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
ps) (NAPs -> NAPs) -> NAPs -> NAPs
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
sps
n_extra :: Int
n_extra = NAPs -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
extra
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"extra =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NAPs -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NAPs
extra
mtv <- ((Arg Type -> TCMT IO (Arg (TelV Type)))
-> Maybe (Arg Type) -> TCMT IO (Maybe (Arg (TelV Type)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse ((Arg Type -> TCMT IO (Arg (TelV Type)))
-> Maybe (Arg Type) -> TCMT IO (Maybe (Arg (TelV Type))))
-> ((Type -> TCMT IO (TelV Type))
-> Arg Type -> TCMT IO (Arg (TelV Type)))
-> (Type -> TCMT IO (TelV Type))
-> Maybe (Arg Type)
-> TCMT IO (Maybe (Arg (TelV Type)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> TCMT IO (TelV Type))
-> Arg Type -> TCMT IO (Arg (TelV Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse) (Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
telViewUpToPath Int
n_extra) (Maybe (Arg Type) -> TCMT IO (Maybe (Arg (TelV Type))))
-> Maybe (Arg Type) -> TCMT IO (Maybe (Arg (TelV Type)))
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe (Arg Type)
clauseType Clause
cl
let ty = ((Arg (TelV Type) -> Arg Type)
-> Maybe (Arg (TelV Type)) -> Maybe (Arg Type)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Arg (TelV Type) -> Arg Type)
-> Maybe (Arg (TelV Type)) -> Maybe (Arg Type))
-> ((TelV Type -> Type) -> Arg (TelV Type) -> Arg Type)
-> (TelV Type -> Type)
-> Maybe (Arg (TelV Type))
-> Maybe (Arg Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TelV Type -> Type) -> Arg (TelV Type) -> Arg Type
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (([DeBruijnPattern] -> PatternSubstitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([DeBruijnPattern] -> [DeBruijnPattern]
forall a. [a] -> [a]
reverse ([DeBruijnPattern] -> [DeBruijnPattern])
-> [DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> NAPs -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg NAPs
extra) PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n_extra PatternSubstitution
s PatternSubstitution -> Type -> Type
forall a. TermSubst a => PatternSubstitution -> a -> a
`applyPatSubst`) (Type -> Type) -> (TelV Type -> Type) -> TelV Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TelV Type -> Type
forall a. TelV a -> a
theCore) Maybe (Arg (TelV Type))
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
, clauseExact = clauseExact cl
, clauseRecursive = clauseRecursive cl
, clauseUnreachable = clauseUnreachable cl
, clauseEllipsis = clauseEllipsis cl
, clauseWhereModule = clauseWhereModule cl
}
where
mps' :: Map Int DeBruijnPattern
mps' =
[(Int, DeBruijnPattern)] -> Map Int DeBruijnPattern
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, DeBruijnPattern)] -> Map Int DeBruijnPattern)
-> [(Int, DeBruijnPattern)] -> Map Int DeBruijnPattern
forall a b. (a -> b) -> a -> b
$
((Int, SplitPattern) -> (Int, DeBruijnPattern))
-> [(Int, SplitPattern)] -> [(Int, DeBruijnPattern)]
forall a b. (a -> b) -> [a] -> [b]
map ((SplitPattern -> DeBruijnPattern)
-> (Int, SplitPattern) -> (Int, DeBruijnPattern)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg (Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
-> (SplitPattern -> Arg (Named_ DeBruijnPattern))
-> SplitPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg SplitPattern -> Arg (Named_ DeBruijnPattern)
fromSplitPattern (NamedArg SplitPattern -> Arg (Named_ DeBruijnPattern))
-> (SplitPattern -> NamedArg SplitPattern)
-> SplitPattern
-> Arg (Named_ DeBruijnPattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitPattern -> NamedArg SplitPattern
forall a. a -> NamedArg a
defaultNamedArg)) [(Int, SplitPattern)]
mps
s :: PatternSubstitution
s = [DeBruijnPattern] -> PatternSubstitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Int] -> (Int -> DeBruijnPattern) -> [DeBruijnPattern]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (case Map Int DeBruijnPattern -> Maybe (Int, DeBruijnPattern)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax Map Int DeBruijnPattern
mps' of
Maybe (Int, DeBruijnPattern)
Nothing -> []
Just (Int
i, DeBruijnPattern
_) -> [Int
0..Int
i]) ((Int -> DeBruijnPattern) -> [DeBruijnPattern])
-> (Int -> DeBruijnPattern) -> [DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ \ Int
i ->
DeBruijnPattern -> Maybe DeBruijnPattern -> DeBruijnPattern
forall a. a -> Maybe a -> a
fromMaybe (Int -> DeBruijnPattern
forall a. DeBruijn a => Int -> a
deBruijnVar Int
i) (Int -> Map Int DeBruijnPattern -> Maybe DeBruijnPattern
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int DeBruijnPattern
mps'))
updateRelevance :: TCM a -> TCM a
updateRelevance :: forall a. TCM a -> TCM a
updateRelevance TCM a
cont =
Maybe (Dom Type) -> TCM a -> (Dom Type -> TCM a) -> TCM a
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target TCM a
cont ((Dom Type -> TCM a) -> TCM a) -> (Dom Type -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ Dom Type
b -> do
let m :: Modality
m = Dom Type -> Modality
forall a. LensModality a => a -> Modality
getModality Dom Type
b
Modality -> TCM a -> TCM a
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
m TCM a
cont
continue
:: [BlockingVar]
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue :: BlockingVars
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue BlockingVars
xs AllowPartialCover
allowPartialCover SplitError -> TCM CoverResult
handle = do
r <- (BlockingVar
-> TCMT IO (Either SplitError (Covering, BlockingVar)))
-> BlockingVars
-> TCMT IO (Either SplitError (Covering, BlockingVar))
forall (m :: * -> *) a err b.
Monad m =>
(a -> m (Either err b)) -> [a] -> m (Either err b)
altM1 (\ BlockingVar
x -> (Covering -> (Covering, BlockingVar))
-> Either SplitError Covering
-> Either SplitError (Covering, BlockingVar)
forall a b. (a -> b) -> Either SplitError a -> Either SplitError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,BlockingVar
x) (Either SplitError Covering
-> Either SplitError (Covering, BlockingVar))
-> TCMT IO (Either SplitError Covering)
-> TCMT IO (Either SplitError (Covering, BlockingVar))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCMT IO (Either SplitError Covering)
split Induction
Inductive AllowPartialCover
allowPartialCover SplitClause
sc BlockingVar
x) BlockingVars
xs
case r of
Left SplitError
err -> SplitError -> TCM CoverResult
handle SplitError
err
Right (Covering Arg Int
n [], BlockingVar
_) ->
do
let qs :: [a]
qs = []
CoverResult -> TCM CoverResult
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoverResult -> TCM CoverResult) -> CoverResult -> TCM CoverResult
forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult (Int -> SplitTree
forall a. Int -> SplitTree' a
SplittingDone (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel)) IntSet
forall a. Null a => a
empty [] [Clause]
forall a. [a]
qs IntSet
forall a. Null a => a
empty
Right (Covering Arg Int
n [(SplitTag, (SplitClause, IInfo))]
scs', BlockingVar
x) -> do
let scs :: [(SplitTag, SplitClause)]
scs = ((SplitTag, (SplitClause, IInfo)) -> (SplitTag, SplitClause))
-> [(SplitTag, (SplitClause, IInfo))] -> [(SplitTag, SplitClause)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SplitTag
t,(SplitClause
sc,IInfo
i)) -> (SplitTag
t,SplitClause
sc)) [(SplitTag, (SplitClause, IInfo))]
scs'
(results_trX, cs) <- QName
-> Arg Int
-> BlockingVar
-> SplitClause
-> [(SplitTag, (SplitClause, IInfo))]
-> [Clause]
-> TCM ([(SplitTag, CoverResult)], [Clause])
createMissingIndexedClauses QName
f Arg Int
n BlockingVar
x SplitClause
sc [(SplitTag, (SplitClause, IInfo))]
scs' [Clause]
cs
(scs, cs, results_hc) <- do
let fallback = ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
-> TCMT
IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(SplitTag, SplitClause)]
scs, [Clause]
cs, [])
caseMaybeM (getPrimitiveName' builtinHComp) fallback $ \ QName
comp -> do
let isComp :: SplitTag -> Bool
isComp = \case
SplitCon QName
c -> QName
comp QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
c
SplitTag
_ -> Bool
False
Maybe (SplitTag, SplitClause)
-> TCMT
IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
-> ((SplitTag, SplitClause)
-> TCMT
IO
([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)]))
-> TCMT
IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (((SplitTag, SplitClause) -> Bool)
-> [(SplitTag, SplitClause)] -> Maybe (SplitTag, SplitClause)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (SplitTag -> Bool
isComp (SplitTag -> Bool)
-> ((SplitTag, SplitClause) -> SplitTag)
-> (SplitTag, SplitClause)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitTag, SplitClause) -> SplitTag
forall a b. (a, b) -> a
fst) [(SplitTag, SplitClause)]
scs) TCMT
IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
fallback (((SplitTag, SplitClause)
-> TCMT
IO
([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)]))
-> TCMT
IO
([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)]))
-> ((SplitTag, SplitClause)
-> TCMT
IO
([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)]))
-> TCMT
IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
forall a b. (a -> b) -> a -> b
$ \ (SplitTag
sp, SplitClause
newSc) -> do
(res,cs') <- QName
-> Arg Int
-> BlockingVar
-> SplitClause
-> SplitClause
-> [Clause]
-> TCM ([(SplitTag, CoverResult)], [Clause])
createMissingHCompClause QName
f Arg Int
n BlockingVar
x SplitClause
sc SplitClause
newSc [Clause]
cs
let scs2 = ((SplitTag, SplitClause) -> Bool)
-> [(SplitTag, SplitClause)] -> [(SplitTag, SplitClause)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((SplitTag, SplitClause) -> Bool)
-> (SplitTag, SplitClause)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitTag -> Bool
isComp (SplitTag -> Bool)
-> ((SplitTag, SplitClause) -> SplitTag)
-> (SplitTag, SplitClause)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitTag, SplitClause) -> SplitTag
forall a b. (a, b) -> a
fst) [(SplitTag, SplitClause)]
scs
return (scs2,cs',res)
let results_extra = [(SplitTag, CoverResult)]
results_hc [(SplitTag, CoverResult)]
-> [(SplitTag, CoverResult)] -> [(SplitTag, CoverResult)]
forall a. [a] -> [a] -> [a]
++ [(SplitTag, CoverResult)]
results_trX
trees_extra = ((SplitTag, CoverResult) -> (SplitTag, SplitTree))
-> [(SplitTag, CoverResult)] -> [(SplitTag, SplitTree)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SplitTag
sp,CoverResult
cr) -> (SplitTag
sp, CoverResult -> SplitTree
coverSplitTree CoverResult
cr)) [(SplitTag, CoverResult)]
results_extra
results <- (++ map snd (results_extra)) <$> mapM ((cover f cs) . snd) scs
let trees = (CoverResult -> SplitTree) -> [CoverResult] -> [SplitTree]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> SplitTree
coverSplitTree [CoverResult]
results
useds = (CoverResult -> IntSet) -> [CoverResult] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverUsedClauses [CoverResult]
results
psss = (CoverResult -> [(Telescope, NAPs)])
-> [CoverResult] -> [[(Telescope, NAPs)]]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [(Telescope, NAPs)]
coverMissingClauses [CoverResult]
results
qsss = (CoverResult -> [Clause]) -> [CoverResult] -> [[Clause]]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [Clause]
coverPatterns [CoverResult]
results
noex = (CoverResult -> IntSet) -> [CoverResult] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverNoExactClauses [CoverResult]
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' = ((SplitTag, SplitClause) -> SplitTree -> (SplitTag, SplitTree))
-> [(SplitTag, SplitClause)]
-> [SplitTree]
-> [(SplitTag, SplitTree)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Int
-> [NamedArg SplitPattern]
-> (SplitTag, SplitClause)
-> SplitTree
-> (SplitTag, SplitTree)
etaRecordSplits (Arg Int -> Int
forall e. Arg e -> e
unArg Arg Int
n) [NamedArg SplitPattern]
ps) [(SplitTag, SplitClause)]
scs [SplitTree]
trees
tree = Arg Int -> LazySplit -> [(SplitTag, SplitTree)] -> SplitTree
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
n LazySplit
StrictSplit ([(SplitTag, SplitTree)]
trees' [(SplitTag, SplitTree)]
-> [(SplitTag, SplitTree)] -> [(SplitTag, SplitTree)]
forall a. [a] -> [a] -> [a]
++ [(SplitTag, SplitTree)]
trees_extra)
return $ CoverResult tree (IntSet.unions useds) (concat psss) (concat qsss) (IntSet.unions noex)
trySplitRes
:: BlockedOnResult
-> Bool
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
-> TCM CoverResult
trySplitRes :: BlockedOnResult
-> Bool
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
-> TCM CoverResult
trySplitRes BlockedOnResult
NotBlockedOnResult Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont
| Bool
finalSplit = TCM CoverResult
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise = TCM CoverResult
cont
trySplitRes (BlockedOnApply ApplyOrIApply
IsApply) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont = do
(tel, sc') <- Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
True SplitClause
sc
if null tel then
if finalSplit then __IMPOSSIBLE__
else cont
else cover f cs sc'
trySplitRes (BlockedOnApply ApplyOrIApply
IsIApply) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont
= do
TCMT IO (Maybe SplitClause)
-> TCM CoverResult
-> (SplitClause -> TCM CoverResult)
-> TCM CoverResult
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> SplitClause -> TCMT IO (Maybe SplitClause)
splitResultPath QName
f SplitClause
sc) TCM CoverResult
fallback ((SplitClause -> TCM CoverResult) -> TCM CoverResult)
-> (SplitClause -> TCM CoverResult) -> TCM CoverResult
forall a b. (a -> b) -> a -> b
$ (QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs (SplitClause -> TCM CoverResult)
-> ((Telescope, SplitClause) -> SplitClause)
-> (Telescope, SplitClause)
-> TCM CoverResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Telescope, SplitClause) -> SplitClause
forall a b. (a, b) -> b
snd) ((Telescope, SplitClause) -> TCM CoverResult)
-> (SplitClause -> TCM (Telescope, SplitClause))
-> SplitClause
-> TCM CoverResult
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
False
where
fallback :: TCM CoverResult
fallback | Bool
finalSplit = TCM CoverResult
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise = TCM CoverResult
cont
trySplitRes (BlockedOnProj Bool
True) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont
| Bool
finalSplit = SplitError -> TCM CoverResult
splitError SplitError
CosplitCatchall
| Bool
otherwise = TCM CoverResult
cont
trySplitRes (BlockedOnProj Bool
False) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont = do
[Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"blocked by projection pattern"
mcov <- QName -> SplitClause -> TCMT IO (Either SplitError Covering)
splitResultRecord QName
f SplitClause
sc
case mcov of
Left SplitError
err
| Bool
finalSplit -> SplitError -> TCM CoverResult
splitError SplitError
err
| Bool
otherwise -> TCM CoverResult
cont
Right (Covering Arg Int
n [(SplitTag, (SplitClause, IInfo))]
scs) -> do
(projs, results) <- [(SplitTag, CoverResult)] -> ([SplitTag], [CoverResult])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(SplitTag, CoverResult)] -> ([SplitTag], [CoverResult]))
-> TCMT IO [(SplitTag, CoverResult)]
-> TCMT IO ([SplitTag], [CoverResult])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
((SplitTag, SplitClause) -> TCMT IO (SplitTag, CoverResult))
-> [(SplitTag, SplitClause)] -> TCMT IO [(SplitTag, CoverResult)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((SplitClause -> TCM CoverResult)
-> (SplitTag, SplitClause) -> TCMT IO (SplitTag, CoverResult)
forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> (SplitTag, a) -> m (SplitTag, b)
traverseF ((SplitClause -> TCM CoverResult)
-> (SplitTag, SplitClause) -> TCMT IO (SplitTag, CoverResult))
-> (SplitClause -> TCM CoverResult)
-> (SplitTag, SplitClause)
-> TCMT IO (SplitTag, CoverResult)
forall a b. (a -> b) -> a -> b
$ QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs (SplitClause -> TCM CoverResult)
-> (SplitClause -> TCMT IO SplitClause)
-> SplitClause
-> TCM CoverResult
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< ((Telescope, SplitClause) -> SplitClause
forall a b. (a, b) -> b
snd ((Telescope, SplitClause) -> SplitClause)
-> (SplitClause -> TCM (Telescope, SplitClause))
-> SplitClause
-> TCMT IO SplitClause
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
False)) (((SplitTag, (SplitClause, IInfo)) -> (SplitTag, SplitClause))
-> [(SplitTag, (SplitClause, IInfo))] -> [(SplitTag, SplitClause)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SplitTag
t,(SplitClause
sc,IInfo
i)) -> (SplitTag
t,SplitClause
sc)) [(SplitTag, (SplitClause, IInfo))]
scs)
let trees = (CoverResult -> SplitTree) -> [CoverResult] -> [SplitTree]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> SplitTree
coverSplitTree [CoverResult]
results
useds = (CoverResult -> IntSet) -> [CoverResult] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverUsedClauses [CoverResult]
results
psss = (CoverResult -> [(Telescope, NAPs)])
-> [CoverResult] -> [[(Telescope, NAPs)]]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [(Telescope, NAPs)]
coverMissingClauses [CoverResult]
results
qsss = (CoverResult -> [Clause]) -> [CoverResult] -> [[Clause]]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [Clause]
coverPatterns [CoverResult]
results
noex = (CoverResult -> IntSet) -> [CoverResult] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverNoExactClauses [CoverResult]
results
tree = Arg Int -> LazySplit -> [(SplitTag, SplitTree)] -> SplitTree
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
n LazySplit
StrictSplit ([(SplitTag, SplitTree)] -> SplitTree)
-> [(SplitTag, SplitTree)] -> SplitTree
forall a b. (a -> b) -> a -> b
$ [SplitTag] -> [SplitTree] -> [(SplitTag, SplitTree)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SplitTag]
projs [SplitTree]
trees
return $ CoverResult tree (IntSet.unions useds) (concat psss) (concat qsss) (IntSet.unions noex)
gatherEtaSplits :: Int -> SplitClause
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
gatherEtaSplits :: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc []
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = [NamedArg SplitPattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise = []
gatherEtaSplits Int
n SplitClause
sc (NamedArg SplitPattern
p:[NamedArg SplitPattern]
ps) = case NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p of
VarP PatternInfo
_ SplitPatVar
x
| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 -> case SplitPattern
p' of
VarP PatternInfo
_ SplitPatVar
_ -> NamedArg SplitPattern
p NamedArg SplitPattern
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
DotP PatternInfo
_ Term
_ -> [NamedArg SplitPattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
ConP ConHead
_ ConPatternInfo
_ [NamedArg SplitPattern]
qs -> [NamedArg SplitPattern]
qs [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
LitP{} -> Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
ProjP{} -> [NamedArg SplitPattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP{} -> [NamedArg SplitPattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
DefP PatternInfo
_ QName
_ [NamedArg SplitPattern]
qs -> [NamedArg SplitPattern]
qs [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
| Bool
otherwise ->
(SplitPattern -> SplitPattern)
-> NamedArg SplitPattern -> NamedArg SplitPattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (\ SplitPattern
_ -> SplitPattern
p') NamedArg SplitPattern
p NamedArg SplitPattern
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
where p' :: SplitPattern
p' = Substitution' SplitPattern -> Int -> SplitPattern
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS (SplitClause -> Substitution' SplitPattern
scSubst SplitClause
sc) (Int -> SplitPattern) -> Int -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Int
splitPatVarIndex SplitPatVar
x
IApplyP{} ->
(SplitPattern -> SplitPattern)
-> NamedArg SplitPattern -> NamedArg SplitPattern
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (Substitution' (SubstArg SplitPattern)
-> SplitPattern -> SplitPattern
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (SplitClause -> Substitution' SplitPattern
scSubst SplitClause
sc)) NamedArg SplitPattern
p NamedArg SplitPattern
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
DotP PatternInfo
_ Term
_ -> NamedArg SplitPattern
p NamedArg SplitPattern
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
ConP ConHead
_ ConPatternInfo
_ [NamedArg SplitPattern]
qs -> Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc ([NamedArg SplitPattern]
qs [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern]
ps)
DefP PatternInfo
_ QName
_ [NamedArg SplitPattern]
qs -> Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc ([NamedArg SplitPattern]
qs [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern]
ps)
LitP{} -> Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc [NamedArg SplitPattern]
ps
ProjP{} -> Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc [NamedArg SplitPattern]
ps
addEtaSplits :: Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits :: Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits Int
k [] SplitTree
t = SplitTree
t
addEtaSplits Int
k (NamedArg SplitPattern
p:[NamedArg SplitPattern]
ps) SplitTree
t = case NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p of
VarP PatternInfo
_ SplitPatVar
_ -> Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [NamedArg SplitPattern]
ps SplitTree
t
DotP PatternInfo
_ Term
_ -> Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [NamedArg SplitPattern]
ps SplitTree
t
ConP ConHead
c ConPatternInfo
cpi [NamedArg SplitPattern]
qs -> Arg Int -> LazySplit -> [(SplitTag, SplitTree)] -> SplitTree
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (NamedArg SplitPattern
p NamedArg SplitPattern -> Int -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int
k) LazySplit
LazySplit [(QName -> SplitTag
SplitCon (ConHead -> QName
conName ConHead
c) , Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits Int
k ([NamedArg SplitPattern]
qs [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern]
ps) SplitTree
t)]
LitP{} -> SplitTree
forall a. HasCallStack => a
__IMPOSSIBLE__
ProjP{} -> SplitTree
forall a. HasCallStack => a
__IMPOSSIBLE__
DefP{} -> SplitTree
forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP{} -> Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [NamedArg SplitPattern]
ps SplitTree
t
etaRecordSplits :: Int -> [NamedArg SplitPattern] -> (SplitTag,SplitClause)
-> SplitTree -> (SplitTag,SplitTree)
etaRecordSplits :: Int
-> [NamedArg SplitPattern]
-> (SplitTag, SplitClause)
-> SplitTree
-> (SplitTag, SplitTree)
etaRecordSplits Int
n [NamedArg SplitPattern]
ps (SplitTag
q , SplitClause
sc) SplitTree
t =
(SplitTag
q , Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits Int
0 (Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc [NamedArg SplitPattern]
ps) SplitTree
t)
inferMissingClause
:: QName
-> SplitClause
-> TCM Clause
inferMissingClause :: QName -> SplitClause -> TCM Clause
inferMissingClause QName
f (SClause Telescope
tel [NamedArg SplitPattern]
ps Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
cps (Just Dom Type
t)) = QName -> TCM Clause -> TCM Clause
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
f (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.infer" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying to infer right-hand side of type" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
t
rhs <-
Telescope -> TCMT IO Term -> TCMT IO Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel
(TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv (Map CheckpointId (Substitution' Term))
-> (Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term))
-> TCMT IO Term
-> TCMT IO Term
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Map CheckpointId (Substitution' Term)
-> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
eCheckpoints (Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a b. a -> b -> a
const Map CheckpointId (Substitution' Term)
cps)
(TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) a.
(MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
ReadTCState tcm) =>
Substitution' Term -> tcm a -> tcm a
checkpoint Substitution' Term
forall a. Substitution' a
IdS
(TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ case Dom Type -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Dom Type
t of
Hiding
_ | Just Term
tac <- Dom Type -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom Type
t -> do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.infer" Int
40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"@tactic rhs"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Dom Type
t ]
(_, v) <- RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t)
v <$ unquoteTactic tac v (unDom t)
Instance{} -> (MetaId, Term) -> Term
forall a b. (a, b) -> b
snd ((MetaId, Term) -> Term) -> TCMT IO (MetaId, Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> m (MetaId, Term)
newInstanceMeta [Char]
"" (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t)
Hiding
Hidden -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
Hiding
NotHidden -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
let cl = Clause { clauseLHSRange :: Range
clauseLHSRange = Range
forall a. Range' a
noRange
, clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
, clauseTel :: Telescope
clauseTel = Telescope
tel
, namedClausePats :: NAPs
namedClausePats = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
, clauseBody :: Maybe Term
clauseBody = Term -> Maybe Term
forall a. a -> Maybe a
Just Term
rhs
, clauseType :: Maybe (Arg Type)
clauseType = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Dom Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom Dom Type
t)
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
, clauseRecursive :: Maybe Bool
clauseRecursive = Maybe Bool
forall a. Maybe a
Nothing
, clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
}
addClauses f [cl]
return cl
inferMissingClause QName
_ (SClause Telescope
_ [NamedArg SplitPattern]
_ Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
_ Maybe (Dom Type)
Nothing) = TCM Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy BlockingVars
bs Telescope
tel = BlockingVars -> TCM BlockingVars
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (BlockingVars -> TCM BlockingVars)
-> BlockingVars -> TCM BlockingVars
forall a b. (a -> b) -> a -> b
$ (BlockingVar -> BlockingVar) -> BlockingVars -> BlockingVars
forall a. (a -> a) -> [a] -> [a]
updateLast BlockingVar -> BlockingVar
setBlockingVarOverlap BlockingVars
xs
where
xs :: BlockingVars
xs = BlockingVars
strict BlockingVars -> BlockingVars -> BlockingVars
forall a. [a] -> [a] -> [a]
++ BlockingVars
lazy
(BlockingVars
lazy, BlockingVars
strict) = (BlockingVar -> Bool)
-> BlockingVars -> (BlockingVars, BlockingVars)
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition BlockingVar -> Bool
blockingVarLazy BlockingVars
bs
isDatatype :: (MonadTCM tcm, MonadError SplitError tcm) =>
Induction -> Dom Type ->
tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
isDatatype :: forall (tcm :: * -> *).
(MonadTCM tcm, MonadError SplitError tcm) =>
Induction
-> Dom Type -> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
isDatatype Induction
ind Dom Type
at = do
let t :: Type
t = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
at
throw :: (Closure Type -> SplitError)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
throw Closure Type -> SplitError
f = SplitError -> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
forall a. SplitError -> tcm a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SplitError
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool))
-> (Closure Type -> SplitError)
-> Closure Type
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Type -> SplitError
f (Closure Type
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool))
-> tcm (Closure Type)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do TCM (Closure Type) -> tcm (Closure Type)
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Closure Type) -> tcm (Closure Type))
-> TCM (Closure Type) -> tcm (Closure Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCM (Closure Type)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Type
t
t' <- TCM Type -> tcm Type
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Type -> tcm Type) -> TCM Type -> tcm Type
forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
mInterval <- liftTCM $ getBuiltinName' builtinInterval
mIsOne <- liftTCM $ getBuiltinName' builtinIsOne
case unEl t' of
Def QName
d [] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mInterval -> (Closure Type -> SplitError)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
throw Closure Type -> SplitError
NotADatatype
Def QName
d [Apply Arg Term
phi] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mIsOne -> do
xs <- TCM [(IntMap Bool, [Term])] -> tcm [(IntMap Bool, [Term])]
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [(IntMap Bool, [Term])] -> tcm [(IntMap Bool, [Term])])
-> TCM [(IntMap Bool, [Term])] -> tcm [(IntMap Bool, [Term])]
forall a b. (a -> b) -> a -> b
$ Term -> TCM [(IntMap Bool, [Term])]
forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval (Term -> TCM [(IntMap Bool, [Term])])
-> TCMT IO Term -> TCM [(IntMap Bool, [Term])]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi)
if null xs
then return $ (IsData, d, [phi], [], [], False)
else throw NotADatatype
Def QName
d Elims
es -> do
let ~(Just Args
args) = Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
def <- TCM Defn -> tcm Defn
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Defn -> tcm Defn) -> TCM Defn -> tcm Defn
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCM Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case def of
Datatype{dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs}
| Bool
otherwise -> do
let (Args
ps, Args
is) = Int -> Args -> (Args, Args)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
np Args
args
(DataOrRecord, QName, Args, Args, [QName], Bool)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataOrRecord
forall p. DataOrRecord' p
IsData, QName
d, Args
ps, Args
is, [QName]
cs, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [QName] -> Bool
forall a. Null a => a -> Bool
null (Defn -> [QName]
dataPathCons Defn
def))
Record{recPars :: Defn -> Int
recPars = Int
np, recConHead :: Defn -> ConHead
recConHead = ConHead
con, recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
i, EtaEquality
recEtaEquality' :: EtaEquality
recEtaEquality' :: Defn -> EtaEquality
recEtaEquality'}
| Maybe Induction
i Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
== Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive Bool -> Bool -> Bool
&& Induction
ind Induction -> Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction
CoInductive ->
(Closure Type -> SplitError)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
throw Closure Type -> SplitError
CoinductiveDatatype
| Bool
otherwise ->
(DataOrRecord, QName, Args, Args, [QName], Bool)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
forall a. a -> tcm a
forall (m :: * -> *) a. Monad m => a -> m a
return (InductionAndEta -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord InductionAndEta { recordInduction :: Maybe Induction
recordInduction=Maybe Induction
i, recordEtaEquality :: EtaEquality
recordEtaEquality=EtaEquality
recEtaEquality' }, QName
d, Args
args, [], [ConHead -> QName
conName ConHead
con], Bool
False)
Defn
_ -> (Closure Type -> SplitError)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
throw Closure Type -> SplitError
NotADatatype
Term
_ -> (Closure Type -> SplitError)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
throw Closure Type -> SplitError
NotADatatype
fixTargetType
:: Quantity
-> SplitTag -> SplitClause -> Dom Type -> TCM SplitClause
fixTargetType :: Quantity
-> SplitTag -> SplitClause -> Dom Type -> TCMT IO SplitClause
fixTargetType Quantity
q SplitTag
tag sc :: SplitClause
sc@SClause{ scTel :: SplitClause -> Telescope
scTel = Telescope
sctel, scSubst :: SplitClause -> Substitution' SplitPattern
scSubst = Substitution' SplitPattern
sigma } Dom Type
target = do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"split clause telescope: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
sctel
]
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"substitution : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' SplitPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Substitution' SplitPattern -> m Doc
prettyTCM Substitution' SplitPattern
sigma
]
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"target type before substitution:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Dom Type
target
, TCMT IO Doc
" after substitution:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Substitution' SplitPattern -> Dom Type -> Dom Type
forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
sigma Dom Type
target)
]
updQuant <- do
let erased :: Bool
erased = case Quantity
q of
Quantity0{} -> Bool
True
Quantity1{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
Quantityω{} -> Bool
False
if Bool
erased then (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom Type -> Dom Type
forall a. a -> a
id else case SplitTag
tag of
SplitCon QName
c -> do
q <- Definition -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Definition -> Quantity) -> TCMT IO Definition -> TCMT IO Quantity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(ReadTCState m, HasConstInfo m) =>
QName -> m Definition
getOriginalConstInfo QName
c
case q of
Quantity0{} -> (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type))
-> (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a b. (a -> b) -> a -> b
$ (Quantity -> Quantity) -> Dom Type -> Dom Type
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
composeQuantity Quantity
q)
Quantity1{} -> (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom Type -> Dom Type
forall a. a -> a
id
Quantityω{} -> (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom Type -> Dom Type
forall a. a -> a
id
SplitLit{} -> (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom Type -> Dom Type
forall a. a -> a
id
SplitCatchall{} -> (Dom Type -> Dom Type) -> TCMT IO (Dom Type -> Dom Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Dom Type -> Dom Type
forall a. a -> a
id
return $ sc { scTarget = Just $ updQuant $ applySplitPSubst sigma target }
insertTrailingArgs
:: Bool
-> SplitClause
-> TCM (Telescope, SplitClause)
insertTrailingArgs :: Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
force sc :: SplitClause
sc@SClause{ scTel :: SplitClause -> Telescope
scTel = Telescope
sctel, scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
ps, scSubst :: SplitClause -> Substitution' SplitPattern
scSubst = Substitution' SplitPattern
sigma, scCheckpoints :: SplitClause -> Map CheckpointId (Substitution' Term)
scCheckpoints = Map CheckpointId (Substitution' Term)
cps, scTarget :: SplitClause -> Maybe (Dom Type)
scTarget = Maybe (Dom Type)
target } = do
let fallback :: TCM (Telescope, SplitClause)
fallback = (Telescope, SplitClause) -> TCM (Telescope, SplitClause)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
forall a. Null a => a
empty, SplitClause
sc)
Maybe (Dom Type)
-> TCM (Telescope, SplitClause)
-> (Dom Type -> TCM (Telescope, SplitClause))
-> TCM (Telescope, SplitClause)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target TCM (Telescope, SplitClause)
fallback ((Dom Type -> TCM (Telescope, SplitClause))
-> TCM (Telescope, SplitClause))
-> (Dom Type -> TCM (Telescope, SplitClause))
-> TCM (Telescope, SplitClause)
forall a b. (a -> b) -> a -> b
$ \ Dom Type
a -> do
if Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Dom Type -> Maybe Term
forall t e. Dom' t e -> Maybe t
domTactic Dom Type
a) Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
force then TCM (Telescope, SplitClause)
fallback else do
(TelV tel b) <- Telescope -> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
sctel (TCMT IO (TelV Type) -> TCMT IO (TelV Type))
-> TCMT IO (TelV Type) -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo (-Int
1) (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
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 = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
xs = (NamedArg SplitPattern -> NamedArg SplitPattern)
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((ArgInfo -> ArgInfo)
-> NamedArg SplitPattern -> NamedArg SplitPattern
forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo ArgInfo -> ArgInfo
hiddenInserted) ([NamedArg SplitPattern] -> [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> a -> b
$ Telescope -> [NamedArg SplitPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
tel
sctel' = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList (Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise Int
n Telescope
sctel) ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' SplitPattern
forall a. Int -> Substitution' a
raiseS Int
n) [NamedArg SplitPattern]
ps [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern]
xs
newTarget = Dom Type -> Maybe (Dom Type)
forall a. a -> Maybe a
Just (Dom Type -> Maybe (Dom Type)) -> Dom Type -> Maybe (Dom Type)
forall a b. (a -> b) -> a -> b
$ (if Bool -> Bool
not (Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel) then Dom Type
a{ domTactic = Nothing } else Dom Type
a) Dom Type -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
b
sc' = SClause
{ scTel :: Telescope
scTel = Telescope
sctel'
, scPats :: [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
ps'
, scSubst :: Substitution' SplitPattern
scSubst = Int -> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
n (Substitution' SplitPattern -> Substitution' SplitPattern)
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' SplitPattern
sigma
, scCheckpoints :: Map CheckpointId (Substitution' Term)
scCheckpoints = Substitution' (SubstArg (Map CheckpointId (Substitution' Term)))
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
n) Map CheckpointId (Substitution' Term)
cps
, scTarget :: Maybe (Dom Type)
scTarget = Maybe (Dom Type)
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 :: ArgInfo -> ArgInfo
hiddenInserted ArgInfo
ai
| ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
UserWritten ArgInfo
ai
| Bool
otherwise = Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
ai
hasHComp :: Sort -> Maybe Level
hasHComp :: Sort -> Maybe Level
hasHComp (Type Level
l) = Level -> Maybe Level
forall a. a -> Maybe a
Just Level
l
hasHComp Sort
_ = Maybe Level
forall a. Maybe a
Nothing
computeHCompSplit :: Telescope
-> PatVarName
-> Telescope
-> QName
-> Args
-> Args
-> Nat
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId Substitution
-> CoverM (Maybe (SplitTag,SplitClause))
computeHCompSplit :: Telescope
-> [Char]
-> Telescope
-> QName
-> Args
-> Args
-> Int
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId (Substitution' Term)
-> CoverM (Maybe (SplitTag, SplitClause))
computeHCompSplit Telescope
delta1 [Char]
n Telescope
delta2 QName
d Args
pars Args
ixs Int
hix Telescope
tel [NamedArg SplitPattern]
ps Map CheckpointId (Substitution' Term)
cps = do
withK <- Bool -> Bool
not (Bool -> Bool)
-> ExceptT SplitError (TCMT IO) Bool
-> ExceptT SplitError (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT SplitError (TCMT IO) Bool
forall (m :: * -> *). HasOptions m => m Bool
cubicalCompatibleOption
if withK then return Nothing else do
dsort <- liftTCM $ (parallelS (reverse $ map unArg pars) `applySubst`) . dataSort . theDef <$> getConstInfo d
hCompName <- fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinHComp
theHCompT <- defType <$> getConstInfo hCompName
caseMaybe (hasHComp dsort) (return Nothing) $ \ Level
dlvl' -> do
let
dlvl :: Term
dlvl = Level -> Term
Level Level
dlvl'
dterm :: Term
dterm = QName -> Elims -> Term
Def QName
d [] Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` (Args
pars Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ Args
ixs)
TelV gamma _ <- TCMT IO (TelV Type) -> ExceptT SplitError (TCMT IO) (TelV Type)
forall (m :: * -> *) a. Monad m => m a -> ExceptT SplitError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (TelV Type) -> ExceptT SplitError (TCMT IO) (TelV Type))
-> TCMT IO (TelV Type) -> ExceptT SplitError (TCMT IO) (TelV Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type
theHCompT Type -> Args -> Type
`piApply` [Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
dlvl , Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
dterm])
case (delta1 `abstract` gamma,IdS) of
(Telescope
delta1',PatternSubstitution
rho0) -> do
let (Substitution' SplitPattern
rho1,Substitution' SplitPattern
rho2) = Int
-> Substitution' SplitPattern
-> (Substitution' SplitPattern, Substitution' SplitPattern)
forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma) (Substitution' SplitPattern
-> (Substitution' SplitPattern, Substitution' SplitPattern))
-> Substitution' SplitPattern
-> (Substitution' SplitPattern, Substitution' SplitPattern)
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Substitution' SplitPattern
toSplitPSubst PatternSubstitution
rho0
let defp :: SplitPattern
defp = PatternInfo -> QName -> [NamedArg SplitPattern] -> SplitPattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
defaultPatternInfo QName
hCompName ([NamedArg SplitPattern] -> SplitPattern)
-> ([NamedArg SplitPattern] -> [NamedArg SplitPattern])
-> [NamedArg SplitPattern]
-> SplitPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg SplitPattern -> NamedArg SplitPattern)
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Origin -> NamedArg SplitPattern -> NamedArg SplitPattern
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) ([NamedArg SplitPattern] -> SplitPattern)
-> [NamedArg SplitPattern] -> SplitPattern
forall a b. (a -> b) -> a -> b
$
(Arg SplitPattern -> NamedArg SplitPattern)
-> [Arg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((SplitPattern -> Named NamedName SplitPattern)
-> Arg SplitPattern -> NamedArg SplitPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SplitPattern -> Named NamedName SplitPattern
forall a name. a -> Named name a
unnamed) [Hiding -> Arg SplitPattern -> Arg SplitPattern
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg SplitPattern -> Arg SplitPattern)
-> Arg SplitPattern -> Arg SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPattern -> Arg SplitPattern
forall a. a -> Arg a
defaultArg (SplitPattern -> Arg SplitPattern)
-> SplitPattern -> Arg SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg SplitPattern)
-> SplitPattern -> SplitPattern
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg SplitPattern)
rho1 (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Term -> SplitPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo (Term -> SplitPattern) -> Term -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Term
dlvl
,Hiding -> Arg SplitPattern -> Arg SplitPattern
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden (Arg SplitPattern -> Arg SplitPattern)
-> Arg SplitPattern -> Arg SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPattern -> Arg SplitPattern
forall a. a -> Arg a
defaultArg (SplitPattern -> Arg SplitPattern)
-> SplitPattern -> Arg SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg SplitPattern)
-> SplitPattern -> SplitPattern
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg SplitPattern)
rho1 (SplitPattern -> SplitPattern) -> SplitPattern -> SplitPattern
forall a b. (a -> b) -> a -> b
$ PatternInfo -> Term -> SplitPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo (Term -> SplitPattern) -> Term -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Term
dterm]
[NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho2 (Telescope -> [NamedArg SplitPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma)
let rho3 :: Substitution' SplitPattern
rho3 = SplitPattern
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
defp Substitution' SplitPattern
rho1
delta2' :: Telescope
delta2' = Substitution' SplitPattern -> Telescope -> Telescope
forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho3 Telescope
delta2
delta' :: Telescope
delta' = Telescope
delta1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2'
rho :: Substitution' SplitPattern
rho = Int -> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2) Substitution' SplitPattern
rho3
let ps' :: [NamedArg SplitPattern]
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho [NamedArg SplitPattern]
ps
let cps' :: Map CheckpointId (Substitution' Term)
cps' = Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps
Maybe (SplitTag, SplitClause)
-> CoverM (Maybe (SplitTag, SplitClause))
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SplitTag, SplitClause)
-> CoverM (Maybe (SplitTag, SplitClause)))
-> Maybe (SplitTag, SplitClause)
-> CoverM (Maybe (SplitTag, SplitClause))
forall a b. (a -> b) -> a -> b
$ (SplitTag, SplitClause) -> Maybe (SplitTag, SplitClause)
forall a. a -> Maybe a
Just ((SplitTag, SplitClause) -> Maybe (SplitTag, SplitClause))
-> (SplitClause -> (SplitTag, SplitClause))
-> SplitClause
-> Maybe (SplitTag, SplitClause)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> SplitTag
SplitCon QName
hCompName,) (SplitClause -> Maybe (SplitTag, SplitClause))
-> SplitClause -> Maybe (SplitTag, SplitClause)
forall a b. (a -> b) -> a -> b
$ Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
delta' [NamedArg SplitPattern]
ps' Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps' Maybe (Dom Type)
forall a. Maybe a
Nothing
computeNeighbourhood
:: Telescope
-> PatVarName
-> Telescope
-> QName
-> Args
-> Args
-> Nat
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId Substitution
-> QName
-> CoverM (Maybe (SplitClause, IInfo))
computeNeighbourhood :: Telescope
-> [Char]
-> Telescope
-> QName
-> Args
-> Args
-> Int
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId (Substitution' Term)
-> QName
-> CoverM (Maybe (SplitClause, IInfo))
computeNeighbourhood Telescope
delta1 [Char]
n Telescope
delta2 QName
d Args
pars Args
ixs Int
hix Telescope
tel [NamedArg SplitPattern]
ps Map CheckpointId (Substitution' Term)
cps QName
c = do
dtype <- TCM Type -> ExceptT SplitError (TCMT IO) Type
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Type -> ExceptT SplitError (TCMT IO) Type)
-> TCM Type -> ExceptT SplitError (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ (Type -> Args -> Type
`piApply` Args
pars) (Type -> Type) -> (Definition -> Type) -> Definition -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
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 $ addContext delta1 $
telViewPathBoundaryP (ctype `piApply` pars)
let Def _ es = d
Just cixs = allApplyElims es
return (gamma0, cixs, boundary)
let (_, Dom{domInfo = info} : _) = splitAt (size tel - hix - 1) (telToList tel)
let preserve ([Char]
x, t :: Type
t@(El Sort
_ (Def QName
d' Elims
_))) | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' = ([Char]
n, Type
t)
preserve ([Char]
x, Type
t) = ([Char]
x, Type
t)
gamma = ((Dom Type -> Dom Type) -> Telescope -> Telescope
forall a b. (a -> b) -> Tele a -> Tele b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Dom Type -> Dom Type) -> Telescope -> Telescope)
-> ((Modality -> Modality) -> Dom Type -> Dom Type)
-> (Modality -> Modality)
-> Telescope
-> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Modality -> Modality) -> Dom Type -> Dom Type
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality) (Modality -> Modality -> Modality
composeModality (ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality ArgInfo
info)) (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ ListTel -> Telescope
telFromList (ListTel -> Telescope)
-> (Telescope -> ListTel) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom ([Char], Type) -> Dom ([Char], Type)) -> ListTel -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map ((([Char], Type) -> ([Char], Type))
-> Dom ([Char], Type) -> Dom ([Char], Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> ([Char], Type)
preserve) (ListTel -> ListTel)
-> (Telescope -> ListTel) -> Telescope -> ListTel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ Telescope
gamma0
delta1Gamma = Telescope
delta1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma
debugInit con ctype d pars ixs cixs delta1 delta2 gamma tel ps hix
cforced <- defForced <$> getConstInfo c
let forced = Int -> IsForced -> [IsForced]
forall a. Int -> a -> [a]
replicate (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta1) IsForced
NotForced [IsForced] -> [IsForced] -> [IsForced]
forall a. [a] -> [a] -> [a]
++ [IsForced]
cforced
flex = [IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
forced Telescope
delta1Gamma
let conIxs = Int -> Args -> Args
forall a. Int -> [a] -> [a]
drop (Args -> Int
forall a. Sized a => a -> Int
size Args
pars) Args
cixs
givenIxs = Int -> Args -> Args
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma) Args
ixs
dtype <- addContext delta1 $ do
let updCoh = Cohesion -> Cohesion -> Cohesion
composeCohesion (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info)
TelV dtel dt <- telView dtype
return $ abstract (mapCohesion updCoh <$> dtel) dt
dsort <- addContext delta1 $ reduce (getSort dtype)
let withKIfStrict = Bool
-> (ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult)
-> ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Sort -> Bool
forall t. Sort' t -> Bool
isStrictDataSort Sort
dsort) ((ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult)
-> ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult)
-> (ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult)
-> ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv Bool
-> (Bool -> Bool)
-> ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eSplitOnStrict ((Bool -> Bool)
-> ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult)
-> (Bool -> Bool)
-> ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True
let flatSplit = Bool -> NoLeftInv -> Maybe NoLeftInv
forall a. Bool -> a -> Maybe a
boolToMaybe (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
== Cohesion
Flat) NoLeftInv
SplitOnFlat
r <- withKIfStrict $ lift $
Bench.billTo [Bench.Coverage, Bench.UnifyIndices] $
unifyIndices' flatSplit
delta1Gamma
flex
(raise (size gamma) dtype)
conIxs
givenIxs
TelV eqTel _ <- telView $ (raise (size gamma) dtype)
let stuck Maybe Blocker
b [UnificationFailure]
errs = do
ExceptT SplitError (TCMT IO) ()
debugCantSplit
SplitError -> CoverM (Maybe (SplitClause, IInfo))
forall a. SplitError -> ExceptT SplitError (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SplitError -> CoverM (Maybe (SplitClause, IInfo)))
-> SplitError -> CoverM (Maybe (SplitClause, IInfo))
forall a b. (a -> b) -> a -> b
$ Maybe Blocker
-> QName
-> Telescope
-> Args
-> Args
-> [UnificationFailure]
-> SplitError
UnificationStuck Maybe Blocker
b (ConHead -> QName
conName ConHead
con) (Telescope
delta1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma) Args
conIxs Args
givenIxs [UnificationFailure]
errs
case r of
NoUnify {} -> ExceptT SplitError (TCMT IO) ()
debugNoUnify ExceptT SplitError (TCMT IO) ()
-> Maybe (SplitClause, IInfo)
-> CoverM (Maybe (SplitClause, IInfo))
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Maybe (SplitClause, IInfo)
forall a. Maybe a
Nothing
UnifyBlocked Blocker
block -> Maybe Blocker
-> [UnificationFailure] -> CoverM (Maybe (SplitClause, IInfo))
stuck (Blocker -> Maybe Blocker
forall a. a -> Maybe a
Just Blocker
block) []
UnifyStuck [UnificationFailure]
errs -> Maybe Blocker
-> [UnificationFailure] -> CoverM (Maybe (SplitClause, IInfo))
stuck Maybe Blocker
forall a. Maybe a
Nothing [UnificationFailure]
errs
Unifies (Telescope
delta1',PatternSubstitution
rho0,NAPs
eqs,Either NoLeftInv (Substitution' Term, Substitution' Term)
tauInv) -> do
let unifyInfo :: IInfo
unifyInfo | Type Level
_ <- Sort
dsort
, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Args -> Bool
forall a. Null a => a -> Bool
null (Args -> Bool) -> Args -> Bool
forall a b. (a -> b) -> a -> b
$ Args
conIxs
, Right (Substitution' Term
tau,Substitution' Term
leftInv) <- Either NoLeftInv (Substitution' Term, Substitution' Term)
tauInv
= UnifyEquiv -> IInfo
TheInfo (UnifyEquiv -> IInfo) -> UnifyEquiv -> IInfo
forall a b. (a -> b) -> a -> b
$ Telescope
-> Telescope
-> Telescope
-> [Term]
-> [Term]
-> PatternSubstitution
-> Substitution' Term
-> Substitution' Term
-> UnifyEquiv
UE Telescope
delta1Gamma Telescope
delta1' Telescope
eqTel ((Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
conIxs) ((Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
givenIxs) PatternSubstitution
rho0 Substitution' Term
tau Substitution' Term
leftInv
| Bool
otherwise
= IInfo
NoInfo
case Either NoLeftInv (Substitution' Term, Substitution' Term)
tauInv of
Right{} -> () -> ExceptT SplitError (TCMT IO) ()
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Left NoLeftInv
SplitOnStrict -> () -> ExceptT SplitError (TCMT IO) ()
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Left NoLeftInv
x -> do
ExceptT SplitError (TCMT IO) Bool
-> ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ExceptT SplitError (TCMT IO) Bool
forall (m :: * -> *). HasOptions m => m Bool
cubicalCompatibleOption (ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ())
-> ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT SplitError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO () -> ExceptT SplitError (TCMT IO) ())
-> TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCMT IO ()) -> (Doc -> Warning) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
UnsupportedIndexedMatch (Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NoLeftInv -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NoLeftInv -> m Doc
prettyTCM NoLeftInv
x
[Char] -> PatternSubstitution -> ExceptT SplitError (TCMT IO) ()
forall {tcm :: * -> *} {a}.
(MonadTCM tcm, PrettyTCM a) =>
[Char] -> a -> tcm ()
debugSubst [Char]
"rho0" PatternSubstitution
rho0
let rho0' :: Substitution' SplitPattern
rho0' = PatternSubstitution -> Substitution' SplitPattern
toSplitPSubst PatternSubstitution
rho0
let (Substitution' SplitPattern
rho1,Substitution' SplitPattern
rho2) = Int
-> Substitution' SplitPattern
-> (Substitution' SplitPattern, Substitution' SplitPattern)
forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
gamma) (Substitution' SplitPattern
-> (Substitution' SplitPattern, Substitution' SplitPattern))
-> Substitution' SplitPattern
-> (Substitution' SplitPattern, Substitution' SplitPattern)
forall a b. (a -> b) -> a -> b
$ Substitution' SplitPattern
rho0'
let cpi :: ConPatternInfo
cpi = ConPatternInfo
noConPatternInfo{ conPInfo = PatternInfo PatOSplit [] , conPRecord = True }
conp :: SplitPattern
conp = ConHead
-> ConPatternInfo -> [NamedArg SplitPattern] -> SplitPattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi ([NamedArg SplitPattern] -> SplitPattern)
-> [NamedArg SplitPattern] -> SplitPattern
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho0' ([NamedArg SplitPattern] -> [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> a -> b
$
(NamedArg SplitPattern -> NamedArg SplitPattern)
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((ArgInfo -> ArgInfo)
-> NamedArg SplitPattern -> NamedArg SplitPattern
forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo ArgInfo -> ArgInfo
hiddenInserted) ([NamedArg SplitPattern] -> [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a b. (a -> b) -> a -> b
$ (forall a1. DeBruijn a1 => Telescope -> [NamedArg a1])
-> Telescope -> Boundary -> [NamedArg SplitPattern]
forall a.
DeBruijn a =>
(forall a1. DeBruijn a1 => Telescope -> [NamedArg a1])
-> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' (Telescope -> Telescope -> [NamedArg a1]
forall a. DeBruijn a => Telescope -> Telescope -> [NamedArg a]
tele2NamedArgs Telescope
gamma0) Telescope
gamma Boundary
boundary
let rho3 :: Substitution' SplitPattern
rho3 = SplitPattern
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
conp Substitution' SplitPattern
rho1
delta2' :: Telescope
delta2' = Substitution' SplitPattern -> Telescope -> Telescope
forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho3 Telescope
delta2
delta' :: Telescope
delta' = Telescope
delta1' Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2'
rho :: Substitution' SplitPattern
rho = Int -> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta2) Substitution' SplitPattern
rho3
[Char] -> Telescope -> ExceptT SplitError (TCMT IO) ()
forall {tcm :: * -> *} {a}.
(MonadTCM tcm, PrettyTCM a) =>
[Char] -> a -> tcm ()
debugTel [Char]
"delta'" Telescope
delta'
[Char]
-> Substitution' SplitPattern -> ExceptT SplitError (TCMT IO) ()
forall {tcm :: * -> *} {a}.
(MonadTCM tcm, PrettyTCM a) =>
[Char] -> a -> tcm ()
debugSubst [Char]
"rho" Substitution' SplitPattern
rho
Telescope
-> [NamedArg SplitPattern] -> ExceptT SplitError (TCMT IO) ()
forall {tcm :: * -> *} {b}.
(MonadTCM tcm, AddContext b) =>
b -> [NamedArg SplitPattern] -> tcm ()
debugPs Telescope
tel [NamedArg SplitPattern]
ps
let ps' :: [NamedArg SplitPattern]
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho [NamedArg SplitPattern]
ps
Telescope
-> [NamedArg SplitPattern] -> ExceptT SplitError (TCMT IO) ()
forall {tcm :: * -> *} {b}.
(MonadTCM tcm, AddContext b) =>
b -> [NamedArg SplitPattern] -> tcm ()
debugPlugged Telescope
delta' [NamedArg SplitPattern]
ps'
let cps' :: Map CheckpointId (Substitution' Term)
cps' = Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps
Maybe (SplitClause, IInfo) -> CoverM (Maybe (SplitClause, IInfo))
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (SplitClause, IInfo) -> CoverM (Maybe (SplitClause, IInfo)))
-> Maybe (SplitClause, IInfo)
-> CoverM (Maybe (SplitClause, IInfo))
forall a b. (a -> b) -> a -> b
$ (SplitClause, IInfo) -> Maybe (SplitClause, IInfo)
forall a. a -> Maybe a
Just ((SplitClause, IInfo) -> Maybe (SplitClause, IInfo))
-> (SplitClause -> (SplitClause, IInfo))
-> SplitClause
-> Maybe (SplitClause, IInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,IInfo
unifyInfo) (SplitClause -> Maybe (SplitClause, IInfo))
-> SplitClause -> Maybe (SplitClause, IInfo)
forall a b. (a -> b) -> a -> b
$ Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
delta' [NamedArg SplitPattern]
ps' Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps' Maybe (Dom Type)
forall a. Maybe a
Nothing
where
debugInit :: ConHead
-> Type
-> QName
-> Args
-> Args
-> Args
-> Telescope
-> Telescope
-> Telescope
-> Telescope
-> [NamedArg SplitPattern]
-> Int
-> ExceptT SplitError (TCMT IO) ()
debugInit ConHead
con Type
ctype QName
d Args
pars Args
ixs Args
cixs Telescope
delta1 Telescope
delta2 Telescope
gamma Telescope
tel [NamedArg SplitPattern]
ps Int
hix = TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ExceptT SplitError (TCMT IO) ())
-> TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"computeNeighbourhood"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"context=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
, TCMT IO Doc
"con =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
con
, TCMT IO Doc
"ctype =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ctype
, TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList (NAPs -> TCMT IO Doc) -> NAPs -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
, TCMT IO Doc
"d =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, TCMT IO Doc
"pars =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
pars
, TCMT IO Doc
"ixs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
ixs
, TCMT IO Doc
"cixs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> Args -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
cixs
, TCMT IO Doc
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta1
, TCMT IO Doc
"delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => [Char] -> m a -> m a
addContext [Char]
n (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta2
, TCMT IO Doc
"gamma =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
gamma
, TCMT IO Doc
"tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
, TCMT IO Doc
"hix =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
hix)
]
]
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
70 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"computeNeighbourhood"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"context=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Telescope -> [Char]) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Char]
forall a. Show a => a -> [Char]
show) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
, TCMT IO Doc
"con =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (ConHead -> [Char]) -> ConHead -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> [Char]
forall a. Show a => a -> [Char]
show) ConHead
con
, TCMT IO Doc
"ctype =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Type -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Char]
forall a. Show a => a -> [Char]
show) Type
ctype
, TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([NamedArg SplitPattern] -> [Char])
-> [NamedArg SplitPattern]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg SplitPattern] -> [Char]
forall a. Show a => a -> [Char]
show) [NamedArg SplitPattern]
ps
, TCMT IO Doc
"d =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (QName -> [Char]) -> QName -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
forall a. Show a => a -> [Char]
show) QName
d
, TCMT IO Doc
"pars =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Args -> [Char]) -> Args -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> [Char]
forall a. Show a => a -> [Char]
show) Args
pars
, TCMT IO Doc
"ixs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Args -> [Char]) -> Args -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> [Char]
forall a. Show a => a -> [Char]
show) Args
ixs
, TCMT IO Doc
"cixs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (Args -> [Char]) -> Args -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> [Char]
forall a. Show a => a -> [Char]
show) Args
cixs
, TCMT IO Doc
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Telescope -> [Char]) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Char]
forall a. Show a => a -> [Char]
show) Telescope
delta1
, TCMT IO Doc
"delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Telescope -> [Char]) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Char]
forall a. Show a => a -> [Char]
show) Telescope
delta2
, TCMT IO Doc
"gamma =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Telescope -> [Char]) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Char]
forall a. Show a => a -> [Char]
show) Telescope
gamma
, TCMT IO Doc
"hix =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
hix)
]
]
debugNoUnify :: ExceptT SplitError (TCMT IO) ()
debugNoUnify =
TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ExceptT SplitError (TCMT IO) ())
-> TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.split.con" Int
20 [Char]
" Constructor impossible!"
debugCantSplit :: ExceptT SplitError (TCMT IO) ()
debugCantSplit =
TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ExceptT SplitError (TCMT IO) ())
-> TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.split.con" Int
20 [Char]
" Bad split!"
debugSubst :: [Char] -> a -> tcm ()
debugSubst [Char]
s a
sub =
TCMT IO () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
sub
]
debugTel :: [Char] -> a -> tcm ()
debugTel [Char]
s a
tel =
TCMT IO () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
tel
]
debugPs :: b -> [NamedArg SplitPattern] -> tcm ()
debugPs b
tel [NamedArg SplitPattern]
ps =
TCMT IO () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ b -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => b -> m a -> m a
addContext b
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList ([NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps)
]
debugPlugged :: b -> [NamedArg SplitPattern] -> tcm ()
debugPlugged b
delta' [NamedArg SplitPattern]
ps' = do
TCMT IO () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ b -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => b -> m a -> m a
addContext b
delta' (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"ps' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList (NAPs -> TCMT IO Doc) -> NAPs -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps'
]
data InsertTrailing
= DoInsertTrailing
| DontInsertTrailing
deriving (InsertTrailing -> InsertTrailing -> Bool
(InsertTrailing -> InsertTrailing -> Bool)
-> (InsertTrailing -> InsertTrailing -> Bool) -> Eq InsertTrailing
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InsertTrailing -> InsertTrailing -> Bool
== :: InsertTrailing -> InsertTrailing -> Bool
$c/= :: InsertTrailing -> InsertTrailing -> Bool
/= :: InsertTrailing -> InsertTrailing -> Bool
Eq, Int -> InsertTrailing -> [Char] -> [Char]
[InsertTrailing] -> [Char] -> [Char]
InsertTrailing -> [Char]
(Int -> InsertTrailing -> [Char] -> [Char])
-> (InsertTrailing -> [Char])
-> ([InsertTrailing] -> [Char] -> [Char])
-> Show InsertTrailing
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> InsertTrailing -> [Char] -> [Char]
showsPrec :: Int -> InsertTrailing -> [Char] -> [Char]
$cshow :: InsertTrailing -> [Char]
show :: InsertTrailing -> [Char]
$cshowList :: [InsertTrailing] -> [Char] -> [Char]
showList :: [InsertTrailing] -> [Char] -> [Char]
Show)
data AllowPartialCover
= YesAllowPartialCover
| NoAllowPartialCover
deriving (AllowPartialCover -> AllowPartialCover -> Bool
(AllowPartialCover -> AllowPartialCover -> Bool)
-> (AllowPartialCover -> AllowPartialCover -> Bool)
-> Eq AllowPartialCover
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AllowPartialCover -> AllowPartialCover -> Bool
== :: AllowPartialCover -> AllowPartialCover -> Bool
$c/= :: AllowPartialCover -> AllowPartialCover -> Bool
/= :: AllowPartialCover -> AllowPartialCover -> Bool
Eq, Int -> AllowPartialCover -> [Char] -> [Char]
[AllowPartialCover] -> [Char] -> [Char]
AllowPartialCover -> [Char]
(Int -> AllowPartialCover -> [Char] -> [Char])
-> (AllowPartialCover -> [Char])
-> ([AllowPartialCover] -> [Char] -> [Char])
-> Show AllowPartialCover
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> AllowPartialCover -> [Char] -> [Char]
showsPrec :: Int -> AllowPartialCover -> [Char] -> [Char]
$cshow :: AllowPartialCover -> [Char]
show :: AllowPartialCover -> [Char]
$cshowList :: [AllowPartialCover] -> [Char] -> [Char]
showList :: [AllowPartialCover] -> [Char] -> [Char]
Show)
splitClauseWithAbsurd :: SplitClause -> Nat -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd :: SplitClause
-> Int -> TCM (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd SplitClause
c Int
x =
CheckEmpty
-> Induction
-> AllowPartialCover
-> InsertTrailing
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' CheckEmpty
CheckEmpty Induction
Inductive AllowPartialCover
NoAllowPartialCover InsertTrailing
DontInsertTrailing SplitClause
c (Int -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Int
x [] [] Bool
True Bool
False)
splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)
splitLast :: Induction
-> Telescope -> NAPs -> TCMT IO (Either SplitError Covering)
splitLast Induction
ind Telescope
tel NAPs
ps = Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCMT IO (Either SplitError Covering)
split Induction
ind AllowPartialCover
NoAllowPartialCover SplitClause
sc (Int -> [ConHead] -> [Literal] -> Bool -> Bool -> BlockingVar
BlockingVar Int
0 [] [] Bool
True Bool
False)
where sc :: SplitClause
sc = Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
tel (NAPs -> [NamedArg SplitPattern]
toSplitPatterns NAPs
ps) Substitution' SplitPattern
forall a. Null a => a
empty Map CheckpointId (Substitution' Term)
forall a. Null a => a
empty Maybe (Dom Type)
forall {t}. Maybe (Dom (Type'' t Term))
target
target :: Maybe (Dom (Type'' t Term))
target = (Dom (Type'' t Term) -> Maybe (Dom (Type'' t Term))
forall a. a -> Maybe a
Just (Dom (Type'' t Term) -> Maybe (Dom (Type'' t Term)))
-> Dom (Type'' t Term) -> Maybe (Dom (Type'' t Term))
forall a b. (a -> b) -> a -> b
$ Type'' t Term -> Dom (Type'' t Term)
forall a. a -> Dom a
defaultDom (Type'' t Term -> Dom (Type'' t Term))
-> Type'' t Term -> Dom (Type'' t Term)
forall a b. (a -> b) -> a -> b
$ Sort' t -> Term -> Type'' t Term
forall t a. Sort' t -> a -> Type'' t a
El (Level' t -> Sort' t
forall t. Level' t -> Sort' t
Prop (Integer -> [PlusLevel' t] -> Level' t
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [])) (Term -> Type'' t Term) -> Term -> Type'' t Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Elims -> Term
Dummy [Char]
"splitLastTarget" [])
split :: Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
split :: Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCMT IO (Either SplitError Covering)
split Induction
ind AllowPartialCover
allowPartialCover SplitClause
sc BlockingVar
x =
(Either SplitClause Covering -> Covering)
-> Either SplitError (Either SplitClause Covering)
-> Either SplitError Covering
forall a b. (a -> b) -> Either SplitError a -> Either SplitError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either SplitClause Covering -> Covering
blendInAbsurdClause (Either SplitError (Either SplitClause Covering)
-> Either SplitError Covering)
-> TCM (Either SplitError (Either SplitClause Covering))
-> TCMT IO (Either SplitError Covering)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CheckEmpty
-> Induction
-> AllowPartialCover
-> InsertTrailing
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' CheckEmpty
NoCheckEmpty Induction
ind AllowPartialCover
allowPartialCover InsertTrailing
DoInsertTrailing SplitClause
sc BlockingVar
x
where
n :: Arg Int
n = SplitClause -> Int -> Arg Int
lookupPatternVar SplitClause
sc (Int -> Arg Int) -> Int -> Arg Int
forall a b. (a -> b) -> a -> b
$ BlockingVar -> Int
blockingVarNo BlockingVar
x
blendInAbsurdClause :: Either SplitClause Covering -> Covering
blendInAbsurdClause :: Either SplitClause Covering -> Covering
blendInAbsurdClause = (SplitClause -> Covering)
-> Either SplitClause Covering -> Covering
forall a b. (a -> b) -> Either a b -> b
fromRight (Covering -> SplitClause -> Covering
forall a b. a -> b -> a
const (Covering -> SplitClause -> Covering)
-> Covering -> SplitClause -> Covering
forall a b. (a -> b) -> a -> b
$ Arg Int -> [(SplitTag, (SplitClause, IInfo))] -> Covering
Covering Arg Int
n [])
lookupPatternVar :: SplitClause -> Int -> Arg Nat
lookupPatternVar :: SplitClause -> Int -> Arg Int
lookupPatternVar SClause{ scTel :: SplitClause -> Telescope
scTel = Telescope
tel, scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
pats } Int
x = Arg DeBruijnPattern
arg Arg DeBruijnPattern -> Int -> Arg Int
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>
if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 then Int
forall a. HasCallStack => a
__IMPOSSIBLE__ else Int
n
where n :: Int
n = if Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
then Int
forall a. HasCallStack => a
__IMPOSSIBLE__
else Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Permutation -> [Int]
permPicks Permutation
perm [Int] -> Int -> Maybe Int
forall a. [a] -> Int -> Maybe a
!!! Int
k
perm :: Permutation
perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ NAPs -> Maybe Permutation
dbPatPerm (NAPs -> Maybe Permutation) -> NAPs -> Maybe Permutation
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
pats
k :: Int
k = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
arg :: Arg DeBruijnPattern
arg = Arg DeBruijnPattern
-> [Arg DeBruijnPattern] -> Int -> Arg DeBruijnPattern
forall a. a -> [a] -> Int -> a
indexWithDefault Arg DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__ (Int -> Telescope -> [Arg DeBruijnPattern]
telVars (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Telescope
tel) Int
k
data CheckEmpty = CheckEmpty | NoCheckEmpty
split' :: CheckEmpty
-> Induction
-> AllowPartialCover
-> InsertTrailing
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' :: CheckEmpty
-> Induction
-> AllowPartialCover
-> InsertTrailing
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError (Either SplitClause Covering))
split' CheckEmpty
checkEmpty Induction
ind AllowPartialCover
allowPartialCover InsertTrailing
inserttrailing
sc :: SplitClause
sc@(SClause Telescope
tel [NamedArg SplitPattern]
ps Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
cps Maybe (Dom Type)
target) (BlockingVar Int
x [ConHead]
pcons' [Literal]
plits Bool
overlap Bool
lazy) =
TCM (Either SplitError (Either SplitClause Covering))
-> TCM (Either SplitError (Either SplitClause Covering))
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Either SplitError (Either SplitClause Covering))
-> TCM (Either SplitError (Either SplitClause Covering)))
-> TCM (Either SplitError (Either SplitClause Covering))
-> TCM (Either SplitError (Either SplitClause Covering))
forall a b. (a -> b) -> a -> b
$ ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
-> TCM (Either SplitError (Either SplitClause Covering))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
-> TCM (Either SplitError (Either SplitClause Covering)))
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
-> TCM (Either SplitError (Either SplitClause Covering))
forall a b. (a -> b) -> a -> b
$ do
Telescope
-> Int
-> [NamedArg SplitPattern]
-> Map CheckpointId (Substitution' Term)
-> ExceptT SplitError (TCMT IO) ()
forall {tcm :: * -> *} {a} {a} {a}.
(MonadTCM tcm, AddContext a, PrettyTCM a, PrettyTCM a, PrettyTCM a,
Show a, Show a, Show a) =>
a -> a -> [NamedArg SplitPattern] -> a -> tcm ()
debugInit Telescope
tel Int
x [NamedArg SplitPattern]
ps Map CheckpointId (Substitution' Term)
cps
(n, t, delta1, delta2) <- do
let (ListTel
tel1, Dom ([Char], Type)
dom : ListTel
tel2) = Int -> ListTel -> (ListTel, ListTel)
forall a. Int -> [a] -> ([a], [a])
splitAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (ListTel -> (ListTel, ListTel)) -> ListTel -> (ListTel, ListTel)
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
([Char], Dom Type, Telescope, Telescope)
-> ExceptT
SplitError (TCMT IO) ([Char], Dom Type, Telescope, Telescope)
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (([Char], Type) -> [Char]
forall a b. (a, b) -> a
fst (([Char], Type) -> [Char]) -> ([Char], Type) -> [Char]
forall a b. (a -> b) -> a -> b
$ Dom ([Char], Type) -> ([Char], Type)
forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
dom, ([Char], Type) -> Type
forall a b. (a, b) -> b
snd (([Char], Type) -> Type) -> Dom ([Char], Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom ([Char], Type)
dom, ListTel -> Telescope
telFromList ListTel
tel1, ListTel -> Telescope
telFromList ListTel
tel2)
let computeNeighborhoods = do
(dr, d, pars, ixs, cons', isHIT) <- ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool)
-> ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool)
forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT (ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool)
-> ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool))
-> ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool)
-> ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool)
forall a b. (a -> b) -> a -> b
$ Induction
-> Dom Type
-> ExceptT
SplitError
(TCMT IO)
(DataOrRecord, QName, Args, Args, [QName], Bool)
forall (tcm :: * -> *).
(MonadTCM tcm, MonadError SplitError tcm) =>
Induction
-> Dom Type -> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
isDatatype Induction
ind Dom Type
t
isFib <- lift $ isFibrant t
cons <- case checkEmpty of
CheckEmpty
CheckEmpty -> ExceptT SplitError (TCMT IO) Bool
-> ExceptT SplitError (TCMT IO) [QName]
-> ExceptT SplitError (TCMT IO) [QName]
-> ExceptT SplitError (TCMT IO) [QName]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool)
-> TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ TCMT IO Bool -> TCMT IO Bool
forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Bool
isEmptyType (Type -> TCMT IO Bool) -> Type -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t) ([QName] -> ExceptT SplitError (TCMT IO) [QName]
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) ([QName] -> ExceptT SplitError (TCMT IO) [QName]
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [QName]
cons')
CheckEmpty
NoCheckEmpty -> [QName] -> ExceptT SplitError (TCMT IO) [QName]
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [QName]
cons'
mns <- forM cons $ \ QName
con -> ((SplitClause, IInfo) -> (SplitTag, (SplitClause, IInfo)))
-> Maybe (SplitClause, IInfo)
-> Maybe (SplitTag, (SplitClause, IInfo))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> SplitTag
SplitCon QName
con,) (Maybe (SplitClause, IInfo)
-> Maybe (SplitTag, (SplitClause, IInfo)))
-> CoverM (Maybe (SplitClause, IInfo))
-> ExceptT
SplitError (TCMT IO) (Maybe (SplitTag, (SplitClause, IInfo)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Telescope
-> [Char]
-> Telescope
-> QName
-> Args
-> Args
-> Int
-> Telescope
-> [NamedArg SplitPattern]
-> Map CheckpointId (Substitution' Term)
-> QName
-> CoverM (Maybe (SplitClause, IInfo))
computeNeighbourhood Telescope
delta1 [Char]
n Telescope
delta2 QName
d Args
pars Args
ixs Int
x Telescope
tel [NamedArg SplitPattern]
ps Map CheckpointId (Substitution' Term)
cps QName
con
hcompsc <- if isFib && (isHIT || not (null ixs)) && not (null mns) && inserttrailing == DoInsertTrailing
then computeHCompSplit delta1 n delta2 d pars ixs x tel ps cps
else return Nothing
let ns = [Maybe (SplitTag, (SplitClause, IInfo))]
-> [(SplitTag, (SplitClause, IInfo))]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (SplitTag, (SplitClause, IInfo))]
mns
return ( dr
, not (null ixs)
, length $ ns
, ns ++ catMaybes ([fmap (fmap (,NoInfo)) hcompsc | not $ null $ ns])
)
computeLitNeighborhoods = do
typeOk <- TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool)
-> TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ do
t' <- Literal -> TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType (Literal -> TCM Type) -> Literal -> TCM Type
forall a b. (a -> b) -> a -> b
$ Literal -> [Literal] -> Literal
forall a. a -> [a] -> a
headWithDefault Literal
forall a. HasCallStack => a
__IMPOSSIBLE__ [Literal]
plits
liftTCM $ dontAssignMetas $ tryConversion $ equalType (unDom t) t'
unless typeOk $ throwError . NotADatatype =<< do liftTCM $ buildClosure (unDom t)
ns <- forM plits $ \Literal
lit -> do
let delta2' :: Telescope
delta2' = Int -> SubstArg Telescope -> Telescope -> Telescope
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 (Literal -> Term
Lit Literal
lit) Telescope
delta2
delta' :: Telescope
delta' = Telescope
delta1 Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2'
rho :: Substitution' SplitPattern
rho = Int -> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
x (Substitution' SplitPattern -> Substitution' SplitPattern)
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPattern
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (Literal -> SplitPattern
forall a. Literal -> Pattern' a
litP Literal
lit) Substitution' SplitPattern
forall a. Substitution' a
idS
ps' :: [NamedArg SplitPattern]
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho [NamedArg SplitPattern]
ps
cps' :: Map CheckpointId (Substitution' Term)
cps' = Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps
(SplitTag, SplitClause)
-> ExceptT SplitError (TCMT IO) (SplitTag, SplitClause)
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> SplitTag
SplitLit Literal
lit , Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
delta' [NamedArg SplitPattern]
ps' Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps' Maybe (Dom Type)
forall a. Maybe a
Nothing)
ca <- do
let delta' = Telescope
tel
varp = PatternInfo -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSplit []) (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPatVar
{ splitPatVarName :: [Char]
splitPatVarName = [Char]
forall a. Underscore a => a
underscore
, splitPatVarIndex :: Int
splitPatVarIndex = Int
0
, splitExcludedLits :: [Literal]
splitExcludedLits = [Literal]
plits
}
rho = Int -> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
x (Substitution' SplitPattern -> Substitution' SplitPattern)
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPattern
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
varp (Substitution' SplitPattern -> Substitution' SplitPattern)
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' SplitPattern
forall a. Int -> Substitution' a
raiseS Int
1
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho [NamedArg SplitPattern]
ps
return (SplitCatchall , SClause delta' ps' rho cps Nothing)
let ns' = ((SplitTag, SplitClause) -> (SplitTag, (SplitClause, IInfo)))
-> [(SplitTag, SplitClause)] -> [(SplitTag, (SplitClause, IInfo))]
forall a b. (a -> b) -> [a] -> [b]
map (((SplitClause -> (SplitClause, IInfo))
-> (SplitTag, SplitClause) -> (SplitTag, (SplitClause, IInfo))
forall a b. (a -> b) -> (SplitTag, a) -> (SplitTag, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,IInfo
NoInfo))) ([(SplitTag, SplitClause)] -> [(SplitTag, (SplitClause, IInfo))])
-> [(SplitTag, SplitClause)] -> [(SplitTag, (SplitClause, IInfo))]
forall a b. (a -> b) -> a -> b
$ [(SplitTag, SplitClause)]
ns [(SplitTag, SplitClause)]
-> [(SplitTag, SplitClause)] -> [(SplitTag, SplitClause)]
forall a. [a] -> [a] -> [a]
++ [ (SplitTag, SplitClause)
ca ]
return (IsData, False, length ns', ns')
(dr, isIndexed, numMatching, ns) <- if null pcons' && not (null plits)
then computeLitNeighborhoods
else computeNeighborhoods
ns <- case target of
Just Dom Type
a -> [(SplitTag, (SplitClause, IInfo))]
-> ((SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) (SplitTag, (SplitClause, IInfo)))
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(SplitTag, (SplitClause, IInfo))]
ns (((SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) (SplitTag, (SplitClause, IInfo)))
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))])
-> ((SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) (SplitTag, (SplitClause, IInfo)))
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))]
forall a b. (a -> b) -> a -> b
$ \ (SplitTag
con,(SplitClause
sc,IInfo
info)) -> TCMT IO (SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) (SplitTag, (SplitClause, IInfo))
forall (m :: * -> *) a. Monad m => m a -> ExceptT SplitError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) (SplitTag, (SplitClause, IInfo)))
-> TCMT IO (SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) (SplitTag, (SplitClause, IInfo))
forall a b. (a -> b) -> a -> b
$ (SplitTag
con,) ((SplitClause, IInfo) -> (SplitTag, (SplitClause, IInfo)))
-> (SplitClause -> (SplitClause, IInfo))
-> SplitClause
-> (SplitTag, (SplitClause, IInfo))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,IInfo
info) (SplitClause -> (SplitTag, (SplitClause, IInfo)))
-> TCMT IO SplitClause -> TCMT IO (SplitTag, (SplitClause, IInfo))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Quantity
-> SplitTag -> SplitClause -> Dom Type -> TCMT IO SplitClause
fixTargetType (Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
t) SplitTag
con SplitClause
sc Dom Type
a
Maybe (Dom Type)
Nothing -> [(SplitTag, (SplitClause, IInfo))]
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))]
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitTag, (SplitClause, IInfo))]
ns
ns <- case inserttrailing of
InsertTrailing
DontInsertTrailing -> [(SplitTag, (SplitClause, IInfo))]
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))]
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitTag, (SplitClause, IInfo))]
ns
InsertTrailing
DoInsertTrailing -> TCMT IO [(SplitTag, (SplitClause, IInfo))]
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))]
forall (m :: * -> *) a. Monad m => m a -> ExceptT SplitError m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [(SplitTag, (SplitClause, IInfo))]
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))])
-> TCMT IO [(SplitTag, (SplitClause, IInfo))]
-> ExceptT SplitError (TCMT IO) [(SplitTag, (SplitClause, IInfo))]
forall a b. (a -> b) -> a -> b
$ [(SplitTag, (SplitClause, IInfo))]
-> ((SplitTag, (SplitClause, IInfo))
-> TCMT IO (SplitTag, (SplitClause, IInfo)))
-> TCMT IO [(SplitTag, (SplitClause, IInfo))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(SplitTag, (SplitClause, IInfo))]
ns (((SplitTag, (SplitClause, IInfo))
-> TCMT IO (SplitTag, (SplitClause, IInfo)))
-> TCMT IO [(SplitTag, (SplitClause, IInfo))])
-> ((SplitTag, (SplitClause, IInfo))
-> TCMT IO (SplitTag, (SplitClause, IInfo)))
-> TCMT IO [(SplitTag, (SplitClause, IInfo))]
forall a b. (a -> b) -> a -> b
$ \(SplitTag
con,(SplitClause
sc,IInfo
info)) ->
(SplitTag
con,) ((SplitClause, IInfo) -> (SplitTag, (SplitClause, IInfo)))
-> ((Telescope, SplitClause) -> (SplitClause, IInfo))
-> (Telescope, SplitClause)
-> (SplitTag, (SplitClause, IInfo))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,IInfo
info) (SplitClause -> (SplitClause, IInfo))
-> ((Telescope, SplitClause) -> SplitClause)
-> (Telescope, SplitClause)
-> (SplitClause, IInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Telescope, SplitClause) -> SplitClause
forall a b. (a, b) -> b
snd ((Telescope, SplitClause) -> (SplitTag, (SplitClause, IInfo)))
-> TCM (Telescope, SplitClause)
-> TCMT IO (SplitTag, (SplitClause, IInfo))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
False SplitClause
sc
mHCompName <- getPrimitiveName' builtinHComp
opts <- pragmaOptions
let withoutK = PragmaOptions -> Bool
optWithoutK PragmaOptions
opts
erasedMatches = PragmaOptions -> Bool
optErasedMatches PragmaOptions
opts
isRecordWithEta = case DataOrRecord
dr of
DataOrRecord
IsData -> Bool
False
IsRecord InductionAndEta
r ->
case EtaEquality -> HasEta
theEtaEquality (InductionAndEta -> EtaEquality
recordEtaEquality InductionAndEta
r) of
YesEta{} -> Bool
True
NoEta{} -> Bool
False
erased <- hasQuantity0 <$> viewTC eQuantity
reportSLn "tc.cover.split" 60 $ "We are in erased context = " ++ show erased
let erasedError ErasedDatatypeReason
reason =
SplitError
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall a. SplitError -> ExceptT SplitError (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (SplitError
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering))
-> (Closure Type -> SplitError)
-> Closure Type
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErasedDatatypeReason -> Closure Type -> SplitError
ErasedDatatype ErasedDatatypeReason
reason (Closure Type
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering))
-> ExceptT SplitError (TCMT IO) (Closure Type)
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
do TCM (Closure Type) -> ExceptT SplitError (TCMT IO) (Closure Type)
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Closure Type) -> ExceptT SplitError (TCMT IO) (Closure Type))
-> TCM (Closure Type)
-> ExceptT SplitError (TCMT IO) (Closure Type)
forall a b. (a -> b) -> a -> b
$ TCM (Closure Type) -> TCM (Closure Type)
forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT (TCM (Closure Type) -> TCM (Closure Type))
-> TCM (Closure Type) -> TCM (Closure Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCM (Closure Type)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t)
case numMatching of
Int
0 -> do
let absurdp :: SplitPattern
absurdp = PatternInfo -> SplitPatVar -> SplitPattern
forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOAbsurd []) (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Literal] -> SplitPatVar
SplitPatVar [Char]
forall a. Underscore a => a
underscore Int
0 []
rho :: Substitution' SplitPattern
rho = Int -> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
x (Substitution' SplitPattern -> Substitution' SplitPattern)
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a b. (a -> b) -> a -> b
$ SplitPattern
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
absurdp (Substitution' SplitPattern -> Substitution' SplitPattern)
-> Substitution' SplitPattern -> Substitution' SplitPattern
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' SplitPattern
forall a. Int -> Substitution' a
raiseS Int
1
ps' :: [NamedArg SplitPattern]
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
rho [NamedArg SplitPattern]
ps
Either SplitClause Covering
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SplitClause Covering
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering))
-> Either SplitClause Covering
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall a b. (a -> b) -> a -> b
$ SplitClause -> Either SplitClause Covering
forall a b. a -> Either a b
Left (SplitClause -> Either SplitClause Covering)
-> SplitClause -> Either SplitClause Covering
forall a b. (a -> b) -> a -> b
$ SClause
{ scTel :: Telescope
scTel = Telescope
tel
, scPats :: [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
ps'
, scSubst :: Substitution' SplitPattern
scSubst = Substitution' SplitPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
, scCheckpoints :: Map CheckpointId (Substitution' Term)
scCheckpoints = Map CheckpointId (Substitution' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
, scTarget :: Maybe (Dom Type)
scTarget = Maybe (Dom Type)
forall a. Maybe a
Nothing
}
Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
erased Bool -> Bool -> Bool
&& Bool -> Bool
not (Dom Type -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity Dom Type
t) ->
ErasedDatatypeReason
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
erasedError ErasedDatatypeReason
SeveralConstructors
Int
1 | Bool -> Bool
not Bool
erased Bool -> Bool -> Bool
&& Bool -> Bool
not (Dom Type -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity Dom Type
t) Bool -> Bool -> Bool
&& Bool
withoutK Bool -> Bool -> Bool
&&
(Bool
isIndexed Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
isRecordWithEta Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
erasedMatches) ->
ErasedDatatypeReason
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
erasedError (if Bool
isIndexed then ErasedDatatypeReason
NoK else ErasedDatatypeReason
NoErasedMatches)
Int
_ -> do
let ptags :: [SplitTag]
ptags = (ConHead -> SplitTag) -> [ConHead] -> [SplitTag]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> SplitTag
SplitCon (QName -> SplitTag) -> (ConHead -> QName) -> ConHead -> SplitTag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName) [ConHead]
pcons' [SplitTag] -> [SplitTag] -> [SplitTag]
forall a. [a] -> [a] -> [a]
++ (Literal -> SplitTag) -> [Literal] -> [SplitTag]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> SplitTag
SplitLit [Literal]
plits
let inferred_tags :: Set SplitTag
inferred_tags = Set SplitTag
-> (QName -> Set SplitTag) -> Maybe QName -> Set SplitTag
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set SplitTag
forall a. Set a
Set.empty (SplitTag -> Set SplitTag
forall a. a -> Set a
Set.singleton (SplitTag -> Set SplitTag)
-> (QName -> SplitTag) -> QName -> Set SplitTag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> SplitTag
SplitCon) Maybe QName
mHCompName
let all_tags :: Set SplitTag
all_tags = [SplitTag] -> Set SplitTag
forall a. Ord a => [a] -> Set a
Set.fromList [SplitTag]
ptags Set SplitTag -> Set SplitTag -> Set SplitTag
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set SplitTag
inferred_tags
Bool
-> ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AllowPartialCover
allowPartialCover AllowPartialCover -> AllowPartialCover -> Bool
forall a. Eq a => a -> a -> Bool
== AllowPartialCover
NoAllowPartialCover Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
overlap) (ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ())
-> ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
[(SplitTag, (SplitClause, IInfo))]
-> ((SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) ())
-> ExceptT SplitError (TCMT IO) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(SplitTag, (SplitClause, IInfo))]
ns (((SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) ())
-> ExceptT SplitError (TCMT IO) ())
-> ((SplitTag, (SplitClause, IInfo))
-> ExceptT SplitError (TCMT IO) ())
-> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ \(SplitTag
tag, (SplitClause
sc, IInfo
_)) -> do
Bool
-> ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SplitTag
tag SplitTag -> Set SplitTag -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SplitTag
all_tags) (ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ())
-> ExceptT SplitError (TCMT IO) ()
-> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
isImpossibleClause <- TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool)
-> TCMT IO Bool -> ExceptT SplitError (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Bool
isEmptyTel (Telescope -> TCMT IO Bool) -> Telescope -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ SplitClause -> Telescope
scTel SplitClause
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")
TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a. TCM a -> ExceptT SplitError (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ExceptT SplitError (TCMT IO) ())
-> TCMT IO () -> ExceptT SplitError (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> TCMT IO ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ DataOrRecord -> Type -> Telescope -> Maybe (Dom Type) -> TCMT IO ()
forall (m :: * -> *) a ty.
(MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a,
PrettyTCM a, LensSort ty, PrettyTCM ty) =>
DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
checkSortOfSplitVar DataOrRecord
dr (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t) Telescope
delta2 Maybe (Dom Type)
target
Either SplitClause Covering
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall a. a -> ExceptT SplitError (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SplitClause Covering
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering))
-> Either SplitClause Covering
-> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
forall a b. (a -> b) -> a -> b
$ Covering -> Either SplitClause Covering
forall a b. b -> Either a b
Right (Covering -> Either SplitClause Covering)
-> Covering -> Either SplitClause Covering
forall a b. (a -> b) -> a -> b
$ Arg Int -> [(SplitTag, (SplitClause, IInfo))] -> Covering
Covering (SplitClause -> Int -> Arg Int
lookupPatternVar SplitClause
sc Int
x) [(SplitTag, (SplitClause, IInfo))]
ns
where
inContextOfT, inContextOfDelta2 :: (MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) => tcm a -> tcm a
inContextOfT :: forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT = Telescope -> tcm a -> tcm a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> Int -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
inContextOfDelta2 :: forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfDelta2 = Telescope -> tcm a -> tcm a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (tcm a -> tcm a) -> (tcm a -> tcm a) -> tcm a -> tcm a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> Int -> tcm a -> tcm a
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible Int
x
debugInit :: a -> a -> [NamedArg SplitPattern] -> a -> tcm ()
debugInit a
tel a
x [NamedArg SplitPattern]
ps a
cps = TCMT IO () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$ TCMT IO () -> TCMT IO ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"TypeChecking.Coverage.split': split"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
tel
, TCMT IO Doc
"x =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x
, TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do a -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => a -> m a -> m a
addContext a
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList (NAPs -> TCMT IO Doc) -> NAPs -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
, TCMT IO Doc
"cps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
cps
]
]
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"TypeChecking.Coverage.split': split"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (a -> [Char]) -> a -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Show a => a -> [Char]
show) a
tel
, TCMT IO Doc
"x =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (a -> [Char]) -> a -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Show a => a -> [Char]
show) a
x
, TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([NamedArg SplitPattern] -> [Char])
-> [NamedArg SplitPattern]
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NamedArg SplitPattern] -> [Char]
forall a. Show a => a -> [Char]
show) [NamedArg SplitPattern]
ps
, TCMT IO Doc
"cps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> (a -> [Char]) -> a -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Show a => a -> [Char]
show) a
cps
]
]
debugHoleAndType :: a -> a -> [Char] -> NAPs -> a -> tcm ()
debugHoleAndType a
delta1 a
delta2 [Char]
s NAPs
ps a
t =
TCMT IO () -> tcm ()
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> tcm ()) -> TCMT IO () -> tcm ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"p =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> [Char]
patVarNameToString [Char]
s)
, TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps
, TCMT IO Doc
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
delta1
, TCMT IO Doc
"delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfDelta2 (a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
delta2)
, TCMT IO Doc
"t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT (a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
t)
]
splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult QName
f SplitClause
sc = do
TCMT IO (Maybe SplitClause)
-> TCM (Either SplitError [SplitClause])
-> (SplitClause -> TCM (Either SplitError [SplitClause]))
-> TCM (Either SplitError [SplitClause])
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> SplitClause -> TCMT IO (Maybe SplitClause)
splitResultPath QName
f SplitClause
sc)
(((Either SplitError Covering -> Either SplitError [SplitClause])
-> TCMT IO (Either SplitError Covering)
-> TCM (Either SplitError [SplitClause])
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Either SplitError Covering -> Either SplitError [SplitClause])
-> TCMT IO (Either SplitError Covering)
-> TCM (Either SplitError [SplitClause]))
-> ((Covering -> [SplitClause])
-> Either SplitError Covering -> Either SplitError [SplitClause])
-> (Covering -> [SplitClause])
-> TCMT IO (Either SplitError Covering)
-> TCM (Either SplitError [SplitClause])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Covering -> [SplitClause])
-> Either SplitError Covering -> Either SplitError [SplitClause]
forall a b. (a -> b) -> Either SplitError a -> Either SplitError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Covering -> [SplitClause]
splitClauses (TCMT IO (Either SplitError Covering)
-> TCM (Either SplitError [SplitClause]))
-> TCMT IO (Either SplitError Covering)
-> TCM (Either SplitError [SplitClause])
forall a b. (a -> b) -> a -> b
$ QName -> SplitClause -> TCMT IO (Either SplitError Covering)
splitResultRecord QName
f SplitClause
sc)
(Either SplitError [SplitClause]
-> TCM (Either SplitError [SplitClause])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SplitError [SplitClause]
-> TCM (Either SplitError [SplitClause]))
-> (SplitClause -> Either SplitError [SplitClause])
-> SplitClause
-> TCM (Either SplitError [SplitClause])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SplitClause] -> Either SplitError [SplitClause]
forall a b. b -> Either a b
Right ([SplitClause] -> Either SplitError [SplitClause])
-> (SplitClause -> [SplitClause])
-> SplitClause
-> Either SplitError [SplitClause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitClause -> [SplitClause] -> [SplitClause]
forall a. a -> [a] -> [a]
:[]))
splitResultPath :: QName -> SplitClause -> TCM (Maybe SplitClause)
splitResultPath :: QName -> SplitClause -> TCMT IO (Maybe SplitClause)
splitResultPath QName
f sc :: SplitClause
sc@(SClause Telescope
tel [NamedArg SplitPattern]
ps Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
_ Maybe (Dom Type)
target) = do
Maybe (Dom Type)
-> TCMT IO (Maybe SplitClause)
-> (Dom Type -> TCMT IO (Maybe SplitClause))
-> TCMT IO (Maybe SplitClause)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target (Maybe SplitClause -> TCMT IO (Maybe SplitClause)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SplitClause
forall a. Maybe a
Nothing) ((Dom Type -> TCMT IO (Maybe SplitClause))
-> TCMT IO (Maybe SplitClause))
-> (Dom Type -> TCMT IO (Maybe SplitClause))
-> TCMT IO (Maybe SplitClause)
forall a b. (a -> b) -> a -> b
$ \ Dom Type
t -> do
TCMT IO (Maybe (Dom Type, Abs Type))
-> TCMT IO (Maybe SplitClause)
-> ((Dom Type, Abs Type) -> TCMT IO (Maybe SplitClause))
-> TCMT IO (Maybe SplitClause)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCMT IO (Maybe (Dom Type, Abs Type))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t)) (Maybe SplitClause -> TCMT IO (Maybe SplitClause)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SplitClause
forall a. Maybe a
Nothing) (((Dom Type, Abs Type) -> TCMT IO (Maybe SplitClause))
-> TCMT IO (Maybe SplitClause))
-> ((Dom Type, Abs Type) -> TCMT IO (Maybe SplitClause))
-> TCMT IO (Maybe SplitClause)
forall a b. (a -> b) -> a -> b
$ \ (Dom Type, Abs Type)
_ -> do
(TelV i b, boundary) <- Int -> Type -> TCM (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary' Int
1 (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t)
let tel' = Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
i
rho = Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS Int
1
ps' = Substitution' (SubstArg [NamedArg SplitPattern])
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
Substitution' (SubstArg [NamedArg SplitPattern])
forall a. Substitution' a
rho (SplitClause -> [NamedArg SplitPattern]
scPats SplitClause
sc) [NamedArg SplitPattern]
-> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
forall a. [a] -> [a] -> [a]
++ Telescope -> Boundary -> [NamedArg SplitPattern]
forall a.
DeBruijn a =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns Telescope
i Boundary
boundary
cps' = Substitution' (SubstArg (Map CheckpointId (Substitution' Term)))
-> Map CheckpointId (Substitution' Term)
-> Map CheckpointId (Substitution' Term)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Map CheckpointId (Substitution' Term)))
forall a. Substitution' a
rho (SplitClause -> Map CheckpointId (Substitution' Term)
scCheckpoints SplitClause
sc)
target' = Dom Type -> Maybe (Dom Type)
forall a. a -> Maybe a
Just (Dom Type -> Maybe (Dom Type)) -> Dom Type -> Maybe (Dom Type)
forall a b. (a -> b) -> a -> b
$ Type
b Type -> Dom Type -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
t
return . Just $ SClause tel' ps' idS cps' target'
splitResultRecord :: QName -> SplitClause -> TCM (Either SplitError Covering)
splitResultRecord :: QName -> SplitClause -> TCMT IO (Either SplitError Covering)
splitResultRecord QName
f sc :: SplitClause
sc@(SClause Telescope
tel [NamedArg SplitPattern]
ps Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
_ Maybe (Dom Type)
target) = do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"splitting result:"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"f =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc
-> (Dom Type -> TCMT IO Doc) -> Maybe (Dom Type) -> TCMT IO Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
forall a. Null a => a
empty Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Maybe (Dom Type)
target)
]
let failure :: a -> TCMT IO (Either a b)
failure = Either a b -> TCMT IO (Either a b)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either a b -> TCMT IO (Either a b))
-> (a -> Either a b) -> a -> TCMT IO (Either a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a b
forall a b. a -> Either a b
Left
Maybe (Dom Type)
-> TCMT IO (Either SplitError Covering)
-> (Dom Type -> TCMT IO (Either SplitError Covering))
-> TCMT IO (Either SplitError Covering)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target (SplitError -> TCMT IO (Either SplitError Covering)
forall {a} {b}. a -> TCMT IO (Either a b)
failure SplitError
CosplitNoTarget) ((Dom Type -> TCMT IO (Either SplitError Covering))
-> TCMT IO (Either SplitError Covering))
-> (Dom Type -> TCMT IO (Either SplitError Covering))
-> TCMT IO (Either SplitError Covering)
forall a b. (a -> b) -> a -> b
$ \ Dom Type
t -> do
(Telescope
-> TCMT IO (Maybe (QName, Args, RecordData))
-> TCMT IO (Maybe (QName, Args, RecordData))
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO (Maybe (QName, Args, RecordData))
-> TCMT IO (Maybe (QName, Args, RecordData)))
-> TCMT IO (Maybe (QName, Args, RecordData))
-> TCMT IO (Maybe (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (Maybe (QName, Args, RecordData))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, RecordData))
isRecordType (Type -> TCMT IO (Maybe (QName, Args, RecordData)))
-> Type -> TCMT IO (Maybe (QName, Args, RecordData))
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t) TCMT IO (Maybe (QName, Args, RecordData))
-> (Maybe (QName, Args, RecordData)
-> TCMT IO (Either SplitError Covering))
-> TCMT IO (Either SplitError Covering)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (QName, Args, RecordData)
Nothing -> Telescope
-> TCMT IO (Either SplitError Covering)
-> TCMT IO (Either SplitError Covering)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO (Either SplitError Covering)
-> TCMT IO (Either SplitError Covering))
-> TCMT IO (Either SplitError Covering)
-> TCMT IO (Either SplitError Covering)
forall a b. (a -> b) -> a -> b
$ do
SplitError -> TCMT IO (Either SplitError Covering)
forall {a} {b}. a -> TCMT IO (Either a b)
failure (SplitError -> TCMT IO (Either SplitError Covering))
-> (Closure Type -> SplitError)
-> Closure Type
-> TCMT IO (Either SplitError Covering)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Type -> SplitError
CosplitNoRecordType (Closure Type -> TCMT IO (Either SplitError Covering))
-> TCM (Closure Type) -> TCMT IO (Either SplitError Covering)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM (Closure Type)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t)
Just (QName
_r, Args
vs, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs }) -> do
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"we are of record type _r = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
_r
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"applied to parameters vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
vs)
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"and have fields fs = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Dom QName] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [Dom QName]
fs
]
let es :: Elims
es = NAPs -> Elims
patternsToElims (NAPs -> Elims) -> NAPs -> Elims
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
let self :: Arg Term
self = Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f [] Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
pargs :: Args
pargs = Args
vs Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ [Arg Term
self]
fieldValues :: [Term]
fieldValues = [Dom QName] -> (Dom QName -> Term) -> [Term]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom QName]
fs ((Dom QName -> Term) -> [Term]) -> (Dom QName -> Term) -> [Term]
forall a b. (a -> b) -> a -> b
$ \ Dom QName
proj -> Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
self Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem (Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
proj)]
[Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"we are self =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
self)
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" field values =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
fieldValues
]
let n :: Arg Int
n = Int -> Arg Int
forall a. a -> Arg a
defaultArg (Int -> Arg Int) -> Int -> Arg Int
forall a b. (a -> b) -> a -> b
$ Permutation -> Int
permRange (Permutation -> Int) -> Permutation -> Int
forall a b. (a -> b) -> a -> b
$ Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ NAPs -> Maybe Permutation
dbPatPerm (NAPs -> Maybe Permutation) -> NAPs -> Maybe Permutation
forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
projOrigin <- TCMT IO Bool
-> TCMT IO ProjOrigin -> TCMT IO ProjOrigin -> TCMT IO ProjOrigin
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optPostfixProjections (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (ProjOrigin -> TCMT IO ProjOrigin
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPostfix) (ProjOrigin -> TCMT IO ProjOrigin
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPrefix)
Right . Covering n <$> do
forM (zip fs $ List.inits fieldValues) $ \ (Dom QName
proj, [Term]
prevFields) -> do
dType <- Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (QName -> TCMT IO Definition) -> QName -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
proj
let
fieldSub = [Term] -> [Term]
forall a. [a] -> [a]
reverse ((Arg Term -> Term) -> Args -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg Args
vs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
prevFields) [Term] -> Substitution' Term -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Impossible -> Substitution' Term
forall a. Impossible -> Substitution' a
EmptyS Impossible
HasCallStack => Impossible
impossible
proj' = Substitution' (SubstArg (Dom QName)) -> Dom QName -> Dom QName
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Dom QName))
fieldSub Dom QName
proj
target' = Dom Type -> Maybe (Dom Type)
forall a. a -> Maybe a
Just (Dom Type -> Maybe (Dom Type)) -> Dom Type -> Maybe (Dom Type)
forall a b. (a -> b) -> a -> b
$ Dom QName
proj' Dom QName -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
dType Type -> Args -> Type
`piApply` Args
pargs
projArg = (QName -> Named NamedName SplitPattern)
-> Arg QName -> NamedArg SplitPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe NamedName -> SplitPattern -> Named NamedName SplitPattern
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
forall a. Maybe a
Nothing (SplitPattern -> Named NamedName SplitPattern)
-> (QName -> SplitPattern) -> QName -> Named NamedName SplitPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProjOrigin -> QName -> SplitPattern
forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
projOrigin) (Arg QName -> NamedArg SplitPattern)
-> Arg QName -> NamedArg SplitPattern
forall a b. (a -> b) -> a -> b
$ Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom (Dom QName -> Arg QName) -> Dom QName -> Arg QName
forall a b. (a -> b) -> a -> b
$ Hiding -> Dom QName -> Dom QName
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden Dom QName
proj
sc' = SplitClause
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', NoInfo))
instance PrettyTCM SplitClause where
prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitClause -> m Doc
prettyTCM (SClause Telescope
tel [NamedArg SplitPattern]
pats Substitution' SplitPattern
sigma Map CheckpointId (Substitution' Term)
cps Maybe (Dom Type)
target) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ m Doc
"SplitClause"
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ m Doc
"tel =" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
, m Doc
"pats =" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((NamedArg SplitPattern -> m Doc)
-> [NamedArg SplitPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SplitPattern -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => SplitPattern -> m Doc
prettyTCM (SplitPattern -> m Doc)
-> (NamedArg SplitPattern -> SplitPattern)
-> NamedArg SplitPattern
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg) [NamedArg SplitPattern]
pats)
, m Doc
"subst =" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' SplitPattern -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Substitution' SplitPattern -> m Doc
prettyTCM Substitution' SplitPattern
sigma
, m Doc
"checkpoints =" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Map CheckpointId (Substitution' Term) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Map CheckpointId (Substitution' Term) -> m Doc
prettyTCM Map CheckpointId (Substitution' Term)
cps
, m Doc
"target =" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
Maybe (Dom Type) -> m Doc -> (Dom Type -> m Doc) -> m Doc
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target m Doc
forall a. Null a => a
empty ((Dom Type -> m Doc) -> m Doc) -> (Dom Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Dom Type
t -> do
Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
t
]
]