{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.Interaction.MakeCase where

import Prelude hiding ((!!), null)

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 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.Common.Pretty ( prettyShow )
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.SplitPattern ( 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.Three
import Agda.Utils.WithDefault (lensKeepDefault)

import Agda.Utils.Impossible

type CaseContext = Maybe ExtLamInfo

-- | For the names the user enters for case-splitting, there can be different actions
--   depending on what the name resolved to.
data SplitAction
  = RevealDotPattern     Name
      -- ^ De Bruijn index of a pattern variable bound to a value, turn into dot pattern.
  | RevealHiddenVariable Int
      -- ^ De Bruijn index of a hidden argument, make this argument visible.
  | SplitOnVariable      Int
      -- ^ De Bruijn index of an unconstrained pattern variable, split on it.
  deriving (Int -> SplitAction -> ShowS
[SplitAction] -> ShowS
SplitAction -> String
(Int -> SplitAction -> ShowS)
-> (SplitAction -> String)
-> ([SplitAction] -> ShowS)
-> Show SplitAction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SplitAction -> ShowS
showsPrec :: Int -> SplitAction -> ShowS
$cshow :: SplitAction -> String
show :: SplitAction -> String
$cshowList :: [SplitAction] -> ShowS
showList :: [SplitAction] -> ShowS
Show)

splitActionToEither3 :: SplitAction -> Either3 Name Int Int
splitActionToEither3 :: SplitAction -> Either3 Name Int Int
splitActionToEither3 = \case
  RevealDotPattern     Name
i -> Name -> Either3 Name Int Int
forall a b c. a -> Either3 a b c
In1 Name
i
  RevealHiddenVariable Int
i -> Int -> Either3 Name Int Int
forall a b c. b -> Either3 a b c
In2 Int
i
  SplitOnVariable      Int
i -> Int -> Either3 Name Int Int
forall a b c. c -> Either3 a b c
In3 Int
i

-- | 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 [SplitAction]
       -- ^ The computed de Bruijn indices of the variables and the inferred action.
parseVariables :: QName
-> Context
-> [AsBinding]
-> InteractionId
-> Range
-> [String]
-> TCM [SplitAction]
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
_) -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SplitAction
SplitOnVariable Int
i)
      -- Case 1b: the variable has been refined.
      -- Andreas, 2025-10-12, issue #7941: We can turn it into an explicit dot pattern.
      (Just Term
v         , PatternBound Hiding
_) -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SplitAction
RevealDotPattern Name
name) -- failInstantiatedVar s v
      -- Case 1c: the variable is bound locally (e.g. a record let)
      (Maybe Term
Nothing        , PatternBound Hiding
_) -> String -> TCMT IO SplitAction
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 SplitAction
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 SplitAction
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 SplitAction
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 SplitAction
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 SplitAction
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 SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenModuleBound String
s
                         | Bool
otherwise -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SplitAction
RevealHiddenVariable Int
i)
      -- Case 2b: there is a variable with that concrete name, but it
      -- has been refined.
      -- Andreas, 2025-10-12, issue #7941: We can turn it into an explicit dot pattern.
      Just (Name
x, Term
v) -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SplitAction
RevealDotPattern Name
x) -- failInstantiatedVar s 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 SplitAction
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 -> ShowS
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 -> ShowS
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 -> ShowS
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 -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
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 -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
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 -> ShowS
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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
", because it is an equality proof bound by a with-abstraction"
  -- failInstantiatedVar s v = interactionError . CaseSplitError =<< sep
  --     [ text $ "Cannot split on variable " ++ s ++ ", because it is bound to"
  --     , prettyTCM 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
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 :: [NamedArg DeBruijnPattern]
namedClausePats   = LHSResult -> [NamedArg DeBruijnPattern]
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 :: ClauseRecursive
clauseRecursive   = ClauseRecursive
MaybeRecursive
                  , 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

  -- See below, CLEAN UP OF THE GENERATED CLAUSES
  let
   filterOutExistingClauses :: [(SplitClause,a)] -> TCM [(SplitClause,a)]
   filterOutExistingClauses [(SplitClause, a)]
scs = do
    -- 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.
    String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case.filter" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"prevClauses:"
      , 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 :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Clause -> m Doc
prettyTCM [Clause]
prevClauses
      ]
    let sclause :: SplitClause
