{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeApplications #-}

{-| Coverage checking, case splitting, and splitting for refine tactics.

 -}

module Agda.TypeChecking.Coverage
  ( SplitClause(..), clauseToSplitClause, insertTrailingArgs
  , Covering(..), splitClauses
  , coverageCheck
  , isCovered
  , splitClauseWithAbsurd
  , splitLast
  , splitResult
  , normaliseProjP
  ) where

import Prelude hiding (null, (!!))  -- do not use partial functions like !!

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 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.Names
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Monad

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.Telescope.Path
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Warnings

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.WithDefault

import Agda.Utils.Impossible
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Control.Monad.State


type CoverM = ExceptT SplitError TCM

-- | Top-level function for checking pattern coverage.
--
--   Effects:
--
--   - Marks unreachable clauses as such in the signature.
--
--   - Adds missing instances clauses to the signature.
--
coverageCheck
  :: QName     -- ^ Name @f@ of definition.
  -> Type      -- ^ Absolute type (including the full parameter telescope).
  -> [Clause]  -- ^ Clauses of @f@.  These are the very clauses of @f@ in the signature.
  -> TCM SplitTree
coverageCheck :: QName -> Type -> [Clause] -> TCM SplitTree
coverageCheck QName
f Type
t [Clause]
cs = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.top" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"entering coverageCheck for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
75 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  of type (raw): " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> [Char]
prettyShow) Type
t
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"  of type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
  TelV Telescope
gamma Type
a <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo (-Int
1) Type
t
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.top" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"coverageCheck: computed telView"

  let -- n             = arity
      -- xs            = variable patterns fitting lgamma
      n :: Int
n            = forall a. Sized a => a -> Int
size Telescope
gamma
      xs :: [NamedArg SplitPattern]
xs           =  forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.top" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"coverageCheck: getDefFreeVars"

      -- The initial module parameter substitutions need to be weakened by the
      -- number of arguments that aren't module parameters.
  Int
fv           <- forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
f

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.top" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"coverageCheck: getting checkpoints"

  -- TODO: does this make sense? Why are we weakening by n - fv?
  Map CheckpointId (Substitution' Term)
checkpoints <- forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> Substitution' a
raiseS (Int
n forall a. Num a => a -> a -> a
- Int
fv)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints

      -- construct the initial split clause
  let sc :: SplitClause
sc = Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
gamma [NamedArg SplitPattern]
xs forall a. Substitution' a
idS Map CheckpointId (Substitution' Term)
checkpoints forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom Type
a

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 forall a b. (a -> b) -> a -> b
$ do
    let prCl :: Clause -> m Doc
prCl Clause
cl = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
cl) forall a b. (a -> b) -> a -> b
$
                  forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Coverage checking " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f forall a. [a] -> [a] -> [a]
++ [Char]
" with patterns:"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
 MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
Clause -> m Doc
prCl [Clause]
cs
      ]

  -- used = actually used clauses for cover
  -- pss  = non-covered cases
  CoverResult SplitTree
splitTree IntSet
used [(Telescope, NAPs)]
pss [Clause]
qss IntSet
noex <- QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs SplitClause
sc

  -- Andreas, 2018-11-12, issue #378:
  -- some indices in @used@ and @noex@ point outside of @cs@,
  -- since missing hcomp clauses have been added during the course of @cover@.
  -- We simply delete theses indices from @noex@.
  [Int]
noex <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
List.filter (forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cs) forall a b. (a -> b) -> a -> b
$ IntSet -> [Int]
IntSet.toList IntSet
noex

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"cover computed!"
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"used clauses: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show IntSet
used
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"non-exact clauses: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Int]
noex
    ]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.splittree" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"generated split tree for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
    , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow SplitTree
splitTree
    ]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.covering" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"covering patterns for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
f
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ Clause
cl -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
cl) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl) [Clause]
qss
    ]

  -- Storing the covering clauses so that checkIApplyConfluence_ can
  -- find them later.
  -- Andreas, 2019-03-27, only needed when --cubical
  -- Jesper, 2022-10-18, also needed for some backends, so keep when flag says so
  PragmaOptions
opts <- forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Maybe a -> Bool
isJust (PragmaOptions -> Maybe Cubical
optCubical PragmaOptions
opts) Bool -> Bool -> Bool
|| PragmaOptions -> Bool
optKeepCoveringClauses PragmaOptions
opts) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
f forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef forall a b. (a -> b) -> a -> b
$ ([Clause] -> [Clause]) -> Defn -> Defn
updateCovering forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const [Clause]
qss


  -- filter out the missing clauses that are absurd.
  [(Telescope, NAPs)]
pss <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [(Telescope, NAPs)]
pss forall a b. (a -> b) -> a -> b
$ \(Telescope
tel,NAPs
ps) ->
    -- Andreas, 2019-04-13, issue #3692: when adding missing absurd
    -- clauses, also put the absurd pattern in.
    forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
checkEmptyTel forall a. Range' a
noRange Telescope
tel) (\ ErrorNonEmpty
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) forall a b. (a -> b) -> a -> b
$ \ Int
l -> do
      -- Now, @l@ is the first type in @tel@ (counting from 0=leftmost)
      -- which is empty.  Turn it into a de Bruijn index @i@.
      let i :: Int
i = forall a. Sized a => a -> Int
size Telescope
tel forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- Int
l
      -- Build a substitution mapping this pattern variable to the absurd pattern.
      let sub :: PatternSubstitution
sub = forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i forall a b. (a -> b) -> a -> b
$ Int -> DeBruijnPattern
absurdP Int
i
        -- ifNotM (isEmptyTel tel) (return True) $ do
      -- Jesper, 2018-11-28, Issue #3407: if the clause is absurd,
      -- add the appropriate absurd clause to the definition.
      let cl :: Clause
cl = Clause { clauseLHSRange :: Range
clauseLHSRange  = forall a. Range' a
noRange
                      , clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
                      , clauseTel :: Telescope
clauseTel       = Telescope
tel
                      , namedClausePats :: NAPs
namedClausePats = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
sub NAPs
ps
                      , clauseBody :: Maybe Term
clauseBody      = forall a. Maybe a
Nothing
                      , clauseType :: Maybe (Arg Type)
clauseType      = forall a. Maybe a
Nothing
                      , clauseCatchall :: Bool
clauseCatchall    = Bool
True       -- absurd clauses are safe as catch-all
                      , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
False
                      , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. a -> Maybe a
Just Bool
False
                      , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False
                      , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                      , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
                      }
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.missing" Int
20 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"adding missing absurd clause"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. QName -> a -> QNamed a
QNamed QName
f Clause
cl
            ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.missing" Int
80 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"l   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
l
        , TCMT IO Doc
"i   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
i
        , TCMT IO Doc
"cl  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. QName -> a -> QNamed a
QNamed QName
f Clause
cl)
        ]
      forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
f [Clause
cl]
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  -- report a warning if there are uncovered cases,
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [(Telescope, NAPs)]
pss) forall a b. (a -> b) -> a -> b
$ do
    Lens' (Set QName) TCState
stLocalPartialDefs forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall a. Ord a => a -> Set a -> Set a
Set.insert QName
f
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((CoverageCheck
YesCoverageCheck forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CoverageCheck TCEnv
eCoverageCheck) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [Clause]
cs forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> [(Telescope, NAPs)] -> Warning
CoverageIssue QName
f [(Telescope, NAPs)]
pss

  -- Andreas, 2017-08-28, issue #2723:
  -- Mark clauses as reachable or unreachable in the signature.
  -- Andreas, 2020-11-19, issue #5065
  -- Remember whether clauses are exact or not.
  let ([Maybe Int]
is0, [Clause]
cs1) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Clause]
cs) forall a b. (a -> b) -> a -> b
$ \ (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 (forall a. Bool -> a -> Maybe a
boolToMaybe Bool
unreachable Int
i, Clause
cl
             { clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
unreachable
             , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
exact
             })
  -- is = indices of unreachable clauses
  let is :: [Int]
is = forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
is0
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"unreachable clauses: " forall a. [a] -> [a] -> [a]
++ if forall a. Null a => a -> Bool
null [Int]
is then [Char]
"(none)" else forall a. Show a => a -> [Char]
show [Int]
is
    ]
  -- Replace the first clauses by @cs1@.  There might be more
  -- added by @inferMissingClause@.
  QName -> ([Clause] -> [Clause]) -> TCMT IO ()
modifyFunClauses QName
f forall a b. (a -> b) -> a -> b
$ \ [Clause]
cs0 -> [Clause]
cs1 forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cs1) [Clause]
cs0

  -- Warn if there are unreachable clauses and mark them as unreachable.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Int]
is) forall a b. (a -> b) -> a -> b
$ do
    -- Warn about unreachable clauses.
    let unreached :: [Clause]
unreached = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. a -> Maybe a
Just Bool
True forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseUnreachable) [Clause]
cs1
    let ranges :: [Range]
ranges    = forall a b. (a -> b) -> [a] -> [b]
map Clause -> Range
clauseFullRange [Clause]
unreached
    forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [Range]
ranges forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> [Range] -> Warning
UnreachableClauses QName
f [Range]
ranges

  -- report a warning if there are clauses that are not preserved as
  -- definitional equalities and --exact-split is enabled
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Int]
noex) forall a b. (a -> b) -> a -> b
$ do
      let noexclauses :: [Clause]
noexclauses = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Clause]
cs1) [Int]
noex
      forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (forall a b. (a -> b) -> [a] -> [b]
map Clause -> Range
clauseLHSRange [Clause]
noexclauses) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ QName -> [Clause] -> Warning
CoverageNoExactSplit QName
f forall a b. (a -> b) -> a -> b
$ [Clause]
noexclauses
  forall (m :: * -> *) a. Monad m => a -> m a
return SplitTree
splitTree

-- | Top-level function for eliminating redundant clauses in the interactive
--   case splitter
isCovered :: QName -> [Clause] -> SplitClause -> TCM Bool
isCovered :: QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause]
cs SplitClause
sc = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.isCovered" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"isCovered"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
      [ TCMT IO Doc
"f  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
      , TCMT IO Doc
"cs = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM 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 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitClause
sc
      ]
    ]
  -- Jesper, 2019-10: introduce trailing arguments (see #3828)
  (Telescope
_ , SplitClause
sc') <- Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
True SplitClause
sc
  CoverResult { coverMissingClauses :: CoverResult -> [(Telescope, NAPs)]
coverMissingClauses = [(Telescope, NAPs)]
missing } <- QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs SplitClause
sc'
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null [(Telescope, NAPs)]
missing
 -- Andreas, 2019-08-08 and 2020-02-11
 -- If there is an error (e.g. unification error), don't report it
 -- to the user.  Rather, assume the clause is not already covered.
 forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | @cover f cs (SClause _ _ ps _) = return (splitTree, used, pss)@.
--   checks that the list of clauses @cs@ covers the given split clause.
--   Returns the @splitTree@, the @used@ clauses, and missing cases @pss@.
--
--   Effect: adds missing instance clauses for @f@ to signature.
--
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) = forall a. TCM a -> TCM a
updateRelevance forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.cover" Int
10 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"checking coverage of pattern:"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitClause
sc
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target sort =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"<none>") (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensSort a => a -> Sort
getSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Maybe (Dom Type)
target
    ]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.cover" Int
80 forall a b. (a -> b) -> a -> b
$ [Char]
"raw target =\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Maybe (Dom Type)
target
  forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS  [Char]
"tc.cover.matching" Int
20 forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.matching" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"clauses when matching:"
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Clause]
cs 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
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.matching" Int
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"ps   :" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. NamedArg a -> a
namedArg NAPs
ps)

  forall (m :: * -> *).
PureTCM m =>
[Clause]
-> [NamedArg SplitPattern]
-> m (Match (Int, [(Int, SplitPattern)]))
match [Clause]
cs [NamedArg SplitPattern]
ps forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Yes (Int
i,[(Int, SplitPattern)]
mps) -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.cover" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"pattern covered by clause " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.cover" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"with mps = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, SplitPattern)]
mps
      Bool
exact <- forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM [(Int, SplitPattern)]
mps forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
isTrivialPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
      let cl0 :: Clause
cl0 = forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Clause]
cs Int
i
      Clause
