    {-# 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 <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
      MetaId -> Range -> TCMT IO ()
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
    updateMetaVarRange MetaId
    mId Range
    rng
      Closure Range
    mi  <- MetaVariable -> Closure Range
    getMetaInfo (MetaVariable -> Closure Range)
    -> TCMT IO MetaVariable -> TCMT IO (Closure Range)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> MetaId -> TCMT IO MetaVariable
    forall (m :: * -> *).
    (MonadFail m, ReadTCState m) =>
    MetaId -> m MetaVariable
    lookupMeta MetaId
    mId
      Closure Range
    -> (Range -> TCM [(Int, NameInScope)]) -> TCM [(Int, NameInScope)]
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure Range
    mi ((Range -> TCM [(Int, NameInScope)]) -> TCM [(Int, NameInScope)])
    -> (Range -> TCM [(Int, NameInScope)]) -> TCM [(Int, NameInScope)]
    forall a b. (a -> b) -> a -> b
    $ \ Range
    r -> do

      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "interaction.case" Int
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        ModuleName
    m   <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
        Telescope
    tel <- ModuleName -> TCMT IO Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m
        [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
         [ TCMT IO Doc
    "parseVariables:"
         , TCMT IO Doc
    "current module  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ModuleName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    m
         , TCMT IO Doc
    "current section =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel)
         , TCMT IO Doc
    "clause context  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PrettyContext -> TCMT IO 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  <- TCMT IO Int
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
    getContextSize
      [(String, Name)]
    xs <- [Int]
    -> (Int -> TCMT IO (String, Name)) -> TCMT IO [(String, Name)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    n) ((Int -> TCMT IO (String, Name)) -> TCMT IO [(String, Name)])
    -> (Int -> TCMT IO (String, Name)) -> TCMT IO [(String, Name)]
    forall a b. (a -> b) -> a -> b
    $ \ Int
    i ->
        (,) (String -> Name -> (String, Name))
    -> TCMT IO String -> TCMT IO (Name -> (String, Name))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Doc -> String
    P.render (Doc -> String) -> TCMT IO Doc -> TCMT IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Int -> Term
    var Int
    i)) TCMT IO (Name -> (String, Name))
    -> TCMT IO Name -> TCMT IO (String, Name)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> TCMT IO Name
    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)] <- [String]
    -> (String -> TCMT IO (Name, Maybe BindingSource))
    -> TCMT IO [(Name, Maybe BindingSource)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [String]
    ss ((String -> TCMT IO (Name, Maybe BindingSource))
     -> TCMT IO [(Name, Maybe BindingSource)])
    -> (String -> TCMT IO (Name, Maybe BindingSource))
    -> TCMT IO [(Name, Maybe BindingSource)]
    forall a b. (a -> b) -> a -> b
    $ \String
    s -> do

        let cname :: QName
    cname = Name -> QName
    C.QName (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ Range -> NameInScope -> NameParts -> Name
    C.Name Range
    r NameInScope
    C.InScope (NameParts -> Name) -> NameParts -> Name
    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]) Maybe (Set Name)
    forall a. Maybe a
    Nothing QName
    cname ScopeM ResolvedName
    -> (ResolvedName -> TCMT IO (Name, Maybe BindingSource))
    -> TCMT IO (Name, Maybe BindingSource)
    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{}       -> String -> TCMT IO (Name, Maybe BindingSource)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failNotVar String
    s
          FieldName{}         -> String -> TCMT IO (Name, Maybe BindingSource)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failNotVar String
    s
          ConstructorName{}   -> String -> TCMT IO (Name, Maybe BindingSource)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failNotVar String
    s
          PatternSynResName{} -> String -> TCMT IO (Name, Maybe BindingSource)
    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 -> (Name, Maybe BindingSource) -> TCMT IO (Name, Maybe BindingSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    x, BindingSource -> Maybe BindingSource
    forall a. a -> Maybe a
    Just BindingSource
    b)

          -- If s is not a name, compare it to the printed variable representation.
          ResolvedName
    UnknownName -> case (String -> [(String, Name)] -> Maybe Name
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup String
    s [(String, Name)]
    xs) of
            Maybe Name
    Nothing -> String -> TCMT IO (Name, Maybe BindingSource)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failUnbound String
    s
            Just Name
    x  -> (Name, Maybe BindingSource) -> TCMT IO (Name, Maybe BindingSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    x, Maybe BindingSource
    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 = (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name)
    -> (Dom' Term (Name, Type) -> (Name, Type))
    -> Dom' Term (Name, Type)
    -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term (Name, Type) -> (Name, Type)
    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 = [Name] -> [Term] -> [(Name, Term)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    clauseCxtNames ((Int -> Term) -> [Int] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Int -> Term
    var [Int
    0..]) [(Name, Term)] -> [(Name, Term)] -> [(Name, Term)]
    forall a. [a] -> [a] -> [a]
    ++
                       (AsBinding -> (Name, Term)) -> [AsBinding] -> [(Name, Term)]
    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 <- ModuleName -> TCMT IO Args
    forall (m :: * -> *).
    (Functor m, Applicative m, HasOptions m, MonadTCEnv m,
     ReadTCState m, MonadDebug m) =>
    ModuleName -> m Args
    moduleParamsToApply (ModuleName -> TCMT IO Args) -> ModuleName -> TCMT IO Args
    forall a b. (a -> b) -> a -> b
    $ QName -> ModuleName
    qnameModule QName
    f
      let isParam :: Int -> Bool
    isParam Int
    i = (Arg Term -> Bool) -> Args -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ((Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int -> Term
    var Int
    i) (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) Args
    params

      [(String, (Name, Maybe BindingSource))]
    -> ((String, (Name, Maybe BindingSource))
        -> TCMT IO (Int, NameInScope))
    -> TCM [(Int, NameInScope)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM ([String]
    -> [(Name, Maybe BindingSource)]
    -> [(String, (Name, Maybe BindingSource))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [String]
    ss [(Name, Maybe BindingSource)]
    abstractNames) (((String, (Name, Maybe BindingSource))
      -> TCMT IO (Int, NameInScope))
     -> TCM [(Int, NameInScope)])
    -> ((String, (Name, Maybe BindingSource))
        -> TCMT IO (Int, NameInScope))
    -> TCM [(Int, NameInScope)]
    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 (Name -> [(Name, Term)] -> Maybe Term
    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) -> (Int, NameInScope) -> TCMT IO (Int, NameInScope)
    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) -> String -> Term -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a} {b}.
    (MonadError TCErr m, PrettyTCM a, PureTCM m,
     MonadInteractionPoints m, MonadFresh NameId m,
     MonadStConcreteNames 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) -> String -> TCMT IO (Int, NameInScope)
    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 ) -> String -> TCMT IO (Int, NameInScope)
    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 ) -> String -> TCMT IO (Int, NameInScope)
    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    ) -> String -> TCMT IO (Int, NameInScope)
    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   ) -> TCMT IO (Int, NameInScope)
    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 ((Name, Term) -> Bool) -> [(Name, Term)] -> Maybe (Name, Term)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    List.find ((Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Name -> Name -> Bool) -> (Name -> Name) -> Name -> Name -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` Name -> Name
    nameConcrete) Name
    name (Name -> Bool) -> ((Name, Term) -> Name) -> (Name, Term) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Term) -> Name
    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 -> String -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failHiddenModuleBound String
    s
                             | Bool
    otherwise -> (Int, NameInScope) -> TCMT IO (Int, NameInScope)
    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) -> String -> Term -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a} {b}.
    (MonadError TCErr m, PrettyTCM a, PureTCM m,
     MonadInteractionPoints m, MonadFresh NameId m,
     MonadStConcreteNames 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 -> String -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failHiddenLocal String
    s

      where

      failNotVar :: String -> m a
    failNotVar String
    s      = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $ String
    "Not a variable: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failUnbound :: String -> m a
    failUnbound String
    s     = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $ String
    "Unbound variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failAmbiguous :: String -> m a
    failAmbiguous String
    s   = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $ String
    "Ambiguous variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failLocal :: String -> m a
    failLocal String
    s       = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot split on local variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failHiddenLocal :: String -> m a
    failHiddenLocal String
    s = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot make hidden lambda-bound variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " visible"
      failModuleBound :: String -> m a
    failModuleBound String
    s = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot split on module parameter " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failHiddenModuleBound :: String -> m a
    failHiddenModuleBound String
    s = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot make hidden module parameter " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " visible"
      failLetBound :: String -> m a
    failLetBound String
    s = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> (String -> TypeError) -> String -> m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> TypeError
    GenericError (String -> m a) -> String -> m a
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot split on let-bound variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failInstantiatedVar :: String -> a -> m b
    failInstantiatedVar String
    s a
    v = TypeError -> m b
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m b) -> (Doc -> TypeError) -> Doc -> m b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> TypeError
    GenericDocError (Doc -> m b) -> m Doc -> m b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [m Doc] -> m Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    sep
          [ String -> m Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> m Doc) -> String -> m Doc
    forall a b. (a -> b) -> a -> b
    $ String
    "Cannot split on variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", because it is bound to"
          , a -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM a
    v
          ]
      failCaseLet :: String -> m a
    failCaseLet String
    s     = TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot split on variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    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 (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    f) TCMT IO Defn
    -> (Defn -> TCM (CaseContext, ClauseZipper))
    -> TCM (CaseContext, ClauseZipper)
    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) = ([Clause], [Clause])
    -> Maybe ([Clause], [Clause]) -> ([Clause], [Clause])
    forall a. a -> Maybe a -> a
    fromMaybe ([Clause], [Clause])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe ([Clause], [Clause]) -> ([Clause], [Clause]))
    -> Maybe ([Clause], [Clause]) -> ([Clause], [Clause])
    forall a b. (a -> b) -> a -> b
    $ Int -> [Clause] -> Maybe ([Clause], [Clause])
    forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
    splitExactlyAt Int
    clauseNo [Clause]
    cs
              (Clause
    c,[Clause]
    cs2)    = (Clause, [Clause])
    -> Maybe (Clause, [Clause]) -> (Clause, [Clause])
    forall a. a -> Maybe a -> a
    fromMaybe (Clause, [Clause])
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe (Clause, [Clause]) -> (Clause, [Clause]))
    -> Maybe (Clause, [Clause]) -> (Clause, [Clause])
    forall a b. (a -> b) -> a -> b
    $ [Clause] -> Maybe (Clause, [Clause])
    forall a. [a] -> Maybe (a, [a])
    uncons [Clause]
    ccs2
          (CaseContext, ClauseZipper) -> TCM (CaseContext, ClauseZipper)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CaseContext
    extlam, ([Clause]
    cs1, Clause
    c, [Clause]
    cs2))
        Defn
    d -> do
          String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "impossible" Int
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "getClauseZipperForIP" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Int -> String
    forall a. Show a => a -> String
    show Int
    clauseNo)
              TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TCMT IO Doc
    "received"
            , String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Defn -> String
    forall a. Show a => a -> String
    show Defn
    d)
            ]
          TCM (CaseContext, ClauseZipper)
    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 = Type
    -> Maybe Substitution
    -> SpineClause
    -> (LHSResult -> TCM (Clause, Context, [AsBinding]))
    -> TCM (Clause, Context, [AsBinding])
    forall a.
    Type
    -> Maybe Substitution
    -> SpineClause
    -> (LHSResult -> TCM a)
    -> TCM a
    checkClauseLHS Type
    t Maybe Substitution
    sub SpineClause
    acl ((LHSResult -> TCM (Clause, Context, [AsBinding]))
     -> TCM (Clause, Context, [AsBinding]))
    -> (LHSResult -> TCM (Clause, Context, [AsBinding]))
    -> TCM (Clause, Context, [AsBinding])
    forall a b. (a -> b) -> a -> b
    $ \ LHSResult
    lhs -> do
      let cl :: Clause
    cl = Clause :: Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause{ clauseLHSRange :: Range
    clauseLHSRange    = SpineClause -> Range
    forall a. HasRange a => a -> Range
    getRange SpineClause
    acl
                     , clauseFullRange :: Range
    clauseFullRange   = SpineClause -> Range
    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        = Maybe Term
    forall a. Maybe a
    Nothing -- We don't need the body for make case
                     , clauseType :: Maybe (Arg Type)
    clauseType        = Arg Type -> Maybe (Arg Type)
    forall a. a -> Maybe a
    Just (LHSResult -> Arg Type
    lhsBodyType LHSResult
    lhs)
                     , clauseCatchall :: Bool
    clauseCatchall    = Bool
    False
                     , clauseExact :: Maybe Bool
    clauseExact       = Maybe Bool
    forall a. Maybe a
    Nothing
                     , clauseRecursive :: Maybe Bool
    clauseRecursive   = Maybe Bool
    forall a. Maybe a
    Nothing
                     , clauseUnreachable :: Maybe Bool
    clauseUnreachable = Maybe Bool
    forall a. Maybe a
    Nothing
                     , clauseEllipsis :: ExpandedEllipsis
    clauseEllipsis    = LHSInfo -> ExpandedEllipsis
    lhsEllipsis (LHSInfo -> ExpandedEllipsis) -> LHSInfo -> ExpandedEllipsis
    forall a b. (a -> b) -> a -> b
    $ SpineLHS -> LHSInfo
    A.spLhsInfo (SpineLHS -> LHSInfo) -> SpineLHS -> LHSInfo
    forall a b. (a -> b) -> a -> b
    $ SpineClause -> SpineLHS
    forall lhs. Clause' lhs -> lhs
    A.clauseLHS SpineClause
    acl
                     }
      Context
    cxt <- TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
      let asb :: [AsBinding]
    asb = LHSResult -> [AsBinding]
    lhsAsBindings LHSResult
    lhs
      (Clause, Context, [AsBinding])
    -> TCM (Clause, Context, [AsBinding])
    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 = InteractionId
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    forall (m :: * -> *) a.
    (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
     MonadTrace m) =>
    InteractionId -> m a -> m a
    withInteractionId InteractionId
    hole (TCM (QName, CaseContext, [Clause])
     -> TCM (QName, CaseContext, [Clause]))
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    forall a b. (a -> b) -> a -> b
    $ Lens' Bool TCEnv
    -> (Bool -> Bool)
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    eMakeCase (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (TCM (QName, CaseContext, [Clause])
     -> TCM (QName, CaseContext, [Clause]))
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    forall a b. (a -> b) -> a -> b
    $ do

      -- Jesper, 2018-12-10: print unsolved metas in dot patterns as _
      (TCEnv -> TCEnv)
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envPrintMetasBare :: Bool
    envPrintMetasBare = Bool
    True }) (TCM (QName, CaseContext, [Clause])
     -> TCM (QName, CaseContext, [Clause]))
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    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} <- InteractionId -> TCMT IO InteractionPoint
    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]
    _ -> (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    -> TCMT
         IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f, Int
    i, Type
    t, Maybe Substitution
    sub, SpineClause
    cl, Closure ()
    clo)
        IPClause
    IPNoClause                -> TypeError
    -> TCMT
         IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError
     -> TCMT
          IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ()))
    -> TypeError
    -> TCMT
         IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    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) <-
        Closure ()
    -> (() -> TCM (Clause, Context, [AsBinding]))
    -> TCM (Clause, Context, [AsBinding])
    forall (m :: * -> *) a c b.
    (MonadTCEnv m, ReadTCState m, LensClosure a c) =>
    c -> (a -> m b) -> m b
    enterClosure Closure ()
    clClos ((() -> TCM (Clause, Context, [AsBinding]))
     -> TCM (Clause, Context, [AsBinding]))
    -> (() -> TCM (Clause, Context, [AsBinding]))
    -> TCM (Clause, Context, [AsBinding])
    forall a b. (a -> b) -> a -> b
    $ \ ()
    _ -> Lens' Bool TCEnv
    -> (Bool -> Bool)
    -> TCM (Clause, Context, [AsBinding])
    -> TCM (Clause, Context, [AsBinding])
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' a TCEnv -> (a -> a) -> m b -> m b
    locallyTC Lens' Bool TCEnv
    eMakeCase (Bool -> Bool -> Bool
    forall a b. a -> b -> a
    const Bool
    True) (TCM (Clause, Context, [AsBinding])
     -> TCM (Clause, Context, [AsBinding]))
    -> TCM (Clause, Context, [AsBinding])
    -> TCM (Clause, Context, [AsBinding])
    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) = KillRangeT ([Clause], [Clause])
    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 = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Permutation -> Permutation)
    -> Maybe Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ 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
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "interaction.case" Int
    100 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "splitting clause:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "f       =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc)
    -> (QName -> String) -> QName -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> String
    forall a. Show a => a -> String
    show) QName
    f
          , TCMT IO Doc
    "context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ((TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc)
    -> (Telescope -> String) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> String
    forall a. Show a => a -> String
    show)) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
          , TCMT IO Doc
    "tel     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc)
    -> (Telescope -> String) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> String
    forall a. Show a => a -> String
    show) Telescope
    tel
          , TCMT IO Doc
    "perm    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Permutation -> String
    forall a. Show a => a -> String
    show Permutation
    perm)
          , TCMT IO Doc
    "ps      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (NAPs -> String) -> NAPs -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NAPs -> String
    forall a. Show a => a -> String
    show) NAPs
    ps
          ]
        ]
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "interaction.case" Int
    60 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "splitting clause:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "f       =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty QName
    f
          , TCMT IO Doc
    "context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ((TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
          , TCMT IO Doc
    "tel     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Telescope
    tel
          , TCMT IO Doc
    "perm    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc)
    -> (Permutation -> String) -> Permutation -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Permutation -> String
    forall a. Show a => a -> String
    show) Permutation
    perm
          , TCMT IO Doc
    "ps      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> NAPs -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty NAPs
    ps
          ]
        ]
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "interaction.case" Int
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "splitting clause:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "f       =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    f
          , TCMT IO Doc
    "context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> ((TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope)
          , TCMT IO Doc
    "tel     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM) Telescope
    tel
          , TCMT IO Doc
    "perm    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (Permutation -> String
    forall a. Show a => a -> String
    show Permutation
    perm)
          , TCMT IO Doc
    "ps      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (NAPs -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
    prettyTCMPatternList NAPs
    ps)
          , TCMT IO Doc
    "ell     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (ExpandedEllipsis -> String
    forall a. Show a => a -> String
    show ExpandedEllipsis
    ell)
          , TCMT IO Doc
    "type    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (Maybe (Arg Type) -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Maybe (Arg Type) -> TCMT IO Doc)
    -> Maybe (Arg Type) -> TCMT IO Doc
    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 [String] -> String
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [String]
    vars String -> String -> Bool
    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 (SplitClause -> TCM Clause) -> SplitClause -> TCM Clause
    forall a b. (a -> b) -> a -> b
    $ Clause -> SplitClause
    clauseToSplitClause Clause
    clause
        (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [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 [String] -> Bool
    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 = Bool
    -> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> TCMT IO [SplitClause]
    -> TCMT IO [SplitClause]
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen (CaseContext -> Bool
    forall a. Maybe a -> Bool
    isJust CaseContext
    casectxt) ((TCMT IO [SplitClause] -> TCMT IO [SplitClause])
     -> TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> TCMT IO [SplitClause]
    -> TCMT IO [SplitClause]
    forall a b. (a -> b) -> a -> b
    $
              (PragmaOptions -> PragmaOptions)
    -> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
    forall (m :: * -> *) a.
    ReadTCState m =>
    (PragmaOptions -> PragmaOptions) -> m a -> m a
    withPragmaOptions ((PragmaOptions -> PragmaOptions)
     -> TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> (PragmaOptions -> PragmaOptions)
    -> TCMT IO [SplitClause]
    -> TCMT IO [SplitClause]
    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 (SplitClause -> TCM (Telescope, SplitClause))
    -> SplitClause -> TCM (Telescope, SplitClause)
    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 Telescope -> Bool
    forall a. Null a => a -> Bool
    null Telescope
    piTel then Bool -> TCMT IO Bool
    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 (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
          Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    imp Bool -> Bool -> Bool
    || (Dom (String, Type) -> Bool) -> [Dom (String, Type)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Dom (String, Type) -> Bool
    forall a. LensHiding a => a -> Bool
    visible (Telescope -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    piTel)
        [SplitClause]
    scs <- if Bool
    newPats then [SplitClause] -> TCMT IO [SplitClause]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SplitClause
    sc] else TCMT IO [SplitClause] -> TCMT IO [SplitClause]
    postProjInExtLam (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
    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 = (Arg (Named_ DeBruijnPattern) -> Maybe (NamedArg DBPatVar))
    -> NAPs -> [NamedArg DBPatVar]
    forall a b. (a -> Maybe b) -> [a] -> Prefix b
    takeWhileJust Arg (Named_ DeBruijnPattern) -> Maybe (NamedArg DBPatVar)
    forall {name} {a}.
    Arg (Named name (Pattern' a)) -> Maybe (Arg (Named name a))
    isVarP (NAPs -> [NamedArg DBPatVar]) -> NAPs -> [NamedArg DBPatVar]
    forall a b. (a -> b) -> a -> b
    $ NAPs -> NAPs
    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))) = Arg (Named name a) -> Maybe (Arg (Named name a))
    forall a. a -> Maybe a
    Just (Arg (Named name a) -> Maybe (Arg (Named name a)))
    -> Arg (Named name a) -> Maybe (Arg (Named name a))
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Named name a -> Arg (Named name a)
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Named name a -> Arg (Named name a))
    -> Named name a -> Arg (Named name a)
    forall a b. (a -> b) -> a -> b
    $ Maybe name -> a -> Named name a
    forall name a. Maybe name -> a -> Named name a
    Named Maybe name
    n a
    x
                  isVarP Arg (Named name (Pattern' a))
    _ = Maybe (Arg (Named name a))
    forall a. Maybe a
    Nothing
              -- If all are already coming from the user, there is really nothing todo!
              Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ((NamedArg DBPatVar -> Bool) -> [NamedArg DBPatVar] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((Origin
    UserWritten Origin -> Origin -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (Origin -> Bool)
    -> (NamedArg DBPatVar -> Origin) -> NamedArg DBPatVar -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DBPatVar -> Origin
    forall a. LensOrigin a => a -> Origin
    getOrigin) [NamedArg DBPatVar]
    trailingPatVars) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
                TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ SplitError -> TypeError
    SplitError SplitError
    err
              -- Otherwise, we make these user-written
              let xs :: [Int]
    xs = (NamedArg DBPatVar -> Int) -> [NamedArg DBPatVar] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map (DBPatVar -> Int
    dbPatVarIndex (DBPatVar -> Int)
    -> (NamedArg DBPatVar -> DBPatVar) -> NamedArg DBPatVar -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg DBPatVar -> DBPatVar
    forall a. NamedArg a -> a
    namedArg) [NamedArg DBPatVar]
    trailingPatVars
              [SplitClause] -> TCMT IO [SplitClause]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [[Int] -> SplitClause -> SplitClause
    makePatternVarsVisible [Int]
    xs SplitClause
    sc]

            Right [SplitClause]
    cov -> TCMT IO Bool
    -> TCMT IO [SplitClause]
    -> TCMT IO [SplitClause]
    -> TCMT IO [SplitClause]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifNotM (PragmaOptions -> Bool
    optCopatterns (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions) TCMT IO [SplitClause]
    forall {a}. TCMT IO a
    failNoCop (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
    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
              [SplitClause] -> TCMT IO [SplitClause]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SplitClause]
    cov
        IPClause -> TCMT IO ()
    checkClauseIsClean IPClause
    ipCl
        (QName
    f, CaseContext
    casectxt,) ([Clause] -> (QName, CaseContext, [Clause]))
    -> TCMT IO [Clause] -> TCM (QName, CaseContext, [Clause])
    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 [SplitClause] -> Bool
    forall a. Null a => a -> Bool
    null [SplitClause]
    scs then
            [Clause] -> TCMT IO [Clause]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ SpineClause -> Clause
    forall a b. LHSToSpine a b => b -> a
    A.spineToLhs (SpineClause -> Clause) -> SpineClause -> Clause
    forall a b. (a -> b) -> a -> b
    $ SpineClause
    absCl{ clauseRHS :: RHS
    A.clauseRHS = RHS -> RHS
    makeRHSEmptyRecord RHS
    rhs } ]
          else (SplitClause -> TCM Clause) -> [SplitClause] -> TCMT IO [Clause]
    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
        String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.case" Int
    30 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "parsedVariables: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [((Int, NameInScope), String)] -> String
    forall a. Show a => a -> String
    show ([(Int, NameInScope)] -> [String] -> [((Int, NameInScope), String)]
    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) = [Either Int Int] -> ([Int], [Int])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either Int Int] -> ([Int], [Int]))
    -> [Either Int Int] -> ([Int], [Int])
    forall a b. (a -> b) -> a -> b
    $ [((Int, NameInScope), String)]
    -> (((Int, NameInScope), String) -> Either Int Int)
    -> [Either Int Int]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for ([(Int, NameInScope)] -> [String] -> [((Int, NameInScope), String)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [(Int, NameInScope)]
    xs [String]
    vars) ((((Int, NameInScope), String) -> Either Int Int)
     -> [Either Int Int])
    -> (((Int, NameInScope), String) -> Either Int Int)
    -> [Either Int Int]
    forall a b. (a -> b) -> a -> b
    $ \ ((Int
    x,NameInScope
    nis), String
    s) ->
              if (NameInScope
    nis NameInScope -> NameInScope -> Bool
    forall a. Eq a => a -> a -> Bool
    == NameInScope
    C.NotInScope) then Int -> Either Int Int
    forall a b. a -> Either a b
    Left Int
    x else Int -> Either Int Int
    forall a b. b -> Either a b
    Right Int
    x
        let sc :: SplitClause
    sc = [Int] -> SplitClause -> SplitClause
    makePatternVarsVisible [Int]
    toShow (SplitClause -> SplitClause) -> SplitClause -> SplitClause
    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
        String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.case" Int
    70 (String -> TCMT IO ()) -> String -> TCMT IO ()
    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 = (Int -> Name) -> [Int] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Int
    i -> (Name, Type) -> Name
    forall a b. (a, b) -> a
    fst ((Name, Type) -> Name) -> (Name, Type) -> Name
    forall a b. (a -> b) -> a -> b
    $ Dom' Term (Name, Type) -> (Name, Type)
    forall t e. Dom' t e -> e
    unDom (Dom' Term (Name, Type) -> (Name, Type))
    -> Dom' Term (Name, Type) -> (Name, Type)
    forall a b. (a -> b) -> a -> b
    $ Context
    clauseCxt Context -> Int -> Dom' Term (Name, Type)
    forall a. [a] -> Int -> a
    !! Int
    i) [Int]
    toSplit
        Bool
    shouldExpandEllipsis <- Bool -> TCMT IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Int] -> Bool
    forall a. Null a => a -> Bool
    null [Int]
    toShow) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    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 <- (Clause -> TCMT IO Bool) -> [Clause] -> TCMT IO [Clause]
    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)) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M`
                                (Bool -> Bool
    not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
    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 <- ((SplitClause, Bool) -> TCMT IO Bool)
    -> [(SplitClause, Bool)] -> TCM [(SplitClause, Bool)]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (Bool -> Bool
    not (Bool -> Bool)
    -> ((SplitClause, Bool) -> TCMT IO Bool)
    -> (SplitClause, Bool)
    -> TCMT IO Bool
    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 [Clause] -> [Clause] -> [Clause]
    forall a. [a] -> [a] -> [a]
    ++ [Clause]
    fcs) (SplitClause -> TCMT IO Bool)
    -> ((SplitClause, Bool) -> SplitClause)
    -> (SplitClause, Bool)
    -> TCMT IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SplitClause, Bool) -> SplitClause
    forall a b. (a, b) -> a
    fst) [(SplitClause, Bool)]
    scs
        String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.case" Int
    70 (String -> TCMT IO ()) -> String -> TCMT IO ()
    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 <- [Maybe Clause] -> [Clause]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe Clause] -> [Clause])
    -> TCMT IO [Maybe Clause] -> TCMT IO [Clause]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
         [(SplitClause, Bool)]
    -> ((SplitClause, Bool) -> TCMT IO (Maybe Clause))
    -> TCMT IO [Maybe Clause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(SplitClause, Bool)]
    scs (((SplitClause, Bool) -> TCMT IO (Maybe Clause))
     -> TCMT IO [Maybe Clause])
    -> ((SplitClause, Bool) -> TCMT IO (Maybe Clause))
    -> TCMT IO [Maybe Clause]
    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 Clause -> Maybe Clause
    forall a. a -> Maybe a
    Just (Clause -> Maybe Clause) -> TCM Clause -> TCMT IO (Maybe Clause)
    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
            TCMT IO Bool
    -> TCMT IO (Maybe Clause)
    -> TCMT IO (Maybe Clause)
    -> TCMT IO (Maybe Clause)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TCMT IO Bool -> TCMT IO Bool
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Bool
    isEmptyTel (SplitClause -> Telescope
    scTel SplitClause
    sc))
              {- then -} (Maybe Clause -> TCMT IO (Maybe Clause)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Clause
    forall a. Maybe a
    Nothing)
              {- else -} (Clause -> Maybe Clause
    forall a. a -> Maybe a
    Just (Clause -> Maybe Clause) -> TCM Clause -> TCMT IO (Maybe Clause)
    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)
        String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "interaction.case" Int
    70 (String -> TCMT IO ()) -> String -> TCMT IO ()
    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 ([Clause] -> Bool
    forall a. Null a => a -> Bool
    null [Clause]
    cs) then [Clause] -> TCMT IO [Clause]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Clause]
    cs
              else ((SplitClause, Bool) -> TCM Clause)
    -> [(SplitClause, Bool)] -> TCMT IO [Clause]
    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 -> TCM Clause)
    -> ((SplitClause, Bool) -> SplitClause)
    -> (SplitClause, Bool)
    -> TCM Clause
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SplitClause, Bool) -> SplitClause
    forall a b. (a, b) -> a
    fst) [(SplitClause, Bool)]
    scs

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

      where
      failNoCop :: TCMT IO a
    failNoCop = TypeError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    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 = [(SplitClause, Bool)] -> TCM [(SplitClause, Bool)]
    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 <- TCMT IO (Either SplitError (Either SplitClause Covering))
    -> TCMT IO (Either SplitError (Either SplitClause Covering))
    forall (m :: * -> *) a.
    (MonadTCEnv m, HasOptions m, MonadDebug m) =>
    m a -> m a
    dontAssignMetas (TCMT IO (Either SplitError (Either SplitClause Covering))
     -> TCMT IO (Either SplitError (Either SplitClause Covering)))
    -> TCMT IO (Either SplitError (Either SplitClause Covering))
    -> TCMT IO (Either SplitError (Either SplitClause Covering))
    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          -> TypeError -> TCM [(SplitClause, Bool)]
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM [(SplitClause, Bool)])
    -> TypeError -> TCM [(SplitClause, Bool)]
    forall a b. (a -> b) -> a -> b
    $ SplitError -> TypeError
    SplitError SplitError
    err
          Right (Left SplitClause
    cl)   -> [(SplitClause, Bool)] -> TCM [(SplitClause, Bool)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(SplitClause
    cl,Bool
    True)]
          Right (Right Covering
    cov) -> [[(SplitClause, Bool)]] -> [(SplitClause, Bool)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[(SplitClause, Bool)]] -> [(SplitClause, Bool)])
    -> TCMT IO [[(SplitClause, Bool)]] -> TCM [(SplitClause, Bool)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
                [SplitClause]
    -> (SplitClause -> TCM [(SplitClause, Bool)])
    -> TCMT IO [[(SplitClause, Bool)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Covering -> [SplitClause]
    splitClauses Covering
    cov) ((SplitClause -> TCM [(SplitClause, Bool)])
     -> TCMT IO [[(SplitClause, Bool)]])
    -> (SplitClause -> TCM [(SplitClause, Bool)])
    -> TCMT IO [[(SplitClause, Bool)]]
    forall a b. (a -> b) -> a -> b
    $ \ SplitClause
    cl ->
                  QName -> [Int] -> SplitClause -> TCM [(SplitClause, Bool)]
    split QName
    f ((Int -> Maybe Int) -> [Int] -> [Int]
    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 SplitPSubstitution -> Term -> Term
    forall a. TermSubst a => SplitPSubstitution -> a -> a
    applySplitPSubst (SplitClause -> SplitPSubstitution
    scSubst SplitClause
    c) (Int -> Term
    var Int
    x) of
        Var Int
    y [] -> Int -> Maybe Int
    forall a. a -> Maybe a
    Just Int
    y
        Term
    _        -> Maybe Int
    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 <- (InteractionPoint -> Bool)
    -> [InteractionPoint] -> [InteractionPoint]
    forall a. (a -> Bool) -> [a] -> [a]
    filter InteractionPoint -> Bool
    ipSolved ([InteractionPoint] -> [InteractionPoint])
    -> (BiMap InteractionId InteractionPoint -> [InteractionPoint])
    -> BiMap InteractionId InteractionPoint
    -> [InteractionPoint]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BiMap InteractionId InteractionPoint -> [InteractionPoint]
    forall k v. BiMap k v -> [v]
    BiMap.elems (BiMap InteractionId InteractionPoint -> [InteractionPoint])
    -> TCMT IO (BiMap InteractionId InteractionPoint)
    -> TCMT IO [InteractionPoint]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' (BiMap InteractionId InteractionPoint) TCState
    -> TCMT IO (BiMap InteractionId InteractionPoint)
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' (BiMap InteractionId InteractionPoint) TCState
    stInteractionPoints
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ((InteractionPoint -> Bool) -> [InteractionPoint] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    List.any ((IPClause -> IPClause -> Bool
    forall a. Eq a => a -> a -> Bool
    == IPClause
    ipCl) (IPClause -> Bool)
    -> (InteractionPoint -> IPClause) -> InteractionPoint -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InteractionPoint -> IPClause
    ipClause) [InteractionPoint]
    sips) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    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 = (NamedArg SplitPattern -> NamedArg SplitPattern)
    -> [NamedArg SplitPattern] -> [NamedArg SplitPattern]
    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 Int -> [Int] -> Bool
    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@
          ArgInfo -> Named NamedName SplitPattern -> NamedArg SplitPattern
    forall e. ArgInfo -> e -> Arg e
    Arg (Origin -> ArgInfo -> ArgInfo
    forall a. LensOrigin a => Origin -> a -> a
    setOrigin Origin
    CaseSplit ArgInfo
    ai) (Named NamedName SplitPattern -> NamedArg SplitPattern)
    -> Named NamedName SplitPattern -> NamedArg SplitPattern
    forall a b. (a -> b) -> a -> b
    $ Maybe NamedName -> SplitPattern -> Named NamedName SplitPattern
    forall name a. Maybe name -> a -> Named name a
    Named Maybe NamedName
    n (SplitPattern -> Named NamedName SplitPattern)
    -> SplitPattern -> Named NamedName SplitPattern
    forall a b. (a -> b) -> a -> b
    $ PatternInfo -> SplitPatVar -> SplitPattern
    forall x. PatternInfo -> x -> Pattern' x
    VarP (PatOrigin -> [Name] -> PatternInfo
    PatternInfo PatOrigin
    PatOSplit []) (SplitPatVar -> SplitPattern) -> SplitPatVar -> SplitPattern
    forall a b. (a -> b) -> a -> b
    $ 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{}            -> RHS :: Expr -> Maybe Expr -> RHS
    A.RHS{ rhsExpr :: Expr
    rhsExpr = ExprInfo -> RecordAssigns -> Expr
    A.Rec ExprInfo
    forall a. Null a => a
    empty RecordAssigns
    forall a. Null a => a
    empty, rhsConcrete :: Maybe Expr
    rhsConcrete = Maybe Expr
    forall a. Maybe a
    Nothing }
      rhs :: RHS
    rhs@A.RewriteRHS{} -> RHS
    rhs{ rewriteRHS :: RHS
    A.rewriteRHS = RHS -> RHS
    makeRHSEmptyRecord (RHS -> RHS) -> RHS -> RHS
    forall a b. (a -> b) -> a -> b
    $ RHS -> RHS
    A.rewriteRHS RHS
    rhs }
      RHS
    A.AbsurdRHS        -> RHS
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      A.WithRHS{}        -> RHS
    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
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "interaction.case" Int
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ TCMT IO Doc
    "Interaction.MakeCase.makeAbsurdClause: split clause:"
        , Int -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
    nest Int
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do (TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc)
    -> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
    getContextTelescope
          , TCMT IO Doc
    "tel     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    tel
          , TCMT IO Doc
    "ps      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> do TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ NAPs -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
    prettyTCMPatternList NAPs
    ps -- P.sep <$> prettyTCMPatterns ps
          , TCMT IO Doc
    "ell     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (ExpandedEllipsis -> String
    forall a. Show a => a -> String
    show ExpandedEllipsis
    ell)
          ]
        ]
      ModuleName -> TCM Clause -> TCM Clause
    forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
    withCurrentModule (QName -> ModuleName
    qnameModule QName
    f) (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
    forall a b. (a -> b) -> a -> b
    $ do
        -- 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
        let c :: Clause
    c = Range
    -> Range
    -> Telescope
    -> NAPs
    -> Maybe Term
    -> Maybe (Arg Type)
    -> Bool
    -> Maybe Bool
    -> Maybe Bool
    -> Maybe Bool
    -> ExpandedEllipsis
    -> Clause
    Clause Range
    forall a. Range' a
    noRange Range
    forall a. Range' a
    noRange Telescope
    tel NAPs
    ps Maybe Term
    forall a. Maybe a
    Nothing (Dom' Term Type -> Arg Type
    forall t a. Dom' t a -> Arg a
    argFromDom (Dom' Term Type -> Arg Type)
    -> Maybe (Dom' Term Type) -> Maybe (Arg Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe (Dom' Term Type)
    t) Bool
    False Maybe Bool
    forall a. Maybe a
    Nothing Maybe Bool
    forall a. Maybe a
    Nothing Maybe Bool
    forall a. Maybe a
    Nothing ExpandedEllipsis
    ell
        let ps :: NAPs
    ps = Clause -> NAPs
    namedClausePats Clause
    c
        TCM Clause -> TCM Clause
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
    forall a b. (a -> b) -> a -> b
    $ QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
    forall i (m :: * -> *).
    (Reify i, MonadReify m) =>
    i -> m (ReifiesTo i)
    reify (QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause)))
    -> QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
    forall a b. (a -> b) -> a -> b
    $ QName -> Clause -> QNamed Clause
    forall a. QName -> a -> QNamed a
    QNamed QName
    f (Clause -> QNamed Clause) -> Clause -> QNamed Clause
    forall a b. (a -> b) -> a -> b
    $ Clause
    c { namedClausePats :: NAPs
    namedClausePats = NAPs
    ps }

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