{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.Interaction.MakeCase where

import Prelude hiding ((!!), null)

import Data.List qualified as List
import Data.Maybe
import Data.Monoid
import Data.Text qualified as T
import Data.Text.Short qualified as TS

import Mikan.Syntax.Common
import Mikan.Syntax.Info
import Mikan.Syntax.Position
import Mikan.Syntax.Concrete qualified as C
import Mikan.Syntax.Concrete.Pattern qualified as C
import Mikan.Syntax.Abstract qualified as A
import Mikan.Syntax.Abstract.Pattern qualified as A
import Mikan.Syntax.Common.Pretty qualified as P
import Mikan.Syntax.Common.Pretty ( prettyShow )
import Mikan.Syntax.Internal
import Mikan.Syntax.Parser.Helpers ( mkValidName )
import Mikan.Syntax.Scope.Base  ( ResolvedName(..), BindingSource(..), exceptKindsOfNames )
import Mikan.Syntax.Scope.Monad ( resolveName' )
import Mikan.Syntax.Translation.InternalToAbstract

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

import Mikan.Interaction.BasicOps qualified as B
import Mikan.Interaction.Options
import Mikan.Interaction.Errors

import Mikan.Utils.BiMap qualified as BiMap
import Mikan.Utils.Function
import Mikan.Utils.Functor
import Mikan.Utils.List
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Utils.Three
import Mikan.Utils.WithDefault (lensKeepDefault)

import Mikan.Utils.Impossible

type CaseContext = Maybe ExtLamInfo

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

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

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

parseVariables
  :: QName           -- ^ The function name.
  -> Context         -- ^ The context of the RHS of the clause we are splitting.
  -> [AsBinding]     -- ^ The as-bindings of the clause we are splitting
  -> InteractionId   -- ^ The hole of this function we are working on.
  -> Range           -- ^ The range of this hole.
  -> [String]        -- ^ The words the user entered in this hole (variable names).
  -> TCM [SplitAction]
       -- ^ The computed de Bruijn indices of the variables and the inferred action.
parseVariables :: QName
-> Context
-> [AsBinding]
-> InteractionId
-> Range
-> [String]
-> TCM [SplitAction]
parseVariables QName
f Context
cxt [AsBinding]
asb InteractionId
ii Range
rng [String]
ss = do

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

  -- Get into the context of the meta.
  mId <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
B.lookupInteractionId InteractionId
ii
  updateMetaVarRange mId rng
  mi  <- getMetaInfo <$> lookupLocalMeta mId
  enterClosure mi $ \ Range
r -> do

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

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

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

    cname <- (String -> TCMT IO QName)
-> (Name -> TCMT IO QName) -> Either String Name -> TCMT IO QName
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> TCMT IO QName
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failParseError (QName -> TCMT IO QName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> TCMT IO QName)
-> (Name -> QName) -> Name -> TCMT IO QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> QName
C.QName) (Either String Name -> TCMT IO QName)
-> Either String Name -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ Bool -> Range -> Text -> Either String Name
mkValidName Bool
False Range
r (String -> Text
T.pack String
s)
    -- Note: the range in the concrete name is only approximate.
    -- Jesper, 2018-12-19: Don't consider generalizable names since
    -- they can be shadowed by hidden variables.
    resolveName' (exceptKindsOfNames [GeneralizeName]) Nothing cname >>= \case

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

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

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

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

  -- First, get context names of the clause.
  let clauseCxtNames = Context -> [Name]
contextNames' Context
cxt

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

  -- We cannot split on module parameters or make them visible
  params <- moduleParamsToApply $ qnameModule f
  let isParam Int
i = (Arg Term -> Bool) -> Args -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Term
var Int
i) (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) Args
params

  forM (zip ss abstractNames) $ \(String
s, (Name
name, Maybe BindingSource
bound)) -> case Maybe BindingSource
bound of
    -- Case 1: variable has a binding site. Check if it also exists in
    -- the clause context so we can split on it.
    Just BindingSource