cl <- SplitClause -> Clause -> [(Int, SplitPattern)] -> TCM Clause
applyCl SplitClause
sc Clause
cl0 [(Int, SplitPattern)]
mps
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CoverResult
        { coverSplitTree :: SplitTree
coverSplitTree      = forall a. Int -> SplitTree' a
SplittingDone (forall a. Sized a => a -> Int
size Telescope
tel)
        , coverUsedClauses :: IntSet
coverUsedClauses    = forall el coll. Singleton el coll => el -> coll
singleton Int
i
        , coverMissingClauses :: [(Telescope, NAPs)]
coverMissingClauses = []
        , coverPatterns :: [Clause]
coverPatterns       = [Clause
cl]
        , coverNoExactClauses :: IntSet
coverNoExactClauses = [Int] -> IntSet
IntSet.fromList [ Int
i | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Bool
exact Bool -> Bool -> Bool
|| Clause -> Bool
clauseCatchall Clause
cl0 ]
        }

    Match (Int, [(Int, SplitPattern)])
No        ->  do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"pattern is not covered"
      let infer :: Dom' a e -> Bool
infer Dom' a e
dom = forall a. LensHiding a => a -> Bool
isInstance Dom' a e
dom Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust (forall t e. Dom' t e -> Maybe t
domTactic Dom' a e
dom)
      if forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False forall {a} {e}. Dom' a e -> Bool
infer Maybe (Dom Type)
target
        then do
          -- Ulf, 2016-10-31: For now we only infer instance clauses. It would
          -- make sense to do it also for hidden, but since the value of a
          -- hidden clause is expected to be forced by later clauses, it's too
          -- late to add it now. If it was inferrable we would have gotten a
          -- type error before getting to this point.
          -- Ulf, 2019-11-21: Also @tactic clauses.
          Clause
cl <- QName -> SplitClause -> TCM Clause
inferMissingClause QName
f SplitClause
sc
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult (forall a. Int -> SplitTree' a
SplittingDone (forall a. Sized a => a -> Int
size Telescope
tel)) forall a. Null a => a
empty [] [Clause
cl] forall a. Null a => a
empty
        else do
          let ps' :: NAPs
ps' = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult (forall a. Int -> SplitTree' a
SplittingDone (forall a. Sized a => a -> Int
size Telescope
tel)) forall a. Null a => a
empty [(Telescope
tel, NAPs
ps')] [] forall a. Null a => a
empty

    -- We need to split!
    -- If all clauses have an unsplit copattern, we try that first.
    Block BlockedOnResult
res BlockingVars
bs -> BlockedOnResult
-> Bool
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
-> TCM CoverResult
trySplitRes BlockedOnResult
res (forall a. Null a => a -> Bool
null BlockingVars
bs) forall a. SplitError -> TCM a
splitError forall a b. (a -> b) -> a -> b
$ do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Null a => a -> Bool
null BlockingVars
bs) forall a. HasCallStack => a
__IMPOSSIBLE__
      -- Otherwise, if there are variables to split, we try them
      -- in the order determined by a split strategy.
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.strategy" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"blocking vars = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow BlockingVars
bs
      -- xs is a non-empty lists of blocking variables
      -- try splitting on one of them
      BlockingVars
xs <- BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy BlockingVars
bs Telescope
tel
      -- Andreas, 2017-10-08, issue #2594
      -- First, try to find split order for complete coverage.
      -- If this fails, try to at least carry out the splitting to the end.
      BlockingVars
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue BlockingVars
xs AllowPartialCover
NoAllowPartialCover forall a b. (a -> b) -> a -> b
$ \ SplitError
_err -> do
        BlockingVars
-> AllowPartialCover
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
continue BlockingVars
xs AllowPartialCover
YesAllowPartialCover forall a b. (a -> b) -> a -> b
$ \ SplitError
err -> do
          forall a. SplitError -> TCM a
splitError SplitError
err
  where
    -- Andreas, 2019-08-07, issue #3966
    -- When we get a SplitError, tighten the error Range to the clauses
    -- that are still candidates for covering the SplitClause.
    splitError :: SplitError -> TCM a
    splitError :: forall a. SplitError -> TCM a
splitError = forall a. TCM a -> TCM a
withRangeOfCandidateClauses forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitError -> TypeError
SplitError

    -- This repeats the matching, but since we are crashing anyway,
    -- the extra work just to compute a better Range does not matter.
    withRangeOfCandidateClauses :: TCM a -> TCM a
    withRangeOfCandidateClauses :: forall a. TCM a -> TCM a
withRangeOfCandidateClauses TCM a
cont = do
      [Clause]
cands <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Clause -> Match a -> Maybe Clause
notNo) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [Clause]
cs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
PureTCM m =>
[NamedArg SplitPattern]
-> Clause -> m (Match (DList (Int, SplitPattern)))
matchClause [NamedArg SplitPattern]
ps) [Clause]
cs
      forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange [Clause]
cands TCM a
cont
      where
        notNo :: Clause -> Match a -> Maybe Clause
        notNo :: forall a. Clause -> Match a -> Maybe Clause
notNo Clause
c = \case
          Yes{}   -> forall a. a -> Maybe a
Just Clause
c
          Block{} -> forall a. a -> Maybe a
Just Clause
c
          No{}    -> forall a. Maybe a
Nothing

    -- Rename the variables in a telescope in accordance with their
    -- first appearance in the given NAPs. This is done to preserve
    -- variable names in IApplyConfluence error messages. Specifically,
    -- consider e.g.
    --
    --  data T : Set where
    --    x : T
    --    p : Path (Path T x x) refl refl
    --  f (p i j) = ...
    --
    -- When generating the covering clause corresponding to f's clause,
    -- the names we have in scope are i and i₁, since those are the
    -- names of both PathP binder arguments. (recall Path A x y = PathP (λ i → A) x y)
    -- So if we tried to print (Var 0 []) in the context of
    -- IApplyConfluence for that clause, what we see isn't j, it's i₁.
    --
    -- This function takes "name suggestions" from both variable
    -- patterns and IApply co/patterns, and replaces any existing names
    -- in the telescope by the name in that pattern.
    renTeleFromNap :: Telescope -> NAPs -> Telescope
    renTeleFromNap :: Telescope -> NAPs -> Telescope
renTeleFromNap Telescope
tel NAPs
ps = ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> a
evalState (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Dom ([Char], Type) -> State Int (Dom ([Char], Type))
upd (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel)) (Int
size forall a. Num a => a -> a -> a
- Int
1)
      where
        -- Fold a single pattern into a map of name suggestions:
        -- In the running example above, we have
        --    f (p i@1 j@0)
        -- so the map that nameSuggest (p ...) returns is {0 → j, 1 → j}
        nameSuggest :: DeBruijnPattern -> IntMap ArgName
        nameSuggest :: DeBruijnPattern -> IntMap [Char]
nameSuggest DeBruijnPattern
ps = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b m.
(PatternLike a b, Monoid m) =>
(Pattern' a -> m) -> b -> m
foldPattern DeBruijnPattern
ps forall a b. (a -> b) -> a -> b
$ \case
          VarP PatternInfo
_ DBPatVar
i | DBPatVar -> [Char]
dbPatVarName DBPatVar
i forall a. Eq a => a -> a -> Bool
/= [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 forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ->
            forall a. Int -> a -> IntMap a
IntMap.singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
i) (DBPatVar -> [Char]
dbPatVarName DBPatVar
i)
          DeBruijnPattern
_ -> forall a. Monoid a => a
mempty

        -- Suggestions from all patterns..
        suggestions :: IntMap [Char]
suggestions = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (DeBruijnPattern -> IntMap [Char]
nameSuggest forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) NAPs
ps

        -- The state will start counting from (length Γ - 1), which is
        -- the *highest* variable index, i.e. the index of the variable
        -- with level 0. Instead of doing a lot of de Bruijn arithmetic
        -- + recursion, traverse handles iteration and the State handles
        -- counting down.
        size :: Int
size = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel)
        upd :: Dom (ArgName , Type) -> State Int (Dom (ArgName , Type))
        upd :: Dom ([Char], Type) -> State Int (Dom ([Char], Type))
upd Dom ([Char], Type)
dom = forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state forall a b. (a -> b) -> a -> b
$ \Int
s -> do
          case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
s IntMap [Char]
suggestions of
            Just [Char]
