{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Monad.MetaVars where
import Prelude hiding (null)
import Control.DeepSeq
import Control.Monad ( (<=<), guard )
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Fail (MonadFail)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
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)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Signature (HasConstInfo)
import Agda.TypeChecking.Substitute
import {-# SOURCE #-} Agda.TypeChecking.Telescope
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Functor ((<.>))
import Agda.Utils.List (nubOn)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Tuple
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Impossible
data MetaKind =
Records
| SingletonRecords
| Levels
deriving (MetaKind -> MetaKind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MetaKind -> MetaKind -> Bool
$c/= :: MetaKind -> MetaKind -> Bool
== :: MetaKind -> MetaKind -> Bool
$c== :: MetaKind -> MetaKind -> Bool
Eq, Int -> MetaKind
MetaKind -> Int
MetaKind -> [MetaKind]
MetaKind -> MetaKind
MetaKind -> MetaKind -> [MetaKind]
MetaKind -> MetaKind -> MetaKind -> [MetaKind]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]
$cenumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]
enumFromTo :: MetaKind -> MetaKind -> [MetaKind]
$cenumFromTo :: MetaKind -> MetaKind -> [MetaKind]
enumFromThen :: MetaKind -> MetaKind -> [MetaKind]
$cenumFromThen :: MetaKind -> MetaKind -> [MetaKind]
enumFrom :: MetaKind -> [MetaKind]
$cenumFrom :: MetaKind -> [MetaKind]
fromEnum :: MetaKind -> Int
$cfromEnum :: MetaKind -> Int
toEnum :: Int -> MetaKind
$ctoEnum :: Int -> MetaKind
pred :: MetaKind -> MetaKind
$cpred :: MetaKind -> MetaKind
succ :: MetaKind -> MetaKind
$csucc :: MetaKind -> MetaKind
Enum, MetaKind
forall a. a -> a -> Bounded a
maxBound :: MetaKind
$cmaxBound :: MetaKind
minBound :: MetaKind
$cminBound :: MetaKind
Bounded, Int -> MetaKind -> ShowS
[MetaKind] -> ShowS
MetaKind -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [MetaKind] -> ShowS
$cshowList :: [MetaKind] -> ShowS
show :: MetaKind -> [Char]
$cshow :: MetaKind -> [Char]
showsPrec :: Int -> MetaKind -> ShowS
$cshowsPrec :: Int -> MetaKind -> ShowS
Show)
allMetaKinds :: [MetaKind]
allMetaKinds :: [MetaKind]
allMetaKinds = [forall a. Bounded a => a
minBound .. 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 :: [MetaKind] -> MetaId -> m ()
updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()
speculateMetas :: m () -> m KeepMetas -> m ()
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
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta" Int
45 forall a b. (a -> b) -> a -> b
$ [Char]
"don't assign metas"
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
env -> TCEnv
env { envAssignMetas :: Bool
envAssignMetas = Bool
False }) m a
cont
getMetaStore :: (ReadTCState m) => m MetaStore
getMetaStore :: forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore = forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' MetaStore TCState
stMetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore MetaStore -> MetaStore
f = Lens' MetaStore TCState
stMetaStore forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` MetaStore -> MetaStore
f
metasCreatedBy :: ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy :: forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy m a
m = do
!Maybe Int
largestMeta <- forall a. NFData a => a -> a
force forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IntMap a -> Maybe (Int, a)
IntMap.lookupMax forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
a
a <- m a
m
MetaStore
ms <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
let createdMetas :: MetaStore
createdMetas = case Maybe Int
largestMeta of
Maybe Int
Nothing -> MetaStore
ms
Just Int
largestMeta -> forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. Int -> IntMap a -> (IntMap a, IntMap a)
IntMap.split Int
largestMeta MetaStore
ms
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, MetaStore
createdMetas)
lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupMeta' :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
m = forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (MetaId -> Int
metaId MetaId
m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
lookupMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m = forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaVariable
failure forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
m
where failure :: m MetaVariable
failure = forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"no such meta variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m
metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
metaType :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x = forall a. Judgement a -> Type
jMetaType forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
m MetaVariable -> MetaVariable
f = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust MetaVariable -> MetaVariable
f forall a b. (a -> b) -> a -> b
$ MetaId -> Int
metaId MetaId
m
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
m MetaVariable
mv = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (MetaId -> Int
metaId MetaId
m) MetaVariable
mv
getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority
getMetaPriority :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaPriority
getMetaPriority = MetaVariable -> MetaPriority
mvPriority forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta
isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isSortMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isSortMeta MetaId
m = MetaVariable -> Bool
isSortMeta_ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ MetaVariable
mv = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
HasType{} -> Bool
False
IsSort{} -> Bool
True
getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
getMetaType :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
m = do
MetaVariable
mv <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type
t
IsSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs :: forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVar{ mvPermutation :: MetaVariable -> Permutation
mvPermutation = Permutation
p } = do
Args
args <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Permutation
p) Args
args
getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m, HasBuiltins m)
=> MetaId -> m Type
getMetaTypeInContext :: forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m = do
mv :: MetaVariable
mv@MetaVar{ mvJudgement :: MetaVariable -> Judgement MetaId
mvJudgement = Judgement MetaId
j } <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
case Judgement MetaId
j of
HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
IsSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize
isGeneralizableMeta :: forall (m :: * -> *).
(ReadTCState m, MonadFail m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta MetaId
x = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Arg DoGeneralize
miGeneralizable forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
class IsInstantiatedMeta a where
isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool
instance IsInstantiatedMeta MetaId where
isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
m = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = 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]
_ -> forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
DontCare Term
v -> Term -> m Bool
loop Term
v
Level Level
l -> forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Level
l
Lam ArgInfo
_ Abs Term
b -> forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Abs Term
b
Con ConHead
_ ConInfo
_ [Elim]
es | Just Args
vs <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es -> forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Args
vs
Term
_ -> 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 forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta [PlusLevel' Term]
ls
isInstantiatedMeta Level
_ = 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 forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Term
l
isInstantiatedMeta PlusLevel' Term
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
isInstantiatedMeta :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => [a] -> m Bool
isInstantiatedMeta = forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(IsInstantiatedMeta a, 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 = forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Abs a -> a
unAbs
isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
isInstantiatedMeta' :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
m = do
MetaVariable
mv <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
InstV [Arg [Char]]
tel Term
v -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
mkLam Term
v [Arg [Char]]
tel
MetaInstantiation
_ -> forall a. Maybe a
Nothing
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas = \case
ValueCmp Comparison
_ CompareAs
_ Term
u Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton (Term
u, Term
v)
ValueCmpOnFace Comparison
_ Term
p Type
_ Term
u Term
v -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton (Term
p, Term
u, Term
v)
ElimCmp [Polarity]
_ [IsForced]
_ Type
_ Term
_ [Elim]
es [Elim]
es' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton ([Elim]
es, [Elim]
es')
LevelCmp Comparison
_ Level
l Level
l' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton (Level -> Term
Level Level
l, Level -> Term
Level Level
l')
UnquoteTactic Term
t Term
h Type
g -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton (Term
t, Term
h, Type
g)
SortCmp Comparison
_ Sort
s1 Sort
s2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)
UnBlock MetaId
x -> forall a. Ord a => a -> Set a -> Set a
Set.insert MetaId
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Listener -> TCM (Set MetaId)
listenerMetas forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
x)
FindInstance MetaId
x Maybe [Candidate]
_ ->
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
x) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton MetaId
x) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton
IsEmpty{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
CheckFunDef{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
CheckSizeLtSat{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
HasBiggerSort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
HasPTSRule{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
CheckMetaInst MetaId
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
CheckType Type
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton Type
t
CheckLockedVars Term
a Type
b Arg Term
c Type
d -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas forall a. a -> Set a
Set.singleton (Term
a, Type
b, Arg Term
c, Type
d)
UsableAtModality{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty
where
listenerMetas :: Listener -> TCM (Set MetaId)
listenerMetas EtaExpand{} = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Set a
Set.empty
listenerMetas (CheckConstraint Int
_ ProblemConstraint
c) = Constraint -> TCM (Set MetaId)
constraintMetas (forall a. Closure a -> a
clValue 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 = 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
Range
r <- forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange
Closure Range
cl <- forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Range
r
DoGeneralize
gen <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' DoGeneralize TCEnv
eGeneralizeMetas
Modality
modality <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Modality TCEnv
eModality
forall (m :: * -> *) a. Monad m => a -> m a
return MetaInfo
{ miClosRange :: Closure Range
miClosRange = Closure Range
cl
, miModality :: Modality
miModality = Modality
modality
, miMetaOccursCheck :: RunMetaOccursCheck
miMetaOccursCheck = RunMetaOccursCheck
b
, miNameSuggestion :: [Char]
miNameSuggestion = [Char]
""
, miGeneralizable :: Arg DoGeneralize
miGeneralizable = forall a. a -> Arg a
defaultArg DoGeneralize
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]
_ -> forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s
Term
u -> do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.name" Int
70 forall a b. (a -> b) -> a -> b
$
[Char]
"cannot set meta name; newMeta returns " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term
u
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
getMetaNameSuggestion :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Char]
getMetaNameSuggestion MetaId
mi = MetaInfo -> [Char]
miNameSuggestion forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaNameSuggestion :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Char]
s Bool -> Bool -> Bool
|| forall a. Underscore a => a -> Bool
isUnderscore [Char]
s) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.name" Int
20 forall a b. (a -> b) -> a -> b
$
[Char]
"setting name of meta " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
mi forall a. [a] -> [a] -> [a]
++ [Char]
" to " forall a. [a] -> [a] -> [a]
++ [Char]
s
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
MetaVariable
mvar { mvInfo :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar) { miNameSuggestion :: [Char]
miNameSuggestion = [Char]
s }}
setMetaGeneralizableArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgInfo -> m ()
setMetaGeneralizableArgInfo MetaId
m ArgInfo
i = forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
MetaVariable
mv { mvInfo :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)
{ miGeneralizable :: Arg DoGeneralize
miGeneralizable = forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
i (MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)) } }
updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mi Range
r = forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi (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 = forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
MetaVariable
mvar { mvInfo :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar) { miMetaOccursCheck :: RunMetaOccursCheck
miMetaOccursCheck = RunMetaOccursCheck
b } }
class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
freshInteractionId :: m InteractionId
default freshInteractionId
:: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
=> m InteractionId
freshInteractionId = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
default modifyInteractionPoints
:: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
=> (InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall i (m :: * -> *). MonadFresh i m => m i
fresh
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
f = Lens' InteractionPoints TCState
stInteractionPoints forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (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
InteractionPoints
m <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
if Bool -> Bool
not Bool
preciseRange Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust Maybe Int
maybeId then InteractionPoints -> m InteractionId
continue InteractionPoints
m else do
forall a b. Maybe a -> b -> (a -> b) -> b
Strict.caseMaybe (Range -> Maybe AbsolutePath
rangeFile Range
r) (InteractionPoints -> m InteractionId
continue InteractionPoints
m) forall a b. (a -> b) -> a -> b
$ \ AbsolutePath
_ -> do
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) forall (m :: * -> *) a. Monad m => a -> m a
return
where
continue :: InteractionPoints -> m InteractionId
continue :: InteractionPoints -> m InteractionId
continue InteractionPoints
m = do
InteractionId
ii <- case Maybe Int
maybeId of
Just Int
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> InteractionId
InteractionId Int
i
Maybe Int
Nothing -> forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
let ip :: InteractionPoint
ip = InteractionPoint { ipRange :: Range
ipRange = Range
r, ipMeta :: Maybe MetaId
ipMeta = forall a. Maybe a
Nothing, ipSolved :: Bool
ipSolved = Bool
False, ipClause :: IPClause
ipClause = IPClause
IPNoClause }
case forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
old) InteractionId
ii InteractionPoint
ip InteractionPoints
m of
(Just InteractionPoint
ip0, InteractionPoints
_)
| InteractionPoint -> Range
ipRange InteractionPoint
ip forall a. Eq a => a -> a -> Bool
/= InteractionPoint -> Range
ipRange InteractionPoint
ip0 -> forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
(Maybe InteractionPoint
Nothing, InteractionPoints
m') -> do
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints (forall a b. a -> b -> a
const InteractionPoints
m')
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
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null Range
r
forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange forall a b. (a -> b) -> a -> b
$ 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
_) | Range
r forall a. Eq a => a -> a -> Bool
== Range
r' = forall a. a -> Maybe a
Just InteractionId
ii
sameRange (InteractionId, InteractionPoint)
_ = forall a. Maybe a
Nothing
connectInteractionPoint
:: MonadInteractionPoints m
=> InteractionId -> MetaId -> m ()
connectInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
mi = do
IPClause
ipCl <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> IPClause
envClause
InteractionPoints
m <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
let ip :: InteractionPoint
ip = InteractionPoint { ipRange :: Range
ipRange = forall a. HasCallStack => a
__IMPOSSIBLE__, ipMeta :: Maybe MetaId
ipMeta = forall a. a -> Maybe a
Just MetaId
mi, ipSolved :: Bool
ipSolved = Bool
False, ipClause :: IPClause
ipClause = IPClause
ipCl }
case forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
new { ipRange :: Range
ipRange = InteractionPoint -> Range
ipRange InteractionPoint
old }) InteractionId
ii InteractionPoint
ip InteractionPoints
m of
(Maybe InteractionPoint
Nothing, InteractionPoints
_) -> forall a. HasCallStack => a
__IMPOSSIBLE__
(Just InteractionPoint
_, InteractionPoints
m') -> forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const InteractionPoints
m'
removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
removeInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii =
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints forall a b. (a -> b) -> a -> b
$ forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> Maybe v) -> k -> BiMap k v -> BiMap k v
BiMap.update (\ InteractionPoint
ip -> forall a. a -> Maybe a
Just InteractionPoint
ip{ ipSolved :: Bool
ipSolved = Bool
True }) InteractionId
ii
{-# SPECIALIZE getInteractionPoints :: TCM [InteractionId] #-}
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionPoints :: forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints = forall k v. BiMap k v -> [k]
BiMap.keys forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas =
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe InteractionPoint -> Maybe MetaId
ipMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. BiMap k v -> [v]
BiMap.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
getUniqueMetasRanges :: (MonadFail m, ReadTCState m) => [MetaId] -> m [Range]
getUniqueMetasRanges :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange
getUnsolvedMetas :: (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedMetas :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedMetas = do
[MetaId]
openMetas <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
[MetaId]
interactionMetas <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges ([MetaId]
openMetas forall a. Eq a => [a] -> [a] -> [a]
List.\\ [MetaId]
interactionMetas)
getUnsolvedInteractionMetas :: (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas = forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId,MetaId)]
getInteractionIdsAndMetas :: forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas =
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {t}. (t, InteractionPoint) -> Maybe (t, MetaId)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. BiMap k v -> [(k, v)]
BiMap.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
where f :: (t, InteractionPoint) -> Maybe (t, MetaId)
f (t
ii, InteractionPoint
ip) = (t
ii,) 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 = forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
BiMap.invLookup MetaId
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
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 =
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m InteractionPoint
err forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup InteractionId
ii forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
where
err :: m InteractionPoint
err = forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"no such interaction point: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show InteractionId
ii
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 = forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaId
err2 forall a b. (a -> b) -> a -> b
$ InteractionPoint -> Maybe MetaId
ipMeta forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
where
err2 :: m MetaId
err2 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"No type nor action available for hole " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow InteractionId
ii 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ InteractionId
ii InteractionPoints
m = InteractionPoint -> Maybe MetaId
ipMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 = forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
Open
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
MetaId
x <- forall i (m :: * -> *). MonadFresh i m => m i
fresh
let j' :: Judgement MetaId
j' = Judgement a
j { jMetaId :: MetaId
jMetaId = MetaId
x }
mv :: MetaVariable
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 = forall a. Set a
Set.empty
, mvFrozen :: Frozen
mvFrozen = Frozen
frozen
, mvTwin :: Maybe MetaId
mvTwin = forall a. Maybe a
Nothing
}
MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
x MetaVariable
mv
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
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 forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint
getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range
getMetaRange :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange = forall a. HasRange a => a -> Range
getRange forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta
getInteractionScope
:: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
=> InteractionId -> m ScopeInfo
getInteractionScope :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope = MetaVariable -> ScopeInfo
getMetaScope forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< 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 = forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaInfo -> Closure Range
miClosRange 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 = forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Range
mI forall a b. (a -> b) -> a -> b
$ \ Range
r ->
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r m a
cont
withInteractionId
:: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m)
=> InteractionId -> m a -> m a
withInteractionId :: forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i m a
ret = do
MetaId
m <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
forall (m :: * -> *) a.
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaId -> m a -> m a
withMetaId MetaId
m m a
ret
withMetaId
:: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m)
=> MetaId -> m a -> m a
withMetaId :: forall (m :: * -> *) a.
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaId -> m a -> m a
withMetaId MetaId
m m a
ret = do
MetaVariable
mv <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
mv m a
ret
getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
getMetaVariables :: forall (m :: * -> *).
ReadTCState m =>
(MetaVariable -> Bool) -> m [MetaId]
getMetaVariables MetaVariable -> Bool
p = do
MetaStore
store <- forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
forall (m :: * -> *) a. Monad m => a -> m a
return [ Int -> MetaId
MetaId Int
i | (Int
i, MetaVariable
mv) <- forall a. IntMap a -> [(Int, a)]
IntMap.assocs MetaStore
store, MetaVariable -> Bool
p MetaVariable
mv ]
getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas = forall (m :: * -> *).
ReadTCState m =>
(MetaVariable -> Bool) -> m [MetaId]
getMetaVariables (MetaInstantiation -> Bool
isOpenMeta forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation)
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta MetaInstantiation
Open = Bool
True
isOpenMeta MetaInstantiation
OpenInstance = 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 =
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners :: Set Listener
mvListeners = forall a. Ord a => a -> Set a -> Set a
Set.insert Listener
l forall a b. (a -> b) -> a -> b
$ MetaVariable -> Set Listener
mvListeners MetaVariable
mv }
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
unlistenToMeta Listener
l MetaId
m =
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners :: Set Listener
mvListeners = forall a. Ord a => a -> Set a -> Set a
Set.delete Listener
l forall a b. (a -> b) -> a -> b
$ MetaVariable -> Set Listener
mvListeners MetaVariable
mv }
getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
getMetaListeners :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
m = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Set Listener
mvListeners forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
clearMetaListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
clearMetaListeners MetaId
m =
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners :: Set Listener
mvListeners = forall a. Set a
Set.empty }
freezeMetas :: MetaStore -> TCM IntSet
freezeMetas :: MetaStore -> TCM IntSet
freezeMetas MetaStore
ms =
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> m a) -> m ()
modifyTCLensM Lens' MetaStore TCState
stMetaStore forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (m :: * -> *).
Monad m =>
Int -> StateT MetaStore (WriterT IntSet m) ()
freeze forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [Int]
IntMap.keys MetaStore
ms)
where
freeze :: Monad m => Int -> StateT MetaStore (WriterT IntSet m) ()
freeze :: forall (m :: * -> *).
Monad m =>
Int -> StateT MetaStore (WriterT IntSet m) ()
freeze Int
m = do
MetaStore
store <- forall s (m :: * -> *). MonadState s m => m s
get
case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
m MetaStore
store of
Just MetaVariable
mvar
| MetaVariable -> Frozen
mvFrozen MetaVariable
mvar forall a. Eq a => a -> a -> Bool
/= Frozen
Frozen -> do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Int -> IntSet
IntSet.singleton Int
m)
forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
m (MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Frozen }) MetaStore
store
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe MetaVariable
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__
unfreezeMetas :: TCM ()
unfreezeMetas :: TCM ()
unfreezeMetas = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map MetaVariable -> MetaVariable
unfreeze
where
unfreeze :: MetaVariable -> MetaVariable
unfreeze :: MetaVariable -> MetaVariable
unfreeze MetaVariable
mvar = MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }
isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isFrozen :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x = do
MetaVariable
mvar <- forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaVariable -> Frozen
mvFrozen MetaVariable
mvar forall a. Eq a => a -> a -> Bool
== Frozen
Frozen
class UnFreezeMeta a where
unfreezeMeta :: MonadMetaSolver m => a -> m ()
instance UnFreezeMeta MetaId where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x = do
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
x forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv -> MetaVariable
mv { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
instance UnFreezeMeta Type where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
unfreezeMeta (El Sort
s Term
t) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Sort
s forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
instance UnFreezeMeta Term where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta (MetaV MetaId
x [Elim]
_) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
unfreezeMeta (Sort Sort
s) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Sort
s
unfreezeMeta (Level Level
l) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Level
l
unfreezeMeta (DontCare Term
t) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
unfreezeMeta (Lam ArgInfo
_ Abs Term
v) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Abs Term
v
unfreezeMeta Term
_ = 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]
_) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
unfreezeMeta Sort
_ = 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) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta [PlusLevel' Term]
ls
instance UnFreezeMeta PlusLevel where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => PlusLevel' Term -> m ()
unfreezeMeta (Plus Integer
_ Term
a) = forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
a
instance UnFreezeMeta a => UnFreezeMeta [a] where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => [a] -> m ()
unfreezeMeta = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta
instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Abs a -> m ()
unfreezeMeta = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta