{-# LANGUAGE NondecreasingIndentation #-}

module Agda.Interaction.MakeCase where

import Prelude hiding ((!!), null)

import Control.Monad

import Data.Either
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Monoid

import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.Syntax.Concrete (NameInScope(..))
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Pattern as C
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Pattern as A
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Scope.Base  ( ResolvedName(..), BindingSource(..), KindOfName(..), exceptKindsOfNames )
import Agda.Syntax.Scope.Monad ( resolveName' )
import Agda.Syntax.Translation.InternalToAbstract

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( SplitPatVar(..) , SplitPattern , applySplitPSubst , fromSplitPatterns )
import Agda.TypeChecking.Empty ( isEmptyTel )
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Def (checkClauseLHS)
import Agda.TypeChecking.Rules.LHS (LHSResult(..))
import Agda.TypeChecking.Rules.LHS.Problem (AsBinding(..))

import Agda.Interaction.Options
import Agda.Interaction.BasicOps

import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size

import Agda.Utils.Impossible

type CaseContext = Maybe ExtLamInfo

-- | Parse variables (visible or hidden), returning their de Bruijn indices.
--   Used in 'makeCase'.

parseVariables
  :: QName           -- ^ The function name.
  -> Context         -- ^ The context of the RHS of the clause we are splitting.
  -> [AsBinding]     -- ^ The as-bindings of the clause we are splitting
  -> InteractionId   -- ^ The hole of this function we are working on.
  -> Range           -- ^ The range of this hole.
  -> [String]        -- ^ The words the user entered in this hole (variable names).
  -> TCM [(Int,NameInScope)] -- ^ The computed de Bruijn indices of the variables to split on,
                             --   with information about whether each variable is in scope.
parseVariables :: QName
-> Context
-> [AsBinding]
-> InteractionId
-> Range
-> [String]
-> TCM [(Int, NameInScope)]
parseVariables QName
f Context
cxt [AsBinding]
asb InteractionId
ii Range
rng [String]
ss = do

  -- We parse the variables in two steps:
  -- (1) Convert the strings given by the user to abstract names,
  --     using the scope information from the interaction meta.
  -- (2) Convert the abstract names to de Bruijn indices,
  --     using the context of the clause.

  -- Get into the context of the meta.
  MetaId
mId <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mId Range
rng
  Closure Range
mi  <- MetaVariable -> Closure Range
getMetaInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mId
  forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Range
mi forall a b. (a -> b) -> a -> b
$ \ Range
r -> do

  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
20 forall a b. (a -> b) -> a -> b
$ do
    ModuleName
m   <- forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
    Telescope
tel <- forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
     [ TCMT IO Doc
"parseVariables:"
     , TCMT IO Doc
"current module  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
m
     , TCMT IO Doc
"current section =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel)
     , TCMT IO Doc
"clause context  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Context -> PrettyContext
PrettyContext Context
cxt)
     ]

  -- Get printed representation of variables in context.  These are
  -- used for recognizing when the user wants to make a hidden
  -- variable (which is not in scope) visible.
  Int
n  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
  [(String, Name)]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Integral a => a -> [a]
downFrom Int
n) forall a b. (a -> b) -> a -> b
$ \ Int
i ->
    (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Doc -> String
P.render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
i)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
i

  -- Step 1: From strings to abstract names
  [(Name, Maybe BindingSource)]
abstractNames :: [(A.Name, Maybe BindingSource)] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [String]
ss forall a b. (a -> b) -> a -> b
$ \String
s -> do

    let cname :: QName
cname = Name -> QName
C.QName forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> NameParts -> Name
C.Name Range
r NameInScope
C.InScope forall a b. (a -> b) -> a -> b
$ String -> NameParts
C.stringNameParts String
s
    -- Note: the range in the concrete name is only approximate.
    -- Jesper, 2018-12-19: Don't consider generalizable names since
    -- they can be shadowed by hidden variables.
    KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
resolveName' ([KindOfName] -> KindsOfNames
exceptKindsOfNames [KindOfName
GeneralizeName]) forall a. Maybe a
Nothing QName
cname forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

      -- Fail if s is a name, but not of a variable.
      DefinedName{}       -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failNotVar String
s
      FieldName{}         -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failNotVar String
s
      ConstructorName{}   -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failNotVar String
s
      PatternSynResName{} -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failNotVar String
s

      -- If s is a variable name, return it together with binding information.
      VarName Name
x BindingSource
b -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, forall a. a -> Maybe a
Just BindingSource
b)

      -- If s is not a name, compare it to the printed variable representation.
      ResolvedName
UnknownName -> case (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s [(String, Name)]
xs) of
        Maybe Name
Nothing -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failUnbound String
s
        Just Name
x  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, forall a. Maybe a
Nothing)

  -- Step 2: Resolve each abstract name to a de Bruijn index.

  -- First, get context names of the clause.
  let clauseCxtNames :: [Name]