bindingSource -> case (Name -> [(Name, Term)] -> Maybe Term
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, Term)]
clauseVars, BindingSource
bindingSource) of
      -- Case 1a: it is also known in the clause telescope and is
      -- actually a variable. If a pattern variable (`PatternBound`)
      -- has been refined to a module parameter we do allow splitting
      -- on it, since the instantiation could as well have been the
      -- other way around (see #2183).
      (Just (Var Int
i []), PatternBound Hiding
_) -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SplitAction
SplitOnVariable Int
i)
      -- Case 1b: the variable has been refined.
      -- Andreas, 2025-10-12, issue #7941: We can turn it into an explicit dot pattern.
      (Just Term
v         , PatternBound Hiding
_) -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SplitAction
RevealDotPattern Name
name) -- failInstantiatedVar s v
      -- Case 1c: the variable is bound locally (e.g. a record let)
      (Maybe Term
Nothing        , PatternBound Hiding
_) -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failCaseLet String
s
      -- Case 1d: module parameter
      (Just (Var Int
i []), BindingSource
LambdaBound ) -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failModuleBound String
s
      -- Case 1e: locally lambda-bound variable
      (Maybe Term
_              , BindingSource
LambdaBound ) -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failLocal String
s
      -- Case 1f: let-bound variable
      (Maybe Term
_              , BindingSource
LetBound    ) -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failLetBound String
s
      -- Case 1g: with-bound variable
      (Maybe Term
_              , BindingSource
WithBound   ) -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failWithBound String
s
      -- Case 1h: macro-bound variable (interactive command impossible in macro context)
      (Maybe Term
_              , BindingSource
MacroBound   ) -> TCMT IO SplitAction
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Case 2: variable has no binding site, so we check if it can be
    -- made visible.
    Maybe BindingSource
Nothing -> case ((Name, Term) -> Bool) -> [(Name, Term)] -> Maybe (Name, Term)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Name -> Name -> Bool) -> (Name -> Name) -> Name -> Name -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> Name
nameConcrete) Name
name (Name -> Bool) -> ((Name, Term) -> Name) -> (Name, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Term) -> Name
forall a b. (a, b) -> a
fst) [(Name, Term)]
clauseVars of
      -- Case 2a: there is a variable with that concrete name in the
      -- clause context. If it is not a parameter, we can make it
      -- visible.
      Just (Name
x, Var Int
i []) | Int -> Bool
isParam Int
i -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenModuleBound String
s
                         | Bool
otherwise -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> SplitAction
RevealHiddenVariable Int
i)
      -- Case 2b: there is a variable with that concrete name, but it
      -- has been refined.
      -- Andreas, 2025-10-12, issue #7941: We can turn it into an explicit dot pattern.
      Just (Name
x, Term
v) -> SplitAction -> TCMT IO SplitAction
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SplitAction
RevealDotPattern Name
x) -- failInstantiatedVar s v
      -- Case 2c: there is no variable with that name. Since it was in
      -- scope for the interaction meta, the only possibility is that
      -- it is a hidden lambda-bound variable.
      Maybe (Name, Term)
Nothing -> String -> TCMT IO SplitAction
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenLocal String
s

  where

  failParseError :: String -> m a
failParseError String
s  = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text String
s
  failNotVar :: String -> m a
failNotVar String
s      = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Not a variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  failUnbound :: String -> m a
failUnbound String
s     = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Unbound variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  failAmbiguous :: String -> m a
failAmbiguous String
s   = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Ambiguous variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  failLocal :: String -> m a
failLocal String
s       = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on local variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  failHiddenLocal :: String -> m a
failHiddenLocal String
s = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot make hidden lambda-bound variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" visible"
  failModuleBound :: String -> m a
failModuleBound String
s = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on module parameter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  failHiddenModuleBound :: String -> m a
failHiddenModuleBound String
s = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot make hidden module parameter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" visible"
  failLetBound :: String -> m a
failLetBound String
s = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on let-bound variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
  failWithBound :: String -> m a
failWithBound String
s = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
", because it is an equality proof bound by a with-abstraction"
  -- failInstantiatedVar s v = interactionError . CaseSplitError =<< sep
  --     [ text $ "Cannot split on variable " ++ s ++ ", because it is bound to"
  --     , prettyTCM v
  --     ]
  failCaseLet :: String -> m a
failCaseLet String
s     = InteractionError -> m a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m a) -> InteractionError -> m a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
P.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
    String
"Cannot split on variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++
    String
", because let-declarations may not be defined by pattern-matching"



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

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

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

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


-- | Entry point for case splitting tactic.

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

  -- Jesper, 2018-12-10: print unsolved metas in dot patterns as _
  (TCEnv -> TCEnv)
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
ePrintMetasBare Bool
True) do

  -- Get function clause which contains the interaction point.
  InteractionPoint { ipMeta = mm, ipClause = ipCl} <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m InteractionPoint