sclause = Clause -> SplitClause
clauseToSplitClause 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
    filterM (not <.> isCovered f (prevClauses ++ fcs) . fst) scs

  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 -> [NamedArg DeBruijnPattern]
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 pure [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 = (NamedArg DeBruijnPattern -> Maybe (NamedArg DBPatVar))
-> [NamedArg DeBruijnPattern] -> [NamedArg DBPatVar]
forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust NamedArg DeBruijnPattern -> Maybe (NamedArg DBPatVar)
forall {name} {a}.
Arg (Named name (Pattern' a)) -> Maybe (Arg (Named name a))
isVarP ([NamedArg DeBruijnPattern] -> [NamedArg DBPatVar])
-> [NamedArg DeBruijnPattern] -> [NamedArg DBPatVar]
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a]
reverse [NamedArg DeBruijnPattern]
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 [[Name] -> [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 do
        scs <- map fst <$> filterOutExistingClauses (map (, ()) scs)
        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 (toDotP, toShow, toSplit) = mapEither3 splitActionToEither3 xs
    let sc0 = Clause -> SplitClause
clauseToSplitClause Clause
clause
    let sc  = [Name] -> [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Name]
toDotP [Int]
toShow SplitClause
sc0
    reportSLn "interaction.case" 30 $ "toDot = " ++ prettyShow toDotP
    reportSLn "interaction.case" 30 $ "splitclause before makePatternVarsVisible: " ++ prettyShow sc0
    reportSLn "interaction.case" 30 $ "splitclause after: " ++ prettyShow sc
    reportSLn "interaction.case" 60 $ "splitclause before makePatternVarsVisible: " ++ show (killRange $ scPats sc0)
    reportSLn "interaction.case" 60 $ "splitclause after: " ++ show (killRange $ scPats sc)
    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.
    scs <- filterOutExistingClauses 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 :: [Name] -> [Nat] -> SplitClause -> SplitClause
makePatternVarsVisible :: [Name] -> [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Name]
xs [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 (Arg ArgInfo
ai (Named Maybe NamedName
n (DotP (PatternInfo (PatOVar Name
x) [Name]
_) Term
v)))
    | Name
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 = ArgInfo -> Named NamedName SplitPattern -> NamedArg SplitPattern
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Maybe NamedName -> SplitPattern -> Named NamedName SplitPattern
forall name a. Maybe name -> a -> Named name a
Named Maybe NamedName
n (PatternInfo -> Term -> SplitPattern
forall x. PatternInfo -> Term -> Pattern' x
DotP (PatOrigin -> [Name] -> PatternInfo
PatternInfo PatOrigin
PatOSplit []) Term
v))
  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
  showImp <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
  let
    ps  = [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns [NamedArg SplitPattern]
sps
    ps' = Bool
-> ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
showImp [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
filterOutGeneralizedVarPatterns [NamedArg DeBruijnPattern]
ps
    -- Internal clause
    cl = Clause
      { clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
      , clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
      , clauseTel :: Telescope
clauseTel       = Telescope
tel
      , namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
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 :: ClauseRecursive
clauseRecursive   = ClauseRecursive
MaybeRecursive
      , 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
      }
  reportSDoc "interaction.case" 10 $ vcat
    [ "Interaction.MakeCase.makeAbsurdClause: split clause:"
    , nest 2 $ vcat
      [ "context =" <+> do (inTopContext . prettyTCM) =<< getContextTelescope
      , "tel     =" <+> do inTopContext $ prettyTCM tel
      , "ps      =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList ps -- P.sep <$> prettyTCMPatterns ps
      , "ps'     =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList ps'
      , "ell     =" <+> text (show ell)
      ]
    ]
  reportSDoc "interaction.case" 10 $
    nest 2 $ vcat
      [ "ps (raw)=" <+> text (show ps)
      ]
  withCurrentModule (qnameModule f) $
    inTopContext $ reify $ QNamed f cl

-- | Drop hidden patterns introduced by generalization with an unparsable name.
--   If we drop one, we need to make the next non-dropped hidden pattern named.
filterOutGeneralizedVarPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
filterOutGeneralizedVarPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
filterOutGeneralizedVarPatterns = Bool -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall {a}. Bool -> [NamedArg a] -> [NamedArg a]
go Bool
False
  where
    go :: Bool -> [NamedArg a] -> [NamedArg a]
go Bool
b [] = []
    go Bool
b (NamedArg a
p : [NamedArg a]
ps)
      | Bool -> (NamedName -> Bool) -> Maybe NamedName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (String -> Bool
isGeneralizedVarName (String -> Bool) -> (NamedName -> String) -> NamedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedName -> String
forall a. Pretty a => a -> String
prettyShow) (NamedArg a -> Maybe (NameOf (NamedArg a))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg a
p) = Bool -> [NamedArg a] -> [NamedArg a]
go Bool
True [NamedArg a]
ps
      | Bool
otherwise = Bool -> (NamedArg a -> NamedArg a) -> NamedArg a -> NamedArg a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (Bool
b Bool -> Bool -> Bool
&& NamedArg a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg a
p Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
Hidden) NamedArg a -> NamedArg a
forall a. NamedArg a -> NamedArg a
makeNamedArgUserWritten NamedArg a
p NamedArg a -> [NamedArg a] -> [NamedArg a]
forall a. a -> [a] -> [a]
: Bool -> [NamedArg a] -> [NamedArg a]
go Bool
False [NamedArg a]
ps

makeNamedArgUserWritten :: NamedArg a -> NamedArg a
makeNamedArgUserWritten :: forall a. NamedArg a -> NamedArg a
makeNamedArgUserWritten (Arg ArgInfo
info (Named Maybe NamedName
n a
a)) = ArgInfo -> Named_ a -> Arg (Named_ a)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Maybe NamedName -> a -> Named_ a
forall name a. Maybe name -> a -> Named name a
Named (Origin -> NamedName -> NamedName
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
UserWritten (NamedName -> NamedName) -> Maybe NamedName -> Maybe NamedName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe NamedName
n) a
a)

-- | Unparseable variable names are those that contain a '.'.
isGeneralizedVarName :: PatVarName -> Bool
isGeneralizedVarName :: String -> Bool
isGeneralizedVarName = Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.'

-- | 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