clauseCxtNames = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) Context
cxt

  -- Valid names to split on are pattern variables of the clause,
  -- plus as-bindings that refer to a variable.
  let clauseVars :: [(Name, Term)]
clauseVars = forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
clauseCxtNames (forall a b. (a -> b) -> [a] -> [b]
map Int -> Term
var [Int
0..]) forall a. [a] -> [a] -> [a]
++
                   forall a b. (a -> b) -> [a] -> [b]
map (\(AsB Name
name Term
v Type
_ Modality
_) -> (Name
name,Term
v)) [AsBinding]
asb

  -- We cannot split on module parameters or make them visible
  Args
params <- forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
 ReadTCState m, MonadDebug m) =>
ModuleName -> m Args
moduleParamsToApply forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
f
  let isParam :: Int -> Bool
isParam Int
i = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((forall a. Eq a => a -> a -> Bool
== Int -> Term
var Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) Args
params

  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 [String]
ss [(Name, Maybe BindingSource)]
abstractNames) forall a b. (a -> b) -> a -> b
$ \(String
s, (Name
name, Maybe BindingSource
bound)) -> case Maybe BindingSource
bound of
    -- Case 1: variable has a binding site. Check if it also exists in
    -- the clause context so we can split on it.
    Just BindingSource
bindingSource -> case (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, Term)]
clauseVars, BindingSource
bindingSource) of
      -- Case 1a: it is also known in the clause telescope and is
      -- actually a variable. If a pattern variable (`PatternBound`)
      -- has been refined to a module parameter we do allow splitting
      -- on it, since the instantiation could as well have been the
      -- other way around (see #2183).
      (Just (Var Int
i []), BindingSource
PatternBound) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, NameInScope
C.InScope)
      -- Case 1b: the variable has been refined.
      (Just Term
v         , BindingSource
PatternBound) -> forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
String -> a -> m b
failInstantiatedVar String
s Term
v
      -- Case 1c: the variable is bound locally (e.g. a record let)
      (Maybe Term
Nothing        , BindingSource
PatternBound) -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failCaseLet String
s
      -- Case 1d: module parameter
      (Just (Var Int
i []), BindingSource
LambdaBound ) -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failModuleBound String
s
      -- Case 1e: locally lambda-bound variable
      (Maybe Term
_              , BindingSource
LambdaBound ) -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failLocal String
s
      -- Case 1f: let-bound variable
      (Maybe Term
_              , BindingSource
LetBound    ) -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failLetBound String
s
      -- Case 1g: with-bound variable (not used?)
      (Maybe Term
_              , BindingSource
WithBound   ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Case 2: variable has no binding site, so we check if it can be
    -- made visible.
    Maybe BindingSource
Nothing -> case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete) Name
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, Term)]
clauseVars of
      -- Case 2a: there is a variable with that concrete name in the
      -- clause context. If it is not a parameter, we can make it
      -- visible.
      Just (Name
x, Var Int
i []) | Int -> Bool
isParam Int
i -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenModuleBound String
s
                         | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, NameInScope
C.NotInScope)
      -- Case 2b: there is a variable with that concrete name, but it
      -- has been refined.
      Just (Name
x, Term
v) -> forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
String -> a -> m b
failInstantiatedVar String
s Term
v
      -- Case 2c: there is no variable with that name. Since it was in
      -- scope for the interaction meta, the only possibility is that
      -- it is a hidden lambda-bound variable.
      Maybe (Name, Term)
Nothing -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenLocal String
s

  where

  failNotVar :: String -> m a
failNotVar String
s      = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ String
"Not a variable: " forall a. [a] -> [a] -> [a]
++ String
s
  failUnbound :: String -> m a
failUnbound String
s     = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ String
"Unbound variable " forall a. [a] -> [a] -> [a]
++ String
s
  failAmbiguous :: String -> m a
failAmbiguous String
s   = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ String
"Ambiguous variable " forall a. [a] -> [a] -> [a]
++ String
s
  failLocal :: String -> m a
failLocal String
s       = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on local variable " forall a. [a] -> [a] -> [a]
++ String
s
  failHiddenLocal :: String -> m a
failHiddenLocal String
s = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"Cannot make hidden lambda-bound variable " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" visible"
  failModuleBound :: String -> m a
failModuleBound String
s = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on module parameter " forall a. [a] -> [a] -> [a]
++ String
s
  failHiddenModuleBound :: String -> m a
failHiddenModuleBound String
s = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"Cannot make hidden module parameter " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" visible"
  failLetBound :: String -> m a
failLetBound String
s = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on let-bound variable " forall a. [a] -> [a] -> [a]
++ String
s
  failInstantiatedVar :: String -> a -> m b
failInstantiatedVar String
s a
v = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Cannot split on variable " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
", because it is bound to"
      , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v
      ]
  failCaseLet :: String -> m a
