{-# LANGUAGE NondecreasingIndentation #-}

module Agda.Interaction.MakeCase where

import Prelude hiding (mapM, mapM_, null)

import Control.Monad hiding (mapM, mapM_, forM)

import Data.Either
import qualified Data.Map as Map
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Traversable (mapM, forM)

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.Term (isModuleFreeVar)

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

import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
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.
  -> Telescope       -- ^ The telescope 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
-> Telescope
-> InteractionId
-> Range
-> [String]
-> TCM [(Int, NameInScope)]
parseVariables QName
f Telescope
tel InteractionId
ii Range
rng [String]
ss = do

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

    -- Get printed representation of variables in context.
    Int
n  <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
    [(String, Int)]
xs <- [Int] -> (Int -> TCMT IO (String, Int)) -> TCMT IO [(String, Int)]
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, Int)) -> TCMT IO [(String, Int)])
-> (Int -> TCMT IO (String, Int)) -> TCMT IO [(String, Int)]
forall a b. (a -> b) -> a -> b
$ \ Int
i -> do
      (,Int
i) (String -> (String, Int))
-> (Doc -> String) -> Doc -> (String, Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
P.render (Doc -> (String, Int)) -> TCMT IO Doc -> TCMT IO (String, Int)
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)

    -- We might be under some lambdas, in which case the context
    -- is bigger than the number of pattern variables.
    let nPatVars :: Int
nPatVars = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel
    let nlocals :: Int
nlocals = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nPatVars
    Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
nlocals Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- cannot be negative

    Int
fv <- QName -> TCMT IO Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
f
    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
      Telescope
cxt <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *). Monad m => [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)
       , String -> TCMT IO Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"function's fvs  = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
fv
       , String -> TCMT IO Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"number of locals= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
nlocals
       , 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) -> 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
cxt
       , TCMT IO Doc
"checkpoints     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do (String -> TCMT IO Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCMT IO Doc)
-> (Map CheckpointId Substitution -> String)
-> Map CheckpointId Substitution
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map CheckpointId Substitution -> String
forall a. Show a => a -> String
show) (Map CheckpointId Substitution -> TCMT IO Doc)
-> TCMT IO (Map CheckpointId Substitution) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Map CheckpointId Substitution)
-> TCMT IO (Map CheckpointId Substitution)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Map CheckpointId Substitution
envCheckpoints
       ]

    -- Resolve each string to a variable.
    [String]
-> (String -> 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]
ss ((String -> TCMT IO (Int, NameInScope))
 -> TCM [(Int, NameInScope)])
-> (String -> TCMT IO (Int, NameInScope))
-> TCM [(Int, NameInScope)]
forall a b. (a -> b) -> a -> b
$ \ String
s -> do
      let failNotVar :: TCMT IO a
failNotVar      = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
"Not a variable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
          failUnbound :: TCMT IO a
failUnbound     = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
"Unbound variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
          failAmbiguous :: TCMT IO a
failAmbiguous   = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
"Ambiguous variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
          failLocal :: TCMT IO a
failLocal       = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
"Cannot split on local variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
          failModuleBound :: TCMT IO a
failModuleBound = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
"Cannot split on module parameter " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
          failLetBound :: p -> m a
failLetBound p
v  = TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 :: a -> m b
failInstantiatedVar a
v = TypeError -> m b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 :: * -> *). Monad m => [m Doc] -> m Doc
sep
              [ String -> m Doc
forall (m :: * -> *). Monad 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 :: TCMT IO a
failCaseLet     = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
"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"

      let cname :: QName
cname = Name -> QName
C.QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> [NamePart] -> Name
C.Name Range
r NameInScope
C.InScope ([NamePart] -> Name) -> [NamePart] -> Name
forall a b. (a -> b) -> a -> b
$ String -> [NamePart]
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 (Int, NameInScope))
-> TCMT IO (Int, NameInScope)
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{}       -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failNotVar
        FieldName{}         -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failNotVar
        ConstructorName{}   -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failNotVar
        PatternSynResName{} -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failNotVar

        -- If s is a variable name in scope, get its de Bruijn index
        -- via the type checker.
        VarName Name
x BindingSource
b -> do
          (Term
v, Dom Type
_) <- Name -> TCMT IO (Term, Dom Type)
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Name -> m (Term, Dom Type)
getVarInfo Name
x
          case (Term
v , BindingSource
b) of
            -- Slightly dangerous: the pattern variable `x` may be
            -- refined to the module parameter `var i`. But in this
            -- case the instantiation could as well be the other way
            -- around, so the new clauses will still make sense.
            (Var Int
i [] , BindingSource
PatternBound) -> do
              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
"resolved variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
              Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nlocals) TCMT IO ()
forall a. TCMT IO a
failCaseLet
              (Int, NameInScope) -> TCMT IO (Int, NameInScope)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nlocals , NameInScope
C.InScope)
            (Var Int
i [] , BindingSource
LambdaBound)
              | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nlocals -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failLocal
              | Bool
otherwise   -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failModuleBound
            (Var Int
i [] , BindingSource
LetBound) -> Term -> TCMT IO (Int, NameInScope)
forall (m :: * -> *) p a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
p -> m a
failLetBound Term
v
            (Term
_        , BindingSource
_       ) -> Term -> TCMT IO (Int, NameInScope)
forall (m :: * -> *) a b.
(MonadError TCErr m, PrettyTCM a, MonadReduce m, MonadAddContext m,
 MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m,
 HasBuiltins m, MonadStConcreteNames m, IsString (m Doc),
 Null (m Doc), Semigroup (m Doc)) =>
a -> m b
failInstantiatedVar Term
v

        -- If s is not a name, compare it to the printed variable representation.
        -- This fallback is to enable splitting on hidden variables.
        ResolvedName
UnknownName -> do
          let xs' :: [(String, Int)]
xs' = ((String, Int) -> Bool) -> [(String, Int)] -> [(String, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool)
-> ((String, Int) -> String) -> (String, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Int) -> String
forall a b. (a, b) -> a
fst) [(String, Int)]
xs
          Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(String, Int)] -> Bool
forall a. Null a => a -> Bool
null [(String, Int)]
xs') (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
forall a. TCMT IO a
failUnbound
          String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.case" Int
20 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"matching names corresponding to indices " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, Int)] -> String
forall a. Show a => a -> String
show [(String, Int)]
xs'
          -- Andreas, 2018-05-28, issue #3095
          -- We want to act on an ambiguous name if it corresponds to only one local index.
          let xs'' :: [Int]
xs'' = ((String, Int) -> Maybe Int) -> [(String, Int)] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (String
_,Int
i) -> if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nlocals then Maybe Int
forall a. Maybe a
Nothing else Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nlocals) [(String, Int)]
xs'
          Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Int] -> Bool
forall a. Null a => a -> Bool
null [Int]
xs'') (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 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"
          -- Filter out variable bound by parent function or module.
          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
              xs''' :: [Int]
xs'''     = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Int -> Bool) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Bool
isParam) [Int]
xs''
          Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Int] -> Bool
forall a. Null a => a -> Bool
null [Int]
xs''') (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 make hidden module parameter " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" visible"
          case [Int]
xs''' of
            []  -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failModuleBound
            [Int
i] -> (Int, NameInScope) -> TCMT IO (Int, NameInScope)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i , NameInScope
C.NotInScope)
            -- Issue 1325: Variable names in context can be ambiguous.
            [Int]
_   -> TCMT IO (Int, NameInScope)
forall a. TCMT IO a
failAmbiguous

-- | 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 :: * -> *). Monad m => [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 :: * -> *). Monad 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 :: * -> *). Monad 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
recheckAbstractClause :: Type -> Maybe Substitution -> SpineClause -> TCM Clause
recheckAbstractClause Type
t Maybe Substitution
sub SpineClause
cl = Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM Clause)
-> TCM Clause
forall a.
Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
sub SpineClause
cl ((LHSResult -> TCM Clause) -> TCM Clause)
-> (LHSResult -> TCM Clause) -> TCM Clause
forall a b. (a -> b) -> a -> b
$ \ LHSResult
lhs ->
  Clause -> TCM Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause :: Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
Clause{ clauseLHSRange :: Range
clauseLHSRange    = SpineClause -> Range
forall t. HasRange t => t -> Range
getRange SpineClause
cl
               , clauseFullRange :: Range
clauseFullRange   = SpineClause -> Range
forall t. HasRange t => t -> Range
getRange SpineClause
cl
               , 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
               , 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
cl
               }

-- | 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 a. InteractionId -> TCM a -> TCM 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
  let meta :: MetaId
meta = MetaId -> Maybe MetaId -> MetaId
forall a. a -> Maybe a -> a
fromMaybe MetaId
forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe MetaId
mm
  (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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 <- Closure () -> (() -> TCM Clause) -> TCM Clause
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure ()
clClos ((() -> TCM Clause) -> TCM Clause)
-> (() -> TCM Clause) -> TCM Clause
forall a b. (a -> b) -> a -> b
$ \ ()
_ -> Lens' Bool TCEnv -> (Bool -> Bool) -> TCM Clause -> TCM 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 Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$
              Type -> Maybe Substitution -> SpineClause -> TCM Clause
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
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 :: * -> *). Monad m => [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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
<+> 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 :: * -> *). Monad m => String -> m Doc
text (ExpandedEllipsis -> String
forall a. Show a => a -> String
show ExpandedEllipsis
ell)
      ]
    ]
  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 :: * -> *). Monad m => [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 :: * -> *). Monad m => [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 :: * -> *). Monad 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 :: * -> *). Monad 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 :: * -> *). Monad 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 :: * -> *). Monad 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 :: * -> *). Monad 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
      ]
    ]

  -- 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 a -> TCMT IO a
