    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.Interaction.MakeCase where

    import Prelude hiding ((!!), null)

    import Data.Either
    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 qualified Agda.Syntax.Common.Pretty as P
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Pattern
    import Agda.Syntax.Parser.Helpers ( mkValidName )
    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.Rules.Def (checkClauseLHS)
    import Agda.TypeChecking.Rules.LHS (LHSResult(..))
    import Agda.TypeChecking.Rules.LHS.Problem (AsBinding(..))

    import Agda.Interaction.Options

    import qualified Agda.Utils.BiMap as BiMap
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Lens   (set)
    import Agda.Utils.List
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Utils.WithDefault (lensKeepDefault)

    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.
      mId <- InteractionId -> TCMT IO MetaId
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m MetaId
    lookupInteractionId InteractionId
    ii
      updateMetaVarRange mId rng
      mi  <- getMetaInfo <$> lookupLocalMeta mId
      enterClosure mi $ \ 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
        m   <- TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
        tel <- lookupSection m
        vcat
         [ "parseVariables:"
         , "current module  =" <+> prettyTCM m
         , "current section =" <+> inTopContext (prettyTCM tel)
         , "clause context  =" <+> prettyTCM (PrettyContext 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.
      n  <- TCMT IO Int
    forall (m :: * -> *). MonadTCEnv m => m Int
    getContextSize
      xs <- forM (downFrom n) $ \ 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
    forall a. Doc a -> 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
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM (Int -> Term
    var Int
    i)) TCMT IO (Name -> (String, Name))
    -> TCMT IO Name -> TCMT IO (String, Name)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> TCMT IO Name
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Name
    nameOfBV Int
    i

      -- Step 1: From strings to abstract names
      abstractNames :: [(A.Name, Maybe BindingSource)] <- forM ss $ \String
    s -> do

        cname <- (String -> TCMT IO QName)
    -> (Name -> TCMT IO QName) -> Either String Name -> TCMT IO QName
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either String -> TCMT IO QName
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failParseError (QName -> TCMT IO QName
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName -> TCMT IO QName)
    -> (Name -> QName) -> Name -> TCMT IO QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> QName
    C.QName) (Either String Name -> TCMT IO QName)
    -> Either String Name -> TCMT IO QName
    forall a b. (a -> b) -> a -> b
    $ Bool -> Range -> String -> Either String Name
    mkValidName Bool
    False Range
    r 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.
        resolveName' (exceptKindsOfNames [GeneralizeName]) Nothing cname >>= \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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    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 = Context -> [Name]
    contextNames' 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] -> [(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 Dom' Term Type
    _) -> (Name
    name,Term
    v)) [AsBinding]
    asb

      -- We cannot split on module parameters or make them visible
      params <- moduleParamsToApply $ qnameModule f
      let 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

      forM (zip ss abstractNames) $ \(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 []), PatternBound Hiding
    _) -> (Int, NameInScope) -> TCMT IO (Int, NameInScope)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int
    i, NameInScope
    C.InScope)
          -- Case 1b: the variable has been refined.
          (Just Term
    v         , PatternBound Hiding
    _) -> String -> Term -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a} {b}.
    (MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
     MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
     IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
    String -> a -> m b
    failInstantiatedVar String
    s Term
    v
          -- Case 1c: the variable is bound locally (e.g. a record let)
          (Maybe Term
    Nothing        , PatternBound Hiding
    _) -> 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
          (Maybe Term
    _              , BindingSource
    WithBound   ) -> String -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failWithBound String
    s
          -- Case 1h: macro-bound variable (interactive command impossible in macro context)
          (Maybe Term
    _              , BindingSource
    MacroBound   ) -> 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 a. a -> TCMT IO a
    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, MonadFresh NameId m,
     MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
     IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
    String -> a -> m b
    failInstantiatedVar String
    s Term
    v
          -- Case 2c: there is no variable with that name. Since it was in
          -- scope for the interaction meta, the only possibility is that
          -- it is a hidden lambda-bound variable.
          Maybe (Name, Term)
    Nothing -> String -> TCMT IO (Int, NameInScope)
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    failHiddenLocal String
    s

      where

      failParseError :: String -> m a
    failParseError String
    s  = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text String
    s
      failNotVar :: String -> m a
    failNotVar String
    s      = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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     = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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   = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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       = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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 = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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 = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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 = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    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 = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $
        String
    "Cannot split on let-bound variable " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s
      failWithBound :: String -> m a
    failWithBound String
    s = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> 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 an equality proof bound by a with-abstraction"
      failInstantiatedVar :: String -> a -> m b
    failInstantiatedVar String
    s a
    v = InteractionError -> m b
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m b)
    -> (Doc -> InteractionError) -> Doc -> m b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> InteractionError
    CaseSplitError (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
    forall (m :: * -> *). MonadPretty m => a -> m Doc
    prettyTCM a
    v
          ]
      failCaseLet :: String -> m a
    failCaseLet String
    s     = InteractionError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> m a) -> InteractionError -> m a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $ String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> String -> 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 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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        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 a. a -> TCMT IO a
    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
    forall (m :: * -> *). MonadPretty m => QName -> 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 { 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 :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
                      , 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
                      , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = WhereDeclarations -> Maybe ModuleName
    A.whereModule (WhereDeclarations -> Maybe ModuleName)
    -> WhereDeclarations -> Maybe ModuleName
    forall a b. (a -> b) -> a -> b
    $ SpineClause -> WhereDeclarations
    forall lhs. Clause' lhs -> WhereDeclarations
    A.clauseWhereDecls SpineClause
    acl
                      }
      cxt <- TCMT IO Context
    forall (m :: * -> *). MonadTCEnv m => m Context
    getContext
      let asb = LHSResult -> [AsBinding]
    lhsAsBindings LHSResult
    lhs
      return (cl, cxt, 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.
    (MonadDebug 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' TCEnv Bool
    -> (Bool -> Bool)
    -> TCM (QName, CaseContext, [Clause])
    -> TCM (QName, CaseContext, [Clause])
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    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 a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
    forall (m :: * -> *) a.
    MonadTCEnv m =>
    (TCEnv -> TCEnv) -> m a -> m a
    localTC (\ TCEnv
    e -> TCEnv
    e { envPrintMetasBare = 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 = mm, ipClause = ipCl} <- InteractionId -> TCMT IO InteractionPoint
    forall (m :: * -> *).
    (ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
    InteractionId -> m InteractionPoint
    lookupInteractionPoint InteractionId
    hole
      (f, clauseNo, clTy, clWithSub, absCl@A.Clause{ clauseRHS = rhs }, clClos) <- case ipCl of
        IPClause QName
    f Int
    i Type
    t Maybe Substitution
    sub SpineClause
    cl Closure ()
    clo -> (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    -> TCMT
         IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
    f, Int
    i, Type
    t, Maybe Substitution
    sub, SpineClause
    cl, Closure ()
    clo)
        IPClause
    IPNoClause                -> InteractionError
    -> TCMT
         IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError
     -> TCMT
          IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ()))
    -> InteractionError
    -> TCMT
         IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $
          Doc
    "Cannot split here, as we are not in a function definition"
      (casectxt, (prevClauses0, _clause, follClauses0)) <- getClauseZipperForIP f 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, clauseCxt, clauseAsBindings) <-
        enterClosure clClos $ \ ()
    _ -> Lens' TCEnv Bool
    -> (Bool -> Bool)
    -> TCM (Clause, Context, [AsBinding])
    -> TCM (Clause, Context, [AsBinding])
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
    Lens' TCEnv Bool
    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 (prevClauses, follClauses) = killRange (prevClauses0, 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 -> 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  = Clause -> Telescope
    clauseTel  Clause
    clause
          ps   = Clause -> NAPs
    namedClausePats Clause
    clause
          ell  = Clause -> ExpandedEllipsis
    clauseEllipsis Clause
    clause
      reportSDoc "interaction.case" 100 $ vcat
        [ "splitting clause:"
        , nest 2 $ vcat
          [ "f       =" <+> (text . show) f
          , "context =" <+> ((inTopContext . (text . show)) =<< getContextTelescope)
          , "tel     =" <+> (text . show) tel
          , "perm    =" <+> text (show perm)
          , "ps      =" <+> (text . show) ps
          ]
        ]
      reportSDoc "interaction.case" 60 $ vcat
        [ "splitting clause:"
        , nest 2 $ vcat
          [ "f       =" <+> pretty f
          , "context =" <+> ((inTopContext . pretty) =<< getContextTelescope)
          , "tel     =" <+> pretty tel
          , "perm    =" <+> (text . show) perm
          , "ps      =" <+> pretty ps
          ]
        ]
      reportSDoc "interaction.case" 10 $ vcat
        [ "splitting clause:"
        , nest 2 $ vcat
          [ "f       =" <+> prettyTCM f
          , "context =" <+> ((inTopContext . prettyTCM) =<< getContextTelescope)
          , "tel     =" <+> (inTopContext . prettyTCM) tel
          , "perm    =" <+> text (show perm)
          , "ps      =" <+> addContext tel (prettyTCMPatternList ps)
          , "ell     =" <+> text (show ell)
          , "type    =" <+> addContext tel (prettyTCM $ clauseType clause)
          ]
        ]

      -- Check split variables.

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

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

      if concat vars == "." then do
        cl <- makeAbstractClause f rhs NoEllipsis $ clauseToSplitClause clause
        return (f, casectxt, [cl])

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

      else if null 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 = Bool
    -> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
    -> TCMT IO [SplitClause]
    -> TCMT IO [SplitClause]
    forall b a. IsBool b => b -> (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
    $ Lens' PragmaOptions Bool -> LensSet PragmaOptions Bool
    forall o i. Lens' o i -> LensSet o i
    set ((WithDefault 'True -> f (WithDefault 'True))
    -> PragmaOptions -> f PragmaOptions
    forall (f :: * -> *).
    Functor f =>
    (WithDefault 'True -> f (WithDefault 'True))
    -> PragmaOptions -> f PragmaOptions
    lensOptPostfixProjections ((WithDefault 'True -> f (WithDefault 'True))
     -> PragmaOptions -> f PragmaOptions)
    -> ((Bool -> f Bool) -> WithDefault 'True -> f (WithDefault 'True))
    -> (Bool -> f Bool)
    -> PragmaOptions
    -> f PragmaOptions
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Bool -> f Bool) -> WithDefault 'True -> f (WithDefault 'True)
    forall a (b :: Bool).
    (Boolean a, Eq a, KnownBool b) =>
    Lens' (WithDefault' a b) a
    Lens' (WithDefault 'True) Bool
    lensKeepDefault) Bool
    True
        (piTel, sc) <- insertTrailingArgs False $ clauseToSplitClause 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).
        newPats <- if null piTel then return False else do
          -- If there were any pattern introduce, they will only have effect
          -- if any of them is shown by the printer
          imp <- optShowImplicit <$> pragmaOptions
          return $ imp || any visible (telToList piTel)
        scs <- if newPats then return [sc] else postProjInExtLam $ do
          res <- splitResult f sc
          case 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 a. a -> TCMT IO a
    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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SplitClause]
    cov
        checkClauseIsClean ipCl
        (f, casectxt,) <$> do
          -- Andreas, 2020-05-18, issue #4536
          -- When result splitting yields no clauses, replace rhs by @record{}@.
          if null scs then
            return [ A.spineToLhs $ absCl{ A.clauseRHS = makeRHSEmptyRecord rhs } ]
          else mapM (makeAbstractClause f rhs ell) scs
      else do
        -- split on variables
        xs <- parseVariables f clauseCxt clauseAsBindings hole rng vars
        reportSLn "interaction.case" 30 $ "parsedVariables: " ++ show (zip xs vars)
        -- Variables that are not in scope yet are brought into scope (@toShow@)
        -- The other variables are split on (@toSplit@).
        let (toShow, toSplit) = partitionEithers $ for (zip xs vars) $ \ ((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 = [Int] -> SplitClause -> SplitClause
    makePatternVarsVisible [Int]
    toShow (SplitClause -> SplitClause) -> SplitClause -> SplitClause
    forall a b. (a -> b) -> a -> b
    $ Clause -> SplitClause
    clauseToSplitClause Clause
    clause
        scs <- split f toSplit sc
        reportSLn "interaction.case" 70 $ "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 = (Int -> Name) -> [Int] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (\Int
    i -> ContextEntry -> Name
    ctxEntryName (ContextEntry -> Name) -> ContextEntry -> Name
    forall a b. (a -> b) -> a -> b
    $ Context
    clauseCxt Context -> Int -> ContextEntry
    forall a. HasCallStack => [a] -> Int -> a
    !! Int
    i) [Int]
    toSplit
        shouldExpandEllipsis <- return (not $ null toShow) `or2M` anyEllipsisVar f absCl splitNames
        let 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 = Clause -> SplitClause
    clauseToSplitClause Clause
    clause
        fcs <- 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))
                       follClauses
        scs <- filterM (not <.> isCovered f (prevClauses ++ fcs) . fst) scs
        reportSLn "interaction.case" 70 $ "makeCase: survived filtering out already covered clauses"
        -- 2. filter out trivially impossible clauses not asked for by the user
        cs <- catMaybes <$> do
         forM scs $ \ (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 a. TCM a -> TCM a
    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
    $ (PragmaOptions -> Bool
    optInferAbsurdClauses (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 Bool -> TCMT IO Bool -> TCMT IO Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    `and2M` Telescope -> TCMT IO Bool
    forall (tcm :: * -> *). MonadTCM tcm => Telescope -> tcm Bool
    isEmptyTel (SplitClause -> Telescope
    scTel SplitClause
    sc))
              {- then -} (Maybe Clause -> TCMT IO (Maybe Clause)
    forall a. a -> TCMT IO a
    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)
        reportSLn "interaction.case" 70 $ "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!)
        cs <- if not (null cs) then pure cs
              else mapM (makeAbstractClause f rhs ell' . fst) scs

        reportSDoc "interaction.case" 65 $ vcat
          [ "split result:"
          , nest 2 $ vcat $ map prettyA cs
          ]
        checkClauseIsClean ipCl
        return (f, casectxt, cs)

      where
      failNoCop :: TCMT IO a
    failNoCop = InteractionError -> TCMT IO a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    InteractionError -> m a
    interactionError (InteractionError -> TCMT IO a) -> InteractionError -> TCMT IO a
    forall a b. (a -> b) -> a -> b
    $ Doc -> InteractionError
    CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
    forall a b. (a -> b) -> a -> b
    $
        Doc
    "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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(SplitClause
    clause,Bool
    False)]
      split QName
    f (Int
    var : [Int]
    vars) SplitClause
    clause = do
        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 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 a. a -> TCMT IO a
    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
        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' TCState (BiMap InteractionId InteractionPoint)
    -> TCMT IO (BiMap InteractionId InteractionPoint)
    forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
    useTC (BiMap InteractionId InteractionPoint
     -> f (BiMap InteractionId InteractionPoint))
    -> TCState -> f TCState
    Lens' TCState (BiMap InteractionId InteractionPoint)
    stInteractionPoints
        when (List.any ((== ipCl) . ipClause) sips) $
          interactionError $ CaseSplitError $ "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 = mapNamedArgPattern mkVis 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 a. Eq a => a -> [a] -> 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{}            -> A.RHS{ rhsExpr :: Expr
    rhsExpr = KwRange -> ExprInfo -> RecordAssigns -> Expr
    A.Rec KwRange
    forall a. Null a => a
    empty 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{ A.rewriteRHS = makeRHSEmptyRecord $ A.rewriteRHS 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
    forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
    prettyTCM) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO Telescope
    forall (m :: * -> *). 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
    forall (m :: * -> *). MonadPretty m => Telescope -> 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
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Telescope -> m a -> m a
    addContext Telescope
    tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ NAPs -> TCMT IO Doc
    forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
    prettyTCMPatternList NAPs
    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
    $
        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)
    forall (m :: * -> *).
    MonadReify m =>
    QNamed Clause -> m (ReifiesTo (QNamed Clause))
    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
          { clauseLHSRange :: Range
    clauseLHSRange  = Range
    forall a. Range' a
    noRange
          , clauseFullRange :: Range
    clauseFullRange = Range
    forall a. Range' a
    noRange
          , clauseTel :: Telescope
    clauseTel       = Telescope
    tel
          , namedClausePats :: NAPs
    namedClausePats = NAPs
    ps
          , clauseBody :: Maybe Term
    clauseBody      = Maybe Term
    forall a. Maybe a
    Nothing
          , clauseType :: Maybe (Arg Type)
    clauseType      = 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
          , clauseCatchall :: Catchall
    clauseCatchall    = Catchall
    forall a. Null a => a
    empty
          , 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    = ExpandedEllipsis
    ell
          , clauseWhereModule :: Maybe ModuleName
    clauseWhereModule = Maybe ModuleName
    forall a. Maybe a
    Nothing
          }

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

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

      lhs <- 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
      reportSDoc "interaction.case" 60 $ "reified lhs: " <+> prettyA lhs
      return $ A.Clause lhs [] rhs A.noWhereDecls empty
      -- 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 a. Eq a => a -> [a] -> 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 a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        ExpandedEllipsis Range
    _ Int
    k -> do
          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, 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'
          reportSDoc "interaction.case.ellipsis" 40 $ vcat
            [ "should we expand the ellipsis?"
            , nest 2 $ "xs           =" <+> prettyList_ (map prettyA xs)
            , nest 2 $ "ellipsisPats =" <+> prettyList_ (map prettyA ellipsisPats)
            ]
          return $ getAny $ A.foldrAPattern anyVar ellipsisPats