failCaseLet String
s     = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on variable " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++
    String
", because let-declarations may not be defined by pattern-matching"



-- | Lookup the clause for an interaction point in the signature.
--   Returns the CaseContext, the previous clauses, the clause itself,
--   and a list of the remaining ones.

type ClauseZipper =
   ( [Clause] -- previous clauses
   , Clause   -- clause of interest
   , [Clause] -- other clauses
   )

getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP QName
f Int
clauseNo = do
  (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funExtLam :: Defn -> CaseContext
funExtLam = CaseContext
extlam} -> do
      let ([Clause]
cs1,[Clause]
ccs2) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
clauseNo [Clause]
cs
          (Clause
c,[Clause]
cs2)    = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe (a, [a])
uncons [Clause]
ccs2
      forall (m :: * -> *) a. Monad m => a -> m a
return (CaseContext
extlam, ([Clause]
cs1, Clause
c, [Clause]
cs2))
    Defn
d -> do
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"impossible" 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
"getClauseZipperForIP" 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 => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
clauseNo)
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"received"
        , forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Defn
d)
        ]
      forall a. HasCallStack => a
__IMPOSSIBLE__

recheckAbstractClause :: Type -> Maybe Substitution -> A.SpineClause -> TCM (Clause, Context, [AsBinding])
recheckAbstractClause :: Type
-> Maybe Substitution
-> SpineClause
-> TCM (Clause, Context, [AsBinding])
recheckAbstractClause Type
t Maybe Substitution
sub SpineClause
acl = forall a.
Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
sub SpineClause
acl forall a b. (a -> b) -> a -> b
$ \ LHSResult
lhs -> do
  let cl :: Clause
cl = Clause { clauseLHSRange :: Range
clauseLHSRange    = forall a. HasRange a => a -> Range
getRange SpineClause
acl
                  , clauseFullRange :: Range
clauseFullRange   = forall a. HasRange a => a -> Range
getRange SpineClause
acl
                  , clauseTel :: Telescope
clauseTel         = LHSResult -> Telescope
lhsVarTele LHSResult
lhs
                  , namedClausePats :: NAPs
namedClausePats   = LHSResult -> NAPs
lhsPatterns LHSResult
lhs
                  , clauseBody :: Maybe Term
clauseBody        = forall a. Maybe a
Nothing -- We don't need the body for make case
                  , clauseType :: Maybe (Arg Type)
clauseType        = forall a. a -> Maybe a
Just (LHSResult -> Arg Type
lhsBodyType LHSResult
lhs)
                  , clauseCatchall :: Bool
clauseCatchall    = Bool
False
                  , clauseExact :: Maybe Bool
clauseExact       = forall a. Maybe a
Nothing
                  , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. Maybe a
Nothing
                  , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. Maybe a
Nothing
                  , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = LHSInfo -> ExpandedEllipsis
lhsEllipsis forall a b. (a -> b) -> a -> b
$ SpineLHS -> LHSInfo
A.spLhsInfo forall a b. (a -> b) -> a -> b
$ forall lhs. Clause' lhs -> lhs
A.clauseLHS SpineClause
acl
                  , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = WhereDeclarations -> Maybe ModuleName
A.whereModule forall a b. (a -> b) -> a -> b
$ forall lhs. Clause' lhs -> WhereDeclarations
A.clauseWhereDecls SpineClause
acl
                  }
  Context
cxt <- forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  let asb :: [AsBinding]
asb = LHSResult -> [AsBinding]
lhsAsBindings LHSResult
lhs
  forall (m :: * -> *) a. Monad m => a -> m a
return (Clause
cl, Context
cxt, [AsBinding]
asb)


-- | Entry point for case splitting tactic.

makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [A.Clause])
makeCase :: InteractionId
-> Range -> String -> TCM (QName, CaseContext, [Clause])
makeCase InteractionId
hole Range
rng String
s = forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
hole 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
eMakeCase (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$ do

  -- Jesper, 2018-12-10: print unsolved metas in dot patterns as _
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envPrintMetasBare :: Bool
envPrintMetasBare = Bool
True }) forall a b. (a -> b) -> a -> b
$ do

  -- Get function clause which contains the interaction point.
  InteractionPoint { ipMeta :: InteractionPoint -> Maybe MetaId
ipMeta = Maybe MetaId
mm, ipClause :: InteractionPoint -> IPClause
ipClause = IPClause
ipCl} <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
hole
  (QName
f, Int
clauseNo, Type
clTy, Maybe Substitution
clWithSub, absCl :: SpineClause
absCl@A.Clause{ clauseRHS :: forall lhs. Clause' lhs -> RHS
clauseRHS = RHS
rhs }, Closure ()
clClos) <- case IPClause
ipCl of
    IPClause QName