B.lookupInteractionPoint InteractionId
hole
  (f, clauseNo, clTy, clWithSub, absCl@A.Clause{ clauseRHS = rhs }, clClos) <- case ipCl of
    IPClause QName
f Int
i Type
t Maybe Substitution
sub SpineClause
cl Closure ()
clo -> (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
-> TCMT
     IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Int
i, Type
t, Maybe Substitution
sub, SpineClause
cl, Closure ()
clo)
    IPClause
IPNoClause                -> InteractionError
-> TCMT
     IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError
 -> TCMT
      IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ()))
-> InteractionError
-> TCMT
     IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$
      Doc
"Cannot split here, as we are not in a function definition"
  (casectxt, (prevClauses0, _clause, follClauses0)) <- getClauseZipperForIP f clauseNo

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

  let (prevClauses, follClauses) = killRange (prevClauses0, follClauses0)
    -- Andreas, 2019-08-08, issue #3966
    -- Kill the ranges of the existing clauses to prevent wrong error
    -- location to be set by the coverage checker (via isCovered)
    -- for test/interaction/Issue191

  -- See below, CLEAN UP OF THE GENERATED CLAUSES
  let
   filterOutExistingClauses :: [(SplitClause,a)] -> TCM [(SplitClause,a)]
   filterOutExistingClauses [(SplitClause, a)]
scs = do
    -- 1. filter out the generated clauses that are already covered
    --    we consider a generated clause already covered if it is covered by:
    --    a. a pre-existing clause defined before the one we splitted (prevClauses)
    --    b. a pre-existing clause defined after the one we splitted (follClauses)
    --       under the condition that it did not cover the one we splitted but was
    --       covered by it (i.e. it was considered unreachable).
    -- The key idea here is:
    --       f m    zero = ?  ---- split on m --->  f (suc m) zero = ?
    --       f zero zero = ?                        f zero    zero = ?
    --       f _    _    = ?                        f _       _    = ?
    -- because [f zero zero] is already defined.
    -- However we ignore [f _ _]: [f m zero] was already a refinement of it,
    -- hinting that we considered it more important than the catchall.
    String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case.filter" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"prevClauses:"
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCMT IO Doc) -> [Clause] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Clause -> m Doc
prettyTCM [Clause]
prevClauses
      ]
    let sclause :: SplitClause
sclause = Clause -> SplitClause
clauseToSplitClause Clause
clause
    fcs <- (Clause -> TCMT IO Bool) -> [Clause] -> TCMT IO [Clause]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\ Clause
cl -> (QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause
clause] (Clause -> SplitClause
clauseToSplitClause Clause
cl)) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
                            (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause
cl] SplitClause
sclause))
                   [Clause]
follClauses
    filterM (not <.> isCovered f (prevClauses ++ fcs) . fst) scs

  let perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
clause
      tel  = Clause -> Telescope
clauseTel  Clause
clause
      ps   = Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
clause
      ell  = Clause -> ExpandedEllipsis
clauseEllipsis Clause
clause
  reportSDoc "interaction.case" 100 $ vcat
    [ "splitting clause:"
    , nest 2 $ vcat
      [ "f       =" <+> (text . show) f
      , "context =" <+> ((inTopContext . (text . show)) =<< getContextTelescope)
      , "tel     =" <+> (text . show) tel
      , "perm    =" <+> text (show perm)
      , "ps      =" <+> (text . show) ps
      ]
    ]
  reportSDoc "interaction.case" 60 $ vcat
    [ "splitting clause:"
    , nest 2 $ vcat
      [ "f       =" <+> pretty f
      , "context =" <+> ((inTopContext . pretty) =<< getContextTelescope)
      , "tel     =" <+> pretty tel
      , "perm    =" <+> (text . show) perm
      , "ps      =" <+> pretty ps
      ]
    ]
  reportSDoc "interaction.case" 10 $ vcat
    [ "splitting clause:"
    , nest 2 $ vcat
      [ "f       =" <+> prettyTCM f
      , "context =" <+> ((inTopContext . prettyTCM) =<< getContextTelescope)
      , "tel     =" <+> (inTopContext . prettyTCM) tel
      , "perm    =" <+> text (show perm)
      , "ps      =" <+> addContext tel (prettyTCMPatternList ps)
      , "ell     =" <+> text (show ell)
      , "type    =" <+> addContext tel (prettyTCM $ clauseType clause)
      ]
    ]

  -- Check split variables.

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

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

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

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

  else if null vars then do
    -- Andreas, 2017-07-24, issue #2654:
    -- When we introduce projection patterns in an extended lambda,
    -- we need to print them postfix.
    let postProjInExtLam = Bool
-> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (CaseContext -> Bool
forall a. Maybe a -> Bool
isJust CaseContext
casectxt) ((TCMT IO [SplitClause] -> TCMT IO [SplitClause])
 -> TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall a b. (a -> b) -> a -> b
$
          (PragmaOptions -> PragmaOptions)
-> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
forall (m :: * -> *) a.
ReadTCState m =>
(PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions ((PragmaOptions -> PragmaOptions)
 -> TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> (PragmaOptions -> PragmaOptions)
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall a b. (a -> b) -> a -> b
$ ASetter PragmaOptions PragmaOptions Bool Bool
-> Bool -> PragmaOptions -> PragmaOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set ((WithDefault 'True -> Identity (WithDefault 'True))
-> PragmaOptions -> Identity PragmaOptions
forall (f :: * -> *).
Functor f =>
(WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions
lensOptPostfixProjections ((WithDefault 'True -> Identity (WithDefault 'True))
 -> PragmaOptions -> Identity PragmaOptions)
-> ((Bool -> Identity Bool)
    -> WithDefault 'True -> Identity (WithDefault 'True))
-> ASetter PragmaOptions PragmaOptions Bool Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Identity Bool)
-> WithDefault 'True -> Identity (WithDefault 'True)
forall a (b :: Bool).
(Boolean a, Eq a, KnownBool b) =>
Lens' (WithDefault' a b) a
Lens' (WithDefault 'True) Bool
lensKeepDefault) Bool
True
    (piTel, sc) <- insertTrailingArgs False $ clauseToSplitClause clause
    -- Andreas, 2015-05-05 If we introduced new function arguments
    -- do not split on result.  This might be more what the user wants.
    -- To split on result, he can then C-c C-c again.
    -- Andreas, 2015-05-21 Issue 1516:  However, if only hidden
    -- arguments are introduced, C-c C-c virtually does nothing
    -- (as they are not shown and get lost on the way to emacs and back).
    newPats <- if null piTel then return False else do
      -- If there were any pattern introduce, they will only have effect
      -- if any of them is shown by the printer
      imp <- optShowImplicit <$> pragmaOptions
      return $ imp || any visible (telToList piTel)
    scs <- if newPats then pure [sc] else postProjInExtLam $ do
      res <- splitResult f sc
      case res of

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

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

        Right [SplitClause]
cov -> TCMT IO Bool
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optCopatterns (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) TCMT IO [SplitClause]
forall {a}. TCMT IO a
failNoCop (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
forall a b. (a -> b) -> a -> b
$ {-else-} do
          -- Andreas, 2016-05-03: do not introduce function arguments after projection.
          -- This is sometimes annoying and can anyway be done by another C-c C-c.
          -- mapM (snd <.> fixTarget) $ splitClauses cov
          [SplitClause] -> TCMT IO [SplitClause]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [SplitClause]
cov
    checkClauseIsClean ipCl
    (f, casectxt,) <$> do
      -- Andreas, 2020-05-18, issue #4536
      -- When result splitting yields no clauses, replace rhs by @record{}@.
      if null scs then
        return [ A.spineToLhs $ absCl{ A.clauseRHS = makeRHSEmptyRecord rhs } ]
      else do
        scs <- map fst <$> filterOutExistingClauses (map (, ()) scs)
        mapM (makeAbstractClause f rhs ell) scs
  else do
    -- split on variables
    xs <- parseVariables f clauseCxt clauseAsBindings hole rng vars
    reportSLn "interaction.case" 30 $ "parsedVariables: " ++ show (zip xs vars)
    -- Variables that are not in scope yet are brought into scope (@toShow@)
    -- The other variables are split on (@toSplit@).
    let (toDotP, toShow, toSplit) = mapEither3 splitActionToEither3 xs
    let sc0 = Clause -> SplitClause
clauseToSplitClause Clause
clause
    let sc  = [Name] -> [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Name]
toDotP [Int]
toShow SplitClause
sc0
    reportSLn "interaction.case" 30 $ "toDot = " ++ prettyShow toDotP
    reportSLn "interaction.case" 30 $ "splitclause before makePatternVarsVisible: " ++ prettyShow sc0
    reportSLn "interaction.case" 30 $ "splitclause after: " ++ prettyShow sc
    reportSLn "interaction.case" 60 $ "splitclause before makePatternVarsVisible: " ++ show (killRange $ scPats sc0)
    reportSLn "interaction.case" 60 $ "splitclause after: " ++ show (killRange $ scPats sc)
    scs <- split f toSplit sc
    reportSLn "interaction.case" 70 $ "makeCase: survived the splitting"

    -- If any of the split variables is hidden by the ellipsis, we
    -- should force the expansion of the ellipsis.
    let splitNames =
          (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (ContextEntry -> Name
ctxEntryName (ContextEntry -> Name) -> (Int -> ContextEntry) -> Int -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> Maybe ContextEntry -> ContextEntry
forall a. a -> Maybe a -> a
fromMaybe ContextEntry
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ContextEntry -> ContextEntry)
-> (Int -> Maybe ContextEntry) -> Int -> ContextEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Context -> Maybe ContextEntry
`cxLookup` Context
clauseCxt))
          [Int]
