{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.Interaction.MakeCase where
import Prelude hiding ((!!), null)
import Control.Monad
import Data.Either
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.Syntax.Concrete (NameInScope(..))
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Pattern as C
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Pattern as A
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Scope.Base ( ResolvedName(..), BindingSource(..), KindOfName(..), exceptKindsOfNames )
import Agda.Syntax.Scope.Monad ( resolveName' )
import Agda.Syntax.Translation.InternalToAbstract
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( SplitPatVar(..) , SplitPattern , applySplitPSubst , fromSplitPatterns )
import Agda.TypeChecking.Empty ( isEmptyTel )
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Rules.Def (checkClauseLHS)
import Agda.TypeChecking.Rules.LHS (LHSResult(..))
import Agda.TypeChecking.Rules.LHS.Problem (AsBinding(..))
import Agda.Interaction.Options
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens (set)
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.WithDefault (lensKeepDefault)
import Agda.Utils.Impossible
type CaseContext = Maybe ExtLamInfo
parseVariables
:: QName
-> Context
-> [AsBinding]
-> InteractionId
-> Range
-> [String]
-> TCM [(Int,NameInScope)]
parseVariables :: QName
-> Context
-> [AsBinding]
-> InteractionId
-> Range
-> [String]
-> TCM [(Int, NameInScope)]
parseVariables QName
f Context
cxt [AsBinding]
asb InteractionId
ii Range
rng [String]
ss = do
mId <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
updateMetaVarRange mId rng
mi <- getMetaInfo <$> lookupLocalMeta mId
enterClosure mi $ \ Range
r -> do
String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
m <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
tel <- lookupSection m
vcat
[ "parseVariables:"
, "current module =" <+> prettyTCM m
, "current section =" <+> inTopContext (prettyTCM tel)
, "clause context =" <+> prettyTCM (PrettyContext cxt)
]
n <- TCMT IO Int
forall (m :: * -> *). (Applicative 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 :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
i
abstractNames :: [(A.Name, Maybe BindingSource)] <- forM ss $ \String
s -> do
let cname :: QName
cname = Name -> QName
C.QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Range -> NameInScope -> NameParts -> Name
C.Name Range
r NameInScope
C.InScope (NameParts -> Name) -> NameParts -> Name
forall a b. (a -> b) -> a -> b
$ String -> NameParts
C.stringNameParts String
s
KindsOfNames -> Maybe (Set Name) -> QName -> ScopeM ResolvedName
resolveName' ([KindOfName] -> KindsOfNames
exceptKindsOfNames [KindOfName
GeneralizeName]) Maybe (Set Name)
forall a. Maybe a
Nothing QName
cname ScopeM ResolvedName
-> (ResolvedName -> TCMT IO (Name, Maybe BindingSource))
-> TCMT IO (Name, Maybe BindingSource)
forall 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
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
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)
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)
let clauseCxtNames = (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
cxt
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 Type
_ Modality
_) -> (Name
name,Term
v)) [AsBinding]
asb
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
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
(Just (Var Int
i []), PatternBound Hiding
_) -> (Int, NameInScope) -> TCMT IO (Int, NameInScope)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, NameInScope
C.InScope)
(Just Term
v , PatternBound Hiding
_) -> String -> Term -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
String -> a -> m b
failInstantiatedVar String
s Term
v
(Maybe Term
Nothing , PatternBound Hiding
_) -> String -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failCaseLet String
s
(Just (Var Int
i []), BindingSource
LambdaBound ) -> String -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failModuleBound String
s
(Maybe Term
_ , BindingSource
LambdaBound ) -> String -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failLocal String
s
(Maybe Term
_ , BindingSource
LetBound ) -> String -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failLetBound String
s
(Maybe Term
_ , BindingSource
WithBound ) -> TCMT IO (Int, NameInScope)
forall a. HasCallStack => a
__IMPOSSIBLE__
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
Just (Name
x, Var Int
i []) | Int -> Bool
isParam Int
i -> String -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenModuleBound String
s
| Bool
otherwise -> (Int, NameInScope) -> TCMT IO (Int, NameInScope)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, NameInScope
C.NotInScope)
Just (Name
x, Term
v) -> String -> Term -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
String -> a -> m b
failInstantiatedVar String
s Term
v
Maybe (Name, Term)
Nothing -> String -> TCMT IO (Int, NameInScope)
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
failHiddenLocal String
s
where
failNotVar :: String -> m a
failNotVar String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Not a variable: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
failUnbound :: String -> m a
failUnbound String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Unbound variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
failAmbiguous :: String -> m a
failAmbiguous String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Ambiguous variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
failLocal :: String -> m a
failLocal String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"Cannot split on local variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
failHiddenLocal :: String -> m a
failHiddenLocal String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"Cannot make hidden lambda-bound variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" visible"
failModuleBound :: String -> m a
failModuleBound String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"Cannot split on module parameter " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
failHiddenModuleBound :: String -> m a
failHiddenModuleBound String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"Cannot make hidden module parameter " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" visible"
failLetBound :: String -> m a
failLetBound String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> (String -> TypeError) -> String -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TypeError
GenericError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$
String
"Cannot split on let-bound variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
failInstantiatedVar :: String -> a -> m b
failInstantiatedVar String
s a
v = TypeError -> m b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m b) -> (Doc -> TypeError) -> Doc -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> m b) -> m Doc -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> m Doc) -> String -> m Doc
forall a b. (a -> b) -> a -> b
$ String
"Cannot split on variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", because it is bound to"
, a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v
]
failCaseLet :: String -> m a
failCaseLet String
s = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"Cannot split on variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
", because let-declarations may not be defined by pattern-matching"
type ClauseZipper =
( [Clause]
, Clause
, [Clause]
)
getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP QName
f Int
clauseNo = do
(Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f) TCMT IO Defn
-> (Defn -> TCM (CaseContext, ClauseZipper))
-> TCM (CaseContext, ClauseZipper)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funExtLam :: Defn -> CaseContext
funExtLam = CaseContext
extlam} -> do
let ([Clause]
cs1,[Clause]
ccs2) = ([Clause], [Clause])
-> Maybe ([Clause], [Clause]) -> ([Clause], [Clause])
forall a. a -> Maybe a -> a
fromMaybe ([Clause], [Clause])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([Clause], [Clause]) -> ([Clause], [Clause]))
-> Maybe ([Clause], [Clause]) -> ([Clause], [Clause])
forall a b. (a -> b) -> a -> b
$ Int -> [Clause] -> Maybe ([Clause], [Clause])
forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
clauseNo [Clause]
cs
(Clause
c,[Clause]
cs2) = (Clause, [Clause])
-> Maybe (Clause, [Clause]) -> (Clause, [Clause])
forall a. a -> Maybe a -> a
fromMaybe (Clause, [Clause])
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Clause, [Clause]) -> (Clause, [Clause]))
-> Maybe (Clause, [Clause]) -> (Clause, [Clause])
forall a b. (a -> b) -> a -> b
$ [Clause] -> Maybe (Clause, [Clause])
forall a. [a] -> Maybe (a, [a])
uncons [Clause]
ccs2
(CaseContext, ClauseZipper) -> TCM (CaseContext, ClauseZipper)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseContext
extlam, ([Clause]
cs1, Clause
c, [Clause]
cs2))
Defn
d -> do
String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"impossible" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"getClauseZipperForIP" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
clauseNo)
TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"received"
, String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Defn -> String
forall a. Show a => a -> String
show Defn
d)
]
TCM (CaseContext, ClauseZipper)
forall a. HasCallStack => a
__IMPOSSIBLE__
recheckAbstractClause :: Type -> Maybe Substitution -> A.SpineClause -> TCM (Clause, Context, [AsBinding])
recheckAbstractClause :: Type
-> Maybe Substitution
-> SpineClause
-> TCM (Clause, Context, [AsBinding])
recheckAbstractClause Type
t Maybe Substitution
sub SpineClause
acl = Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM (Clause, Context, [AsBinding]))
-> TCM (Clause, Context, [AsBinding])
forall a.
Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
sub SpineClause
acl ((LHSResult -> TCM (Clause, Context, [AsBinding]))
-> TCM (Clause, Context, [AsBinding]))
-> (LHSResult -> TCM (Clause, Context, [AsBinding]))
-> TCM (Clause, Context, [AsBinding])
forall a b. (a -> b) -> a -> b
$ \ LHSResult
lhs -> do
let cl :: Clause
cl = Clause { clauseLHSRange :: Range
clauseLHSRange = SpineClause -> Range
forall a. HasRange a => a -> Range
getRange SpineClause
acl
, clauseFullRange :: Range
clauseFullRange = SpineClause -> Range
forall a. HasRange a => a -> Range
getRange SpineClause
acl
, clauseTel :: Telescope
clauseTel = LHSResult -> Telescope
lhsVarTele LHSResult
lhs
, namedClausePats :: NAPs
namedClausePats = LHSResult -> NAPs
lhsPatterns LHSResult
lhs
, clauseBody :: Maybe Term
clauseBody = Maybe Term
forall a. Maybe a
Nothing
, clauseType :: Maybe (Arg Type)
clauseType = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (LHSResult -> Arg Type
lhsBodyType LHSResult
lhs)
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = Maybe Bool
forall a. Maybe a
Nothing
, clauseRecursive :: Maybe Bool
clauseRecursive = Maybe Bool
forall a. Maybe a
Nothing
, clauseUnreachable :: Maybe Bool
clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = LHSInfo -> ExpandedEllipsis
lhsEllipsis (LHSInfo -> ExpandedEllipsis) -> LHSInfo -> ExpandedEllipsis
forall a b. (a -> b) -> a -> b
$ SpineLHS -> LHSInfo
A.spLhsInfo (SpineLHS -> LHSInfo) -> SpineLHS -> LHSInfo
forall a b. (a -> b) -> a -> b
$ SpineClause -> SpineLHS
forall lhs. Clause' lhs -> lhs
A.clauseLHS SpineClause
acl
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = WhereDeclarations -> Maybe ModuleName
A.whereModule (WhereDeclarations -> Maybe ModuleName)
-> WhereDeclarations -> Maybe ModuleName
forall a b. (a -> b) -> a -> b
$ SpineClause -> WhereDeclarations
forall lhs. Clause' lhs -> WhereDeclarations
A.clauseWhereDecls SpineClause
acl
}
cxt <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
let asb = LHSResult -> [AsBinding]
lhsAsBindings LHSResult
lhs
return (cl, cxt, asb)
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, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
hole (TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause]))
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall a b. (a -> b) -> a -> b
$ Lens' 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
(TCEnv -> TCEnv)
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envPrintMetasBare = True }) (TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause]))
-> TCM (QName, CaseContext, [Clause])
-> TCM (QName, CaseContext, [Clause])
forall a b. (a -> b) -> a -> b
$ do
InteractionPoint { ipMeta = mm, ipClause = ipCl} <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
hole
(f, clauseNo, clTy, clWithSub, absCl@A.Clause{ clauseRHS = rhs }, clClos) <- case ipCl of
IPClause QName
f Int
i Type
t Maybe Substitution
sub SpineClause
cl Closure ()
clo -> (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
-> TCMT
IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f, Int
i, Type
t, Maybe Substitution
sub, SpineClause
cl, Closure ()
clo)
IPClause
IPNoClause -> TypeError
-> TCMT
IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError
-> TCMT
IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ()))
-> TypeError
-> TCMT
IO (QName, Int, Type, Maybe Substitution, SpineClause, Closure ())
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"Cannot split here, as we are not in a function definition"
(casectxt, (prevClauses0, _clause, follClauses0)) <- getClauseZipperForIP f clauseNo
(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)
let perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
clause
tel = Clause -> Telescope
clauseTel Clause
clause
ps = Clause -> NAPs
namedClausePats Clause
clause
ell = Clause -> ExpandedEllipsis
clauseEllipsis Clause
clause
reportSDoc "interaction.case" 100 $ vcat
[ "splitting clause:"
, nest 2 $ vcat
[ "f =" <+> (text . show) f
, "context =" <+> ((inTopContext . (text . show)) =<< getContextTelescope)
, "tel =" <+> (text . show) tel
, "perm =" <+> text (show perm)
, "ps =" <+> (text . show) ps
]
]
reportSDoc "interaction.case" 60 $ vcat
[ "splitting clause:"
, nest 2 $ vcat
[ "f =" <+> pretty f
, "context =" <+> ((inTopContext . pretty) =<< getContextTelescope)
, "tel =" <+> pretty tel
, "perm =" <+> (text . show) perm
, "ps =" <+> pretty ps
]
]
reportSDoc "interaction.case" 10 $ vcat
[ "splitting clause:"
, nest 2 $ vcat
[ "f =" <+> prettyTCM f
, "context =" <+> ((inTopContext . prettyTCM) =<< getContextTelescope)
, "tel =" <+> (inTopContext . prettyTCM) tel
, "perm =" <+> text (show perm)
, "ps =" <+> addContext tel (prettyTCMPatternList ps)
, "ell =" <+> text (show ell)
, "type =" <+> addContext tel (prettyTCM $ clauseType clause)
]
]
let vars = String -> [String]
words String
s
if concat vars == "." then do
cl <- makeAbstractClause f rhs NoEllipsis $ clauseToSplitClause clause
return (f, casectxt, [cl])
else if null vars then do
let postProjInExtLam = Bool
-> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (CaseContext -> Bool
forall a. Maybe a -> Bool
isJust CaseContext
casectxt) ((TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall a b. (a -> b) -> a -> b
$
(PragmaOptions -> PragmaOptions)
-> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
forall (m :: * -> *) a.
ReadTCState m =>
(PragmaOptions -> PragmaOptions) -> m a -> m a
withPragmaOptions ((PragmaOptions -> PragmaOptions)
-> TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> (PragmaOptions -> PragmaOptions)
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall a b. (a -> b) -> a -> b
$ Lens' PragmaOptions Bool -> LensSet PragmaOptions Bool
forall o i. Lens' o i -> LensSet o i
set ((WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions
lensOptPostfixProjections ((WithDefault 'True -> f (WithDefault 'True))
-> PragmaOptions -> f PragmaOptions)
-> ((Bool -> f Bool) -> WithDefault 'True -> f (WithDefault 'True))
-> (Bool -> f Bool)
-> PragmaOptions
-> f PragmaOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> f Bool) -> WithDefault 'True -> f (WithDefault 'True)
forall a (b :: Bool).
(Boolean a, Eq a, KnownBool b) =>
Lens' (WithDefault' a b) a
Lens' (WithDefault 'True) Bool
lensKeepDefault) Bool
True
(piTel, sc) <- insertTrailingArgs False $ clauseToSplitClause clause
newPats <- if null piTel then return False else do
imp <- optShowImplicit <$> pragmaOptions
return $ imp || any visible (telToList piTel)
scs <- if newPats then return [sc] else postProjInExtLam $ do
res <- splitResult f sc
case res of
Left SplitError
err -> do
let trailingPatVars :: [NamedArg DBPatVar]
trailingPatVars :: [NamedArg DBPatVar]
trailingPatVars = (Arg (Named_ DeBruijnPattern) -> Maybe (NamedArg DBPatVar))
-> NAPs -> [NamedArg DBPatVar]
forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust Arg (Named_ DeBruijnPattern) -> Maybe (NamedArg DBPatVar)
forall {name} {a}.
Arg (Named name (Pattern' a)) -> Maybe (Arg (Named name a))
isVarP (NAPs -> [NamedArg DBPatVar]) -> NAPs -> [NamedArg DBPatVar]
forall a b. (a -> b) -> a -> b
$ NAPs -> NAPs
forall a. [a] -> [a]
reverse NAPs
ps
isVarP :: Arg (Named name (Pattern' a)) -> Maybe (Arg (Named name a))
isVarP (Arg ArgInfo
ai (Named Maybe name
n (VarP PatternInfo
_ a
x))) = Arg (Named name a) -> Maybe (Arg (Named name a))
forall a. a -> Maybe a
Just (Arg (Named name a) -> Maybe (Arg (Named name a)))
-> Arg (Named name a) -> Maybe (Arg (Named name a))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Named name a -> Arg (Named name a)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Named name a -> Arg (Named name a))
-> Named name a -> Arg (Named name a)
forall a b. (a -> b) -> a -> b
$ Maybe name -> a -> Named name a
forall name a. Maybe name -> a -> Named name a
Named Maybe name
n a
x
isVarP Arg (Named name (Pattern' a))
_ = Maybe (Arg (Named name a))
forall a. Maybe a
Nothing
Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((NamedArg DBPatVar -> Bool) -> [NamedArg DBPatVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Origin
UserWritten Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
==) (Origin -> Bool)
-> (NamedArg DBPatVar -> Origin) -> NamedArg DBPatVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DBPatVar -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin) [NamedArg DBPatVar]
trailingPatVars) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError SplitError
err
let xs :: [Int]
xs = (NamedArg DBPatVar -> Int) -> [NamedArg DBPatVar] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (DBPatVar -> Int
dbPatVarIndex (DBPatVar -> Int)
-> (NamedArg DBPatVar -> DBPatVar) -> NamedArg DBPatVar -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DBPatVar -> DBPatVar
forall a. NamedArg a -> a
namedArg) [NamedArg DBPatVar]
trailingPatVars
[SplitClause] -> TCMT IO [SplitClause]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Int]
xs SplitClause
sc]
Right [SplitClause]
cov -> TCMT IO Bool
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
-> TCMT IO [SplitClause]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optCopatterns (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) TCMT IO [SplitClause]
forall {a}. TCMT IO a
failNoCop (TCMT IO [SplitClause] -> TCMT IO [SplitClause])
-> TCMT IO [SplitClause] -> TCMT IO [SplitClause]
forall a b. (a -> b) -> a -> b
$ do
[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
if null scs then
return [ A.spineToLhs $ absCl{ A.clauseRHS = makeRHSEmptyRecord rhs } ]
else mapM (makeAbstractClause f rhs ell) scs
else do
xs <- parseVariables f clauseCxt clauseAsBindings hole rng vars
reportSLn "interaction.case" 30 $ "parsedVariables: " ++ show (zip xs vars)
let (toShow, toSplit) = partitionEithers $ for (zip xs vars) $ \ ((Int
x,NameInScope
nis), String
s) ->
if (NameInScope
nis NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope) then Int -> Either Int Int
forall a b. a -> Either a b
Left Int
x else Int -> Either Int Int
forall a b. b -> Either a b
Right Int
x
let sc = [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [Int]
toShow (SplitClause -> SplitClause) -> SplitClause -> SplitClause
forall a b. (a -> b) -> a -> b
$ Clause -> SplitClause
clauseToSplitClause Clause
clause
scs <- split f toSplit sc
reportSLn "interaction.case" 70 $ "makeCase: survived the splitting"
let splitNames = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name) -> (Name, Type) -> Name
forall a b. (a -> b) -> a -> b
$ Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type) -> (Name, Type)
forall a b. (a -> b) -> a -> b
$ Context
clauseCxt Context -> Int -> Dom' Term (Name, Type)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i) [Int]
toSplit
shouldExpandEllipsis <- return (not $ null toShow) `or2M` anyEllipsisVar f absCl splitNames
let ell' | Bool
shouldExpandEllipsis = ExpandedEllipsis
NoEllipsis
| Bool
otherwise = ExpandedEllipsis
ell
let sclause = Clause -> SplitClause
clauseToSplitClause Clause
clause
fcs <- filterM (\ Clause
cl -> (QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause
clause] (Clause -> SplitClause
clauseToSplitClause Clause
cl)) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
(Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> [Clause] -> SplitClause -> TCMT IO Bool
isCovered QName
f [Clause
cl] SplitClause
sclause))
follClauses
scs <- filterM (not <.> isCovered f (prevClauses ++ fcs) . fst) scs
reportSLn "interaction.case" 70 $ "makeCase: survived filtering out already covered clauses"
cs <- catMaybes <$> do
forM scs $ \ (SplitClause
sc, Bool
isAbsurd) -> if Bool
isAbsurd
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
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
isEmptyTel (SplitClause -> Telescope
scTel SplitClause
sc))
(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)
(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"
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 = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
String
"OPTION --copatterns needed to split on result here"
split :: QName -> [Nat] -> SplitClause -> TCM [(SplitClause, Bool)]
split :: QName -> [Int] -> SplitClause -> TCM [(SplitClause, Bool)]
split QName
f [] SplitClause
clause = [(SplitClause, Bool)] -> TCM [(SplitClause, Bool)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitClause
clause,Bool
False)]
split QName
f (Int
var : [Int]
vars) SplitClause
clause = do
z <- TCMT IO (Either SplitError (Either SplitClause Covering))
-> TCMT IO (Either SplitError (Either SplitClause Covering))
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCMT IO (Either SplitError (Either SplitClause Covering))
-> TCMT IO (Either SplitError (Either SplitClause Covering)))
-> TCMT IO (Either SplitError (Either SplitClause Covering))
-> TCMT IO (Either SplitError (Either SplitClause Covering))
forall a b. (a -> b) -> a -> b
$ SplitClause
-> Int -> TCMT IO (Either SplitError (Either SplitClause Covering))
splitClauseWithAbsurd SplitClause
clause Int
var
case z of
Left SplitError
err -> TypeError -> TCM [(SplitClause, Bool)]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [(SplitClause, Bool)])
-> TypeError -> TCM [(SplitClause, Bool)]
forall a b. (a -> b) -> a -> b
$ SplitError -> TypeError
SplitError SplitError
err
Right (Left SplitClause
cl) -> [(SplitClause, Bool)] -> TCM [(SplitClause, Bool)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(SplitClause
cl,Bool
True)]
Right (Right Covering
cov) -> [[(SplitClause, Bool)]] -> [(SplitClause, Bool)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(SplitClause, Bool)]] -> [(SplitClause, Bool)])
-> TCMT IO [[(SplitClause, Bool)]] -> TCM [(SplitClause, Bool)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[SplitClause]
-> (SplitClause -> TCM [(SplitClause, Bool)])
-> TCMT IO [[(SplitClause, Bool)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Covering -> [SplitClause]
splitClauses Covering
cov) ((SplitClause -> TCM [(SplitClause, Bool)])
-> TCMT IO [[(SplitClause, Bool)]])
-> (SplitClause -> TCM [(SplitClause, Bool)])
-> TCMT IO [[(SplitClause, Bool)]]
forall a b. (a -> b) -> a -> b
$ \ SplitClause
cl ->
QName -> [Int] -> SplitClause -> TCM [(SplitClause, Bool)]
split QName
f ((Int -> Maybe Int) -> [Int] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> Prefix b
mapMaybe (SplitClause -> Int -> Maybe Int
newVar SplitClause
cl) [Int]
vars) SplitClause
cl
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
checkClauseIsClean :: IPClause -> TCM ()
checkClauseIsClean :: IPClause -> TCMT IO ()
checkClauseIsClean IPClause
ipCl = do
sips <- (InteractionPoint -> Bool)
-> [InteractionPoint] -> [InteractionPoint]
forall a. (a -> Bool) -> [a] -> [a]
filter InteractionPoint -> Bool
ipSolved ([InteractionPoint] -> [InteractionPoint])
-> (BiMap InteractionId InteractionPoint -> [InteractionPoint])
-> BiMap InteractionId InteractionPoint
-> [InteractionPoint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BiMap InteractionId InteractionPoint -> [InteractionPoint]
forall k v. BiMap k v -> [v]
BiMap.elems (BiMap InteractionId InteractionPoint -> [InteractionPoint])
-> TCMT IO (BiMap InteractionId InteractionPoint)
-> TCMT IO [InteractionPoint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (BiMap InteractionId InteractionPoint)
-> TCMT IO (BiMap InteractionId InteractionPoint)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (BiMap InteractionId InteractionPoint
-> f (BiMap InteractionId InteractionPoint))
-> TCState -> f TCState
Lens' TCState (BiMap InteractionId InteractionPoint)
stInteractionPoints
when (List.any ((== ipCl) . ipClause) sips) $
typeError $ GenericError $ "Cannot split as clause rhs has been refined. Please reload"
makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause
makePatternVarsVisible :: [Int] -> SplitClause -> SplitClause
makePatternVarsVisible [] SplitClause
sc = SplitClause
sc
makePatternVarsVisible [Int]
is sc :: SplitClause
sc@SClause{ scPats :: SplitClause -> [NamedArg SplitPattern]
scPats = [NamedArg SplitPattern]
ps } =
SplitClause
sc{ scPats = mapNamedArgPattern mkVis ps }
where
mkVis :: NamedArg SplitPattern -> NamedArg SplitPattern
mkVis :: NamedArg SplitPattern -> NamedArg SplitPattern
mkVis (Arg ArgInfo
ai (Named Maybe NamedName
n (VarP PatternInfo
o (SplitPatVar String
x Int
i [Literal]
ls))))
| Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
is =
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
makeRHSEmptyRecord :: A.RHS -> A.RHS
makeRHSEmptyRecord :: RHS -> RHS
makeRHSEmptyRecord = \case
A.RHS{} -> A.RHS{ rhsExpr :: Expr
rhsExpr = ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
forall a. Null a => a
empty RecordAssigns
forall a. Null a => a
empty, rhsConcrete :: Maybe Expr
rhsConcrete = Maybe Expr
forall a. Maybe a
Nothing }
rhs :: RHS
rhs@A.RewriteRHS{} -> RHS
rhs{ A.rewriteRHS = makeRHSEmptyRecord $ A.rewriteRHS rhs }
RHS
A.AbsurdRHS -> RHS
forall a. HasCallStack => a
__IMPOSSIBLE__
A.WithRHS{} -> RHS
forall a. HasCallStack => a
__IMPOSSIBLE__
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell (SClause Telescope
tel [NamedArg SplitPattern]
sps SplitPSubstitution
_ Map CheckpointId Substitution
_ Maybe (Dom' Term Type)
t) = do
let ps :: NAPs
ps = [NamedArg SplitPattern] -> NAPs
fromSplitPatterns [NamedArg SplitPattern]
sps
String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"interaction.case" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Interaction.MakeCase.makeAbsurdClause: split clause:"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do (TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc)
-> (Telescope -> TCMT IO Doc) -> Telescope -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM) (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (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
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
, TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ NAPs -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => NAPs -> m Doc
prettyTCMPatternList NAPs
ps
, TCMT IO Doc
"ell =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (ExpandedEllipsis -> String
forall a. Show a => a -> String
show ExpandedEllipsis
ell)
]
]
ModuleName -> TCM Clause -> TCM Clause
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (QName -> ModuleName
qnameModule QName
f) (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$
TCM Clause -> TCM Clause
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Clause -> TCM Clause) -> TCM Clause -> TCM Clause
forall a b. (a -> b) -> a -> b
$ QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
QNamed Clause -> m (ReifiesTo (QNamed Clause))
reify (QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause)))
-> QNamed Clause -> TCMT IO (ReifiesTo (QNamed Clause))
forall a b. (a -> b) -> a -> b
$ QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
f (Clause -> QNamed Clause) -> Clause -> QNamed Clause
forall a b. (a -> b) -> a -> b
$ Clause
{ clauseLHSRange :: Range
clauseLHSRange = Range
forall a. Range' a
noRange
, clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
, clauseTel :: Telescope
clauseTel = Telescope
tel
, namedClausePats :: NAPs
namedClausePats = NAPs
ps
, clauseBody :: Maybe Term
clauseBody = Maybe Term
forall a. Maybe a
Nothing
, clauseType :: Maybe (Arg Type)
clauseType = Dom' Term Type -> Arg Type
forall t a. Dom' t a -> Arg a
argFromDom (Dom' Term Type -> Arg Type)
-> Maybe (Dom' Term Type) -> Maybe (Arg Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Dom' Term Type)
t
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = Maybe Bool
forall a. Maybe a
Nothing
, clauseRecursive :: Maybe Bool
clauseRecursive = Maybe Bool
forall a. Maybe a
Nothing
, clauseUnreachable :: Maybe Bool
clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
ell
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
}
makeAbstractClause :: QName -> A.RHS -> ExpandedEllipsis -> SplitClause -> TCM A.Clause
makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbstractClause QName
f RHS
rhs ExpandedEllipsis
ell SplitClause
cl = do
lhs <- Clause -> LHS
forall lhs. Clause' lhs -> lhs
A.clauseLHS (Clause -> LHS) -> TCM Clause -> TCMT IO LHS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
makeAbsurdClause QName
f ExpandedEllipsis
ell SplitClause
cl
reportSDoc "interaction.case" 60 $ "reified lhs: " <+> prettyA lhs
return $ A.Clause lhs [] rhs A.noWhereDecls 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