f Int
i Type
t Maybe Substitution
sub SpineClause
cl Closure ()
clo [Closure IPBoundary]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Int
i, Type
t, Maybe Substitution
sub, SpineClause
cl, Closure ()
clo)
    IPClause
IPNoClause                -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
      String
"Cannot split here, as we are not in a function definition"
  (CaseContext
casectxt, ([Clause]
prevClauses0, Clause
_clause, [Clause]
follClauses0)) <- QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP QName
f Int
clauseNo

  -- Instead of using the actual internal clause, we retype check the abstract clause (with
  -- eMakeCase = True). This disables the forcing translation in the unifier, which allows us to
  -- split on forced variables.
  (Clause
clause, Context
clauseCxt, [AsBinding]
clauseAsBindings) <-
    forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure ()
clClos 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
eMakeCase (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$
      Type
-> Maybe Substitution
-> SpineClause
-> TCM (Clause, Context, [AsBinding])
recheckAbstractClause Type
clTy Maybe Substitution
clWithSub SpineClause
absCl

  let ([Clause]
prevClauses, [Clause]
follClauses) = forall a. KillRange a => KillRangeT a
killRange ([Clause]
prevClauses0, [Clause]
follClauses0)
    -- Andreas, 2019-08-08, issue #3966
    -- Kill the ranges of the existing clauses to prevent wrong error
    -- location to be set by the coverage checker (via isCovered)
    -- for test/interaction/Issue191
  let perm :: Permutation
perm = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
clause
      tel :: Telescope
tel  = Clause -> Telescope
clauseTel  Clause
clause
      ps :: NAPs
ps   = Clause -> NAPs
namedClausePats Clause
clause
      ell :: ExpandedEllipsis
ell  = Clause -> ExpandedEllipsis
clauseEllipsis Clause
clause
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
100 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"splitting clause:"
    , 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
"f       =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) QName
f
      , 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 => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
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
"tel     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Telescope
tel
      , TCMT IO Doc
"perm    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Permutation
perm)
      , TCMT IO Doc
"ps      =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) NAPs
ps
      ]
    ]
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" 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
"splitting clause:"
    , 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
"f       =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
f
      , 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 :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty) 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
"tel     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
tel
      , TCMT IO Doc
"perm    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) Permutation
perm
      , 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 =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" 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 clause:"
    , 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
"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
"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
"tel     =" 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) Telescope
tel
      , TCMT IO Doc
"perm    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Permutation
perm)
      , TCMT IO Doc
"ps      =" 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 (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps)
      , TCMT IO Doc
"ell     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show ExpandedEllipsis
ell)
      , TCMT IO Doc
"type    =" 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 forall a b. (a -> b) -> a -> b
$ Clause -> Maybe (Arg Type)
clauseType Clause
clause)
      ]
    ]

  -- Check split variables.

  let vars :: [String]
vars = String -> [String]
words String
s

  -- If the user just entered ".", do nothing.
  -- This will expand an ellipsis, if present.

  if forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String]
vars forall a. Eq a => a -> a -> Bool
== String
"." then do
    Clause
cl <- QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbstractClause QName
f RHS
rhs ExpandedEllipsis
NoEllipsis forall a b. (a -> b) -> a -> b
$ Clause -> SplitClause
clauseToSplitClause Clause
clause
    forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, CaseContext
casectxt, [Clause
cl])

  -- If we have no split variables, split on result.

  else if forall a. Null a => a -> Bool
null [String]
vars then do
    -- Andreas, 2017-07-24, issue #2654:
    -- When we introduce projection patterns in an extended lambda,
    -- we need to print them postfix.
    let postProjInExtLam :: TCMT IO [SplitClause] -> TCMT IO [SplitClause]
postProjInExtLam = forall a. Bool -> (a -> a) -> a -> a
applyWhen (forall a. Maybe a -> Bool
isJust CaseContext
casectxt) forall a b. (a -> b) -> a -> b
$
          forall (m :: * -> *) a.