nm' -> ( Dom ([Char], Type)
dom{ domName :: Maybe NamedName
domName = forall a. a -> Maybe a
Just (forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
CaseSplit (forall a. a -> Ranged a
unranged [Char]
nm'))
                             , unDom :: ([Char], Type)
unDom = ([Char]
nm' , forall a b. (a, b) -> b
snd (forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
dom))
                             } , Int
s forall a. Num a => a -> a -> a
- Int
1)
            Maybe [Char]
Nothing -> (Dom ([Char], Type)
dom , Int
s forall a. Num a => a -> a -> a
- Int
1)

    applyCl :: SplitClause -> Clause -> [(Nat, SplitPattern)] -> TCM Clause
    applyCl :: SplitClause -> Clause -> [(Int, SplitPattern)] -> TCM Clause
applyCl SClause{scTel :: SplitClause -> Telescope
scTel = Telescope
pretel, scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
sps} Clause
cl [(Int, SplitPattern)]
mps
        | Telescope
tel <- Telescope -> NAPs -> Telescope
renTeleFromNap Telescope
pretel (Clause -> NAPs
namedClausePats Clause
cl) = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
        let ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
cl
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"applyCl"
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
tel
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NAPs
ps
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"mps    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, SplitPattern)]
mps
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"s      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PatternSubstitution
s
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps[s]  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (PatternSubstitution
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` NAPs
ps)

        -- If a matching clause has fewer patterns than the split
        -- clause we ought to copy over the extra ones.
        -- e.g. if the user wrote:
        --
        --   bar : Bool -> Bool
        --   bar false = false
        --   bar = \ _ -> true
        --
        -- then for the second clause the @extra@ patterns will be @[true]@.

        let extra :: NAPs
extra = forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
ps) forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
sps
            n_extra :: Int
n_extra = forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
extra

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"extra  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty NAPs
extra

        -- When we add the extra patterns we also update the type
        -- and the body of the clause.

        Maybe (Arg (TelV Type))
mtv <- (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall (m :: * -> *). PureTCM m => Int -> Type -> m (TelV Type)
telViewUpToPath Int
n_extra) forall a b. (a -> b) -> a -> b
$ Clause -> Maybe (Arg Type)
clauseType Clause
cl
        let ty :: Maybe (Arg Type)
ty = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ((forall a. DeBruijn a => [a] -> Substitution' a
parallelS (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs
extra) forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` forall a. Int -> Substitution' a -> Substitution' a
liftS Int
n_extra PatternSubstitution
s forall a. TermSubst a => PatternSubstitution -> a -> a
`applyPatSubst`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TelV a -> a
theCore) Maybe (Arg (TelV Type))
mtv

        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.applyCl" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"new ty =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Maybe (Arg Type)
ty

        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
             Clause { clauseLHSRange :: Range
clauseLHSRange  = Clause -> Range
clauseLHSRange Clause
cl
                    , clauseFullRange :: Range
clauseFullRange = Clause -> Range
clauseFullRange Clause
cl
                    , clauseTel :: Telescope
clauseTel       = Telescope
tel
                    , namedClausePats :: NAPs
namedClausePats = (PatternSubstitution
s forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` NAPs
ps) forall a. [a] -> [a] -> [a]
++ NAPs
extra
                    , clauseBody :: Maybe Term
clauseBody      = (forall t. Apply t => t -> Elims -> t
`applyE` NAPs -> Elims
patternsToElims NAPs
extra) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PatternSubstitution
s forall a. TermSubst a => PatternSubstitution -> a -> a
`applyPatSubst`) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Clause -> Maybe Term
clauseBody Clause
cl
                    , clauseType :: Maybe (Arg Type)
clauseType      = Maybe (Arg Type)
ty
                    , clauseCatchall :: Bool
clauseCatchall    = Clause -> Bool
clauseCatchall Clause
cl
                    , clauseExact :: Maybe Bool
clauseExact       = Clause -> Maybe Bool
clauseExact Clause
cl
                    , clauseRecursive :: Maybe Bool
clauseRecursive   = Clause -> Maybe Bool
clauseRecursive Clause
cl
                    , clauseUnreachable :: Maybe Bool
clauseUnreachable = Clause -> Maybe Bool
clauseUnreachable Clause
cl
                    , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = Clause -> ExpandedEllipsis
clauseEllipsis Clause
cl
                    , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Clause -> Maybe ModuleName
clauseWhereModule Clause
cl
                    }
      where
      mps' :: Map Int DeBruijnPattern
mps' =
        forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$
        forall a b. (a -> b) -> [a] -> [b]
map (forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (forall a. NamedArg a -> a
namedArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg SplitPattern -> Arg (Named_ DeBruijnPattern)
fromSplitPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg)) [(Int, SplitPattern)]
mps
      s :: PatternSubstitution
s = forall a. DeBruijn a => [a] -> Substitution' a
parallelS (forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (case 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]) forall a b. (a -> b) -> a -> b
$ \ Int
i ->
                     forall a. a -> Maybe a -> a
fromMaybe (forall a. DeBruijn a => Int -> a
deBruijnVar Int
i) (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 =
      -- Don't do anything if there is no target type info.
      forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target TCM a
cont forall a b. (a -> b) -> a -> b
$ \ Dom Type
b -> do
        -- TODO (2018-10-16): if proofs get erased in the compiler, also wake erased vars!
        let m :: Modality
m = forall a. LensModality a => a -> Modality
getModality Dom Type
b
        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
      Either SplitError (Covering, BlockingVar)
r <- forall (m :: * -> *) a err b.
Monad m =>
(a -> m (Either err b)) -> [a] -> m (Either err b)
altM1 (\ BlockingVar
x -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,BlockingVar
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
split Induction
Inductive AllowPartialCover
allowPartialCover SplitClause
sc BlockingVar
x) BlockingVars
xs
      case Either SplitError (Covering, BlockingVar)
r of
        Left SplitError
err -> SplitError -> TCM CoverResult
handle SplitError
err
        -- If we get the empty covering, we have reached an impossible case
        -- and are done.
        Right (Covering Arg Int
n [], BlockingVar
_) ->
         do
          -- TODO Andrea: I guess an empty pattern is not part of the cover?
          let qs :: [a]
qs = []
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult (forall a. Int -> SplitTree' a
SplittingDone (forall a. Sized a => a -> Int
size Telescope
tel)) forall a. Null a => a
empty [] forall a. [a]
qs forall a. Null a => a
empty
        Right (Covering Arg Int
n [(SplitTag, (SplitClause, IInfo))]
scs', BlockingVar
x) -> do
          let scs :: [(SplitTag, SplitClause)]
scs = forall a b. (a -> b) -> [a] -> [b]
map (\(SplitTag
t,(SplitClause
sc,IInfo
i)) -> (SplitTag
t,SplitClause
sc)) [(SplitTag, (SplitClause, IInfo))]
scs'

          ([(SplitTag, CoverResult)]
results_trX, [Clause]
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
          ([(SplitTag, SplitClause)]
scs, [Clause]
cs, [(SplitTag, CoverResult)]
results_hc) <- do
            let fallback :: TCMT
  IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return ([(SplitTag, SplitClause)]
scs, [Clause]
cs, [])
            forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getPrimitiveName' [Char]
builtinHComp) TCMT
  IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
fallback forall a b. (a -> b) -> a -> b
$ \ QName
comp -> do
            let isComp :: SplitTag -> Bool
isComp = \case
                  SplitCon QName
c -> QName
comp forall a. Eq a => a -> a -> Bool
== QName
c
                  SplitTag
_ -> Bool
False
            forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (SplitTag -> Bool
isComp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(SplitTag, SplitClause)]
scs) TCMT
  IO ([(SplitTag, SplitClause)], [Clause], [(SplitTag, CoverResult)])
fallback forall a b. (a -> b) -> a -> b
$ \ (SplitTag
sp, SplitClause
newSc) -> do
            ([(SplitTag, CoverResult)]
res,[Clause]
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)]
scs2 = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitTag -> Bool
isComp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(SplitTag, SplitClause)]
scs
            forall (m :: * -> *) a. Monad m => a -> m a
return ([(SplitTag, SplitClause)]
scs2,[Clause]
cs',[(SplitTag, CoverResult)]
res)
          let results_extra :: [(SplitTag, CoverResult)]
results_extra = [(SplitTag, CoverResult)]
results_hc forall a. [a] -> [a] -> [a]
++ [(SplitTag, CoverResult)]
results_trX
              trees_extra :: [(SplitTag, SplitTree)]
trees_extra = forall a b. (a -> b) -> [a] -> [b]
map (\(SplitTag
sp,CoverResult
cr) -> (SplitTag
sp, CoverResult -> SplitTree
coverSplitTree CoverResult
cr)) [(SplitTag, CoverResult)]
results_extra

          [CoverResult]
results <- (forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd ([(SplitTag, CoverResult)]
results_extra)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(SplitTag, SplitClause)]
scs
          let trees :: [SplitTree]
trees = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> SplitTree
coverSplitTree      [CoverResult]
results
              useds :: [IntSet]
useds = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverUsedClauses    [CoverResult]
results
              psss :: [[(Telescope, NAPs)]]
psss  = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [(Telescope, NAPs)]
coverMissingClauses [CoverResult]
results
              qsss :: [[Clause]]
qsss  = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [Clause]
coverPatterns       [CoverResult]
results
              noex :: [IntSet]
noex  = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverNoExactClauses [CoverResult]
results
          -- Jesper, 2016-03-10  We need to remember which variables were
          -- eta-expanded by the unifier in order to generate a correct split
          -- tree (see Issue 1872).
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.eta" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"etaRecordSplits"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"n   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Arg Int
n)
              , TCMT IO Doc
"scs = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [(SplitTag, SplitClause)]
scs
              , TCMT IO Doc
"ps  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList ([NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps)
              ]
            ]
          let trees' :: [(SplitTag, SplitTree)]
trees' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Int
-> [NamedArg SplitPattern]
-> (SplitTag, SplitClause)
-> SplitTree
-> (SplitTag, SplitTree)
etaRecordSplits (forall e. Arg e -> e
unArg Arg Int
n) [NamedArg SplitPattern]
ps) [(SplitTag, SplitClause)]
scs [SplitTree]
trees
              tree :: SplitTree
tree   = forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
n LazySplit
StrictSplit ([(SplitTag, SplitTree)]
trees' forall a. [a] -> [a] -> [a]
++ [(SplitTag, SplitTree)]
trees_extra) -- TODO: Lazy?
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult SplitTree
tree (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet]
useds) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Telescope, NAPs)]]
psss) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Clause]]
qsss) (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet]
noex)

    -- Try to split result
    trySplitRes
      :: BlockedOnResult                  -- Are we blocked on the result?
      -> Bool                             -- Is this the last thing we try?
      -> (SplitError -> TCM CoverResult)  -- Handler for 'SplitError'
      -> TCM CoverResult                  -- Continuation
      -> TCM CoverResult
    -- not blocked on result: try regular splits
    trySplitRes :: BlockedOnResult
-> Bool
-> (SplitError -> TCM CoverResult)
-> TCM CoverResult
-> TCM CoverResult
trySplitRes BlockedOnResult
NotBlockedOnResult Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont
      | Bool
finalSplit = forall a. HasCallStack => a
__IMPOSSIBLE__ -- there must be *some* reason we are blocked
      | Bool
otherwise  = TCM CoverResult
cont
    -- blocked on arguments that are not yet introduced:

    -- we must split on a variable so that the target type becomes a pi type
    trySplitRes (BlockedOnApply ApplyOrIApply
IsApply) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont = do
      -- Andreas, 2021-12-31, issue #5712.
      -- If there is a tactic to solve the clause, we might not have inserted
      -- trailing args (due to #5358).  Now we force it!
      (Telescope
tel, SplitClause
sc') <- Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
True SplitClause
sc
      if forall a. Null a => a -> Bool
null Telescope
tel then
        if Bool
finalSplit then forall a. HasCallStack => a
__IMPOSSIBLE__ -- already ruled out by lhs checker
        else TCM CoverResult
cont
      else QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs SplitClause
sc'

    -- ...or it was an IApply pattern, so we might just need to introduce the variable now.
    trySplitRes (BlockedOnApply ApplyOrIApply
IsIApply) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont
       = do
         forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> SplitClause -> TCM (Maybe SplitClause)
splitResultPath QName
f SplitClause
sc) TCM CoverResult
fallback forall a b. (a -> b) -> a -> b
$ (QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) 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 = forall a. HasCallStack => a
__IMPOSSIBLE__ -- already ruled out by lhs checker?
                 | Bool
otherwise  = TCM CoverResult
cont

    -- blocked on result but there are catchalls:
    -- try regular splits if there are any, or else throw an error,
    -- this is nicer than continuing and reporting unreachable clauses
    -- (see issue #2833)
    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
    -- all clauses have an unsplit copattern: try to split
    trySplitRes (BlockedOnProj Bool
False) Bool
finalSplit SplitError -> TCM CoverResult
splitError TCM CoverResult
cont = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"blocked by projection pattern"
      -- forM is a monadic map over a Maybe here
      Either SplitError Covering
mcov <- QName -> SplitClause -> TCM (Either SplitError Covering)
splitResultRecord QName
f SplitClause
sc
      case Either SplitError Covering
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
          -- If result splitting was successful, continue coverage checking.
          ([SplitTag]
projs, [CoverResult]
results) <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (m :: * -> *) a b.
(Decoration t, Functor m) =>
(a -> m b) -> t a -> m (t b)
traverseF forall a b. (a -> b) -> a -> b
$ QName -> [Clause] -> SplitClause -> TCM CoverResult
cover QName
f [Clause]
cs forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
False)) (forall a b. (a -> b) -> [a] -> [b]
map (\(SplitTag
t,(SplitClause
sc,IInfo
i)) -> (SplitTag
t,SplitClause
sc)) [(SplitTag, (SplitClause, IInfo))]
scs)
            -- OR:
            -- forM scs $ \ (proj, sc') -> (proj,) <$> do
            --   cover f cs =<< do
            --     snd <$> fixTarget sc'
          let trees :: [SplitTree]
trees = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> SplitTree
coverSplitTree [CoverResult]
results
              useds :: [IntSet]
useds = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverUsedClauses [CoverResult]
results
              psss :: [[(Telescope, NAPs)]]
psss  = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [(Telescope, NAPs)]
coverMissingClauses [CoverResult]
results
              qsss :: [[Clause]]
qsss  = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> [Clause]
coverPatterns [CoverResult]
results
              noex :: [IntSet]
noex  = forall a b. (a -> b) -> [a] -> [b]
map CoverResult -> IntSet
coverNoExactClauses [CoverResult]
results
              tree :: SplitTree
tree  = forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
n LazySplit
StrictSplit forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [SplitTag]
projs [SplitTree]
trees   -- TODO: Lazy?
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SplitTree
-> IntSet
-> [(Telescope, NAPs)]
-> [Clause]
-> IntSet
-> CoverResult
CoverResult SplitTree
tree (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet]
useds) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Telescope, NAPs)]]
psss) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Clause]]
qsss) (forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions [IntSet]
noex)

    gatherEtaSplits :: Int -> SplitClause
                    -> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
    gatherEtaSplits :: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc []
       | Int
n forall a. Ord a => a -> a -> Bool
>= Int
0    = forall a. HasCallStack => a
__IMPOSSIBLE__ -- we should have encountered the main
                                    -- split by now already
       | Bool
otherwise = []
    gatherEtaSplits Int
n SplitClause
sc (NamedArg SplitPattern
p:[NamedArg SplitPattern]
ps) = case forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p of
      VarP PatternInfo
_ SplitPatVar
x
       | Int
n forall a. Eq a => a -> a -> Bool
== Int
0    -> case SplitPattern
p' of -- this is the main split
           VarP  PatternInfo
_ SplitPatVar
_    -> NamedArg SplitPattern
p forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
           DotP  PatternInfo
_ Term
_    -> forall a. HasCallStack => a
__IMPOSSIBLE__
           ConP  ConHead
_ ConPatternInfo
_ [NamedArg SplitPattern]
qs -> [NamedArg SplitPattern]
qs 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{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__
           IApplyP{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
           DefP  PatternInfo
_ QName
_ [NamedArg SplitPattern]
qs -> [NamedArg SplitPattern]
qs forall a. [a] -> [a] -> [a]
++ Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps -- __IMPOSSIBLE__ -- Andrea: maybe?
       | Bool
otherwise ->
           forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (\ SplitPattern
_ -> SplitPattern
p') NamedArg SplitPattern
p forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (Int
nforall a. Num a => a -> a -> a
-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
        where p' :: SplitPattern
p' = forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS (SplitClause -> Substitution' SplitPattern
scSubst SplitClause
sc) forall a b. (a -> b) -> a -> b
$ SplitPatVar -> Int
splitPatVarIndex SplitPatVar
x
      IApplyP{}   ->
           forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (SplitClause -> Substitution' SplitPattern
scSubst SplitClause
sc)) NamedArg SplitPattern
p forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (Int
nforall a. Num a => a -> a -> a
-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps
      DotP  PatternInfo
_ Term
_    -> NamedArg SplitPattern
p forall a. a -> [a] -> [a]
: Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits (Int
nforall a. Num a => a -> a -> a
-Int
1) SplitClause
sc [NamedArg SplitPattern]
ps -- count dot patterns
      ConP  ConHead
_ ConPatternInfo
_ [NamedArg SplitPattern]
qs -> Int
-> SplitClause
-> [NamedArg SplitPattern]
-> [NamedArg SplitPattern]
gatherEtaSplits Int
n SplitClause
sc ([NamedArg SplitPattern]
qs 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 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 forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p of
      VarP  PatternInfo
_ SplitPatVar
_     -> Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits (Int
kforall a. Num a => a -> a -> a
+Int
1) [NamedArg SplitPattern]
ps SplitTree
t
      DotP  PatternInfo
_ Term
_     -> Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits (Int
kforall a. Num a => a -> a -> a
+Int
1) [NamedArg SplitPattern]
ps SplitTree
t
      ConP ConHead
c ConPatternInfo
cpi [NamedArg SplitPattern]
qs -> forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (NamedArg SplitPattern
p 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 forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern]
ps) SplitTree
t)]
      LitP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__
      ProjP{}       -> forall a. HasCallStack => a
__IMPOSSIBLE__
      DefP{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- Andrea: maybe?
      IApplyP{}     -> Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
addEtaSplits (Int
kforall 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)


-- | Append a instance clause to the clauses of a function.
inferMissingClause
  :: QName
       -- ^ Function name.
  -> SplitClause
       -- ^ Clause to add.  Clause hiding (in 'clauseType') must be 'Instance'.
   -> 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)) = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
f forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.infer" Int
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Trying to infer right-hand side of type" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
t
  Term
rhs <-
    forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel
    forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Map CheckpointId (Substitution' Term)) TCEnv
eCheckpoints (forall a b. a -> b -> a
const Map CheckpointId (Substitution' Term)
cps)
    forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm,
 ReadTCState tcm) =>
Substitution' Term -> tcm a -> tcm a
checkpoint forall a. Substitution' a
IdS    -- introduce a fresh checkpoint
    forall a b. (a -> b) -> a -> b
$ case forall a. LensHiding a => a -> Hiding
getHiding Dom Type
t of
        Hiding
_ | Just Term
tac <- forall t e. Dom' t e -> Maybe t
domTactic Dom Type
t -> do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.infer" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"@tactic rhs"
            , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Dom Type
t ]
          (MetaId
_, Term
v) <- forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
DontRunMetaOccursCheck Comparison
CmpLeq (forall t e. Dom' t e -> e
unDom Dom Type
t)
          Term
v forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term -> Term -> Type -> TCMT IO ()
unquoteTactic Term
tac Term
v (forall t e. Dom' t e -> e
unDom Dom Type
t)
        Instance{} -> forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadMetaSolver m =>
[Char] -> Type -> m (MetaId, Term)
newInstanceMeta [Char]
"" (forall t e. Dom' t e -> e
unDom Dom Type
t)
        Hiding
Hidden     -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Hiding
NotHidden  -> forall a. HasCallStack => a
__IMPOSSIBLE__
  let cl :: Clause
cl = Clause { clauseLHSRange :: Range
clauseLHSRange  = forall a. Range' a
noRange
                  , clauseFullRange :: Range
clauseFullRange = forall a. Range' a
noRange
                  , clauseTel :: Telescope
clauseTel       = Telescope
tel
                  , namedClausePats :: NAPs
namedClausePats = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
                  , clauseBody :: Maybe Term
clauseBody      = forall a. a -> Maybe a
Just Term
rhs
                  , clauseType :: Maybe (Arg Type)
clauseType      = forall a. a -> Maybe a
Just (forall t a. Dom' t a -> Arg a
argFromDom Dom Type
t)
                  , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                  , clauseExact :: Maybe Bool
clauseExact       = forall a. a -> Maybe a
Just Bool
True
                  , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. Maybe a
Nothing     -- could be recursive
                  , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. a -> Maybe a
Just Bool
False  -- missing, thus, not unreachable
                  , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
NoEllipsis
                  , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
                  }
  forall (m :: * -> *).
(MonadConstraint m, MonadTCState m) =>
QName -> [Clause] -> m ()
addClauses QName
f [Clause
cl]  -- Important: add at the end.
  forall (m :: * -> *) a. Monad m => a -> m a
return Clause
cl
inferMissingClause QName
_ (SClause Telescope
_ [NamedArg SplitPattern]
_ Substitution' SplitPattern
_ Map CheckpointId (Substitution' Term)
_ Maybe (Dom Type)
Nothing) = forall a. HasCallStack => a
__IMPOSSIBLE__

splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy :: BlockingVars -> Telescope -> TCM BlockingVars
splitStrategy BlockingVars
bs Telescope
tel = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> [a] -> [a]
updateLast BlockingVar -> BlockingVar
setBlockingVarOverlap BlockingVars
xs
  -- Make sure we do not insists on precomputed coverage when
  -- we make our last try to split.
  -- Otherwise, we will not get a nice error message.
  where
    xs :: BlockingVars
xs             = BlockingVars
strict forall a. [a] -> [a] -> [a]
++ BlockingVars
lazy
    (BlockingVars
lazy, BlockingVars
strict) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition BlockingVar -> Bool
blockingVarLazy BlockingVars
bs
{- KEEP!
--  Andreas, 2012-10-13
--  The following split strategy which prefers all-constructor columns
--  fails on test/fail/CoverStrategy
    xs       = ys ++ zs
    (ys, zs) = partition allConstructors bs
    allConstructors :: BlockingVar -> Bool
    allConstructors = isJust . snd
-}


-- | Check that a type is a non-irrelevant datatype or a record with
-- named constructor. Unless the 'Induction' argument is 'CoInductive'
-- the data type must be inductive.
isDatatype :: (MonadTCM tcm, MonadError SplitError tcm) =>
              Induction -> Dom Type ->
              tcm (DataOrRecord, QName, [Arg Term], [Arg Term], [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       = 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 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Type -> SplitError
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Type
t
  Type
t' <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
  Maybe QName
mInterval <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinInterval
  Maybe QName
mIsOne <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinName' [Char]
builtinIsOne
  case forall t a. Type'' t a -> a
unEl Type
t' of
    Def QName
d [] | forall a. a -> Maybe a
Just QName
d 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] | forall a. a -> Maybe a
Just QName
d forall a. Eq a => a -> a -> Bool
== Maybe QName
mIsOne -> do
                [(IntMap Bool, [Term])]
xs <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall e. Arg e -> e
unArg Arg Term
phi)
                if forall a. Null a => a -> Bool
null [(IntMap Bool, [Term])]
xs
                   then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (DataOrRecord
IsData, QName
d, [Arg Term
phi], [], [], Bool
False)
                   else (Closure Type -> SplitError)
-> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
throw Closure Type -> SplitError
NotADatatype
    Def QName
d Elims
es -> do
      let ~(Just Args
args) = forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      Defn
def <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
      case Defn
def of
        Datatype{dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs}
          | Bool
otherwise -> do
              let (Args
ps, Args
is) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
np Args
args
              forall (m :: * -> *) a. Monad m => a -> m a
return (DataOrRecord
IsData, QName
d, Args
ps, Args
is, [QName]
cs, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ 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' :: Defn -> EtaEquality
recEtaEquality' :: EtaEquality
recEtaEquality'}
          | Maybe Induction
i forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Induction
CoInductive Bool -> Bool -> Bool
&& Induction
ind 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 ->
              forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Induction -> EtaEquality -> DataOrRecord
IsRecord Maybe Induction
i 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

-- | Update the target type of the split clause after a case split.
fixTargetType
  :: Quantity  -- ^ The quantity of the thing that is split.
  -> 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
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"split clause telescope: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
sctel
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"substitution          : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution' SplitPattern
sigma
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"target type before substitution:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Dom Type
target
      , TCMT IO Doc
"             after substitution:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
sigma Dom Type
target)
      ]

    -- We update the target quantity to 0 for erased constructors, but
    -- not if the match is made in an erased position, or if the
    -- original constructor definition is not erased.
    Dom Type -> Dom Type
updQuant <- do
      let erased :: Bool
erased = case Quantity
q of
            Quantity0{} -> Bool
True
            Quantity1{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
            Quantityω{} -> Bool
False
      if Bool
erased then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id else case SplitTag
tag of
        SplitCon QName
c -> do
          Quantity
q <- forall a. LensQuantity a => a -> Quantity
getQuantity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(ReadTCState m, HasConstInfo m) =>
QName -> m Definition
getOriginalConstInfo QName
c
          case Quantity
q of
            Quantity0{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity (Quantity -> Quantity -> Quantity
composeQuantity Quantity
q)
            Quantity1{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id
            Quantityω{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id
        SplitLit{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id
        SplitCatchall{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id

    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SplitClause
sc { scTarget :: Maybe (Dom Type)
scTarget = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Dom Type -> Dom Type
updQuant forall a b. (a -> b) -> a -> b
$ forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
sigma Dom Type
target }


-- | Add more patterns to split clause if the target type is a function type.
--   Returns the domains of the function type (if any).
insertTrailingArgs
  :: Bool         -- ^ Force insertion even when there is a 'domTactic'?
  -> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Null a => a
empty, SplitClause
sc)
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target TCM (Telescope, SplitClause)
fallback forall a b. (a -> b) -> a -> b
$ \ Dom Type
a -> do
    if forall a. Maybe a -> Bool
isJust (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 Telescope
tel Type
b) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
sctel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo (-Int
1) forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
a
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
15 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"target type telescope: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
sctel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
      , TCMT IO Doc
"target type core     : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
sctel forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
b
      ]
    let n :: Int
n         = forall a. Sized a => a -> Int
size Telescope
tel
        -- Andreas, 2016-10-04 issue #2236
        -- Need to set origin to "Inserted" to avoid printing of hidden patterns.
        xs :: [NamedArg SplitPattern]
xs        = forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo ArgInfo -> ArgInfo
hiddenInserted) forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
tel
        -- Compute new split clause
        sctel' :: Telescope
sctel'    = ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList (forall a. Subst a => Int -> a -> a
raise Int
n Telescope
sctel) forall a. [a] -> [a] -> [a]
++ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
        -- Dot patterns in @ps@ need to be raised!  (Issue 1298)
        ps' :: [NamedArg SplitPattern]
ps'       = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> Substitution' a
raiseS Int
n) [NamedArg SplitPattern]
ps forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern]
xs
        newTarget :: Maybe (Dom Type)
newTarget = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (if Bool -> Bool
not (forall a. Null a => a -> Bool
null Telescope
tel) then Dom Type
a{ domTactic :: Maybe Term
domTactic = forall a. Maybe a
Nothing } else Dom Type
a) forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
b
        sc' :: SplitClause
sc'       = SClause
          { scTel :: Telescope
scTel    = Telescope
sctel'
          , scPats :: [NamedArg SplitPattern]
scPats   = [NamedArg SplitPattern]
ps'
          , scSubst :: Substitution' SplitPattern
scSubst  = forall a. Int -> Substitution' a -> Substitution' a
wkS Int
n forall a b. (a -> b) -> a -> b
$ Substitution' SplitPattern
sigma -- Should be wkS instead of liftS since
                                     -- variables are only added to new tel.
          , scCheckpoints :: Map CheckpointId (Substitution' Term)
scCheckpoints        = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> Substitution' a
raiseS Int
n) Map CheckpointId (Substitution' Term)
cps
          , scTarget :: Maybe (Dom Type)
scTarget = Maybe (Dom Type)
newTarget
          }
    -- Separate debug printing to find cause of crash (Issue 1374)
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"new split clause telescope   : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
sctel'
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"new split clause patterns    : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
sctel' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps'
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"new split clause substitution: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (SplitClause -> Substitution' SplitPattern
scSubst SplitClause
sc')
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"new split clause target      : " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
sctel' forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Dom Type)
newTarget
      ]
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.target" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"new split clause"
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitClause
sc'
      ]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then (forall a. Null a => a
empty, SplitClause
sc { scTarget :: Maybe (Dom Type)
scTarget = Maybe (Dom Type)
newTarget }) else (Telescope
tel, SplitClause
sc')

-- Andreas, 2017-01-18, issue #819, set visible arguments to UserWritten.
-- Otherwise, they will be printed as _.
hiddenInserted :: ArgInfo -> ArgInfo
hiddenInserted :: ArgInfo -> ArgInfo
hiddenInserted ArgInfo
ai
  | forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
UserWritten ArgInfo
ai
  | Bool
otherwise  = forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
ai


-- | Checks if a type in this sort supports hcomp.
--   currently all such types will have a Level.
--   precondition: Sort in whnf and not blocked.
hasHComp :: Sort -> Maybe Level
hasHComp :: Sort -> Maybe Level
hasHComp (Type Level
l) = forall a. a -> Maybe a
Just Level
l
hasHComp Sort
_        = forall a. Maybe a
Nothing


computeHCompSplit  :: Telescope   -- ^ Telescope before split point.
  -> PatVarName                   -- ^ Name of pattern variable at split point.
  -> Telescope                    -- ^ Telescope after split point.
  -> QName                        -- ^ Name of datatype to split at.
  -> Args                         -- ^ Data type parameters.
  -> Args                         -- ^ Data type indices.
  -> Nat                          -- ^ Index of split variable.
  -> Telescope                    -- ^ Telescope for the patterns.
  -> [NamedArg SplitPattern]      -- ^ Patterns before doing the split.
  -> Map CheckpointId Substitution -- ^ Current checkpoints
  -- -> QName                        -- ^ Constructor to fit into hole.
  -> CoverM (Maybe (SplitTag,SplitClause))   -- ^ New split clause if successful.
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
  Bool
withK   <- Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optCubicalCompatible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  if Bool
withK then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing else do
    -- Get the type of the datatype
  -- Δ1 ⊢ dtype
  Sort
dsort <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ (forall a. DeBruijn a => [a] -> Substitution' a
parallelS (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
pars) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Sort
dataSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
  QName
hCompName <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getPrimitiveName' [Char]
builtinHComp
  Type
theHCompT <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
hCompName

  -- TODO can dsort be blocked or not in whnf?
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Sort -> Maybe Level
hasHComp Sort
dsort) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ Level
dlvl' -> do
  let
    dlvl :: Term
dlvl = Level -> Term
Level Level
dlvl'
    dterm :: Term
dterm = QName -> Elims -> Term
Def QName
d [] forall t. Apply t => t -> Args -> t
`apply` (Args
pars forall a. [a] -> [a] -> [a]
++ Args
ixs)
  -- Δ1 ⊢ gamma
  TelV Telescope
gamma Type
_ <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type
theHCompT Type -> Args -> Type
`piApply` [forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ Term
dlvl , forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ Term
dterm])
  case (Telescope
delta1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma,forall a. Substitution' a
IdS) of
    (Telescope
delta1',PatternSubstitution
rho0) -> do
--      debugSubst "rho0" rho0

      -- We have Δ₁' ⊢ ρ₀ : Δ₁Γ, so split it into the part for Δ₁ and the part for Γ
      let (Substitution' SplitPattern
rho1,Substitution' SplitPattern
rho2) = forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (forall a. Sized a => a -> Int
size Telescope
gamma) forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> Substitution' SplitPattern
toSplitPSubst PatternSubstitution
rho0

      let defp :: SplitPattern
defp = forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
defaultPatternInfo QName
hCompName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) forall a b. (a -> b) -> a -> b
$ -- should there be a different Origin here?
                   forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed) [forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho1 forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo forall a b. (a -> b) -> a -> b
$ Term
dlvl
                                      ,forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho1 forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo forall a b. (a -> b) -> a -> b
$ Term
dterm]
                   forall a. [a] -> [a] -> [a]
++ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho2 (forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Telescope
gamma) -- rho0?
      -- Compute final context and substitution
      let rho3 :: Substitution' SplitPattern
rho3    = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
defp Substitution' SplitPattern
rho1            -- Δ₁' ⊢ ρ₃ : Δ₁(x:D)
          delta2' :: Telescope
delta2' = forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho3 Telescope
delta2  -- Δ₂' = Δ₂ρ₃
          delta' :: Telescope
delta'  = Telescope
delta1' forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2' -- Δ'  = Δ₁'Δ₂'
          rho :: Substitution' SplitPattern
rho     = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
delta2) Substitution' SplitPattern
rho3   -- Δ' ⊢ ρ : Δ₁(x:D)Δ₂

      -- debugTel "delta'" delta'
      -- debugSubst "rho" rho
      -- debugPs tel ps

      -- Apply the substitution
      let ps' :: [NamedArg SplitPattern]
ps' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho [NamedArg SplitPattern]
ps
      -- debugPlugged delta' ps'

      let cps' :: Map CheckpointId (Substitution' Term)
cps' = forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps

      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> SplitTag
SplitCon QName
hCompName,) 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' forall a. Maybe a
Nothing -- target fixed later


-- | @computeNeighbourhood delta1 delta2 d pars ixs hix tel ps con@
--
--   @
--      delta1   Telescope before split point
--      n        Name of pattern variable at split point
--      delta2   Telescope after split point
--      d        Name of datatype to split at
--      pars     Data type parameters
--      ixs      Data type indices
--      hix      Index of split variable
--      tel      Telescope for patterns ps
--      ps       Patterns before doing the split
--      cps      Current module parameter checkpoints
--      con      Constructor to fit into hole
--   @
--   @dtype == d pars ixs@
computeNeighbourhood
  :: Telescope                    -- ^ Telescope before split point.
  -> PatVarName                   -- ^ Name of pattern variable at split point.
  -> Telescope                    -- ^ Telescope after split point.
  -> QName                        -- ^ Name of datatype to split at.
  -> Args                         -- ^ Data type parameters.
  -> Args                         -- ^ Data type indices.
  -> Nat                          -- ^ Index of split variable.
  -> Telescope                    -- ^ Telescope for the patterns.
  -> [NamedArg SplitPattern]      -- ^ Patterns before doing the split.
  -> Map CheckpointId Substitution -- ^ Current checkpoints
  -> QName                        -- ^ Constructor to fit into hole.
  -> CoverM (Maybe (SplitClause, IInfo))   -- ^ New split clause if successful.
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

  -- Get the type of the datatype
  Type
dtype <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ (Type -> Args -> Type
`piApply` Args
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d

  -- Get the real constructor name
  ConHead
con <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> Either a b -> b
fromRight forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Either SigError ConHead)
getConForm QName
c
  ConHead
con <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ConHead
con { conName :: QName
conName = QName
c }  -- What if we restore the current name?
                                       -- Andreas, 2013-11-29 changes nothing!

  -- Get the type of the constructor
  Type
ctype <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
con

  -- Lookup the type of the constructor at the given parameters
  (Telescope
gamma0, Args
cixs, Boundary
boundary) <- do
    (TelV Telescope
gamma0 (El Sort
_ Term
d), Boundary
boundary) <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). PureTCM m => Type -> m (TelV Type, Boundary)
telViewPathBoundaryP (Type
ctype Type -> Args -> Type
`piApply` Args
pars)
    let Def QName
_ Elims
es = Term
d
        Just Args
cixs = forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
    forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope
gamma0, Args
cixs, Boundary
boundary)

  let (ListTel
_, Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} : ListTel
_) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Int
size Telescope
tel forall a. Num a => a -> a -> a
- Int
hix forall a. Num a => a -> a -> a
- Int
1) (forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel)

  -- Andreas, 2012-02-25 preserve name suggestion for recursive arguments
  -- of constructor

  let preserve :: ([Char], Type) -> ([Char], Type)
preserve ([Char]
x, t :: Type
t@(El Sort
_ (Def QName
d' Elims
_))) | QName
d forall a. Eq a => a -> a -> Bool
== QName
d' = ([Char]
n, Type
t)
      preserve ([Char]
x, Type
t) = ([Char]
x, Type
t)
      gamma :: Telescope
gamma  = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality) (Modality -> Modality -> Modality
composeModality (forall a. LensModality a => a -> Modality
getModality ArgInfo
info)) forall a b. (a -> b) -> a -> b
$ ListTel -> Telescope
telFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char], Type) -> ([Char], Type)
preserve) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList forall a b. (a -> b) -> a -> b
$ Telescope
gamma0
      delta1Gamma :: Telescope
delta1Gamma = Telescope
delta1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma

  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

  [IsForced]
cforced <- Definition -> [IsForced]
defForced forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
      -- Variables in Δ₁ are not forced, since the unifier takes care to not introduce forced
      -- variables.
  let forced :: [IsForced]
forced = forall a. Int -> a -> [a]
replicate (forall a. Sized a => a -> Int
size Telescope
delta1) IsForced
NotForced forall a. [a] -> [a] -> [a]
++ [IsForced]
cforced
      flex :: FlexibleVars
flex   = [IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
forced Telescope
delta1Gamma -- All variables are flexible

  -- Unify constructor target and given type (in Δ₁Γ)
  let conIxs :: Args
conIxs   = forall a. Int -> [a] -> [a]
drop (forall a. Sized a => a -> Int
size Args
pars) Args
cixs
      givenIxs :: Args
givenIxs = forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
gamma) Args
ixs

  -- Andrea 2019-07-17 propagate the Cohesion to the equation telescope
  -- TODO: should we propagate the modality in general?
  -- See also LHS checking.
  Type
dtype <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ do
         let updCoh :: Cohesion -> Cohesion
updCoh = Cohesion -> Cohesion -> Cohesion
composeCohesion (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info)
         TelV Telescope
dtel Type
dt <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
dtype
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. Abstract t => Telescope -> t -> t
abstract (forall a. LensCohesion a => (Cohesion -> Cohesion) -> a -> a
mapCohesion Cohesion -> Cohesion
updCoh forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
dtel) Type
dt
  Sort
dsort <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall a. LensSort a => a -> Sort
getSort Type
dtype)

  ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult
withKIfStrict <- case Sort
dsort of
    SSet{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eSplitOnStrict forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True
    Sort
_      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. a -> a
id

  -- Should we attempt to compute a left inverse for this clause? When
  -- --cubical-compatible --flat-split is given, we don't generate a
  -- left inverse (at all). This means that, when the coverage checker
  -- gets to the clause this was in, it won't generate a (malformed!)
  -- transpX clause for @♭ matching.
  -- TODO(Amy): properly support transpX when @♭ stuff is in the
  -- context.
  let flatSplit :: Maybe NoLeftInv
flatSplit = forall a. Bool -> a -> Maybe a
boolToMaybe (forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info forall a. Eq a => a -> a -> Bool
== Cohesion
Flat) NoLeftInv
SplitOnFlat

  FullUnificationResult
r <- ExceptT SplitError (TCMT IO) FullUnificationResult
-> ExceptT SplitError (TCMT IO) FullUnificationResult
withKIfStrict forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadError TCErr m) =>
Maybe NoLeftInv
-> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m FullUnificationResult
unifyIndices' Maybe NoLeftInv
flatSplit
         Telescope
delta1Gamma
         FlexibleVars
flex
         (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
gamma) Type
dtype)
         Args
conIxs
         Args
givenIxs

  TelV Telescope
eqTel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
gamma) Type
dtype)

  let stuck :: Maybe Blocker
-> [UnificationFailure] -> CoverM (Maybe (SplitClause, IInfo))
stuck Maybe Blocker
b [UnificationFailure]
errs = do
        ExceptT SplitError (TCMT IO) ()
debugCantSplit
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
gamma) Args
conIxs Args
givenIxs [UnificationFailure]
errs


  case FullUnificationResult
r of
    NoUnify {} -> ExceptT SplitError (TCMT IO) ()
debugNoUnify forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a. Maybe a
Nothing

    UnifyBlocked Blocker
block -> Maybe Blocker
-> [UnificationFailure] -> CoverM (Maybe (SplitClause, IInfo))
stuck (forall a. a -> Maybe a
Just Blocker
block) []

    UnifyStuck [UnificationFailure]
errs -> Maybe Blocker
-> [UnificationFailure] -> CoverM (Maybe (SplitClause, IInfo))
stuck 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     -- only types of sort Type l have trX constructors:
                                          -- re #3733: update if we add transp for other sorts.
                    , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ Args
conIxs -- no point propagating this info if trivial?
                    , Right (Substitution' Term
tau,Substitution' Term
leftInv) <- Either NoLeftInv (Substitution' Term, Substitution' Term)
tauInv
            = UnifyEquiv -> IInfo
TheInfo 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 (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
conIxs) (forall a b. (a -> b) -> [a] -> [b]
map 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Left NoLeftInv
SplitOnStrict -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Left NoLeftInv
x -> do
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optCubicalCompatible forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                 forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall a b. (a -> b) -> a -> b
$ do
            -- re #3733: TODO better error msg.
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
UnsupportedIndexedMatch forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NoLeftInv
x

      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

      -- We have Δ₁' ⊢ ρ₀ : Δ₁Γ, so split it into the part for Δ₁ and the part for Γ
      let (Substitution' SplitPattern
rho1,Substitution' SplitPattern
rho2) = forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (forall a. Sized a => a -> Int
size Telescope
gamma) forall a b. (a -> b) -> a -> b
$ Substitution' SplitPattern
rho0'

      -- Andreas, 2015-05-01  I guess it is fine to use no @conPType@
      -- as the result of splitting is never used further down the pipeline.
      -- After splitting, Agda reloads the file.
      -- Andreas, 2017-09-03, issue #2729: remember that pattern was generated by case split.
      let cpi :: ConPatternInfo
cpi  = ConPatternInfo
noConPatternInfo{ conPInfo :: PatternInfo
conPInfo = PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSplit [] , conPRecord :: Bool
conPRecord = Bool
True }
          conp :: SplitPattern
conp = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
con ConPatternInfo
cpi forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho0' forall a b. (a -> b) -> a -> b
$
                   forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo ArgInfo -> ArgInfo
hiddenInserted) forall a b. (a -> b) -> a -> b
$ forall a.
DeBruijn a =>
(forall a1. DeBruijn a1 => Telescope -> [NamedArg a1])
-> Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns' (forall a. DeBruijn a => Telescope -> Telescope -> [NamedArg a]
tele2NamedArgs Telescope
gamma0) Telescope
gamma Boundary
boundary
          -- Andreas, 2016-09-08, issue #2166: use gamma0 for correct argument names

      -- Compute final context and substitution
      let rho3 :: Substitution' SplitPattern
rho3    = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
conp Substitution' SplitPattern
rho1            -- Δ₁' ⊢ ρ₃ : Δ₁(x:D)
          delta2' :: Telescope
delta2' = forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho3 Telescope
delta2  -- Δ₂' = Δ₂ρ₃
          delta' :: Telescope
delta'  = Telescope
delta1' forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2' -- Δ'  = Δ₁'Δ₂'
          rho :: Substitution' SplitPattern
rho     = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
delta2) Substitution' SplitPattern
rho3   -- Δ' ⊢ ρ : Δ₁(x:D)Δ₂

      forall {tcm :: * -> *} {a}.
(MonadTCM tcm, PrettyTCM a) =>
[Char] -> a -> tcm ()
debugTel [Char]
"delta'" Telescope
delta'
      forall {tcm :: * -> *} {a}.
(MonadTCM tcm, PrettyTCM a) =>
[Char] -> a -> tcm ()
debugSubst [Char]
"rho" Substitution' SplitPattern
rho
      forall {tcm :: * -> *} {b}.
(MonadTCM tcm, AddContext b) =>
b -> [NamedArg SplitPattern] -> tcm ()
debugPs Telescope
tel [NamedArg SplitPattern]
ps

      -- Apply the substitution
      let ps' :: [NamedArg SplitPattern]
ps' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho [NamedArg SplitPattern]
ps
      forall {tcm :: * -> *} {b}.
(MonadTCM tcm, AddContext b) =>
b -> [NamedArg SplitPattern] -> tcm ()
debugPlugged Telescope
delta' [NamedArg SplitPattern]
ps'

      let cps' :: Map CheckpointId (Substitution' Term)
cps'  = forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps

      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,IInfo
unifyInfo) 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' forall a. Maybe a
Nothing -- target fixed later

  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 = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"computeNeighbourhood"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"context=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
          , TCMT IO Doc
"con    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
con
          , TCMT IO Doc
"ctype  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ctype
          , TCMT IO Doc
"ps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
          , TCMT IO Doc
"d      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
          , TCMT IO Doc
"pars   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
pars
          , TCMT IO Doc
"ixs    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ixs
          , TCMT IO Doc
"cixs   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma  forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
cixs
          , TCMT IO Doc
"delta1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta1
          , TCMT IO Doc
"delta2 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [Char]
n forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta2
          , TCMT IO Doc
"gamma  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
          , TCMT IO Doc
"tel  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
          , TCMT IO Doc
"hix    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Int
hix)
          ]
        ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
70 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"computeNeighbourhood"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"context=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
          , TCMT IO Doc
"con    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) ConHead
con
          , TCMT IO Doc
"ctype  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Type
ctype
          , TCMT IO Doc
"ps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [NamedArg SplitPattern]
ps
          , TCMT IO Doc
"d      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) QName
d
          , TCMT IO Doc
"pars   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Args
pars
          , TCMT IO Doc
"ixs    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Args
ixs
          , TCMT IO Doc
"cixs   =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Args
cixs
          , TCMT IO Doc
"delta1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Telescope
delta1
          , TCMT IO Doc
"delta2 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Telescope
delta2
          , TCMT IO Doc
"gamma  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Telescope
gamma
          , TCMT IO Doc
"hix    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (forall a. Show a => a -> [Char]
show Int
hix)
          ]
        ]

    debugNoUnify :: ExceptT SplitError (TCMT IO) ()
debugNoUnify =
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ 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 =
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ 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 =
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" =") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
sub
        ]

    debugTel :: [Char] -> a -> tcm ()
debugTel [Char]
s a
tel =
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" =") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
tel
        ]

    debugPs :: b -> [NamedArg SplitPattern] -> tcm ()
debugPs b
tel [NamedArg SplitPattern]
ps =
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 forall a b. (a -> b) -> a -> b
$
        forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext b
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"ps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split.con" Int
20 forall a b. (a -> b) -> a -> b
$
        forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext b
delta' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"ps'    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps'
          ]

-- | Introduce trailing pattern variables?
data InsertTrailing
  = DoInsertTrailing
  | DontInsertTrailing
  deriving (InsertTrailing -> InsertTrailing -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InsertTrailing -> InsertTrailing -> Bool
$c/= :: InsertTrailing -> InsertTrailing -> Bool
== :: InsertTrailing -> InsertTrailing -> Bool
$c== :: InsertTrailing -> InsertTrailing -> Bool
Eq, Int -> InsertTrailing -> ShowS
[InsertTrailing] -> ShowS
InsertTrailing -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [InsertTrailing] -> ShowS
$cshowList :: [InsertTrailing] -> ShowS
show :: InsertTrailing -> [Char]
$cshow :: InsertTrailing -> [Char]
showsPrec :: Int -> InsertTrailing -> ShowS
$cshowsPrec :: Int -> InsertTrailing -> ShowS
Show)

-- | Allow partial covering for split?
data AllowPartialCover
  = YesAllowPartialCover  -- To try to coverage-check incomplete splits.
  | NoAllowPartialCover   -- Default.
  deriving (AllowPartialCover -> AllowPartialCover -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AllowPartialCover -> AllowPartialCover -> Bool
$c/= :: AllowPartialCover -> AllowPartialCover -> Bool
== :: AllowPartialCover -> AllowPartialCover -> Bool
$c== :: AllowPartialCover -> AllowPartialCover -> Bool
Eq, Int -> AllowPartialCover -> ShowS
[AllowPartialCover] -> ShowS
AllowPartialCover -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [AllowPartialCover] -> ShowS
$cshowList :: [AllowPartialCover] -> ShowS
show :: AllowPartialCover -> [Char]
$cshow :: AllowPartialCover -> [Char]
showsPrec :: Int -> AllowPartialCover -> ShowS
$cshowsPrec :: Int -> AllowPartialCover -> ShowS
Show)

-- | Entry point from @Interaction.MakeCase@.
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)
  -- Andreas, 2016-05-03, issue 1950:
  -- Do not introduce trailing pattern vars after split,
  -- because this does not work for with-clauses.

-- | Entry point from @TypeChecking.Empty@ and @Interaction.BasicOps@.
--   @splitLast CoInductive@ is used in the @refine@ tactics.

splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)
splitLast :: Induction -> Telescope -> NAPs -> TCM (Either SplitError Covering)
splitLast Induction
ind Telescope
tel NAPs
ps = Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCM (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) forall a. Null a => a
empty forall a. Null a => a
empty forall {t}. Maybe (Dom (Type'' t Term))
target
        -- TODO 2ltt: allows (Empty_fib -> Empty_strict) which is not conservative
        target :: Maybe (Dom (Type'' t Term))
target = (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Dom a
defaultDom forall a b. (a -> b) -> a -> b
$ forall t a. Sort' t -> a -> Type'' t a
El (forall t. Level' t -> Sort' t
Prop (forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [])) forall a b. (a -> b) -> a -> b
$ [Char] -> Elims -> Term
Dummy [Char]
"splitLastTarget" [])

-- | @split ind splitClause x = return res@
--   splits @splitClause@ at pattern var @x@ (de Bruijn index).
--
--   Possible results @res@ are:
--
--   1. @Left err@:
--      Splitting failed.
--
--   2. @Right covering@:
--      A covering set of split clauses, one for each valid constructor.
--      This could be the empty set (denoting an absurd clause).

split :: Induction
         -- ^ Coinductive constructors are allowed if this argument is
         -- 'CoInductive'.
      -> AllowPartialCover
         -- ^ Don't fail if computed 'Covering' does not cover all constructors.
      -> SplitClause
      -> BlockingVar
      -> TCM (Either SplitError Covering)
split :: Induction
-> AllowPartialCover
-> SplitClause
-> BlockingVar
-> TCM (Either SplitError Covering)
split Induction
ind AllowPartialCover
allowPartialCover SplitClause
sc BlockingVar
x =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either SplitClause Covering -> Covering
blendInAbsurdClause 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 forall a b. (a -> b) -> a -> b
$ BlockingVar -> Int
blockingVarNo BlockingVar
x
    blendInAbsurdClause :: Either SplitClause Covering -> Covering
    blendInAbsurdClause :: Either SplitClause Covering -> Covering
blendInAbsurdClause = forall a b. (a -> b) -> Either a b -> b
fromRight (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Arg Int -> [(SplitTag, (SplitClause, IInfo))] -> Covering
Covering Arg Int
n [])

-- | Convert a de Bruijn index relative to the clause telescope to a de Bruijn
--   level. The result should be the argument position (counted from left,
--   starting with 0) to split at (dot patterns included!).
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 forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>
    if Int
n forall a. Ord a => a -> a -> Bool
< Int
0 then forall a. HasCallStack => a
__IMPOSSIBLE__ else Int
n
  where n :: Int
n = if Int
k forall a. Ord a => a -> a -> Bool
< Int
0
            then forall a. HasCallStack => a
__IMPOSSIBLE__
            else forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Permutation -> [Int]
permPicks Permutation
perm forall a. [a] -> Int -> Maybe a
!!! Int
k
        perm :: Permutation
perm = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ NAPs -> Maybe Permutation
dbPatPerm forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
pats
        k :: Int
k = forall a. Sized a => a -> Int
size Telescope
tel forall a. Num a => a -> a -> a
- Int
x forall a. Num a => a -> a -> a
- Int
1
        arg :: Arg DeBruijnPattern
arg = forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (Int -> Telescope -> [Arg DeBruijnPattern]
telVars (forall a. Sized a => a -> Int
size Telescope
tel) Telescope
tel) Int
k


data CheckEmpty = CheckEmpty | NoCheckEmpty

-- | @split' ind pc ft splitClause x = return res@
--   splits @splitClause@ at pattern var @x@ (de Bruijn index).
--
--   Possible results @res@ are:
--
--   1. @Left err@:
--      Splitting failed.
--
--   2. @Right (Left splitClause')@:
--      Absurd clause (type of @x@ has 0 valid constructors).
--
--   3. @Right (Right covering)@:
--      A covering set of split clauses, one for each valid constructor.

split' :: CheckEmpty
          -- ^ Use isEmptyType to check whether the type of the variable to
          -- split on is empty. This switch is necessary to break the cycle
          -- between split' and isEmptyType.
       -> Induction
          -- ^ Coinductive constructors are allowed if this argument is
          -- 'CoInductive'.
       -> AllowPartialCover
          -- ^ Don't fail if computed 'Covering' does not cover all constructors.
       -> InsertTrailing
          -- ^ If 'DoInsertTrailing', introduce new trailing variable patterns.
       -> 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) =
 forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
  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

  -- Split the telescope at the variable
  -- t = type of the variable,  Δ₁ ⊢ t
  ([Char]
n, Dom Type
t, Telescope
delta1, Telescope
delta2) <- do
    let (ListTel
tel1, Dom ([Char], Type)
dom : ListTel
tel2) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall a. Sized a => a -> Int
size Telescope
tel forall a. Num a => a -> a -> a
- Int
x forall a. Num a => a -> a -> a
- Int
1) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom ([Char], Type)
dom, forall a b. (a, b) -> b
snd 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)

  -- Compute the neighbourhoods for the constructors
  let computeNeighborhoods :: ExceptT
  SplitError
  (TCMT IO)
  (DataOrRecord, Bool, Int, [(SplitTag, (SplitClause, IInfo))])
computeNeighborhoods = do
        -- Check that t is a datatype or a record
        -- Andreas, 2010-09-21, isDatatype now directly throws an exception if it fails
        -- cons = constructors of this datatype
        (DataOrRecord
dr, QName
d, Args
pars, Args
ixs, [QName]
cons', Bool
isHIT) <- forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *).
(MonadTCM tcm, MonadError SplitError tcm) =>
Induction
-> Dom Type -> tcm (DataOrRecord, QName, Args, Args, [QName], Bool)
isDatatype Induction
ind Dom Type
t
        Bool
isFib <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(LensSort a, PureTCM m, MonadBlock m) =>
a -> m Bool
isFibrant Dom Type
t
        [QName]
cons <- case CheckEmpty
checkEmpty of
          CheckEmpty
CheckEmpty   -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Bool
isEmptyType forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
t) (forall (f :: * -> *) a. Applicative f => a -> f a
pure []) (forall (f :: * -> *) a. Applicative f => a -> f a
pure [QName]
cons')
          CheckEmpty
NoCheckEmpty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [QName]
cons'
        [Maybe (SplitTag, (SplitClause, IInfo))]
mns  <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [QName]
cons forall a b. (a -> b) -> a -> b
$ \ QName
con -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> SplitTag
SplitCon QName
con,) 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
        Maybe (SplitTag, SplitClause)
hcompsc <- if Bool
isFib Bool -> Bool -> Bool
&& (Bool
isHIT Bool -> Bool -> Bool
|| (forall a. Sized a => a -> Int
size Args
ixs forall a. Ord a => a -> a -> Bool
> Int
0)) Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null [Maybe (SplitTag, (SplitClause, IInfo))]
mns) Bool -> Bool -> Bool
&& InsertTrailing
inserttrailing forall a. Eq a => a -> a -> Bool
== InsertTrailing
DoInsertTrailing
                   then 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
x Telescope
tel [NamedArg SplitPattern]
ps Map CheckpointId (Substitution' Term)
cps
                   else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        let ns :: [(SplitTag, (SplitClause, IInfo))]
ns = forall a. [Maybe a] -> [a]
catMaybes [Maybe (SplitTag, (SplitClause, IInfo))]
mns
        forall (m :: * -> *) a. Monad m => a -> m a
return ( DataOrRecord
dr
               , Bool -> Bool
not (forall a. Null a => a -> Bool
null Args
ixs) -- Is "d" indexed?
               , forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ [(SplitTag, (SplitClause, IInfo))]
ns
               , [(SplitTag, (SplitClause, IInfo))]
ns forall a. [a] -> [a] -> [a]
++ forall a. [Maybe a] -> [a]
catMaybes ([forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,IInfo
NoInfo)) Maybe (SplitTag, SplitClause)
hcompsc | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null forall a b. (a -> b) -> a -> b
$ [(SplitTag, (SplitClause, IInfo))]
ns])
               )

      computeLitNeighborhoods :: ExceptT
  SplitError
  (TCMT IO)
  (DataOrRecord, Bool, Int, [(SplitTag, (SplitClause, IInfo))])
computeLitNeighborhoods = do
        Bool
typeOk <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
          Type
t' <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> a
headWithDefault {-'-} forall a. HasCallStack => a
__IMPOSSIBLE__ [Literal]
plits
          forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType (forall t e. Dom' t e -> e
unDom Dom Type
t) Type
t'
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
typeOk forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Type -> SplitError
NotADatatype forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (forall t e. Dom' t e -> e
unDom Dom Type
t)
        [(SplitTag, SplitClause)]
ns <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Literal]
plits forall a b. (a -> b) -> a -> b
$ \Literal
lit -> do
          let delta2' :: Telescope
delta2' = forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 (Literal -> Term
Lit Literal
lit) Telescope
delta2
              delta' :: Telescope
delta'  = Telescope
delta1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
delta2'
              rho :: Substitution' SplitPattern
rho     = forall a. Int -> Substitution' a -> Substitution' a
liftS Int
x forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (forall a. Literal -> Pattern' a
litP Literal
lit) forall a. Substitution' a
idS
              ps' :: [NamedArg SplitPattern]
ps'     = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho [NamedArg SplitPattern]
ps
              cps' :: Map CheckpointId (Substitution' Term)
cps'    = forall a. TermSubst a => Substitution' SplitPattern -> a -> a
applySplitPSubst Substitution' SplitPattern
rho Map CheckpointId (Substitution' Term)
cps
          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' forall a. Maybe a
Nothing)
        (SplitTag, SplitClause)
ca <- do
          let delta' :: Telescope
delta' = Telescope
tel -- telescope is unchanged for catchall branch
              varp :: SplitPattern
varp   = forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSplit []) forall a b. (a -> b) -> a -> b
$ SplitPatVar
                         { splitPatVarName :: [Char]
splitPatVarName   = forall a. Underscore a => a
underscore
                         , splitPatVarIndex :: Int
splitPatVarIndex  = Int
0
                         , splitExcludedLits :: [Literal]
splitExcludedLits = [Literal]
plits
                         }
              rho :: Substitution' SplitPattern
rho    = forall a. Int -> Substitution' a -> Substitution' a
liftS Int
x forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
varp forall a b. (a -> b) -> a -> b
$ forall a. Int -> Substitution' a
raiseS Int
1
              ps' :: [NamedArg SplitPattern]
ps'    = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho [NamedArg SplitPattern]
ps
          forall (m :: * -> *) a. Monad m => a -> m a
return (SplitTag
SplitCatchall , 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 forall a. Maybe a
Nothing)

        -- If Agda is changed so that the type of a literal can belong
        -- to an inductive family (with at least one index), then the
        -- following code should be changed (the constructor False
        -- stands for "not indexed").
        let ns' :: [(SplitTag, (SplitClause, IInfo))]
ns' = forall a b. (a -> b) -> [a] -> [b]
map ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,IInfo
NoInfo))) forall a b. (a -> b) -> a -> b
$ [(SplitTag, SplitClause)]
ns forall a. [a] -> [a] -> [a]
++ [ (SplitTag, SplitClause)
ca ]
        forall (m :: * -> *) a. Monad m => a -> m a
return (DataOrRecord
IsData, Bool
False, forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SplitTag, (SplitClause, IInfo))]
ns', [(SplitTag, (SplitClause, IInfo))]
ns')

  -- numMatching is the number of proper constructors matching, excluding hcomp.
  -- for literals this considers the catchall clause as 1 extra constructor.
  (DataOrRecord
dr, Bool
isIndexed, Int
numMatching, [(SplitTag, (SplitClause, IInfo))]
ns) <- if forall a. Null a => a -> Bool
null [ConHead]
pcons' Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Null a => a -> Bool
null [Literal]
plits)
        then ExceptT
  SplitError
  (TCMT IO)
  (DataOrRecord, Bool, Int, [(SplitTag, (SplitClause, IInfo))])
computeLitNeighborhoods
        else ExceptT
  SplitError
  (TCMT IO)
  (DataOrRecord, Bool, Int, [(SplitTag, (SplitClause, IInfo))])
computeNeighborhoods

  [(SplitTag, (SplitClause, IInfo))]
ns <- case Maybe (Dom Type)
target of
    Just Dom Type
a  -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(SplitTag, (SplitClause, IInfo))]
ns forall a b. (a -> b) -> a -> b
$ \ (SplitTag
con,(SplitClause
sc,IInfo
info)) -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (SplitTag
con,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,IInfo
info) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                 Quantity
-> SplitTag -> SplitClause -> Dom Type -> TCMT IO SplitClause
fixTargetType (forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
t) SplitTag
con SplitClause
sc Dom Type
a
    Maybe (Dom Type)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitTag, (SplitClause, IInfo))]
ns

  [(SplitTag, (SplitClause, IInfo))]
ns <- case InsertTrailing
inserttrailing of
    InsertTrailing
DontInsertTrailing -> forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitTag, (SplitClause, IInfo))]
ns
    InsertTrailing
DoInsertTrailing   -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(SplitTag, (SplitClause, IInfo))]
ns forall a b. (a -> b) -> a -> b
$ \(SplitTag
con,(SplitClause
sc,IInfo
info)) ->
      (SplitTag
con,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,IInfo
info) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
False SplitClause
sc

  Maybe QName
mHCompName <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getPrimitiveName' [Char]
builtinHComp
  Bool
withoutK   <- forall (b :: Bool). KnownBool b => WithDefault b -> Bool
collapseDefault forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> WithDefault 'False
optWithoutK forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions

  Bool
erased <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensQuantity a => a -> Bool
hasQuantity0
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.cover.split" Int
60 forall a b. (a -> b) -> a -> b
$ [Char]
"We are in erased context = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Bool
erased
  let erasedError :: Bool -> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
erasedError Bool
causedByWithoutK =
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Closure Type -> SplitError
ErasedDatatype Bool
causedByWithoutK forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          do forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (forall t e. Dom' t e -> e
unDom Dom Type
t)

  case Int
numMatching of
    Int
0  -> do
      let absurdp :: SplitPattern
absurdp = forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOAbsurd []) forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> [Literal] -> SplitPatVar
SplitPatVar forall a. Underscore a => a
underscore Int
0 []
          rho :: Substitution' SplitPattern
rho = forall a. Int -> Substitution' a -> Substitution' a
liftS Int
x forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS SplitPattern
absurdp forall a b. (a -> b) -> a -> b
$ forall a. Int -> Substitution' a
raiseS Int
1
          ps' :: [NamedArg SplitPattern]
ps' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' SplitPattern
rho [NamedArg SplitPattern]
ps
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ SClause
               { scTel :: Telescope
scTel  = Telescope
tel
               , scPats :: [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
ps'
               , scSubst :: Substitution' SplitPattern
scSubst              = forall a. HasCallStack => a
__IMPOSSIBLE__ -- not used
               , scCheckpoints :: Map CheckpointId (Substitution' Term)
scCheckpoints        = forall a. HasCallStack => a
__IMPOSSIBLE__ -- not used
               , scTarget :: Maybe (Dom Type)
scTarget             = forall a. Maybe a
Nothing
               }

    -- Andreas, 2018-10-17: If more than one constructor matches, we cannot erase.
    Int
n | Int
n forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
erased Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. LensQuantity a => a -> Bool
usableQuantity Dom Type
t) ->
      Bool -> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
erasedError Bool
False

    -- If exactly one constructor matches and the K rule is turned
    -- off, then we only allow erasure for non-indexed data types
    -- (#4172).
    Int
1 | Bool -> Bool
not Bool
erased Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. LensQuantity a => a -> Bool
usableQuantity Dom Type
t) Bool -> Bool -> Bool
&&
          Bool
withoutK Bool -> Bool -> Bool
&& Bool
isIndexed ->
      Bool -> ExceptT SplitError (TCMT IO) (Either SplitClause Covering)
erasedError Bool
True

    Int
_ -> do

      -- Andreas, 2012-10-10 fail if precomputed constructor set does not cover
      -- all the data type constructors
      -- Andreas, 2017-10-08 ... unless partial covering is explicitly allowed.
      let ptags :: [SplitTag]
ptags = forall a b. (a -> b) -> [a] -> [b]
map (QName -> SplitTag
SplitCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName) [ConHead]
pcons' forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Literal -> SplitTag
SplitLit [Literal]
plits
      -- clauses for hcomp will be automatically generated.
      let inferred_tags :: Set SplitTag
inferred_tags = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Set a
Set.empty (forall a. a -> Set a
Set.singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> SplitTag
SplitCon) Maybe QName
mHCompName
      let all_tags :: Set SplitTag
all_tags = forall a. Ord a => [a] -> Set a
Set.fromList [SplitTag]
ptags forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set SplitTag
inferred_tags

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AllowPartialCover
allowPartialCover forall a. Eq a => a -> a -> Bool
== AllowPartialCover
NoAllowPartialCover Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
overlap) forall a b. (a -> b) -> a -> b
$
        forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [(SplitTag, (SplitClause, IInfo))]
ns forall a b. (a -> b) -> a -> b
$ \(SplitTag
tag, (SplitClause
sc, IInfo
_)) -> do
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SplitTag
tag forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SplitTag
all_tags) forall a b. (a -> b) -> a -> b
$ do
            Bool
isImpossibleClause <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Bool
isEmptyTel forall a b. (a -> b) -> a -> b
$ SplitClause -> Telescope
scTel SplitClause
sc
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
isImpossibleClause forall a b. (a -> b) -> a -> b
$ do
              forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Missing case for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitTag
tag
                , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SplitClause
sc
                ]
              forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([Char] -> SplitError
GenericSplitError [Char]
"precomputed set of constructors does not cover all cases")

      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT forall a b. (a -> b) -> a -> b
$ 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 (forall t e. Dom' t e -> e
unDom Dom Type
t) Telescope
delta2 Maybe (Dom Type)
target
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right 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      = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (Int
x forall a. Num a => a -> a -> a
+ Int
1)
    inContextOfDelta2 :: forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfDelta2 = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext HasCallStack => Impossible
impossible Int
x

    -- Debug printing
    debugInit :: a -> a -> [NamedArg SplitPattern] -> a -> tcm ()
debugInit a
tel a
x [NamedArg SplitPattern]
ps a
cps = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"TypeChecking.Coverage.split': split"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"tel     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
tel
          , TCMT IO Doc
"x       =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x
          , TCMT IO Doc
"ps      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext a
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
          , TCMT IO Doc
"cps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
cps
          ]
        ]
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"TypeChecking.Coverage.split': split"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"tel     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) a
tel
          , TCMT IO Doc
"x       =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) a
x
          , TCMT IO Doc
"ps      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) [NamedArg SplitPattern]
ps
          , TCMT IO Doc
"cps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.top" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
        [ TCMT IO Doc
"p      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (ShowS
patVarNameToString [Char]
s)
        , TCMT IO Doc
"ps     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps
        , TCMT IO Doc
"delta1 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
delta1
        , TCMT IO Doc
"delta2 =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfDelta2 (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
delta2)
        , TCMT IO Doc
"t      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCM tcm, MonadAddContext tcm, MonadDebug tcm) =>
tcm a -> tcm a
inContextOfT (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t)
        ]


-- | splitResult for MakeCase, tries to introduce IApply or ProjP copatterns
splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult QName
f SplitClause
sc = do
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (QName -> SplitClause -> TCM (Maybe SplitClause)
splitResultPath QName
f SplitClause
sc)
             ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Covering -> [SplitClause]
splitClauses forall a b. (a -> b) -> a -> b
$ QName -> SplitClause -> TCM (Either SplitError Covering)
splitResultRecord QName
f SplitClause
sc)
             (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[]))


-- | Tries to split the result to introduce an IApply pattern.
splitResultPath :: QName -> SplitClause -> TCM (Maybe SplitClause)
splitResultPath :: QName -> SplitClause -> TCM (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
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ Dom Type
t -> do
        forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (Dom Type, Abs Type))
isPath (forall t e. Dom' t e -> e
unDom Dom Type
t)) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ (Dom Type, Abs Type)
_ -> do
               (TelV Telescope
i Type
b, Boundary
boundary) <- forall (m :: * -> *).
PureTCM m =>
Int -> Type -> m (TelV Type, Boundary)
telViewUpToPathBoundary' Int
1 (forall t e. Dom' t e -> e
unDom Dom Type
t)
               let tel' :: Telescope
tel' = forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel Telescope
i
                   rho :: Substitution' a
rho  = forall a. Int -> Substitution' a
raiseS Int
1
                   ps' :: [NamedArg SplitPattern]
ps' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst forall a. Substitution' a
rho (SplitClause -> [NamedArg SplitPattern]
scPats SplitClause
sc) forall a. [a] -> [a] -> [a]
++ forall a.
DeBruijn a =>
Telescope -> Boundary -> [NamedArg (Pattern' a)]
telePatterns Telescope
i Boundary
boundary
                   cps' :: Map CheckpointId (Substitution' Term)
cps' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst forall a. Substitution' a
rho (SplitClause -> Map CheckpointId (Substitution' Term)
scCheckpoints SplitClause
sc)
                   target' :: Maybe (Dom Type)
target' = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Type
b forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
t
               forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Telescope
-> [NamedArg SplitPattern]
-> Substitution' SplitPattern
-> Map CheckpointId (Substitution' Term)
-> Maybe (Dom Type)
-> SplitClause
SClause Telescope
tel' [NamedArg SplitPattern]
ps' forall a. Substitution' a
idS Map CheckpointId (Substitution' Term)
cps' Maybe (Dom Type)
target'

-- | @splitResultRecord f sc = return res@
--
--   If the target type of @sc@ is a record type, a covering set of
--   split clauses is returned (@sc@ extended by all valid projection patterns),
--   otherwise @res == Left _@.
--   Note that the empty set of split clauses is returned if the record has no fields.
splitResultRecord :: QName -> SplitClause -> TCM (Either SplitError Covering)
splitResultRecord :: QName -> SplitClause -> TCM (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
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.split" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"splitting result:"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"f      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
f
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"target =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Maybe (Dom Type)
target)
    ]
  -- if we want to split projections, but have no target type, we give up
  let failure :: a -> TCMT IO (Either a b)
failure = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target (forall {a} {b}. a -> TCMT IO (Either a b)
failure SplitError
CosplitNoTarget) forall a b. (a -> b) -> a -> b
$ \ Dom Type
t -> do
    Maybe (QName, Args, Defn)
isR <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom Type
t
    case Maybe (QName, Args, Defn)
isR of
      Just (QName
_r, Args
vs, Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs }) -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"we are of record type _r = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
_r
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"applied to parameters vs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs)
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"and have fields       fs = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [Dom QName]
fs
          ]
        -- Andreas, 2018-06-09, issue #2170, we always have irrelevant projections
        -- available on the lhs.
        -- -- Andreas, 2018-03-19, issue #2971, check that we have a "strong" record type,
        -- -- i.e., with all the projections.  Otherwise, we may not split.
        -- ifNotM (strongRecord fs) (failure CosplitIrrelevantProjections) $ {-else-} do
        let es :: Elims
es = NAPs -> Elims
patternsToElims forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
        -- Note: module parameters are part of ps
        let self :: Arg Term
self  = forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
f [] forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
            pargs :: Args
pargs = Args
vs forall a. [a] -> [a] -> [a]
++ [Arg Term
self]
            fieldValues :: [Term]
fieldValues = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Dom QName]
fs forall a b. (a -> b) -> a -> b
$ \ Dom QName
proj -> forall e. Arg e -> e
unArg Arg Term
self forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem (forall t e. Dom' t e -> e
unDom Dom QName
proj)]
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover" Int
20 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"we are              self =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall e. Arg e -> e
unArg Arg Term
self)
          , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text   [Char]
"            field values =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
fieldValues
          ]
        let n :: Arg Int
n = forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ Permutation -> Int
permRange forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ NAPs -> Maybe Permutation
dbPatPerm forall a b. (a -> b) -> a -> b
$ [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
ps
            -- Andreas & James, 2013-11-19 includes the dot patterns!
            -- See test/succeed/CopatternsAndDotPatterns.agda for a case with dot patterns
            -- and copatterns which fails for @n = size tel@ with a broken case tree.

        -- Andreas, 2016-07-22 read the style of projections from the user's lips
        ProjOrigin
projOrigin <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optPostfixProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPostfix) (forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPrefix)
        forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Int -> [(SplitTag, (SplitClause, IInfo))] -> Covering
Covering Arg Int
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Dom QName]
fs forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]]
List.inits [Term]
fieldValues) forall a b. (a -> b) -> a -> b
$ \ (Dom QName
proj, [Term]
prevFields) -> do
            -- compute the new target
            Type
dType <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom QName
proj -- WRONG: typeOfConst $ unArg proj
            let -- Substitution for parameters and previous fields. Needs to be applied to potential
                -- tactic in proj.
                fieldSub :: Substitution' Term
fieldSub = forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg Args
vs forall a. [a] -> [a] -> [a]
++ [Term]
prevFields) forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Impossible -> Substitution' a
EmptyS HasCallStack => Impossible
impossible
                proj' :: Dom QName
proj'    = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
fieldSub Dom QName
proj
                -- type of projection instantiated at self
                target' :: Maybe (Dom Type)
target' = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Dom QName
proj' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Type
dType Type -> Args -> Type
`piApply` Args
pargs      -- Always visible (#2287)
                projArg :: NamedArg SplitPattern
projArg = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall name a. Maybe name -> a -> Named name a
Named forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
projOrigin) forall a b. (a -> b) -> a -> b
$ forall t a. Dom' t a -> Arg a
argFromDom forall a b. (a -> b) -> a -> b
$ forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
NotHidden Dom QName
proj
                sc' :: SplitClause
sc' = SplitClause
sc { scPats :: [NamedArg SplitPattern]
scPats   = SplitClause -> [NamedArg SplitPattern]
scPats SplitClause
sc forall a. [a] -> [a] -> [a]
++ [NamedArg SplitPattern
projArg]
                         , scSubst :: Substitution' SplitPattern
scSubst  = forall a. Substitution' a
idS
                         , scTarget :: Maybe (Dom Type)
scTarget = Maybe (Dom Type)
target'
                         }
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cover.copattern" Int
40 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
              [ TCMT IO Doc
"fieldSub for" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall t e. Dom' t e -> e
unDom Dom QName
proj)
              , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution' Term
fieldSub ]
            forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> SplitTag
SplitCon (forall t e. Dom' t e -> e
unDom Dom QName
proj), (SplitClause
sc', IInfo
NoInfo))
      Maybe (QName, Args, Defn)
_ -> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (forall t e. Dom' t e -> e
unDom Dom Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {a} {b}. a -> TCMT IO (Either a b)
failure forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Type -> SplitError
CosplitNoRecordType
  -- Andreas, 2018-06-09, issue #2170: splitting with irrelevant fields is always fine!
  -- where
  -- -- A record type is strong if it has all the projections.
  -- -- This is the case if --irrelevant-projections or no field is irrelevant.
  -- -- TODO: what about shape irrelevance?
  -- strongRecord :: [Arg QName] -> TCM Bool
  -- strongRecord fs = (optIrrelevantProjections <$> pragmaOptions) `or2M`
  --   (return $ not $ any isIrrelevant fs)


-- * Boring instances

-- | For debugging only.
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) = forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ m Doc
"SplitClause"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ m Doc
"tel          =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
      , m Doc
"pats         =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg SplitPattern]
pats)
      , m Doc
"subst        =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution' SplitPattern
sigma
      , m Doc
"checkpoints  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Map CheckpointId (Substitution' Term)
cps
      , m Doc
"target       =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
          forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Dom Type)
target forall a. Null a => a
empty forall a b. (a -> b) -> a -> b
$ \ Dom Type
t -> do
            forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
t
      -- Triggers crash (see Issue 1374).
      -- , "subst target = " <+> do
      --     caseMaybe target empty $ \ t -> do
      --       addContext tel $ prettyTCM $ applySubst sigma t
      ]
    ]