postProjInExtLam = Bool -> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall a. Bool -> (a -> a) -> a -> a
applyWhen (CaseContext -> Bool
forall a. Maybe a -> Bool
isJust CaseContext
casectxt) ((TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a)
-> (TCMT IO a -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall a b. (a -> b) -> a -> b
$
          (PragmaOptions -> PragmaOptions) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
ReadTCState m =>
(PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions ((PragmaOptions -> PragmaOptions) -> TCMT IO a -> TCMT IO a)
-> (PragmaOptions -> PragmaOptions) -> TCMT IO a -> TCMT IO a
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]
forall a. TCMT IO a -> TCMT IO a
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 NamedName (Pattern' DBPatVar))
 -> Maybe (NamedArg DBPatVar))
-> NAPs -> [NamedArg DBPatVar]
forall a b. (a -> Maybe b) -> [a] -> [b]
takeWhileJust Arg (Named NamedName (Pattern' DBPatVar))
-> 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
<$> (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
-> Telescope
-> InteractionId
-> Range
-> [String]
-> TCM [(Int, NameInScope)]
parseVariables QName
f Telescope
tel 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.
    [Name]
splitNames <- (Int -> TCMT IO Name) -> [Int] -> TCMT IO [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> TCMT IO Name
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV [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 :: * -> *). Monad m => [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 :: * -> *). Monad m => [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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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] -> [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. Subst Term 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])
-> (Map InteractionId InteractionPoint -> [InteractionPoint])
-> Map InteractionId InteractionPoint
-> [InteractionPoint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map InteractionId InteractionPoint -> [InteractionPoint]
forall k a. Map k a -> [a]
Map.elems (Map InteractionId InteractionPoint -> [InteractionPoint])
-> TCMT IO (Map InteractionId InteractionPoint)
-> TCMT IO [InteractionPoint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Map InteractionId InteractionPoint) TCState
-> TCMT IO (Map InteractionId InteractionPoint)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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

-- | 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 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 :: * -> *). Monad m => [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 :: * -> *). Monad m => [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 :: * -> *). Monad 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
-> 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 Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom (Dom Type -> Arg Type) -> Maybe (Dom Type) -> Maybe (Arg Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Dom Type)
t) Bool
False Maybe Bool
forall a. Maybe a
Nothing Maybe Bool
forall a. Maybe a
Nothing ExpandedEllipsis
ell
    -- Normalise the dot patterns
    NAPs
ps <- Telescope -> TCMT IO NAPs -> TCMT IO NAPs
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO NAPs -> TCMT IO NAPs) -> TCMT IO NAPs -> TCMT IO NAPs
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO NAPs
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (NAPs -> TCMT IO NAPs) -> NAPs -> TCMT IO NAPs
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
c
    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
"normalized patterns: " 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 :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps
    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 -> TCM Clause
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (QNamed Clause -> TCM Clause) -> QNamed Clause -> TCM 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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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 :: [NamedArg Pattern]
ps  = SpineLHS -> [NamedArg Pattern]
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
      [NamedArg Pattern]
ps' <- (QName, [NamedArg Pattern]) -> [NamedArg Pattern]
forall a b. (a, b) -> b
snd ((QName, [NamedArg Pattern]) -> [NamedArg Pattern])
-> TCMT IO (QName, [NamedArg Pattern])
-> TCMT IO [NamedArg Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> [NamedArg Pattern]
-> [NamedArg Pattern]
-> TCMT IO (QName, [NamedArg Pattern])
forall (m :: * -> *).
MonadReify m =>
QName
-> [NamedArg Pattern]
-> [NamedArg Pattern]
-> m (QName, [NamedArg Pattern])
reifyDisplayFormP QName
f [NamedArg Pattern]
ps []
      let ellipsisPats :: A.Patterns
          ellipsisPats :: [NamedArg Pattern]
ellipsisPats = ([NamedArg Pattern], [NamedArg Pattern]) -> [NamedArg Pattern]
forall a b. (a, b) -> a
fst (([NamedArg Pattern], [NamedArg Pattern]) -> [NamedArg Pattern])
-> ([NamedArg Pattern], [NamedArg Pattern]) -> [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Int
-> [NamedArg Pattern] -> ([NamedArg Pattern], [NamedArg Pattern])
forall p. IsWithP p => Int -> [p] -> ([p], [p])
C.splitEllipsis Int
k [NamedArg Pattern]
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 :: * -> *). Monad m => [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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[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 c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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 :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
prettyList_ ((NamedArg Pattern -> TCMT IO Doc)
-> [NamedArg Pattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg Pattern -> TCMT IO Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [NamedArg Pattern]
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 -> Any -> Any) -> [NamedArg Pattern] -> Any
forall a p m.
(APatternLike a p, Monoid m) =>
(Pattern' a -> m -> m) -> p -> m
A.foldrAPattern Pattern -> Any -> Any
anyVar [NamedArg Pattern]
ellipsisPats