toSplit
    shouldExpandEllipsis <- return (not $ null toShow) `or2M` anyEllipsisVar f absCl splitNames
    let ell' | Bool
shouldExpandEllipsis = ExpandedEllipsis
NoEllipsis
             | Bool
otherwise            = ExpandedEllipsis
ell

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

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

  where
  failNoCop :: TCMT IO a
failNoCop = InteractionError -> TCMT IO a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> TCMT IO a) -> InteractionError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ Doc -> InteractionError
CaseSplitError (Doc -> InteractionError) -> Doc -> InteractionError
forall a b. (a -> b) -> a -> b
$
    Doc
"OPTION --copatterns needed to split on result here"

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

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

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

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

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

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

makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell (SClause Telescope
tel [NamedArg SplitPattern]
sps SplitPSubstitution
_ Map CheckpointId Substitution
_ Maybe (Dom' Term Type)
t) = do
  showImp <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
  let
    ps  = [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns [NamedArg SplitPattern]
sps
    ps' = Bool
-> ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
showImp [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
filterOutGeneralizedVarPatterns [NamedArg DeBruijnPattern]
ps
    -- Internal clause
    cl = Clause
      { clauseLHSRange :: Range
clauseLHSRange  = Range
forall a. Range' a
noRange
      , clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
      , clauseTel :: Telescope
clauseTel       = Telescope
tel
      , namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps'
      , clauseBody :: Maybe Term
clauseBody      = Maybe Term
forall a. Maybe a
Nothing
      , clauseType :: Maybe (Arg Type)
clauseType      = Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term Type -> Arg Type)
-> Maybe (Dom' Term Type) -> Maybe (Arg Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Dom' Term Type)
t
      , clauseCatchall :: Catchall
clauseCatchall    = Catchall
forall a. Null a => a
empty
      , clauseRecursive :: ClauseRecursive
clauseRecursive   = ClauseRecursive
MaybeRecursive
      , clauseUnreachable :: Maybe Bool
clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing
      , clauseEllipsis :: ExpandedEllipsis
clauseEllipsis    = ExpandedEllipsis
ell
      , clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
      }
  reportSDoc "interaction.case" 10 $ vcat
    [ "Interaction.MakeCase.makeAbsurdClause: split clause:"
    , nest 2 $ vcat
      [ "context =" <+> do (inTopContext . prettyTCM) =<< getContextTelescope
      , "tel     =" <+> do inTopContext $ prettyTCM tel
      , "ps      =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList ps -- P.sep <$> prettyTCMPatterns ps
      , "ps'     =" <+> do inTopContext $ addContext tel $ prettyTCMPatternList ps'
      , "ell     =" <+> text (show ell)
      ]
    ]
  reportSDoc "interaction.case" 10 $
    nest 2 $ vcat
      [ "ps (raw)=" <+> text (show ps)
      ]
  withCurrentModule (qnameModule f) $
    inTopContext $ reify $ QNamed f cl

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

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

-- | Unparseable variable names are those that contain a '.'.
isGeneralizedVarName :: PatVarName -> Bool
isGeneralizedVarName :: ArgName -> Bool
isGeneralizedVarName = (Char -> Bool) -> ArgName -> Bool
TS.any (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.')

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

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

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

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