ReadTCState m =>
(PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions forall a b. (a -> b) -> a -> b
$ \ PragmaOptions
opt -> PragmaOptions
opt { optPostfixProjections :: Bool
optPostfixProjections = Bool
True }
    (Telescope
piTel, SplitClause
sc) <- Bool -> SplitClause -> TCM (Telescope, SplitClause)
insertTrailingArgs Bool
False forall a b. (a -> b) -> a -> b
$ Clause -> SplitClause
clauseToSplitClause Clause
clause
    -- Andreas, 2015-05-05 If we introduced new function arguments
    -- do not split on result.  This might be more what the user wants.
    -- To split on result, he can then C-c C-c again.
    -- Andreas, 2015-05-21 Issue 1516:  However, if only hidden
    -- arguments are introduced, C-c C-c virtually does nothing
    -- (as they are not shown and get lost on the way to emacs and back).
    Bool
newPats <- if forall a. Null a => a -> Bool
null Telescope
piTel then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
      -- If there were any pattern introduce, they will only have effect
      -- if any of them is shown by the printer
      Bool
imp <- PragmaOptions -> Bool
optShowImplicit 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 forall a b. (a -> b) -> a -> b
$ Bool
imp Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. LensHiding a => a -> Bool
visible (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
piTel)
    [SplitClause]
scs <- if Bool
newPats then forall (m :: * -> *) a. Monad m => a -> m a
return [SplitClause
sc] else TCMT IO [SplitClause] -> TCMT IO [SplitClause]
postProjInExtLam forall a b. (a -> b) -> a -> b
$ do
      Either SplitError [SplitClause]
res <- QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult QName
f SplitClause
sc
      case Either SplitError [SplitClause]
res of

        Left SplitError
err  -> do
          -- Andreas, 2017-12-16, issue #2871
          -- If there is nothing to split, introduce trailing hidden arguments.

          -- Get trailing hidden pattern variables
          let trailingPatVars :: [NamedArg DBPatVar]
              trailingPatVars :: [NamedArg DBPatVar]
trailingPatVars = forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust forall {name} {a}.
Arg (Named name (Pattern' a)) -> Maybe (Arg (Named name a))
isVarP forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse NAPs
ps
              isVarP :: Arg (Named name (Pattern' a)) -> Maybe (Arg (Named name a))
isVarP (Arg ArgInfo
ai (Named Maybe name
n (VarP PatternInfo
_ a
x))) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named Maybe name
n a
x
              isVarP Arg (Named name (Pattern' a))
_ = forall a. Maybe a
Nothing
          -- If all are already coming from the user, there is really nothing todo!
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Origin
UserWritten forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensOrigin a => a -> Origin
getOrigin) [NamedArg DBPatVar]
trailingPatVars) forall a b. (a -> b) -> a -> b
$ do
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError SplitError
err
          -- Otherwise, we make these user-written
          let xs :: [Int]
xs = forall a b. (a -> b) -> [a] -> [b]
map (DBPatVar -> Int
dbPatVarIndex forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg DBPatVar]
trailingPatVars
          forall (m :: * -> *) a. Monad m => a -> m a
return [[Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Int]
xs SplitClause
sc]

        Right [SplitClause]
cov -> forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optCopatterns forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) forall {a}. TCMT IO a
failNoCop forall a b. (a -> b) -> a -> b
$ {-else-} do
          -- Andreas, 2016-05-03: do not introduce function arguments after projection.
          -- This is sometimes annoying and can anyway be done by another C-c C-c.
          -- mapM (snd <.> fixTarget) $ splitClauses cov
          forall (m :: * -> *) a. Monad m => a -> m a
return [SplitClause]
cov
    IPClause -> TCMT IO ()
checkClauseIsClean IPClause
ipCl
    (QName
f, CaseContext
casectxt,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      -- Andreas, 2020-05-18, issue #4536
      -- When result splitting yields no clauses, replace rhs by @record{}@.
      if forall a. Null a => a -> Bool
null [SplitClause]
scs then
        forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a b. LHSToSpine a b => b -> a
A.spineToLhs forall a b. (a -> b) -> a -> b
$ SpineClause
absCl{ clauseRHS :: RHS
A.clauseRHS = RHS -> RHS
makeRHSEmptyRecord RHS
rhs } ]
      else forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbstractClause QName
f RHS
rhs ExpandedEllipsis
ell) [SplitClause]
scs
  else do
    -- split on variables
    [(Int, NameInScope)]
xs <- QName
-> Context
-> [AsBinding]
-> InteractionId
-> Range
-> [String]
-> TCM [(Int, NameInScope)]
parseVariables QName
f Context
clauseCxt [AsBinding]
clauseAsBindings InteractionId
hole Range
rng [String]
vars
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.case" Int
30 forall a b. (a -> b) -> a -> b
$ String
"parsedVariables: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. [a] -> [b] -> [(a, b)]
zip [(Int, NameInScope)]
xs [String]
vars)
    -- Variables that are not in scope yet are brought into scope (@toShow@)
    -- The other variables are split on (@toSplit@).
    let ([Int]
toShow, [Int]
toSplit) = forall a b. [Either a b] -> ([a], [b])
partitionEithers 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, NameInScope)]
xs [String]
vars) forall a b. (a -> b) -> a -> b
$ \ ((Int
x,NameInScope
nis), String
s) ->
          if (NameInScope
nis forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope) then forall a b. a -> Either a b
Left Int
x else forall a b. b -> Either a b
Right Int
x
    let sc :: SplitClause
sc = [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Int]
toShow forall a b. (a -> b) -> a -> b
$ Clause -> SplitClause
clauseToSplitClause Clause
clause
    [(SplitClause, Bool)]
