{-# LANGUAGE NondecreasingIndentation #-}

module Agda.Interaction.MakeCase where

import Prelude hiding (null)

import Control.Monad

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

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

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

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

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

import Agda.Utils.Impossible

type CaseContext = Maybe ExtLamInfo

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  where

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



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

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

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

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


-- | Entry point for case splitting tactic.

makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [A.Clause])
makeCase :: InteractionId
-> Range -> String -> TCM (QName, CaseContext, [Clause])
makeCase InteractionId
hole Range
rng String
s = InteractionId
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
hole (TCM (QName, CaseContext, [Clause])
 -> TCM (QName, CaseContext, [Clause]))
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall a b. (a -> b) -> a -> b
$ Lens' Bool TCEnv
-> (Bool -> Bool)
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eMakeCase (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCM (QName, CaseContext, [Clause])
 -> TCM (QName, CaseContext, [Clause]))
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall a b. (a -> b) -> a -> b
$ do

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

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

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

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

  -- Check split variables.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell (SClause Telescope
tel [NamedArg SplitPattern]
sps SplitPSubstitution
_ Map CheckpointId Substitution
_ Maybe (Dom' Term Type)
t) = do
  let ps :: NAPs
ps = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
sps
  String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"Interaction.MakeCase.makeAbsurdClause: split clause:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      , TCMT IO Doc
"tel     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
      , TCMT IO Doc
"ps      =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps -- P.sep <$> prettyTCMPatterns ps
      , TCMT IO Doc
"ell     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (ExpandedEllipsis -> String
forall a. Show a => a -> String
show ExpandedEllipsis
ell)
      ]
    ]
  ModuleName -> TCM Clause -> TCM Clause
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (QName -> ModuleName
qnameModule QName
f) (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$ do
    -- Andreas, 2015-05-29 Issue 635
    -- Contract implicit record patterns before printing.
    -- c <- translateRecordPatterns $ Clause noRange tel perm ps NoBody t False
    -- Jesper, 2015-09-19 Don't contract, since we do on-demand splitting
    let c :: Clause
c = Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause Range
forall a. Range' a
noRange Range
forall a. Range' a
noRange Telescope
tel NAPs
ps Maybe Term
forall a. Maybe a
Nothing (Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term Type -> Arg Type)
-> Maybe (Dom' Term Type) -> Maybe (Arg Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Dom' Term Type)
t) Bool
False Maybe Bool
forall a. Maybe a
Nothing Maybe Bool
forall a. Maybe a
Nothing Maybe Bool
forall a. Maybe a
Nothing ExpandedEllipsis
ell
    let ps :: NAPs
ps = Clause -> NAPs
namedClausePats Clause
c
    TCM Clause -> TCM Clause
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$ QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause)))
-> QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
forall a b. (a -> b) -> a -> b
$ QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
f (Clause -> QNamed Clause) -> Clause -> QNamed Clause
forall a b. (a -> b) -> a -> b
$ Clause
c { namedClausePats :: NAPs
namedClausePats = NAPs
ps }


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

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

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

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