{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Monad.MetaVars where
import Prelude hiding (null)
import Control.Monad.State
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.Map as Map
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 Agda.Utils.Except
import Agda.Utils.Functor ((<.>))
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
(MetaKind -> MetaKind -> Bool)
-> (MetaKind -> MetaKind -> Bool) -> Eq MetaKind
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]
(MetaKind -> MetaKind)
-> (MetaKind -> MetaKind)
-> (Int -> MetaKind)
-> (MetaKind -> Int)
-> (MetaKind -> [MetaKind])
-> (MetaKind -> MetaKind -> [MetaKind])
-> (MetaKind -> MetaKind -> [MetaKind])
-> (MetaKind -> MetaKind -> MetaKind -> [MetaKind])
-> Enum 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
MetaKind -> MetaKind -> Bounded MetaKind
forall a. a -> a -> Bounded a
maxBound :: MetaKind
$cmaxBound :: MetaKind
minBound :: MetaKind
$cminBound :: MetaKind
Bounded, Int -> MetaKind -> ShowS
[MetaKind] -> ShowS
MetaKind -> String
(Int -> MetaKind -> ShowS)
-> (MetaKind -> String) -> ([MetaKind] -> ShowS) -> Show MetaKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MetaKind] -> ShowS
$cshowList :: [MetaKind] -> ShowS
show :: MetaKind -> String
$cshow :: MetaKind -> String
showsPrec :: Int -> MetaKind -> ShowS
$cshowsPrec :: Int -> MetaKind -> ShowS
Show)
allMetaKinds :: [MetaKind]
allMetaKinds :: [MetaKind]
allMetaKinds = [MetaKind
forall a. Bounded a => a
minBound .. MetaKind
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 :: m a -> m a
dontAssignMetas cont :: m a
cont = do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "tc.meta" 45 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "don't assign metas"
(TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ env :: TCEnv
env -> TCEnv
env { envAssignMetas :: Bool
envAssignMetas = Bool
False }) m a
cont
getMetaStore :: (ReadTCState m) => m MetaStore
getMetaStore :: m MetaStore
getMetaStore = Lens' MetaStore TCState -> m MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' MetaStore TCState
stMetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore f :: MetaStore -> MetaStore
f = Lens' MetaStore TCState
stMetaStore Lens' MetaStore TCState -> (MetaStore -> MetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` MetaStore -> MetaStore
f
metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet)
metasCreatedBy :: m a -> m (a, IntSet)
metasCreatedBy m :: m a
m = do
IntSet
before <- MetaStore -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (MetaStore -> IntSet) -> m MetaStore -> m IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' MetaStore TCState -> m MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
a
a <- m a
m
IntSet
after <- MetaStore -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (MetaStore -> IntSet) -> m MetaStore -> m IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' MetaStore TCState -> m MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
(a, IntSet) -> m (a, IntSet)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, IntSet
after IntSet -> IntSet -> IntSet
IntSet.\\ IntSet
before)
lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupMeta' :: MetaId -> m (Maybe MetaVariable)
lookupMeta' m :: MetaId
m = Int -> MetaStore -> Maybe MetaVariable
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (MetaId -> Int
metaId MetaId
m) (MetaStore -> Maybe MetaVariable)
-> m MetaStore -> m (Maybe MetaVariable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m MetaStore
forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
lookupMeta :: MetaId -> m MetaVariable
lookupMeta m :: MetaId
m = m MetaVariable -> m (Maybe MetaVariable) -> m MetaVariable
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaVariable
forall a. m a
failure (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)
lookupMeta' MetaId
m
where failure :: m a
failure = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ "no such meta variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
m
metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
metaType :: MetaId -> m Type
metaType x :: MetaId
x = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type)
-> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Type) -> m MetaVariable -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM m :: MetaId
m f :: MetaVariable -> MetaVariable
f = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (MetaVariable -> MetaVariable) -> Int -> MetaStore -> MetaStore
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust MetaVariable -> MetaVariable
f (Int -> MetaStore -> MetaStore) -> Int -> MetaStore -> MetaStore
forall a b. (a -> b) -> a -> b
$ MetaId -> Int
metaId MetaId
m
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar m :: MetaId
m mv :: MetaVariable
mv = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> MetaVariable -> MetaStore -> MetaStore
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 :: 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta
isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isSortMeta :: MetaId -> m Bool
isSortMeta m :: MetaId
m = MetaVariable -> Bool
isSortMeta_ (MetaVariable -> Bool) -> m MetaVariable -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ mv :: 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 :: MetaId -> m Type
getMetaType m :: MetaId
m = do
MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
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{} -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs :: MetaVariable -> m Args
getMetaContextArgs MetaVar{ mvPermutation :: MetaVariable -> Permutation
mvPermutation = Permutation
p } = do
Args
args <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return (Args -> m Args) -> Args -> m Args
forall a b. (a -> b) -> a -> b
$ Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Permutation
p) Args
args
getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m)
=> MetaId -> m Type
getMetaTypeInContext :: MetaId -> m Type
getMetaTypeInContext m :: MetaId
m = do
mv :: MetaVariable
mv@MetaVar{ mvJudgement :: MetaVariable -> Judgement MetaId
mvJudgement = Judgement MetaId
j } <- MetaId -> m MetaVariable
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 } -> Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> 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__
isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize
isGeneralizableMeta :: MetaId -> m DoGeneralize
isGeneralizableMeta x :: 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 :: * -> *).
(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 :: MetaId -> m Bool
isInstantiatedMeta m :: 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 :: Term -> m Bool
isInstantiatedMeta = Term -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Term -> m Bool
loop where
loop :: Term -> m Bool
loop v :: Term
v =
case Term
v of
MetaV x :: MetaId
x _ -> MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
DontCare v :: Term
v -> Term -> m Bool
loop Term
v
Level l :: Level
l -> Level -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Level
l
Lam _ b :: Abs Term
b -> Abs Term -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Abs Term
b
Con _ _ es :: Elims
es | Just vs :: Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> Args -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Args
vs
_ -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta Level where
isInstantiatedMeta :: Level -> m Bool
isInstantiatedMeta (Max n :: Integer
n ls :: [PlusLevel' Term]
ls) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = [PlusLevel' Term] -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta [PlusLevel' Term]
ls
isInstantiatedMeta _ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta PlusLevel where
isInstantiatedMeta :: PlusLevel' Term -> m Bool
isInstantiatedMeta (Plus n :: Integer
n l :: LevelAtom' Term
l) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = LevelAtom' Term -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta LevelAtom' Term
l
isInstantiatedMeta _ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta LevelAtom where
isInstantiatedMeta :: LevelAtom' Term -> m Bool
isInstantiatedMeta (MetaLevel x :: MetaId
x es :: Elims
es) = MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
isInstantiatedMeta _ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
isInstantiatedMeta :: [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
isInstantiatedMeta
instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
isInstantiatedMeta :: Maybe a -> m Bool
isInstantiatedMeta = [a] -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, 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 :: Arg a -> m Bool
isInstantiatedMeta = a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, 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 :: Abs a -> m Bool
isInstantiatedMeta = a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, 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
isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
isInstantiatedMeta' :: MetaId -> m (Maybe Term)
isInstantiatedMeta' m :: MetaId
m = do
MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
Maybe Term -> m (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> m (Maybe Term)) -> Maybe Term -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
InstV tel :: [Arg String]
tel v :: Term
v -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Arg String -> Term -> Term) -> Term -> [Arg String] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg String -> Term -> Term
mkLam Term
v [Arg String]
tel
_ -> Maybe Term
forall a. Maybe a
Nothing
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas c :: Constraint
c = Constraint -> TCM (Set MetaId)
metas Constraint
c
where
metas :: Constraint -> TCM (Set MetaId)
metas c :: Constraint
c = case Constraint
c of
ValueCmp _ t :: CompareAs
t u :: Term
u v :: Term
v -> Set MetaId -> TCM (Set MetaId)
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) -> (CompareAs, Term, Term) -> Set MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (CompareAs
t, Term
u, Term
v)
ValueCmpOnFace _ p :: Term
p t :: Type
t u :: Term
u v :: Term
v -> Set MetaId -> TCM (Set MetaId)
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, Term, Term) -> Set MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
p, Type
t, Term
u, Term
v)
ElimCmp _ _ t :: Type
t u :: Term
u es :: Elims
es es' :: Elims
es' -> Set MetaId -> TCM (Set MetaId)
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, Term, Elims, Elims) -> Set MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Type
t, Term
u, Elims
es, Elims
es')
LevelCmp _ l :: Level
l l' :: Level
l' -> Set MetaId -> TCM (Set MetaId)
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 a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Level -> Term
Level Level
l, Level -> Term
Level Level
l')
UnquoteTactic m :: Maybe MetaId
m t :: Term
t h :: Term
h g :: Type
g -> Set MetaId -> TCM (Set MetaId)
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. Ord a => [a] -> Set a
Set.fromList [MetaId
x | Just x :: MetaId
x <- [Maybe MetaId
m]] Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (MetaId -> Set MetaId) -> (Term, Term, Type) -> Set MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
t, Term
h, Type
g)
Guarded c :: Constraint
c _ -> Constraint -> TCM (Set MetaId)
metas Constraint
c
TelCmp _ _ _ tel1 :: Telescope
tel1 tel2 :: Telescope
tel2 -> Set MetaId -> TCM (Set MetaId)
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) -> (Telescope, Telescope) -> Set MetaId
forall a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Telescope
tel1, Telescope
tel2)
SortCmp _ s1 :: Sort
s1 s2 :: Sort
s2 -> Set MetaId -> TCM (Set MetaId)
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 a m. (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)
UnBlock x :: 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)
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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
x)
FindInstance{} -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
IsEmpty{} -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckFunDef{} -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckSizeLtSat{} -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
HasBiggerSort{} -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
HasPTSRule{} -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
CheckMetaInst x :: MetaId
x -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
listenerMetas :: Listener -> TCM (Set MetaId)
listenerMetas EtaExpand{} = Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Set a
Set.empty
listenerMetas (CheckConstraint _ c :: 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 :: 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' :: RunMetaOccursCheck -> m MetaInfo
createMetaInfo' b :: RunMetaOccursCheck
b = do
Range
r <- m Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange
Closure Range
cl <- Range -> m (Closure Range)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Range
r
DoGeneralize
gen <- Lens' DoGeneralize TCEnv -> m DoGeneralize
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' DoGeneralize TCEnv
eGeneralizeMetas
MetaInfo -> m MetaInfo
forall (m :: * -> *) a. Monad m => a -> m a
return MetaInfo :: Closure Range
-> RunMetaOccursCheck -> String -> Arg DoGeneralize -> MetaInfo
MetaInfo
{ miClosRange :: Closure Range
miClosRange = Closure Range
cl
, miMetaOccursCheck :: RunMetaOccursCheck
miMetaOccursCheck = RunMetaOccursCheck
b
, miNameSuggestion :: String
miNameSuggestion = ""
, miGeneralizable :: Arg DoGeneralize
miGeneralizable = Arg DoGeneralize -> Arg DoGeneralize
forall a. LensHiding a => a -> a
hide (Arg DoGeneralize -> Arg DoGeneralize)
-> Arg DoGeneralize -> Arg DoGeneralize
forall a b. (a -> b) -> a -> b
$ DoGeneralize -> Arg DoGeneralize
forall a. a -> Arg a
defaultArg DoGeneralize
gen
}
setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
setValueMetaName :: Term -> String -> m ()
setValueMetaName v :: Term
v s :: String
s = do
case Term
v of
MetaV mi :: MetaId
mi _ -> MetaId -> String -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> String -> m ()
setMetaNameSuggestion MetaId
mi String
s
u :: Term
u -> do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "tc.meta.name" 70 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$
"cannot set meta name; newMeta returns " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
u
() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
getMetaNameSuggestion :: MetaId -> m String
getMetaNameSuggestion mi :: MetaId
mi = MetaInfo -> String
miNameSuggestion (MetaInfo -> String)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> String) -> m MetaVariable -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaNameSuggestion :: MetaId -> String -> m ()
setMetaNameSuggestion mi :: MetaId
mi s :: String
s = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
forall a. Null a => a -> Bool
null String
s Bool -> Bool -> Bool
|| String -> Bool
forall a. Underscore a => a -> Bool
isUnderscore String
s) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "tc.meta.name" 20 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$
"setting name of meta " String -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
mi String -> ShowS
forall a. [a] -> [a] -> [a]
++ " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
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
$ \ mvar :: MetaVariable
mvar ->
MetaVariable
mvar { mvInfo :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar) { miNameSuggestion :: String
miNameSuggestion = String
s }}
setMetaArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
setMetaArgInfo :: MetaId -> ArgInfo -> m ()
setMetaArgInfo m :: MetaId
m i :: 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
$ \ mv :: MetaVariable
mv ->
MetaVariable
mv { mvInfo :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)
{ miGeneralizable :: Arg DoGeneralize
miGeneralizable = ArgInfo -> Arg DoGeneralize -> Arg DoGeneralize
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 :: MetaId -> Range -> m ()
updateMetaVarRange mi :: MetaId
mi r :: Range
r = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi (Range -> MetaVariable -> MetaVariable
forall t. SetRange t => Range -> t -> t
setRange Range
r)
setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck :: MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck mi :: MetaId
mi b :: 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
$ \ mvar :: 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
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m) where
freshInteractionId :: ReaderT r m InteractionId
freshInteractionId = m InteractionId -> ReaderT r m InteractionId
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> ReaderT r m ()
modifyInteractionPoints = m () -> ReaderT r m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ())
-> ((InteractionPoints -> InteractionPoints) -> m ())
-> (InteractionPoints -> InteractionPoints)
-> ReaderT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints
instance MonadInteractionPoints m => MonadInteractionPoints (StateT r m) where
freshInteractionId :: StateT r m InteractionId
freshInteractionId = m InteractionId -> StateT r m InteractionId
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> StateT r m ()
modifyInteractionPoints = m () -> StateT r m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT r m ())
-> ((InteractionPoints -> InteractionPoints) -> m ())
-> (InteractionPoints -> InteractionPoints)
-> StateT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints
instance MonadInteractionPoints TCM where
freshInteractionId :: TCM InteractionId
freshInteractionId = TCM InteractionId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints f :: InteractionPoints -> InteractionPoints
f = Lens' InteractionPoints TCState
stInteractionPoints Lens' InteractionPoints TCState
-> (InteractionPoints -> InteractionPoints) -> TCM ()
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 :: Bool -> Range -> Maybe Int -> m InteractionId
registerInteractionPoint preciseRange :: Bool
preciseRange r :: Range
r maybeId :: Maybe Int
maybeId = do
InteractionPoints
m <- Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
if Bool -> Bool
not Bool
preciseRange Bool -> Bool -> Bool
|| Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
maybeId then InteractionPoints -> m InteractionId
continue InteractionPoints
m else do
Maybe AbsolutePath
-> m InteractionId
-> (AbsolutePath -> m InteractionId)
-> m InteractionId
forall a b. Maybe a -> b -> (a -> b) -> b
Strict.caseMaybe (Range -> Maybe AbsolutePath
rangeFile Range
r) (InteractionPoints -> m InteractionId
continue InteractionPoints
m) ((AbsolutePath -> m InteractionId) -> m InteractionId)
-> (AbsolutePath -> m InteractionId) -> m InteractionId
forall a b. (a -> b) -> a -> b
$ \ _ -> 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 (m :: * -> *) a. Monad m => a -> m a
return
where
continue :: InteractionPoints -> m InteractionId
continue :: InteractionPoints -> m InteractionId
continue m :: InteractionPoints
m = do
InteractionId
ii <- case Maybe Int
maybeId of
Just i :: Int
i -> InteractionId -> m InteractionId
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
Nothing -> m InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
let ip :: InteractionPoint
ip = InteractionPoint :: Range -> Maybe MetaId -> Bool -> IPClause -> InteractionPoint
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 }
case (InteractionId
-> InteractionPoint -> InteractionPoint -> InteractionPoint)
-> InteractionId
-> InteractionPoint
-> InteractionPoints
-> (Maybe InteractionPoint, InteractionPoints)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (\ key :: InteractionId
key new :: InteractionPoint
new old :: InteractionPoint
old -> InteractionPoint
old) InteractionId
ii InteractionPoint
ip InteractionPoints
m of
(Just ip0 :: InteractionPoint
ip0, _)
| 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 (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
(Nothing, m' :: 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 (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
findInteractionPoint_ r :: Range
r m :: 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 a. Map k a -> [(k, a)]
Map.toList InteractionPoints
m
where
sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange (ii :: InteractionId
ii, InteractionPoint r' :: Range
r' _ _ _) | 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 _ = Maybe InteractionId
forall a. Maybe a
Nothing
connectInteractionPoint
:: MonadInteractionPoints m
=> InteractionId -> MetaId -> m ()
connectInteractionPoint :: InteractionId -> MetaId -> m ()
connectInteractionPoint ii :: InteractionId
ii mi :: MetaId
mi = do
IPClause
ipCl <- (TCEnv -> IPClause) -> m IPClause
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> IPClause
envClause
InteractionPoints
m <- Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
let ip :: InteractionPoint
ip = InteractionPoint :: Range -> Maybe MetaId -> Bool -> IPClause -> InteractionPoint
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 }
case (InteractionId
-> InteractionPoint -> InteractionPoint -> InteractionPoint)
-> InteractionId
-> InteractionPoint
-> InteractionPoints
-> (Maybe InteractionPoint, InteractionPoints)
forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (\ key :: InteractionId
key new :: InteractionPoint
new old :: InteractionPoint
old -> InteractionPoint
new { ipRange :: Range
ipRange = InteractionPoint -> Range
ipRange InteractionPoint
old }) InteractionId
ii InteractionPoint
ip InteractionPoints
m of
(Nothing, _) -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
(Just _, m' :: 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 :: InteractionId -> m ()
removeInteractionPoint ii :: 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 a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (\ ip :: InteractionPoint
ip -> InteractionPoint -> Maybe InteractionPoint
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 :: m [InteractionId]
getInteractionPoints = InteractionPoints -> [InteractionId]
forall k a. Map k a -> [k]
Map.keys (InteractionPoints -> [InteractionId])
-> m InteractionPoints -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionMetas :: 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 a. Map k a -> [a]
Map.elems (InteractionPoints -> [MetaId])
-> m InteractionPoints -> m [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId,MetaId)]
getInteractionIdsAndMetas :: 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 a. Map k a -> [(k, a)]
Map.toList (InteractionPoints -> [(InteractionId, MetaId)])
-> m InteractionPoints -> m [(InteractionId, MetaId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
where f :: (t, InteractionPoint) -> Maybe (t, MetaId)
f (ii :: t
ii, ip :: 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 :: MetaId -> m (Maybe InteractionId)
isInteractionMeta x :: MetaId
x = MetaId -> [(MetaId, InteractionId)] -> Maybe InteractionId
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
x ([(MetaId, InteractionId)] -> Maybe InteractionId)
-> ([(InteractionId, MetaId)] -> [(MetaId, InteractionId)])
-> [(InteractionId, MetaId)]
-> Maybe InteractionId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, MetaId) -> (MetaId, InteractionId))
-> [(InteractionId, MetaId)] -> [(MetaId, InteractionId)]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, MetaId) -> (MetaId, InteractionId)
forall a b. (a, b) -> (b, a)
swap ([(InteractionId, MetaId)] -> Maybe InteractionId)
-> m [(InteractionId, MetaId)] -> m (Maybe InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
{-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
lookupInteractionPoint
:: (MonadFail m, ReadTCState m, MonadError TCErr m)
=> InteractionId -> m InteractionPoint
lookupInteractionPoint :: InteractionId -> m InteractionPoint
lookupInteractionPoint ii :: InteractionId
ii =
m InteractionPoint
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m InteractionPoint
forall a. m a
err (m (Maybe InteractionPoint) -> m InteractionPoint)
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$ InteractionId -> InteractionPoints -> Maybe InteractionPoint
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InteractionId
ii (InteractionPoints -> Maybe InteractionPoint)
-> m InteractionPoints -> m (Maybe InteractionPoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
where
err :: m a
err = String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ "no such interaction point: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
lookupInteractionId
:: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
=> InteractionId -> m MetaId
lookupInteractionId :: InteractionId -> m MetaId
lookupInteractionId ii :: InteractionId
ii = m MetaId -> m (Maybe MetaId) -> m MetaId
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaId
forall a. m a
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 a
err2 = TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ "No type nor action available for hole " String -> ShowS
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Pretty a => a -> String
prettyShow InteractionId
ii String -> ShowS
forall a. [a] -> [a] -> [a]
++ ". Possible cause: the hole has not been reached during type checking (do you see yellow?)"
lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
lookupInteractionMeta :: InteractionId -> m (Maybe MetaId)
lookupInteractionMeta ii :: 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' InteractionPoints TCState -> m InteractionPoints
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_ ii :: InteractionId
ii m :: 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 a. Ord k => k -> Map k a -> Maybe a
Map.lookup InteractionId
ii InteractionPoints
m
newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
newMeta :: Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta = 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
Open
newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
Judgement a -> TCM MetaId
newMetaTCM' :: MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMetaTCM' inst :: MetaInstantiation
inst frozen :: Frozen
frozen mi :: MetaInfo
mi p :: MetaPriority
p perm :: Permutation
perm j :: Judgement a
j = do
MetaId
x <- TCM MetaId
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 :: MetaInfo
-> MetaPriority
-> Permutation
-> Judgement MetaId
-> MetaInstantiation
-> Set Listener
-> Frozen
-> Maybe MetaId
-> MetaVariable
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
}
MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
x MetaVariable
mv
MetaId -> TCM MetaId
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 :: 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 :: (MonadFail m, ReadTCState m) => MetaId -> m Range
getMetaRange :: MetaId -> m Range
getMetaRange = MetaVariable -> Range
forall t. HasRange t => t -> 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta
getInteractionScope :: InteractionId -> TCM ScopeInfo
getInteractionScope :: InteractionId -> TCM ScopeInfo
getInteractionScope = MetaVariable -> ScopeInfo
getMetaScope (MetaVariable -> ScopeInfo)
-> (MetaId -> TCMT IO MetaVariable) -> MetaId -> TCM ScopeInfo
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta (MetaId -> TCM ScopeInfo)
-> (InteractionId -> TCM MetaId) -> InteractionId -> TCM ScopeInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< InteractionId -> TCM MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId
withMetaInfo' :: MetaVariable -> TCM a -> TCM a
withMetaInfo' :: MetaVariable -> TCM a -> TCM a
withMetaInfo' mv :: MetaVariable
mv = Closure Range -> TCM a -> TCM a
forall a. Closure Range -> TCM a -> TCM 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 :: Closure Range -> TCM a -> TCM a
withMetaInfo :: Closure Range -> TCM a -> TCM a
withMetaInfo mI :: Closure Range
mI cont :: TCM a
cont = Closure Range -> (Range -> TCM a) -> TCM a
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Range
mI ((Range -> TCM a) -> TCM a) -> (Range -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ r :: Range
r ->
Range -> TCM a -> TCM a
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r TCM a
cont
getMetaVariableSet :: ReadTCState m => m IntSet
getMetaVariableSet :: m IntSet
getMetaVariableSet = MetaStore -> IntSet
forall a. IntMap a -> IntSet
IntMap.keysSet (MetaStore -> IntSet) -> m MetaStore -> m IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m MetaStore
forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
getMetaVariables :: (MetaVariable -> Bool) -> m [MetaId]
getMetaVariables p :: MetaVariable -> Bool
p = do
MetaStore
store <- m MetaStore
forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
[MetaId] -> m [MetaId]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Int -> MetaId
MetaId Int
i | (i :: Int
i, mv :: MetaVariable
mv) <- MetaStore -> [(Int, MetaVariable)]
forall a. IntMap a -> [(Int, a)]
IntMap.assocs MetaStore
store, MetaVariable -> Bool
p MetaVariable
mv ]
getInstantiatedMetas :: ReadTCState m => m [MetaId]
getInstantiatedMetas :: m [MetaId]
getInstantiatedMetas = (MetaVariable -> Bool) -> m [MetaId]
forall (m :: * -> *).
ReadTCState m =>
(MetaVariable -> Bool) -> m [MetaId]
getMetaVariables (MetaInstantiation -> Bool
isInst (MetaInstantiation -> Bool)
-> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation)
where
isInst :: MetaInstantiation -> Bool
isInst Open = Bool
False
isInst OpenInstance = Bool
False
isInst BlockedConst{} = Bool
False
isInst PostponedTypeCheckingProblem{} = Bool
False
isInst InstV{} = Bool
True
getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: m [MetaId]
getOpenMetas = (MetaVariable -> Bool) -> m [MetaId]
forall (m :: * -> *).
ReadTCState m =>
(MetaVariable -> Bool) -> m [MetaId]
getMetaVariables (MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool)
-> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation)
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta Open = Bool
True
isOpenMeta OpenInstance = Bool
True
isOpenMeta BlockedConst{} = Bool
True
isOpenMeta PostponedTypeCheckingProblem{} = Bool
True
isOpenMeta InstV{} = Bool
False
listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
listenToMeta :: Listener -> MetaId -> m ()
listenToMeta l :: Listener
l m :: 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
$ \mv :: MetaVariable
mv -> MetaVariable
mv { mvListeners :: Set Listener
mvListeners = Listener -> Set Listener -> Set Listener
forall a. Ord a => a -> Set a -> Set a
Set.insert Listener
l (Set Listener -> Set Listener) -> Set Listener -> Set Listener
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Set Listener
mvListeners MetaVariable
mv }
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta :: Listener -> MetaId -> m ()
unlistenToMeta l :: Listener
l m :: 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
$ \mv :: MetaVariable
mv -> MetaVariable
mv { mvListeners :: Set Listener
mvListeners = Listener -> Set Listener -> Set Listener
forall a. Ord a => a -> Set a -> Set a
Set.delete Listener
l (Set Listener -> Set Listener) -> Set Listener -> Set Listener
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Set Listener
mvListeners MetaVariable
mv }
getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
getMetaListeners :: MetaId -> m [Listener]
getMetaListeners m :: 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
clearMetaListeners :: MetaId -> m ()
clearMetaListeners m :: 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
$ \mv :: MetaVariable
mv -> MetaVariable
mv { mvListeners :: Set Listener
mvListeners = Set Listener
forall a. Set a
Set.empty }
withFreezeMetas :: TCM a -> TCM a
withFreezeMetas :: TCM a -> TCM a
withFreezeMetas cont :: TCM a
cont = do
Set MetaId
ms <- [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList ([MetaId] -> Set MetaId) -> TCMT IO [MetaId] -> TCM (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [MetaId]
freezeMetas
a
x <- TCM a
cont
(MetaId -> Bool) -> TCM ()
unfreezeMetas' (MetaId -> Set MetaId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set MetaId
ms)
a -> TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
freezeMetas :: TCM [MetaId]
freezeMetas :: TCMT IO [MetaId]
freezeMetas = (MetaId -> Bool) -> TCMT IO [MetaId]
freezeMetas' ((MetaId -> Bool) -> TCMT IO [MetaId])
-> (MetaId -> Bool) -> TCMT IO [MetaId]
forall a b. (a -> b) -> a -> b
$ Bool -> MetaId -> Bool
forall a b. a -> b -> a
const Bool
True
freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]
freezeMetas' :: (MetaId -> Bool) -> TCMT IO [MetaId]
freezeMetas' p :: MetaId -> Bool
p = WriterT [MetaId] TCM () -> TCMT IO [MetaId]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT [MetaId] TCM () -> TCMT IO [MetaId])
-> WriterT [MetaId] TCM () -> TCMT IO [MetaId]
forall a b. (a -> b) -> a -> b
$ Lens' MetaStore TCState
-> (MetaStore -> WriterT [MetaId] TCM MetaStore)
-> WriterT [MetaId] TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> m a) -> m ()
modifyTCLensM Lens' MetaStore TCState
stMetaStore ((MetaStore -> WriterT [MetaId] TCM MetaStore)
-> WriterT [MetaId] TCM ())
-> (MetaStore -> WriterT [MetaId] TCM MetaStore)
-> WriterT [MetaId] TCM ()
forall a b. (a -> b) -> a -> b
$ (Int -> MetaVariable -> WriterT [MetaId] TCM MetaVariable)
-> MetaStore -> WriterT [MetaId] TCM MetaStore
forall (t :: * -> *) a b.
Applicative t =>
(Int -> a -> t b) -> IntMap a -> t (IntMap b)
IntMap.traverseWithKey (MetaId -> MetaVariable -> WriterT [MetaId] TCM MetaVariable
forall (m :: * -> *).
Monad m =>
MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable
freeze (MetaId -> MetaVariable -> WriterT [MetaId] TCM MetaVariable)
-> (Int -> MetaId)
-> Int
-> MetaVariable
-> WriterT [MetaId] TCM MetaVariable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MetaId
MetaId)
where
freeze :: Monad m => MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable
freeze :: MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable
freeze m :: MetaId
m mvar :: MetaVariable
mvar
| MetaId -> Bool
p MetaId
m Bool -> Bool -> Bool
&& MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
/= Frozen
Frozen = do
[MetaId] -> WriterT [MetaId] m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [MetaId
m]
MetaVariable -> WriterT [MetaId] m MetaVariable
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> WriterT [MetaId] m MetaVariable)
-> MetaVariable -> WriterT [MetaId] m MetaVariable
forall a b. (a -> b) -> a -> b
$ MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Frozen }
| Bool
otherwise = MetaVariable -> WriterT [MetaId] m MetaVariable
forall (m :: * -> *) a. Monad m => a -> m a
return MetaVariable
mvar
unfreezeMetas :: TCM ()
unfreezeMetas :: TCM ()
unfreezeMetas = (MetaId -> Bool) -> TCM ()
unfreezeMetas' ((MetaId -> Bool) -> TCM ()) -> (MetaId -> Bool) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> MetaId -> Bool
forall a b. a -> b -> a
const Bool
True
unfreezeMetas' :: (MetaId -> Bool) -> TCM ()
unfreezeMetas' :: (MetaId -> Bool) -> TCM ()
unfreezeMetas' cond :: MetaId -> Bool
cond = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Int -> MetaVariable -> MetaVariable) -> MetaStore -> MetaStore
forall a b. (Int -> a -> b) -> IntMap a -> IntMap b
IntMap.mapWithKey ((Int -> MetaVariable -> MetaVariable) -> MetaStore -> MetaStore)
-> (Int -> MetaVariable -> MetaVariable) -> MetaStore -> MetaStore
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaVariable -> MetaVariable
unfreeze (MetaId -> MetaVariable -> MetaVariable)
-> (Int -> MetaId) -> Int -> MetaVariable -> MetaVariable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MetaId
MetaId
where
unfreeze :: MetaId -> MetaVariable -> MetaVariable
unfreeze :: MetaId -> MetaVariable -> MetaVariable
unfreeze m :: MetaId
m mvar :: MetaVariable
mvar
| MetaId -> Bool
cond MetaId
m = MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }
| Bool
otherwise = MetaVariable
mvar
isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isFrozen :: MetaId -> m Bool
isFrozen x :: MetaId
x = do
MetaVariable
mvar <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
== Frozen
Frozen
class UnFreezeMeta a where
unfreezeMeta :: MonadMetaSolver m => a -> m ()
instance UnFreezeMeta MetaId where
unfreezeMeta :: MetaId -> m ()
unfreezeMeta x :: MetaId
x = 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
$ \ mv :: MetaVariable
mv -> MetaVariable
mv { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }
Type -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x
instance UnFreezeMeta Type where
unfreezeMeta :: Type -> m ()
unfreezeMeta (El s :: Sort
s t :: Term
t) = Sort -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Sort
s m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
instance UnFreezeMeta Term where
unfreezeMeta :: Term -> m ()
unfreezeMeta (MetaV x :: MetaId
x _) = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
unfreezeMeta (Sort s :: Sort
s) = Sort -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Sort
s
unfreezeMeta (Level l :: Level
l) = Level -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Level
l
unfreezeMeta (DontCare t :: Term
t) = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
unfreezeMeta (Lam _ v :: Abs Term
v) = Abs Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Abs Term
v
unfreezeMeta _ = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance UnFreezeMeta Sort where
unfreezeMeta :: Sort -> m ()
unfreezeMeta (MetaS x :: MetaId
x _) = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
unfreezeMeta _ = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
instance UnFreezeMeta Level where
unfreezeMeta :: Level -> m ()
unfreezeMeta (Max _ ls :: [PlusLevel' Term]
ls) = [PlusLevel' Term] -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta [PlusLevel' Term]
ls
instance UnFreezeMeta PlusLevel where
unfreezeMeta :: PlusLevel' Term -> m ()
unfreezeMeta (Plus _ a :: LevelAtom' Term
a) = LevelAtom' Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta LevelAtom' Term
a
instance UnFreezeMeta LevelAtom where
unfreezeMeta :: LevelAtom' Term -> m ()
unfreezeMeta (MetaLevel x :: MetaId
x _) = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
unfreezeMeta (BlockedLevel _ t :: Term
t) = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
unfreezeMeta (NeutralLevel _ t :: Term
t) = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
unfreezeMeta (UnreducedLevel t :: Term
t) = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta Term
t
instance UnFreezeMeta a => UnFreezeMeta [a] where
unfreezeMeta :: [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 ()
unfreezeMeta
instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
unfreezeMeta :: 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 ()
unfreezeMeta