scs <- QName -> [Int] -> SplitClause -> TCM [(SplitClause, Bool)]
split QName
f [Int]
toSplit SplitClause
sc
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.case" Int
70 forall a b. (a -> b) -> a -> b
$ String
"makeCase: survived the splitting"

    -- If any of the split variables is hidden by the ellipsis, we
    -- should force the expansion of the ellipsis.
    let splitNames :: [Name]
splitNames = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ Context
clauseCxt forall a. HasCallStack => [a] -> Int -> a
!! Int
i) [Int]
toSplit
    Bool
shouldExpandEllipsis <- forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null [Int]
toShow) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` QName -> SpineClause -> [Name] -> TCMT IO Bool
anyEllipsisVar QName
f SpineClause
absCl [Name]
splitNames
    let ell' :: ExpandedEllipsis
ell' | Bool
shouldExpandEllipsis = ExpandedEllipsis
NoEllipsis
             | Bool
otherwise            = ExpandedEllipsis
ell

    -- CLEAN UP OF THE GENERATED CLAUSES
    -- 1. filter out the generated clauses that are already covered
    --    we consider a generated clause already covered if it is covered by:
    --    a. a pre-existing clause defined before the one we splitted (prevClauses)
    --    b. a pre-existing clause defined after the one we splitted (follClauses)
    --       under the condition that it did not cover the one we splitted but was
    --       covered by it (i.e. it was considered unreachable).
    -- The key idea here is:
    --       f m    zero = ?  ---- split on m --->  f (suc m) zero = ?
    --       f zero zero = ?                        f zero    zero = ?
    --       f _    _    = ?                        f _       _    = ?
    -- because [f zero zero] is already defined.
    -- However we ignore [f _ _]: [f m zero] was already a refinement of it,
    -- hinting that we considered it more important than the catchall.
    let sclause :: SplitClause
sclause = Clause -> SplitClause
clauseToSplitClause Clause
clause
    [Clause]
fcs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\ Clause
cl -> (QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause
clause] (Clause -> SplitClause
clauseToSplitClause Clause
cl)) forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
                            (Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause
cl] SplitClause
sclause))
                   [Clause]
follClauses
    [(SplitClause, Bool)]
scs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f ([Clause]
prevClauses forall a. [a] -> [a] -> [a]
++ [Clause]
fcs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(SplitClause, Bool)]
scs
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.case" Int
70 forall a b. (a -> b) -> a -> b
$ String
"makeCase: survived filtering out already covered clauses"
    -- 2. filter out trivially impossible clauses not asked for by the user
    [Clause]
cs <- forall a. [Maybe a] -> [a]
catMaybes 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 [(SplitClause, Bool)]
scs forall a b. (a -> b) -> a -> b
$ \ (SplitClause
sc, Bool
isAbsurd) -> if Bool
isAbsurd
      -- absurd clause coming from a split asked for by the user
      then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell' SplitClause
sc
      -- trivially empty clause due to the refined patterns
      else
        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
$ Telescope -> TCMT IO Bool
isEmptyTel (SplitClause -> Telescope
scTel SplitClause
sc))
          {- then -} (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing)
          {- else -} (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbstractClause QName
f RHS
rhs ExpandedEllipsis
ell' SplitClause
sc)
    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.case" Int
70 forall a b. (a -> b) -> a -> b
$ String
"makeCase: survived filtering out impossible clauses"
    -- 3. If the cleanup removed everything then we know that none of the clauses where
    --    absurd but that all of them were trivially empty. In this case we rewind and
    --    insert all the clauses (garbage in, garbage out!)
    [Clause]
cs <- if Bool -> Bool
not (forall a. Null a => a -> Bool
null [Clause]
cs) then forall (f :: * -> *) a. Applicative f => a -> f a
pure [Clause]
cs
          else forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbstractClause QName
f RHS
rhs ExpandedEllipsis
ell' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(SplitClause, Bool)]
scs

    forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"split result:"
      , 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 a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cs
      ]
    IPClause -> TCMT IO ()
checkClauseIsClean IPClause
ipCl
    forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, CaseContext
casectxt, [Clause]
cs)

  where
  failNoCop :: TCMT IO a
failNoCop = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    String
"OPTION --copatterns needed to split on result here"

  -- Split clause on given variables, return the resulting clauses together
  -- with a bool indicating whether each clause is absurd
  split :: QName -> [Nat] -> SplitClause -> TCM [(SplitClause, Bool)]
  split :: QName -> [Int] -> SplitClause -> TCM [(SplitClause, Bool)]
split QName
f [] SplitClause
clause = forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitClause
clause,Bool
False)]
  split QName
f (Int
var : [Int]
vars) SplitClause
clause = do
    Either SplitError (Either SplitClause Covering)
z <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ SplitClause
-> Int -> TCMT IO (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd SplitClause
clause Int
var
    case Either SplitError (Either SplitClause Covering)
z of
      Left SplitError
err          -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError SplitError
err
      Right (Left SplitClause
cl)   -> forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitClause
cl,Bool
True)]
      Right (Right Covering
cov) -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 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 (Covering -> [SplitClause]
splitClauses Covering
cov) forall a b. (a -> b) -> a -> b
$ \ SplitClause
cl ->
              QName -> [Int] -> SplitClause -> TCM [(SplitClause, Bool)]
split QName
f (forall a b. (a -> Maybe b) -> [a] -> Prefix b
mapMaybe (SplitClause -> Int -> Maybe Int
newVar SplitClause
cl) [Int]
vars) SplitClause
cl

  -- Finds the new variable corresponding to an old one, if any.
  newVar :: SplitClause -> Nat -> Maybe Nat
  newVar :: SplitClause -> Int -> Maybe Int
newVar SplitClause
c Int
x = case forall a. TermSubst a => SplitPSubstitution -> a -> a
applySplitPSubst (SplitClause -> SplitPSubstitution
scSubst SplitClause
c) (Int -> Term
var Int
x) of
    Var Int
y [] -> forall a. a -> Maybe a
Just Int
y
    Term
_        -> forall a. Maybe a
Nothing

  -- Check whether clause has been refined after last load.
  -- In this case, we refuse to split, as this might lose the refinements.
  checkClauseIsClean :: IPClause -> TCM ()
  checkClauseIsClean :: IPClause -> TCMT IO ()
checkClauseIsClean IPClause
ipCl = do
    [InteractionPoint]
sips <- forall a. (a -> Bool) -> [a] -> [a]
filter InteractionPoint -> Bool
ipSolved forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. BiMap k v -> [v]
BiMap.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BiMap InteractionId InteractionPoint) TCState
stInteractionPoints
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.any ((forall a. Eq a => a -> a -> Bool
== IPClause
ipCl) forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> IPClause
ipClause) [InteractionPoint]
sips) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ String
"Cannot split as clause rhs has been refined.  Please reload"

-- | Make the given pattern variables visible by marking their origin as
--   'CaseSplit' and pattern origin as 'PatOSplit' in the 'SplitClause'.
makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause
makePatternVarsVisible :: [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [] SplitClause
sc = SplitClause
sc
makePatternVarsVisible [Int]
is sc :: SplitClause
sc@SClause{ scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
ps } =
  SplitClause
sc{ scPats :: [NamedArg SplitPattern]
scPats = forall a p.
MapNamedArgPattern a p =>
(NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
mapNamedArgPattern NamedArg SplitPattern -> NamedArg SplitPattern
mkVis [NamedArg SplitPattern]
ps }
  where
  mkVis :: NamedArg SplitPattern -> NamedArg SplitPattern
  mkVis :: NamedArg SplitPattern -> NamedArg SplitPattern
mkVis (Arg ArgInfo
ai (Named Maybe NamedName
n (VarP PatternInfo
o (SplitPatVar String
x Int
i [Literal]
ls))))
    | Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is =
      -- We could introduce extra consistency checks, like
      -- if visible ai then __IMPOSSIBLE__ else
      -- or passing the parsed name along and comparing it with @x@
      forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
CaseSplit ArgInfo
ai) forall a b. (a -> b) -> a -> b
$ forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
n forall a b. (a -> b) -> a -> b
$ forall x. PatternInfo -> x -> Pattern' x
VarP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSplit []) forall a b. (a -> b) -> a -> b
$ String -> Int -> [Literal] -> SplitPatVar
SplitPatVar String
x Int
i [Literal]
ls
  mkVis NamedArg SplitPattern
np = NamedArg SplitPattern
np

-- | If a copattern split yields no clauses, we must be at an empty record type.
--   In this case, replace the rhs by @record{}@
makeRHSEmptyRecord :: A.RHS -> A.RHS
makeRHSEmptyRecord :: RHS -> RHS
makeRHSEmptyRecord = \case
  A.RHS{}            -> A.RHS{ rhsExpr :: Expr
rhsExpr = ExprInfo -> RecordAssigns -> Expr
A.Rec forall a. Null a => a
empty forall a. Null a => a
empty, rhsConcrete :: Maybe Expr
rhsConcrete = forall a. Maybe a
Nothing }
  rhs :: RHS
rhs@A.RewriteRHS{} -> RHS
rhs{ rewriteRHS :: RHS
A.rewriteRHS = RHS -> RHS
makeRHSEmptyRecord forall a b. (a -> b) -> a -> b
$ RHS -> RHS
A.rewriteRHS RHS
rhs }
  RHS
A.AbsurdRHS        -> forall a. HasCallStack => a
__IMPOSSIBLE__
  A.WithRHS{}        -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Make clause with no rhs (because of absurd match).

makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell (SClause Telescope
tel [NamedArg SplitPattern]
sps SplitPSubstitution
_ Map CheckpointId Substitution
_ Maybe (Dom' Term Type)
t) = do
  let ps :: NAPs
ps = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
sps
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" 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
"Interaction.MakeCase.makeAbsurdClause: split clause:"
    , 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
<+> do (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
"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
"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 NAPs
ps -- P.sep <$> prettyTCMPatterns ps
      , TCMT IO Doc
"ell     =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show ExpandedEllipsis
ell)
      ]
    ]
  forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (QName -> ModuleName
qnameModule QName
f) forall a b. (a -> b) -> a -> b
$
    -- Andreas, 2015-05-29 Issue 635
    -- Contract implicit record patterns before printing.
    -- c <- translateRecordPatterns $ Clause noRange tel perm ps NoBody t False
    -- Jesper, 2015-09-19 Don't contract, since we do on-demand splitting
    forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ forall a. QName -> a -> QNamed a
QNamed QName
f forall a b. (a -> b) -> a -> b
$ 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 = NAPs
ps
      , clauseBody :: Maybe Term
clauseBody      = forall a. Maybe a
Nothing
      , clauseType :: Maybe (Arg Type)
clauseType      = forall t a. Dom' t a -> Arg a
argFromDom forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Dom' Term Type)
t
      , clauseCatchall :: Bool
clauseCatchall    = Bool
False
      , clauseExact :: Maybe Bool
clauseExact       = forall a. Maybe a
Nothing
      , clauseRecursive :: Maybe Bool
clauseRecursive   = forall a. Maybe a
Nothing
      , clauseUnreachable :: Maybe Bool
clauseUnreachable = forall a. Maybe a
Nothing
      , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
ell
      , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = forall a. Maybe a
Nothing
      }

-- | Make a clause with a question mark as rhs.

makeAbstractClause :: QName -> A.RHS -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbstractClause QName
f RHS
rhs ExpandedEllipsis
ell SplitClause
cl = do

  LHS
lhs <- forall lhs. Clause' lhs -> lhs
A.clauseLHS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell SplitClause
cl
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"reified lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA LHS
lhs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [] RHS
rhs WhereDeclarations
A.noWhereDecls Bool
False
  -- let ii = InteractionId (-1)  -- Dummy interaction point since we never type check this.
  --                              -- Can end up in verbose output though (#1842), hence not __IMPOSSIBLE__.
  -- let info = A.emptyMetaInfo   -- metaNumber = Nothing in order to print as ?, not ?n
  -- return $ A.Clause lhs [] (A.RHS $ A.QuestionMark info ii) [] False

anyEllipsisVar :: QName -> A.SpineClause -> [Name] -> TCM Bool
anyEllipsisVar :: QName -> SpineClause -> [Name] -> TCMT IO Bool
anyEllipsisVar QName
f SpineClause
cl [Name]
xs = do
  let lhs :: SpineLHS
lhs = forall lhs. Clause' lhs -> lhs
A.clauseLHS SpineClause
cl
      ps :: Patterns
ps  = SpineLHS -> Patterns
A.spLhsPats SpineLHS
lhs
      ell :: ExpandedEllipsis
ell = LHSInfo -> ExpandedEllipsis
lhsEllipsis forall a b. (a -> b) -> a -> b
$ SpineLHS -> LHSInfo
A.spLhsInfo SpineLHS
lhs
      anyVar :: A.Pattern -> Any -> Any
      anyVar :: Pattern -> Any -> Any
anyVar Pattern
p Any
acc = Bool -> Any
Any forall a b. (a -> b) -> a -> b
$ Any -> Bool
getAny Any
acc Bool -> Bool -> Bool
|| case Pattern
p of
        A.VarP BindName
x -> BindName -> Name
A.unBind BindName
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
xs
        Pattern
_        -> Bool
False
  case ExpandedEllipsis
ell of
    ExpandedEllipsis
NoEllipsis           -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    ExpandedEllipsis Range
_ Int
k -> do
      Patterns
ps' <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadReify m =>
QName -> Patterns -> Patterns -> m (QName, Patterns)
reifyDisplayFormP QName
f Patterns
ps []
      let ellipsisPats :: A.Patterns
          ellipsisPats :: Patterns
ellipsisPats = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall p. IsWithP p => Int -> [p] -> ([p], [p])
C.splitEllipsis Int
k Patterns
ps'
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case.ellipsis" 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
"should we expand the ellipsis?"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"xs           =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Name]
xs)
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ellipsisPats =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Patterns
ellipsisPats)
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Any -> Bool
getAny forall a b. (a -> b) -> a -> b
$ forall p m.
(APatternLike p, Monoid m) =>
(Pattern' (ADotT p) -> m -> m) -> p -> m
A.foldrAPattern Pattern -> Any -> Any
anyVar Patterns
ellipsisPats