{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Monad.MetaVars where
import Prelude hiding (null)
import Control.Monad ( (<=<), forM_, guard )
import Control.Monad.Except ( MonadError )
import Control.Monad.State ( StateT, execStateT, get, put )
import Control.Monad.Trans ( MonadTrans, lift )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Reader ( ReaderT(ReaderT), runReaderT )
import Control.Monad.Writer ( WriterT, execWriterT, tell )
import Control.Monad.Fail (MonadFail)
import qualified Data.HashMap.Strict as HMap
import qualified Data.List as List
import qualified Data.Map.Strict as MapS
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import GHC.Stack (HasCallStack)
import Agda.Syntax.Common
import Agda.Syntax.Info ( MetaKind (InstanceMeta, UnificationMeta), MetaNameSuggestion )
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin (HasBuiltins)
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Constraints (MonadConstraint(..))
import Agda.TypeChecking.Monad.Debug
(MonadDebug, reportSLn, __IMPOSSIBLE_VERBOSE__)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Signature (HasConstInfo)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Substitute
import {-# SOURCE #-} Agda.TypeChecking.Telescope
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Lens
import Agda.Utils.List (nubOn)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Tuple
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Impossible
data MetaClass =
Records
| SingletonRecords
| Levels
deriving (MetaClass -> MetaClass -> Bool
(MetaClass -> MetaClass -> Bool)
-> (MetaClass -> MetaClass -> Bool) -> Eq MetaClass
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaClass -> MetaClass -> Bool
== :: MetaClass -> MetaClass -> Bool
$c/= :: MetaClass -> MetaClass -> Bool
/= :: MetaClass -> MetaClass -> Bool
Eq, Int -> MetaClass
MetaClass -> Int
MetaClass -> [MetaClass]
MetaClass -> MetaClass
MetaClass -> MetaClass -> [MetaClass]
MetaClass -> MetaClass -> MetaClass -> [MetaClass]
(MetaClass -> MetaClass)
-> (MetaClass -> MetaClass)
-> (Int -> MetaClass)
-> (MetaClass -> Int)
-> (MetaClass -> [MetaClass])
-> (MetaClass -> MetaClass -> [MetaClass])
-> (MetaClass -> MetaClass -> [MetaClass])
-> (MetaClass -> MetaClass -> MetaClass -> [MetaClass])
-> Enum MetaClass
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: MetaClass -> MetaClass
succ :: MetaClass -> MetaClass
$cpred :: MetaClass -> MetaClass
pred :: MetaClass -> MetaClass
$ctoEnum :: Int -> MetaClass
toEnum :: Int -> MetaClass
$cfromEnum :: MetaClass -> Int
fromEnum :: MetaClass -> Int
$cenumFrom :: MetaClass -> [MetaClass]
enumFrom :: MetaClass -> [MetaClass]
$cenumFromThen :: MetaClass -> MetaClass -> [MetaClass]
enumFromThen :: MetaClass -> MetaClass -> [MetaClass]
$cenumFromTo :: MetaClass -> MetaClass -> [MetaClass]
enumFromTo :: MetaClass -> MetaClass -> [MetaClass]
$cenumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass]
enumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass]
Enum, MetaClass
MetaClass -> MetaClass -> Bounded MetaClass
forall a. a -> a -> Bounded a
$cminBound :: MetaClass
minBound :: MetaClass
$cmaxBound :: MetaClass
maxBound :: MetaClass
Bounded, Int -> MetaClass -> [Char] -> [Char]
[MetaClass] -> [Char] -> [Char]
MetaClass -> [Char]
(Int -> MetaClass -> [Char] -> [Char])
-> (MetaClass -> [Char])
-> ([MetaClass] -> [Char] -> [Char])
-> Show MetaClass
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> MetaClass -> [Char] -> [Char]
showsPrec :: Int -> MetaClass -> [Char] -> [Char]
$cshow :: MetaClass -> [Char]
show :: MetaClass -> [Char]
$cshowList :: [MetaClass] -> [Char] -> [Char]
showList :: [MetaClass] -> [Char] -> [Char]
Show)
allMetaClasses :: [MetaClass]
allMetaClasses :: [MetaClass]
allMetaClasses = [MetaClass
forall a. Bounded a => a
minBound .. MetaClass
forall a. Bounded a => a
maxBound]
data KeepMetas = KeepMetas | RollBackMetas
class ( MonadConstraint m
, MonadReduce m
, MonadAddContext m
, MonadTCEnv m
, ReadTCState m
, HasBuiltins m
, HasConstInfo m
, MonadDebug m
) => MonadMetaSolver m where
newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
Judgement a -> m MetaId
assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
etaExpandMeta :: [MetaClass] -> MetaId -> m ()
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()
speculateMetas :: m () -> m KeepMetas -> m ()
instance MonadMetaSolver m => MonadMetaSolver (ReaderT r m) where
newMeta' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> ReaderT r m MetaId
newMeta' MetaInstantiation
inst Frozen
f MetaInfo
i MetaPriority
p Permutation
perm Judgement a
j = m MetaId -> ReaderT r m MetaId
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m MetaId -> ReaderT r m MetaId) -> m MetaId -> ReaderT r m MetaId
forall a b. (a -> b) -> a -> b
$ MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
inst Frozen
f MetaInfo
i MetaPriority
p Permutation
perm Judgement a
j
assignV :: CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> ReaderT r m ()
assignV CompareDirection
dir MetaId
m Args
us Term
v CompareAs
cmp = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignV CompareDirection
dir MetaId
m Args
us Term
v CompareAs
cmp
assignTerm' :: MonadMetaSolver (ReaderT r m) =>
MetaId -> [Arg [Char]] -> Term -> ReaderT r m ()
assignTerm' MetaId
m [Arg [Char]]
us Term
v = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg [Char]] -> Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
m [Arg [Char]]
us Term
v
etaExpandMeta :: [MetaClass] -> MetaId -> ReaderT r m ()
etaExpandMeta [MetaClass]
k MetaId
m = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ [MetaClass] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaClass] -> MetaId -> m ()
etaExpandMeta [MetaClass]
k MetaId
m
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> ReaderT r m ()
updateMetaVar MetaId
m MetaVariable -> MetaVariable
f = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m MetaVariable -> MetaVariable
f
speculateMetas :: ReaderT r m () -> ReaderT r m KeepMetas -> ReaderT r m ()
speculateMetas ReaderT r m ()
fallback ReaderT r m KeepMetas
m = (r -> m ()) -> ReaderT r m ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m ()) -> ReaderT r m ()) -> (r -> m ()) -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ \r
x -> m () -> m KeepMetas -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
m () -> m KeepMetas -> m ()
speculateMetas (ReaderT r m () -> r -> m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m ()
fallback r
x) (ReaderT r m KeepMetas -> r -> m KeepMetas
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m KeepMetas
m r
x)
dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
dontAssignMetas :: forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas m a
cont = do
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta" Int
45 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"don't assign metas"
(TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
env -> TCEnv
env { envAssignMetas = False }) m a
cont
isRemoteMeta :: ReadTCState m => m (MetaId -> Bool)
isRemoteMeta :: forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta = do
h <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
return (\MetaId
m -> ModuleNameHash
h ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
/= MetaId -> ModuleNameHash
metaModule MetaId
m)
nextLocalMeta :: ReadTCState m => m MetaId
nextLocalMeta :: forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta = Lens' TCState MetaId -> m MetaId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (MetaId -> f MetaId) -> TCState -> f TCState
Lens' TCState MetaId
stFreshMetaId
data LocalMetaStores = LocalMetaStores
{ LocalMetaStores -> LocalMetaStore
openMetas :: LocalMetaStore
, LocalMetaStores -> LocalMetaStore
solvedMetas :: LocalMetaStore
}
metasCreatedBy ::
forall m a. ReadTCState m => m a -> m (a, LocalMetaStores)
metasCreatedBy :: forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy m a
m = do
!nextMeta <- m MetaId
forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta
a <- m
os <- created stOpenMetaStore nextMeta
ss <- created stSolvedMetaStore nextMeta
return (a, LocalMetaStores { openMetas = os, solvedMetas = ss })
where
created :: Lens' TCState LocalMetaStore -> MetaId -> m LocalMetaStore
created :: Lens' TCState LocalMetaStore -> MetaId -> m LocalMetaStore
created Lens' TCState LocalMetaStore
store MetaId
next = do
ms <- Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
store
return $ case MapS.splitLookup next ms of
(LocalMetaStore
_, Maybe MetaVariable
Nothing, LocalMetaStore
ms) -> LocalMetaStore
ms
(LocalMetaStore
_, Just MetaVariable
m, LocalMetaStore
ms) -> MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
next MetaVariable
m LocalMetaStore
ms
lookupLocalMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m = do
mv <- LocalMetaStore -> Maybe MetaVariable
lkup (LocalMetaStore -> Maybe MetaVariable)
-> m LocalMetaStore -> m (Maybe MetaVariable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stSolvedMetaStore
case mv of
mv :: Maybe MetaVariable
mv@Just{} -> Maybe MetaVariable -> m (Maybe MetaVariable)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe MetaVariable
mv
Maybe MetaVariable
Nothing -> LocalMetaStore -> Maybe MetaVariable
lkup (LocalMetaStore -> Maybe MetaVariable)
-> m LocalMetaStore -> m (Maybe MetaVariable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
where
lkup :: LocalMetaStore -> Maybe MetaVariable
lkup = MetaId -> LocalMetaStore -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m
lookupLocalMeta ::
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m =
m MetaVariable -> m (Maybe MetaVariable) -> m MetaVariable
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM ([Char] -> m MetaVariable
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
err) (m (Maybe MetaVariable) -> m MetaVariable)
-> m (Maybe MetaVariable) -> m MetaVariable
forall a b. (a -> b) -> a -> b
$ MetaId -> m (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
where
err :: [Char]
err = [Char]
"no such local meta-variable " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m
{-# SPECIALIZE lookupMeta :: MetaId -> TCM (Maybe (Either RemoteMetaVariable MetaVariable)) #-}
lookupMeta ::
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m = do
mv <- MetaId -> m (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
case mv of
Just MetaVariable
mv -> Maybe (Either RemoteMetaVariable MetaVariable)
-> m (Maybe (Either RemoteMetaVariable MetaVariable))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either RemoteMetaVariable MetaVariable
-> Maybe (Either RemoteMetaVariable MetaVariable)
forall a. a -> Maybe a
Just (MetaVariable -> Either RemoteMetaVariable MetaVariable
forall a b. b -> Either a b
Right MetaVariable
mv))
Maybe MetaVariable
Nothing -> (RemoteMetaVariable -> Either RemoteMetaVariable MetaVariable)
-> Maybe RemoteMetaVariable
-> Maybe (Either RemoteMetaVariable MetaVariable)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RemoteMetaVariable -> Either RemoteMetaVariable MetaVariable
forall a b. a -> Either a b
Left (Maybe RemoteMetaVariable
-> Maybe (Either RemoteMetaVariable MetaVariable))
-> (HashMap MetaId RemoteMetaVariable -> Maybe RemoteMetaVariable)
-> HashMap MetaId RemoteMetaVariable
-> Maybe (Either RemoteMetaVariable MetaVariable)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId
-> HashMap MetaId RemoteMetaVariable -> Maybe RemoteMetaVariable
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup MetaId
m (HashMap MetaId RemoteMetaVariable
-> Maybe (Either RemoteMetaVariable MetaVariable))
-> m (HashMap MetaId RemoteMetaVariable)
-> m (Maybe (Either RemoteMetaVariable MetaVariable))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (HashMap MetaId RemoteMetaVariable)
-> m (HashMap MetaId RemoteMetaVariable)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (HashMap MetaId RemoteMetaVariable
-> f (HashMap MetaId RemoteMetaVariable))
-> TCState -> f TCState
Lens' TCState (HashMap MetaId RemoteMetaVariable)
stImportedMetaStore
{-# SPECIALIZE lookupMetaInstantiation :: MetaId -> TCM MetaInstantiation #-}
lookupMetaInstantiation ::
ReadTCState m => MetaId -> m MetaInstantiation
lookupMetaInstantiation :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m = do
mi <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
case mi of
Just (Left RemoteMetaVariable
mv) -> MetaInstantiation -> m MetaInstantiation
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Instantiation -> MetaInstantiation
InstV (Instantiation -> MetaInstantiation)
-> Instantiation -> MetaInstantiation
forall a b. (a -> b) -> a -> b
$ RemoteMetaVariable -> Instantiation
rmvInstantiation RemoteMetaVariable
mv)
Just (Right MetaVariable
mv) -> MetaInstantiation -> m MetaInstantiation
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> m MetaInstantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
lookupMetaJudgement :: ReadTCState m => MetaId -> m (Judgement MetaId)
lookupMetaJudgement :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m = do
mi <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
case mi of
Just (Left RemoteMetaVariable
mv) -> Judgement MetaId -> m (Judgement MetaId)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RemoteMetaVariable -> Judgement MetaId
rmvJudgement RemoteMetaVariable
mv)
Just (Right MetaVariable
mv) -> Judgement MetaId -> m (Judgement MetaId)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> m (Judgement MetaId)
forall a. HasCallStack => a
__IMPOSSIBLE__
lookupMetaModality :: ReadTCState m => MetaId -> m Modality
lookupMetaModality :: forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m = do
mi <- MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
case mi of
Just (Left RemoteMetaVariable
mv) -> Modality -> m Modality
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RemoteMetaVariable -> Modality
rmvModality RemoteMetaVariable
mv)
Just (Right MetaVariable
mv) -> Modality -> m Modality
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality MetaVariable
mv)
Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> m Modality
forall a. HasCallStack => a
__IMPOSSIBLE__
{-# INLINE metaType #-}
metaType :: ReadTCState m => MetaId -> m Type
metaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> m (Judgement MetaId) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Judgement MetaId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
x
updateMetaVarTCM ::
HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM :: HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
m MetaVariable -> MetaVariable
f = do
mv <- MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
case mv of
Maybe MetaVariable
Nothing -> do
mv <- MetaId -> TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
case mv of
Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> [Char] -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__
([Char]
"Meta-variable not found: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m)
Just{} -> [Char] -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__
([Char]
"Attempt to update remote meta-variable: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m)
Just MetaVariable
mv -> do
let mv' :: MetaVariable
mv' = MetaVariable -> MetaVariable
f MetaVariable
mv
insert :: Lens' TCState LocalMetaStore -> TCM ()
insert = (Lens' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m MetaVariable
mv')
delete :: Lens' TCState LocalMetaStore -> TCM ()
delete = (Lens' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` MetaId -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> Map k a -> Map k a
MapS.delete MetaId
m)
case ( MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
, MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv')
) of
(Bool
True, Bool
True) -> Lens' TCState LocalMetaStore -> TCM ()
insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
(Bool
False, Bool
False) -> Lens' TCState LocalMetaStore -> TCM ()
insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stSolvedMetaStore
(Bool
True, Bool
False) -> do
Lens' TCState LocalMetaStore -> TCM ()
delete (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
Lens' TCState LocalMetaStore -> TCM ()
insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stSolvedMetaStore
(Bool
False, Bool
True) -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
m MetaVariable
mv
| MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv) = Lens' TCState LocalMetaStore -> TCM ()
insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
| Bool
otherwise = Lens' TCState LocalMetaStore -> TCM ()
insert (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stSolvedMetaStore
where
insert :: Lens' TCState LocalMetaStore -> TCM ()
insert = (Lens' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m MetaVariable
mv)
{-# INLINE getMetaPriority #-}
getMetaPriority ::
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaPriority
getMetaPriority :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaPriority
getMetaPriority = MetaVariable -> MetaPriority
mvPriority (MetaVariable -> MetaPriority)
-> (MetaId -> m MetaVariable) -> MetaId -> m MetaPriority
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta
isSortMeta :: ReadTCState m => MetaId -> m Bool
isSortMeta :: forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
isSortMeta MetaId
m = Judgement MetaId -> Bool
forall a. Judgement a -> Bool
isSortJudgement (Judgement MetaId -> Bool) -> m (Judgement MetaId) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Judgement MetaId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ MetaVariable
mv = Judgement MetaId -> Bool
forall a. Judgement a -> Bool
isSortJudgement (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
isSortJudgement :: Judgement a -> Bool
isSortJudgement :: forall a. Judgement a -> Bool
isSortJudgement HasType{} = Bool
False
isSortJudgement IsSort{} = Bool
True
metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
metaInstantiationToMetaKind = \case
OpenMeta MetaKind
k -> MetaKind
k
InstV{} -> MetaKind
forall a. Null a => a
empty
BlockedConst{} -> MetaKind
forall a. Null a => a
empty
PostponedTypeCheckingProblem{} -> MetaKind
forall a. Null a => a
empty
{-# SPECIALIZE getMetaType :: MetaId -> TCM Type #-}
getMetaType :: ReadTCState m => MetaId -> m Type
getMetaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m = do
j <- MetaId -> m (Judgement MetaId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m
return $ case j of
HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type
t
IsSort{} -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__
{-# SPECIALIZE getMetaContextArgs :: MetaVariable -> TCM Args #-}
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs :: forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVar{ mvPermutation :: MetaVariable -> Permutation
mvPermutation = Permutation
p } = do
args <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
return $ permute (takeP (length args) p) args
{-# SPECIALIZE getMetaTypeInContext :: MetaId -> TCM Type #-}
getMetaTypeInContext ::
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext :: forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m = do
mv@MetaVar{ mvJudgement = j } <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
case j of
HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> m Type
piApplyM Type
t (Args -> m Type) -> m Args -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaVariable -> m Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
IsSort{} -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__
{-# SPECIALIZE isGeneralizableMeta :: MetaId -> TCM DoGeneralize #-}
isGeneralizableMeta ::
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta MetaId
x =
Arg DoGeneralize -> DoGeneralize
forall e. Arg e -> e
unArg (Arg DoGeneralize -> DoGeneralize)
-> (MetaVariable -> Arg DoGeneralize)
-> MetaVariable
-> DoGeneralize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaInfo -> Arg DoGeneralize)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Arg DoGeneralize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> DoGeneralize) -> m MetaVariable -> m DoGeneralize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
class IsInstantiatedMeta a where
isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool
{-# SPECIALIZE isInstantiatedMeta :: Term -> TCM Bool #-}
{-# SPECIALIZE isInstantiatedMeta :: Type -> TCM Bool #-}
instance IsInstantiatedMeta MetaId where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
m = Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Maybe Term)
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
m
instance IsInstantiatedMeta Term where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Term -> m Bool
isInstantiatedMeta = Term -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Term -> m Bool
loop where
loop :: Term -> m Bool
loop Term
v =
case Term
v of
MetaV MetaId
x [Elim]
_ -> MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
x
DontCare Term
v -> Term -> m Bool
loop Term
v
Level Level
l -> Level -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Level -> m Bool
isInstantiatedMeta Level
l
Lam ArgInfo
_ Abs Term
b -> Abs Term -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Abs Term -> m Bool
isInstantiatedMeta Abs Term
b
Con ConHead
_ ConInfo
_ [Elim]
es | Just Args
vs <- [Elim] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es -> Args -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Args -> m Bool
isInstantiatedMeta Args
vs
Term
_ -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta Level where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Level -> m Bool
isInstantiatedMeta (Max Integer
n [PlusLevel' Term]
ls) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = [PlusLevel' Term] -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
[PlusLevel' Term] -> m Bool
isInstantiatedMeta [PlusLevel' Term]
ls
isInstantiatedMeta Level
_ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta PlusLevel where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
PlusLevel' Term -> m Bool
isInstantiatedMeta (Plus Integer
n Term
l) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Term -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Term -> m Bool
isInstantiatedMeta Term
l
isInstantiatedMeta PlusLevel' Term
_ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
isInstantiatedMeta :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => [a] -> m Bool
isInstantiatedMeta = [m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Bool) -> [a] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *). (MonadFail m, ReadTCState m) => a -> m Bool
isInstantiatedMeta
instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Maybe a -> m Bool
isInstantiatedMeta = [a] -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *). (MonadFail m, ReadTCState m) => [a] -> m Bool
isInstantiatedMeta ([a] -> m Bool) -> (Maybe a -> [a]) -> Maybe a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList
instance IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Arg a -> m Bool
isInstantiatedMeta = a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *). (MonadFail m, ReadTCState m) => a -> m Bool
isInstantiatedMeta (a -> m Bool) -> (Arg a -> a) -> Arg a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg
instance IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Abs a -> m Bool
isInstantiatedMeta = a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *). (MonadFail m, ReadTCState m) => a -> m Bool
isInstantiatedMeta (a -> m Bool) -> (Abs a -> a) -> Abs a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs a -> a
forall a. Abs a -> a
unAbs
{-# SPECIALIZE isInstantiatedMeta' :: MetaId -> TCM (Maybe Term) #-}
isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
isInstantiatedMeta' :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
m = do
inst <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
return $ case inst of
InstV Instantiation
inst -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
mkLam (Instantiation -> Term
instBody Instantiation
inst) (Instantiation -> [Arg [Char]]
instTel Instantiation
inst)
MetaInstantiation
_ -> Maybe Term
forall a. Maybe a
Nothing
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas = \case
ValueCmp Comparison
_ CompareAs
_ Term
u Term
v -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> (Term, Term) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
u, Term
v)
ValueCmpOnFace Comparison
_ Term
p Type
_ Term
u Term
v -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term, Term) -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> (Term, Term, Term) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
p, Term
u, Term
v)
ElimCmp [Polarity]
_ [IsForced]
_ Type
_ Term
_ [Elim]
es [Elim]
es' -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> ([Elim], [Elim]) -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> ([Elim], [Elim]) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton ([Elim]
es, [Elim]
es')
LevelCmp Comparison
_ Level
l Level
l' -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> (Term, Term) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Level -> Term
Level Level
l, Level -> Term
Level Level
l')
UnquoteTactic Term
t Term
h Type
g -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term, Type) -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> (Term, Term, Type) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
t, Term
h, Type
g)
SortCmp Comparison
_ Sort
s1 Sort
s2 -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> (Term, Term) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)
UnBlock MetaId
x -> MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => a -> Set a -> Set a
Set.insert MetaId
x (Set MetaId -> Set MetaId)
-> ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId)
-> TCMT IO [Set MetaId] -> TCM (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Listener -> TCM (Set MetaId))
-> [Listener] -> TCMT IO [Set MetaId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Listener -> TCM (Set MetaId)
listenerMetas ([Listener] -> TCMT IO [Set MetaId])
-> TCMT IO [Listener] -> TCMT IO [Set MetaId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO [Listener]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
x)
FindInstance MetaId
x Maybe [Candidate]
_ ->
TCMT IO (Maybe Term)
-> TCM (Set MetaId)
-> (Term -> TCM (Set MetaId))
-> TCM (Set MetaId)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (MetaId -> TCMT IO (Maybe Term)
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
x) (Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
x) ((Term -> TCM (Set MetaId)) -> TCM (Set MetaId))
-> (Term -> TCM (Set MetaId)) -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId))
-> (Term -> Set MetaId) -> Term -> TCM (Set MetaId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Set MetaId) -> Term -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Term -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton
ResolveInstanceHead{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
IsEmpty{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckFunDef{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckSizeLtSat{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
HasBiggerSort{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
HasPTSRule{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckDataSort{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckMetaInst MetaId
x -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckType Type
t -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> Type -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Type -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton Type
t
CheckLockedVars Term
a Type
b Arg Term
c Type
d -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId)
-> (Term, Type, Arg Term, Type) -> Set MetaId
forall m.
Monoid m =>
(MetaId -> m) -> (Term, Type, Arg Term, Type) -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
a, Type
b, Arg Term
c, Type
d)
UsableAtModality{} -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
where
listenerMetas :: Listener -> TCM (Set MetaId)
listenerMetas EtaExpand{} = Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Set a
Set.empty
listenerMetas (CheckConstraint Int
_ ProblemConstraint
c) = Constraint -> TCM (Set MetaId)
constraintMetas (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c)
createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo :: forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo = RunMetaOccursCheck -> m MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
RunMetaOccursCheck
createMetaInfo'
:: (MonadTCEnv m, ReadTCState m)
=> RunMetaOccursCheck -> m MetaInfo
createMetaInfo' :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b = do
r <- m Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange
cl <- buildClosure r
gen <- viewTC eGeneralizeMetas
modality <- currentModality
return MetaInfo
{ miClosRange = cl
, miModality = modality
, miMetaOccursCheck = b
, miNameSuggestion = ""
, miGeneralizable = defaultArg gen
}
setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
setValueMetaName :: forall (m :: * -> *). MonadMetaSolver m => Term -> [Char] -> m ()
setValueMetaName Term
v [Char]
s = do
case Term
v of
MetaV MetaId
mi [Elim]
_ -> MetaId -> [Char] -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s
Term
u -> do
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.name" Int
70 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
[Char]
"cannot set meta name; newMeta returns " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Show a => a -> [Char]
show Term
u
() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getMetaNameSuggestion ::
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaNameSuggestion
getMetaNameSuggestion :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Char]
getMetaNameSuggestion MetaId
mi =
MetaInfo -> [Char]
miNameSuggestion (MetaInfo -> [Char])
-> (MetaVariable -> MetaInfo) -> MetaVariable -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> [Char]) -> m MetaVariable -> m [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaNameSuggestion :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Char] -> Bool
forall a. Null a => a -> Bool
null [Char]
s Bool -> Bool -> Bool
|| [Char] -> Bool
forall a. Underscore a => a -> Bool
isUnderscore [Char]
s) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.name" Int
20 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
[Char]
"setting name of meta " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
mi [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
MetaVariable
mvar { mvInfo = (mvInfo mvar) { miNameSuggestion = s }}
setMetaGeneralizableArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo MetaId
m ArgInfo
i = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
MetaVariable
mv { mvInfo = (mvInfo mv)
{ miGeneralizable = setArgInfo i (miGeneralizable (mvInfo mv)) } }
updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mi Range
r = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi (Range -> MetaVariable -> MetaVariable
forall a. SetRange a => Range -> a -> a
setRange Range
r)
setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck MetaId
mi RunMetaOccursCheck
b = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
MetaVariable
mvar { mvInfo = (mvInfo mvar) { miMetaOccursCheck = b } }
class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
freshInteractionId :: m InteractionId
default freshInteractionId
:: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
=> m InteractionId
freshInteractionId = n InteractionId -> t n InteractionId
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
default modifyInteractionPoints
:: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
=> (InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints = n () -> m ()
n () -> t n ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n () -> m ())
-> ((InteractionPoints -> InteractionPoints) -> n ())
-> (InteractionPoints -> InteractionPoints)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoints -> InteractionPoints) -> n ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints
instance MonadInteractionPoints m => MonadInteractionPoints (IdentityT m)
instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)
instance MonadInteractionPoints m => MonadInteractionPoints (StateT s m)
instance MonadInteractionPoints TCM where
freshInteractionId :: TCM InteractionId
freshInteractionId = TCM InteractionId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
f = (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints Lens' TCState InteractionPoints
-> (InteractionPoints -> InteractionPoints) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` InteractionPoints -> InteractionPoints
f
registerInteractionPoint
:: forall m. MonadInteractionPoints m
=> Bool -> Range -> Maybe Nat -> m InteractionId
registerInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Int -> m InteractionId
registerInteractionPoint Bool
preciseRange Range
r Maybe Int
maybeId = do
m <- Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
if not preciseRange || isJust maybeId then continue m else do
Strict.caseMaybe (rangeFile r) (continue m) $ \ RangeFile
_ -> do
Maybe InteractionId
-> m InteractionId
-> (InteractionId -> m InteractionId)
-> m InteractionId
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Range -> InteractionPoints -> Maybe InteractionId
findInteractionPoint_ Range
r InteractionPoints
m) (InteractionPoints -> m InteractionId
continue InteractionPoints
m) InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
where
continue :: InteractionPoints -> m InteractionId
continue :: InteractionPoints -> m InteractionId
continue InteractionPoints
m = do
ii <- case Maybe Int
maybeId of
Just Int
i -> InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (InteractionId -> m InteractionId)
-> InteractionId -> m InteractionId
forall a b. (a -> b) -> a -> b
$ Int -> InteractionId
InteractionId Int
i
Maybe Int
Nothing -> m InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
let ip = InteractionPoint { ipRange :: Range
ipRange = Range
r, ipMeta :: Maybe MetaId
ipMeta = Maybe MetaId
forall a. Maybe a
Nothing, ipSolved :: Bool
ipSolved = Bool
False, ipClause :: IPClause
ipClause = IPClause
IPNoClause, ipBoundary :: IPBoundary
ipBoundary = Map (IntMap Bool) Term -> IPBoundary
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary Map (IntMap Bool) Term
forall a. Monoid a => a
mempty }
case BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
old) ii ip m of
(Just InteractionPoint
ip0, InteractionPoints
_)
| InteractionPoint -> Range
ipRange InteractionPoint
ip Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= InteractionPoint -> Range
ipRange InteractionPoint
ip0 -> m InteractionId
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise -> InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
(Maybe InteractionPoint
Nothing, InteractionPoints
m') -> do
(InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints (InteractionPoints -> InteractionPoints -> InteractionPoints
forall a b. a -> b -> a
const InteractionPoints
m')
InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
findInteractionPoint_ Range
r InteractionPoints
m = do
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Range -> Bool
forall a. Null a => a -> Bool
null Range
r
[InteractionId] -> Maybe InteractionId
forall a. [a] -> Maybe a
listToMaybe ([InteractionId] -> Maybe InteractionId)
-> [InteractionId] -> Maybe InteractionId
forall a b. (a -> b) -> a -> b
$ ((InteractionId, InteractionPoint) -> Maybe InteractionId)
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange ([(InteractionId, InteractionPoint)] -> [InteractionId])
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> b) -> a -> b
$ InteractionPoints -> [(InteractionId, InteractionPoint)]
forall k v. BiMap k v -> [(k, v)]
BiMap.toList InteractionPoints
m
where
sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange (InteractionId
ii, InteractionPoint Range
r' Maybe MetaId
_ Bool
False IPClause
_ IPBoundary
_) | Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
r' = InteractionId -> Maybe InteractionId
forall a. a -> Maybe a
Just InteractionId
ii
sameRange (InteractionId, InteractionPoint)
_ = Maybe InteractionId
forall a. Maybe a
Nothing
{-# INLINABLE connectInteractionPoint #-}
connectInteractionPoint
:: MonadInteractionPoints m
=> InteractionId -> MetaId -> m ()
connectInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
mi = do
ipCl <- (TCEnv -> IPClause) -> m IPClause
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> IPClause
envClause
m <- useR stInteractionPoints
let ip = InteractionPoint { ipRange :: Range
ipRange = Range
forall a. HasCallStack => a
__IMPOSSIBLE__, ipMeta :: Maybe MetaId
ipMeta = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
mi, ipSolved :: Bool
ipSolved = Bool
False, ipClause :: IPClause
ipClause = IPClause
ipCl, ipBoundary :: IPBoundary
ipBoundary = Map (IntMap Bool) Term -> IPBoundary
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary Map (IntMap Bool) Term
forall a. Monoid a => a
mempty }
case BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
new { ipRange = ipRange old }) ii ip m of
(Maybe InteractionPoint
Nothing, InteractionPoints
_) -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
(Just InteractionPoint
_, InteractionPoints
m') -> (InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoints -> InteractionPoints) -> m ())
-> (InteractionPoints -> InteractionPoints) -> m ()
forall a b. (a -> b) -> a -> b
$ InteractionPoints -> InteractionPoints -> InteractionPoints
forall a b. a -> b -> a
const InteractionPoints
m'
removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
removeInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii =
(InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoints -> InteractionPoints) -> m ())
-> (InteractionPoints -> InteractionPoints) -> m ()
forall a b. (a -> b) -> a -> b
$ (InteractionPoint -> Maybe InteractionPoint)
-> InteractionId -> InteractionPoints -> InteractionPoints
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> Maybe v) -> k -> BiMap k v -> BiMap k v
BiMap.update (\ InteractionPoint
ip -> InteractionPoint -> Maybe InteractionPoint
forall a. a -> Maybe a
Just InteractionPoint
ip{ ipSolved = True }) InteractionId
ii
{-# SPECIALIZE getInteractionPoints :: TCM [InteractionId] #-}
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionPoints :: forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints = InteractionPoints -> [InteractionId]
forall k v. BiMap k v -> [k]
BiMap.keys (InteractionPoints -> [InteractionId])
-> m InteractionPoints -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas =
(InteractionPoint -> Maybe MetaId)
-> [InteractionPoint] -> [MetaId]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe InteractionPoint -> Maybe MetaId
ipMeta ([InteractionPoint] -> [MetaId])
-> (InteractionPoints -> [InteractionPoint])
-> InteractionPoints
-> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoint -> Bool)
-> [InteractionPoint] -> [InteractionPoint]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (InteractionPoint -> Bool) -> InteractionPoint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved) ([InteractionPoint] -> [InteractionPoint])
-> (InteractionPoints -> [InteractionPoint])
-> InteractionPoints
-> [InteractionPoint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoints -> [InteractionPoint]
forall k v. BiMap k v -> [v]
BiMap.elems (InteractionPoints -> [MetaId])
-> m InteractionPoints -> m [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
getUniqueMetasRanges ::
(HasCallStack, MonadDebug m, ReadTCState m) => [MetaId] -> m [Range]
getUniqueMetasRanges :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges = ([Range] -> [Range]) -> m [Range] -> m [Range]
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Range -> Range) -> [Range] -> [Range]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn Range -> Range
forall a. a -> a
id) (m [Range] -> m [Range])
-> ([MetaId] -> m [Range]) -> [MetaId] -> m [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> m Range) -> [MetaId] -> m [Range]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange
getUnsolvedMetas ::
(HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
getUnsolvedMetas :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedMetas = do
openMetas <- m [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
interactionMetas <- getInteractionMetas
getUniqueMetasRanges (openMetas List.\\ interactionMetas)
getUnsolvedInteractionMetas ::
(HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas = [MetaId] -> m [Range]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges ([MetaId] -> m [Range]) -> m [MetaId] -> m [Range]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId,MetaId)]
getInteractionIdsAndMetas :: forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas =
((InteractionId, InteractionPoint)
-> Maybe (InteractionId, MetaId))
-> [(InteractionId, InteractionPoint)] -> [(InteractionId, MetaId)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe (InteractionId, MetaId)
forall {t}. (t, InteractionPoint) -> Maybe (t, MetaId)
f ([(InteractionId, InteractionPoint)] -> [(InteractionId, MetaId)])
-> (InteractionPoints -> [(InteractionId, InteractionPoint)])
-> InteractionPoints
-> [(InteractionId, MetaId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, InteractionPoint) -> Bool)
-> [(InteractionId, InteractionPoint)]
-> [(InteractionId, InteractionPoint)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((InteractionId, InteractionPoint) -> Bool)
-> (InteractionId, InteractionPoint)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved (InteractionPoint -> Bool)
-> ((InteractionId, InteractionPoint) -> InteractionPoint)
-> (InteractionId, InteractionPoint)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId, InteractionPoint) -> InteractionPoint
forall a b. (a, b) -> b
snd) ([(InteractionId, InteractionPoint)]
-> [(InteractionId, InteractionPoint)])
-> (InteractionPoints -> [(InteractionId, InteractionPoint)])
-> InteractionPoints
-> [(InteractionId, InteractionPoint)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoints -> [(InteractionId, InteractionPoint)]
forall k v. BiMap k v -> [(k, v)]
BiMap.toList (InteractionPoints -> [(InteractionId, MetaId)])
-> m InteractionPoints -> m [(InteractionId, MetaId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
where f :: (t, InteractionPoint) -> Maybe (t, MetaId)
f (t
ii, InteractionPoint
ip) = (t
ii,) (MetaId -> (t, MetaId)) -> Maybe MetaId -> Maybe (t, MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionPoint -> Maybe MetaId
ipMeta InteractionPoint
ip
isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)
isInteractionMeta :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
x = Tag InteractionPoint -> InteractionPoints -> Maybe InteractionId
forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
BiMap.invLookup Tag InteractionPoint
MetaId
x (InteractionPoints -> Maybe InteractionId)
-> m InteractionPoints -> m (Maybe InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
{-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
lookupInteractionPoint
:: (MonadFail m, ReadTCState m, MonadError TCErr m)
=> InteractionId -> m InteractionPoint
lookupInteractionPoint :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii =
m InteractionPoint
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m InteractionPoint
err (m (Maybe InteractionPoint) -> m InteractionPoint)
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$ InteractionId -> InteractionPoints -> Maybe InteractionPoint
forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup InteractionId
ii (InteractionPoints -> Maybe InteractionPoint)
-> m InteractionPoints -> m (Maybe InteractionPoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
where
err :: m InteractionPoint
err = [Char] -> m InteractionPoint
forall a. [Char] -> m a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> m InteractionPoint) -> [Char] -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$ [Char]
"no such interaction point: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Show a => a -> [Char]
show InteractionId
ii
{-# SPECIALIZE lookupInteractionId :: InteractionId -> TCM MetaId #-}
lookupInteractionId
:: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
=> InteractionId -> m MetaId
lookupInteractionId :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii = m MetaId -> m (Maybe MetaId) -> m MetaId
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaId
err2 (m (Maybe MetaId) -> m MetaId) -> m (Maybe MetaId) -> m MetaId
forall a b. (a -> b) -> a -> b
$ InteractionPoint -> Maybe MetaId
ipMeta (InteractionPoint -> Maybe MetaId)
-> m InteractionPoint -> m (Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
where
err2 :: m MetaId
err2 = TypeError -> m MetaId
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m MetaId) -> TypeError -> m MetaId
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$ [Char]
"No type nor action available for hole " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow InteractionId
ii [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
". Possible cause: the hole has not been reached during type checking (do you see yellow?)"
lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
lookupInteractionMeta :: forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii = InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ InteractionId
ii (InteractionPoints -> Maybe MetaId)
-> m InteractionPoints -> m (Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ InteractionId
ii InteractionPoints
m = InteractionPoint -> Maybe MetaId
ipMeta (InteractionPoint -> Maybe MetaId)
-> Maybe InteractionPoint -> Maybe MetaId
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> InteractionPoints -> Maybe InteractionPoint
forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup InteractionId
ii InteractionPoints
m
newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
newMeta :: forall (m :: * -> *) a.
MonadMetaSolver m =>
Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta = MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' (MetaKind -> MetaInstantiation
OpenMeta MetaKind
UnificationMeta)
newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
Judgement a -> TCM MetaId
newMetaTCM' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMetaTCM' MetaInstantiation
inst Frozen
frozen MetaInfo
mi MetaPriority
p Permutation
perm Judgement a
j = do
x <- TCM MetaId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
let j' = Judgement a
j { jMetaId = x }
mv = MetaVar{ mvInfo :: MetaInfo
mvInfo = MetaInfo
mi
, mvPriority :: MetaPriority
mvPriority = MetaPriority
p
, mvPermutation :: Permutation
mvPermutation = Permutation
perm
, mvJudgement :: Judgement MetaId
mvJudgement = Judgement MetaId
j'
, mvInstantiation :: MetaInstantiation
mvInstantiation = MetaInstantiation
inst
, mvListeners :: Set Listener
mvListeners = Set Listener
forall a. Set a
Set.empty
, mvFrozen :: Frozen
mvFrozen = Frozen
frozen
, mvTwin :: Maybe MetaId
mvTwin = Maybe MetaId
forall a. Maybe a
Nothing
}
insertMetaVar x mv
return x
{-# SPECIALIZE getInteractionRange :: InteractionId -> TCM Range #-}
getInteractionRange
:: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m)
=> InteractionId -> m Range
getInteractionRange :: forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange = InteractionPoint -> Range
ipRange (InteractionPoint -> Range)
-> (InteractionId -> m InteractionPoint)
-> InteractionId
-> m Range
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint
getMetaRange ::
(HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Range
getMetaRange :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange = MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange (MetaVariable -> Range)
-> (MetaId -> m MetaVariable) -> MetaId -> m Range
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta
getInteractionScope ::
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope :: forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope =
MetaVariable -> ScopeInfo
getMetaScope (MetaVariable -> ScopeInfo)
-> (MetaId -> m MetaVariable) -> MetaId -> m ScopeInfo
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta (MetaId -> m ScopeInfo)
-> (InteractionId -> m MetaId) -> InteractionId -> m ScopeInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< InteractionId -> m MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId
withMetaInfo' :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => MetaVariable -> m a -> m a
withMetaInfo' :: forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
mv = Closure Range -> m a -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)
withMetaInfo :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => Closure Range -> m a -> m a
withMetaInfo :: forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
mI m a
cont = Closure Range -> (Range -> m a) -> m a
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Range
mI ((Range -> m a) -> m a) -> (Range -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \ Range
r ->
Range -> m a -> m a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r m a
cont
withInteractionId ::
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId :: forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i m a
ret = do
m <- InteractionId -> m MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
withMetaId m ret
withMetaId ::
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
ReadTCState m) =>
MetaId -> m a -> m a
withMetaId :: forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
ReadTCState m) =>
MetaId -> m a -> m a
withMetaId MetaId
m m a
ret = do
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
withMetaInfo' mv ret
getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas = LocalMetaStore -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys (LocalMetaStore -> [MetaId]) -> m LocalMetaStore -> m [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta OpenMeta{} = Bool
True
isOpenMeta BlockedConst{} = Bool
True
isOpenMeta PostponedTypeCheckingProblem{} = Bool
True
isOpenMeta InstV{} = Bool
False
listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
listenToMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta Listener
l MetaId
m =
MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners = Set.insert l $ mvListeners mv }
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
unlistenToMeta Listener
l MetaId
m =
MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners = Set.delete l $ mvListeners mv }
getMetaListeners ::
(HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m [Listener]
getMetaListeners :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
m = Set Listener -> [Listener]
forall a. Set a -> [a]
Set.toList (Set Listener -> [Listener])
-> (MetaVariable -> Set Listener) -> MetaVariable -> [Listener]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Set Listener
mvListeners (MetaVariable -> [Listener]) -> m MetaVariable -> m [Listener]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
clearMetaListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
clearMetaListeners MetaId
m =
MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners = Set.empty }
etaExpandMetaSafe :: (MonadMetaSolver m) => MetaId -> m ()
etaExpandMetaSafe :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe = [MetaClass] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaClass] -> MetaId -> m ()
etaExpandMeta [MetaClass
SingletonRecords,MetaClass
Levels]
etaExpandListeners :: MonadMetaSolver m => MetaId -> m ()
etaExpandListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
m = do
ls <- MetaId -> m [Listener]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
m
clearMetaListeners m
mapM_ wakeupListener ls
wakeupListener :: MonadMetaSolver m => Listener -> m ()
wakeupListener :: forall (m :: * -> *). MonadMetaSolver m => Listener -> m ()
wakeupListener (EtaExpand MetaId
x) = MetaId -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
wakeupListener (CheckConstraint Int
_ ProblemConstraint
c) = do
(Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints (ProblemConstraint
cProblemConstraint -> Constraints -> Constraints
forall a. a -> [a] -> [a]
:)
m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints
solveAwakeConstraints :: (MonadConstraint m) => m ()
solveAwakeConstraints :: forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints = Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
False
solveAwakeConstraints' :: (MonadConstraint m) => Bool -> m ()
solveAwakeConstraints' :: forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' = (ProblemConstraint -> Bool) -> Bool -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints (Bool -> ProblemConstraint -> Bool
forall a b. a -> b -> a
const Bool
True)
{-# SPECIALIZE freezeMetas :: LocalMetaStore -> TCM (Set MetaId) #-}
freezeMetas :: forall m. MonadTCState m => LocalMetaStore -> m (Set MetaId)
freezeMetas :: forall (m :: * -> *).
MonadTCState m =>
LocalMetaStore -> m (Set MetaId)
freezeMetas LocalMetaStore
ms =
WriterT (Set MetaId) m () -> m (Set MetaId)
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT (Set MetaId) m () -> m (Set MetaId))
-> WriterT (Set MetaId) m () -> m (Set MetaId)
forall a b. (a -> b) -> a -> b
$
Lens' TCState LocalMetaStore
-> (LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
-> WriterT (Set MetaId) m ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> m a) -> m ()
modifyTCLensM (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore ((LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
-> WriterT (Set MetaId) m ())
-> (LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
-> WriterT (Set MetaId) m ()
forall a b. (a -> b) -> a -> b
$
StateT LocalMetaStore (WriterT (Set MetaId) m) ()
-> LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT ((MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> [MetaId] -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze ([MetaId] -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> [MetaId] -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a b. (a -> b) -> a -> b
$ LocalMetaStore -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys LocalMetaStore
ms)
where
freeze :: MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze :: MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze MetaId
m = do
store <- StateT LocalMetaStore (WriterT (Set MetaId) m) LocalMetaStore
forall s (m :: * -> *). MonadState s m => m s
get
case MapS.lookup m store of
Just MetaVariable
mvar
| MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
/= Frozen
Frozen -> do
WriterT (Set MetaId) m ()
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall (m :: * -> *) a. Monad m => m a -> StateT LocalMetaStore m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT (Set MetaId) m ()
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> WriterT (Set MetaId) m ()
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a b. (a -> b) -> a -> b
$ Set MetaId -> WriterT (Set MetaId) m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
m)
LocalMetaStore -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (LocalMetaStore
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> LocalMetaStore
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m (MetaVariable
mvar { mvFrozen = Frozen }) LocalMetaStore
store
| Bool
otherwise -> () -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a. a -> StateT LocalMetaStore (WriterT (Set MetaId) m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe MetaVariable
Nothing -> () -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a. a -> StateT LocalMetaStore (WriterT (Set MetaId) m) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
unfreezeMetas :: TCM ()
unfreezeMetas :: TCM ()
unfreezeMetas = (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore Lens' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` (MetaVariable -> MetaVariable) -> LocalMetaStore -> LocalMetaStore
forall a b k. (a -> b) -> Map k a -> Map k b
MapS.map MetaVariable -> MetaVariable
unfreeze
where
unfreeze :: MetaVariable -> MetaVariable
unfreeze :: MetaVariable -> MetaVariable
unfreeze MetaVariable
mvar = MetaVariable
mvar { mvFrozen = Instantiable }
{-# SPECIALIZE isFrozen :: MetaId -> TCM Bool #-}
isFrozen ::
(HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Bool
isFrozen :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x = do
mvar <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
return $ mvFrozen mvar == Frozen
withFrozenMetas ::
(MonadMetaSolver m, MonadTCState m)
=> m a -> m a
withFrozenMetas :: forall (m :: * -> *) a.
(MonadMetaSolver m, MonadTCState m) =>
m a -> m a
withFrozenMetas m a
act = do
openMetas <- Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
frozenMetas <- freezeMetas openMetas
result <- act
forM_ frozenMetas $ \MetaId
m ->
MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv -> MetaVariable
mv { mvFrozen = Instantiable }
return result
class UnFreezeMeta a where
unfreezeMeta :: MonadMetaSolver m => a -> m ()
instance UnFreezeMeta MetaId where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (((MetaId -> Bool) -> MetaId -> Bool
forall a b. (a -> b) -> a -> b
$ MetaId
x) ((MetaId -> Bool) -> Bool) -> m (MetaId -> Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (MetaId -> Bool)
forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
x ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv -> MetaVariable
mv { mvFrozen = Instantiable }
Type -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
unfreezeMeta (Type -> m ()) -> m Type -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
{-# SPECIALIZE unfreezeMeta :: MetaId -> TCM () #-}
instance UnFreezeMeta Type where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
unfreezeMeta (El Sort
s Term
t) = Sort -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta Sort
s m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta Term
t
instance UnFreezeMeta Term where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta (MetaV MetaId
x [Elim]
_) = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x
unfreezeMeta (Sort Sort
s) = Sort -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta Sort
s
unfreezeMeta (Level Level
l) = Level -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Level -> m ()
unfreezeMeta Level
l
unfreezeMeta (DontCare Term
t) = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta Term
t
unfreezeMeta (Lam ArgInfo
_ Abs Term
v) = Abs Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Abs Term -> m ()
unfreezeMeta Abs Term
v
unfreezeMeta Term
_ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance UnFreezeMeta Sort where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta (MetaS MetaId
x [Elim]
_) = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x
unfreezeMeta Sort
_ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance UnFreezeMeta Level where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Level -> m ()
unfreezeMeta (Max Integer
_ [PlusLevel' Term]
ls) = [PlusLevel' Term] -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[PlusLevel' Term] -> m ()
unfreezeMeta [PlusLevel' Term]
ls
instance UnFreezeMeta PlusLevel where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => PlusLevel' Term -> m ()
unfreezeMeta (Plus Integer
_ Term
a) = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta Term
a
instance UnFreezeMeta a => UnFreezeMeta [a] where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => [a] -> m ()
unfreezeMeta = (a -> m ()) -> [a] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ a -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => a -> m ()
unfreezeMeta
instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Abs a -> m ()
unfreezeMeta = (a -> m ()) -> Abs a -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ a -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => a -> m ()
unfreezeMeta