{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Monad.MetaVars where

import Prelude hiding (null)

import Control.Monad                ( (<=<), forM_, guard )
import Control.Monad.Except         ( MonadError )
import Control.Monad.State          ( StateT, execStateT, get, put )
import Control.Monad.Trans          ( MonadTrans, lift )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Reader         ( ReaderT(ReaderT), runReaderT )
import Control.Monad.Writer         ( WriterT, execWriterT, tell )
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)

import qualified Data.HashMap.Strict as HMap
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import qualified Data.Map.Strict as MapS
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Foldable as Fold

import GHC.Stack (HasCallStack)

import Agda.Syntax.Common
import Agda.Syntax.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, __IMPOSSIBLE_VERBOSE__)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Signature (HasConstInfo)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Substitute
import {-# SOURCE #-} Agda.TypeChecking.Telescope

import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Functor ((<.>))
import Agda.Utils.Lens
import Agda.Utils.List (nubOn)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Tuple
import qualified Agda.Utils.Maybe.Strict as Strict

import Agda.Utils.Impossible

-- | Various kinds of metavariables.

data MetaKind =
    Records
    -- ^ Meta variables of record type.
  | SingletonRecords
    -- ^ Meta variables of \"hereditarily singleton\" record type.
  | Levels
    -- ^ Meta variables of level type, if type-in-type is activated.
  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)

-- | All possible metavariable kinds.

allMetaKinds :: [MetaKind]
allMetaKinds :: [MetaKind]
allMetaKinds = [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound]

data KeepMetas = KeepMetas | RollBackMetas

-- | Monad service class for creating, solving and eta-expanding of
--   metavariables.
class ( MonadConstraint m
      , MonadReduce m
      , MonadAddContext m
      , MonadTCEnv m
      , ReadTCState m
      , HasBuiltins m
      , HasConstInfo m
      , MonadDebug m
      ) => MonadMetaSolver m where
  -- | Generate a new meta variable with some instantiation given.
  --   For instance, the instantiation could be a 'PostponedTypeCheckingProblem'.
  newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
              Judgement a -> m MetaId

  -- * Solve constraint @x vs = v@.

  -- | Assign to an open metavar which may not be frozen.
  --   First check that metavar args are in pattern fragment.
  --     Then do extended occurs check on given thing.
  --
  --   Assignment is aborted by throwing a @PatternErr@ via a call to
  --   @patternViolation@.  This error is caught by @catchConstraint@
  --   during equality checking (@compareAtom@) and leads to
  --   restoration of the original constraints.
  assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()

  -- | Directly instantiate the metavariable. Skip pattern check,
  -- occurs check and frozen check. Used for eta expanding frozen
  -- metas.
  assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()

  -- | Eta-expand a local meta-variable, if it is of the specified
  -- kind. Don't do anything if the meta-variable is a blocked term.
  etaExpandMeta :: [MetaKind] -> MetaId -> m ()

  -- | Update the status of the metavariable
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()

  -- | 'speculateMetas fallback m' speculatively runs 'm', but if the
  --    result is 'RollBackMetas' any changes to metavariables are
  --    rolled back and 'fallback' is run instead.
  speculateMetas :: m () -> m KeepMetas -> m ()

instance MonadMetaSolver m => MonadMetaSolver (ReaderT r m) where
  newMeta' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> ReaderT r m MetaId
newMeta' MetaInstantiation
inst Frozen
f MetaInfo
i MetaPriority
p Permutation
perm Judgement a
j = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
inst Frozen
f MetaInfo
i MetaPriority
p Permutation
perm Judgement a
j
  assignV :: CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> ReaderT r m ()
assignV CompareDirection
dir MetaId
m Args
us Term
v CompareAs
cmp = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignV CompareDirection
dir MetaId
m Args
us Term
v CompareAs
cmp
  assignTerm' :: MonadMetaSolver (ReaderT r m) =>
MetaId -> [Arg [Char]] -> Term -> ReaderT r m ()
assignTerm' MetaId
m [Arg [Char]]
us Term
v = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadMetaSolver m, MonadMetaSolver m) =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
m [Arg [Char]]
us Term
v
  etaExpandMeta :: [MetaKind] -> MetaId -> ReaderT r m ()
etaExpandMeta [MetaKind]
k MetaId
m = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadMetaSolver m =>
[MetaKind] -> MetaId -> m ()
etaExpandMeta [MetaKind]
k MetaId
m
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> ReaderT r m ()
updateMetaVar MetaId
m MetaVariable -> MetaVariable
f = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m MetaVariable -> MetaVariable
f
  speculateMetas :: ReaderT r m () -> ReaderT r m KeepMetas -> ReaderT r m ()
speculateMetas ReaderT r m ()
fallback ReaderT r m KeepMetas
m = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \r
x -> forall (m :: * -> *).
MonadMetaSolver m =>
m () -> m KeepMetas -> m ()
speculateMetas (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m ()
fallback r
x) (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m KeepMetas
m r
x)

-- | Switch off assignment of metas.
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

-- | Is the meta-variable from another top-level module?

isRemoteMeta :: ReadTCState m => m (MetaId -> Bool)
isRemoteMeta :: forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta = do
  ModuleNameHash
h <- forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
  forall (m :: * -> *) a. Monad m => a -> m a
return (\MetaId
m -> ModuleNameHash
h forall a. Eq a => a -> a -> Bool
/= MetaId -> ModuleNameHash
metaModule MetaId
m)

-- | If another meta-variable is created, then it will get this
-- 'MetaId' (unless the state is changed too much, for instance by
-- 'setTopLevelModule').

nextLocalMeta :: ReadTCState m => m MetaId
nextLocalMeta :: forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta = forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' MetaId TCState
stFreshMetaId

-- | Pairs of local meta-stores.

data LocalMetaStores = LocalMetaStores
  { LocalMetaStores -> LocalMetaStore
openMetas :: LocalMetaStore
    -- ^ A 'MetaStore' containing open meta-variables.
  , LocalMetaStores -> LocalMetaStore
solvedMetas :: LocalMetaStore
    -- ^ A 'MetaStore' containing instantiated meta-variables.
  }

-- | Run a computation and record which new metas it created.
metasCreatedBy ::
  forall m a. ReadTCState m => m a -> m (a, LocalMetaStores)
metasCreatedBy :: forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy m a
m = do
  !MetaId
nextMeta <- forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta
  a
a         <- m a
m
  LocalMetaStore
os        <- Lens' LocalMetaStore TCState -> MetaId -> m LocalMetaStore
created Lens' LocalMetaStore TCState
stOpenMetaStore   MetaId
nextMeta
  LocalMetaStore
ss        <- Lens' LocalMetaStore TCState -> MetaId -> m LocalMetaStore
created Lens' LocalMetaStore TCState
stSolvedMetaStore MetaId
nextMeta
  forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, LocalMetaStores { openMetas :: LocalMetaStore
openMetas = LocalMetaStore
os, solvedMetas :: LocalMetaStore
solvedMetas = LocalMetaStore
ss })
  where
  created :: Lens' LocalMetaStore TCState -> MetaId -> m LocalMetaStore
  created :: Lens' LocalMetaStore TCState -> MetaId -> m LocalMetaStore
created Lens' LocalMetaStore TCState
store MetaId
next = do
    LocalMetaStore
ms <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' LocalMetaStore TCState
store
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case forall k a. Ord k => k -> Map k a -> (Map k a, Maybe a, Map k a)
MapS.splitLookup MetaId
next LocalMetaStore
ms of
      (LocalMetaStore
_, Maybe MetaVariable
Nothing, LocalMetaStore
ms) -> LocalMetaStore
ms
      (LocalMetaStore
_, Just MetaVariable
m,  LocalMetaStore
ms) -> forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
next MetaVariable
m LocalMetaStore
ms

-- | Find information about the given local meta-variable, if any.

lookupLocalMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m = do
  Maybe MetaVariable
mv <- LocalMetaStore -> Maybe MetaVariable
lkup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' LocalMetaStore TCState
stSolvedMetaStore
  case Maybe MetaVariable
mv of
    mv :: Maybe MetaVariable
mv@Just{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Maybe MetaVariable
mv
    Maybe MetaVariable
Nothing   -> LocalMetaStore -> Maybe MetaVariable
lkup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' LocalMetaStore TCState
stOpenMetaStore
  where
  lkup :: LocalMetaStore -> Maybe MetaVariable
lkup = forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m

-- | Find information about the given local meta-variable.

lookupLocalMeta ::
  (HasCallStack, MonadDebug m, ReadTCState m) =>
  MetaId -> m MetaVariable
lookupLocalMeta :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m =
  forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
err) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
  where
  err :: [Char]
err = [Char]
"no such local meta-variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m

-- | Find information about the (local or remote) meta-variable, if
-- any.
--
-- If no meta-variable is found, then the reason could be that the
-- dead-code elimination
-- ('Agda.TypeChecking.DeadCode.eliminateDeadCode') failed to find the
-- meta-variable, perhaps because some 'NamesIn' instance is
-- incorrectly defined.

lookupMeta ::
  ReadTCState m =>
  MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m = do
  Maybe MetaVariable
mv <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
  case Maybe MetaVariable
mv of
    Just MetaVariable
mv -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (forall a b. b -> Either a b
Right MetaVariable
mv))
    Maybe MetaVariable
Nothing -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup MetaId
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' (HashMap MetaId RemoteMetaVariable) TCState
stImportedMetaStore

-- | Find the meta-variable's instantiation.

lookupMetaInstantiation ::
  ReadTCState m => MetaId -> m MetaInstantiation
lookupMetaInstantiation :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m = do
  Maybe (Either RemoteMetaVariable MetaVariable)
mi <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
  case Maybe (Either RemoteMetaVariable MetaVariable)
mi of
    Just (Left RemoteMetaVariable
mv)  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Instantiation -> MetaInstantiation
InstV forall a b. (a -> b) -> a -> b
$ RemoteMetaVariable -> Instantiation
rmvInstantiation RemoteMetaVariable
mv)
    Just (Right MetaVariable
mv) -> forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
    Maybe (Either RemoteMetaVariable MetaVariable)
Nothing         -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Find the meta-variable's judgement.

lookupMetaJudgement :: ReadTCState m => MetaId -> m (Judgement MetaId)
lookupMetaJudgement :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m = do
  Maybe (Either RemoteMetaVariable MetaVariable)
mi <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
  case Maybe (Either RemoteMetaVariable MetaVariable)
mi of
    Just (Left RemoteMetaVariable
mv)  -> forall (m :: * -> *) a. Monad m => a -> m a
return (RemoteMetaVariable -> Judgement MetaId
rmvJudgement RemoteMetaVariable
mv)
    Just (Right MetaVariable
mv) -> forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)
    Maybe (Either RemoteMetaVariable MetaVariable)
Nothing         -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Find the meta-variable's modality.

lookupMetaModality :: ReadTCState m => MetaId -> m Modality
lookupMetaModality :: forall (m :: * -> *). ReadTCState m => MetaId -> m Modality
lookupMetaModality MetaId
m = do
  Maybe (Either RemoteMetaVariable MetaVariable)
mi <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
  case Maybe (Either RemoteMetaVariable MetaVariable)
mi of
    Just (Left RemoteMetaVariable
mv)  -> forall (m :: * -> *) a. Monad m => a -> m a
return (RemoteMetaVariable -> Modality
rmvModality RemoteMetaVariable
mv)
    Just (Right MetaVariable
mv) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. LensModality a => a -> Modality
getModality MetaVariable
mv)
    Maybe (Either RemoteMetaVariable MetaVariable)
Nothing         -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | The type of a term or sort meta-variable.
metaType :: ReadTCState m => MetaId -> m Type
metaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x = forall a. Judgement a -> Type
jMetaType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
x

-- | Update the information associated with a local meta-variable.
updateMetaVarTCM ::
  HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM :: HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
m MetaVariable -> MetaVariable
f = do
  Maybe MetaVariable
mv <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
  case Maybe MetaVariable
mv of
    Maybe MetaVariable
Nothing -> do
      Maybe (Either RemoteMetaVariable MetaVariable)
mv <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
      case Maybe (Either RemoteMetaVariable MetaVariable)
mv of
        Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__
                     ([Char]
"Meta-variable not found: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow MetaId
m)
        Just{}  -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__
                     ([Char]
"Attempt to update remote meta-variable: " forall a. [a] -> [a] -> [a]
++
                      forall a. Pretty a => a -> [Char]
prettyShow MetaId
m)
    Just MetaVariable
mv -> do
      let mv' :: MetaVariable
mv'    = MetaVariable -> MetaVariable
f MetaVariable
mv
          insert :: Lens' LocalMetaStore TCState -> TCM ()
insert = (forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m MetaVariable
mv')
          delete :: Lens' LocalMetaStore TCState -> TCM ()
delete = (forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => k -> Map k a -> Map k a
MapS.delete MetaId
m)
      case ( MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
           , MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv')
           ) of
        (Bool
True,  Bool
True)  -> Lens' LocalMetaStore TCState -> TCM ()
insert Lens' LocalMetaStore TCState
stOpenMetaStore
        (Bool
False, Bool
False) -> Lens' LocalMetaStore TCState -> TCM ()
insert Lens' LocalMetaStore TCState
stSolvedMetaStore
        (Bool
True,  Bool
False) -> do
          Lens' LocalMetaStore TCState -> TCM ()
delete Lens' LocalMetaStore TCState
stOpenMetaStore
          Lens' LocalMetaStore TCState -> TCM ()
insert Lens' LocalMetaStore TCState
stSolvedMetaStore
        (Bool
False, Bool
True)  -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Insert a new meta-variable with associated information into the
-- local meta store.
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
m MetaVariable
mv
  | MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv) = Lens' LocalMetaStore TCState -> TCM ()
insert Lens' LocalMetaStore TCState
stOpenMetaStore
  | Bool
otherwise                       = Lens' LocalMetaStore TCState -> TCM ()
insert Lens' LocalMetaStore TCState
stSolvedMetaStore
  where
  insert :: Lens' LocalMetaStore TCState -> TCM ()
insert = (forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m MetaVariable
mv)

-- | Returns the 'MetaPriority' of the given local meta-variable.
getMetaPriority ::
  (HasCallStack, MonadDebug m, ReadTCState m) =>
  MetaId -> m MetaPriority
getMetaPriority :: forall (m :: * -> *).
(HasCallStack, MonadDebug 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta

isSortMeta :: ReadTCState m => MetaId -> m Bool
isSortMeta :: forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
isSortMeta MetaId
m = forall a. Judgement a -> Bool
isSortJudgement forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m

isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ MetaVariable
mv = forall a. Judgement a -> Bool
isSortJudgement (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv)

isSortJudgement :: Judgement a -> Bool
isSortJudgement :: forall a. Judgement a -> Bool
isSortJudgement HasType{} = Bool
False
isSortJudgement IsSort{}  = Bool
True

getMetaType :: ReadTCState m => MetaId -> m Type
getMetaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m = do
  Judgement MetaId
j <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Judgement MetaId
j of
    HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type
t
    IsSort{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Compute the context variables that a local meta-variable should
-- be applied to, accounting for pruning.
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

-- | Given a local meta-variable, return the type applied to the
-- current context.
getMetaTypeInContext ::
  (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
   MonadTCEnv m, ReadTCState m) =>
  MetaId -> m Type
getMetaTypeInContext :: forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m,
 MonadTCEnv m, ReadTCState m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m = do
  mv :: MetaVariable
mv@MetaVar{ mvJudgement :: MetaVariable -> Judgement MetaId
mvJudgement = Judgement MetaId
j } <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta 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__

-- | Is it a local meta-variable that might be generalized?
isGeneralizableMeta ::
  (HasCallStack, MonadDebug m, ReadTCState m) =>
  MetaId -> m DoGeneralize
isGeneralizableMeta :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x

-- | Check whether all metas are instantiated.
--   Precondition: argument is a meta (in some form) or a list of metas.
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

-- | Does not worry about raising.
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
  MetaInstantiation
inst <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case MetaInstantiation
inst of
    InstV Instantiation
inst -> 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 (Instantiation -> Term
instBody Instantiation
inst) (Instantiation -> [Arg [Char]]
instTel Instantiation
inst)
    MetaInstantiation
_          -> forall a. Maybe a
Nothing

-- | Returns all metavariables in a constraint. Slightly complicated by the
--   fact that blocked terms are represented by two meta variables. To find the
--   second one we need to look up the meta listeners for the one in the
--   UnBlock constraint.
--   This is used for the purpose of deciding if a metavariable is constrained or if it can be
--   generalized over (see Agda.TypeChecking.Generalize).
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas :: Constraint -> TCM (Set MetaId)
constraintMetas = \case
    -- We don't use allMetas here since some constraints should not stop us from generalizing. For
    -- instance CheckSizeLtSat (see #3694). We also have to check meta listeners to get metas of
    -- UnBlock constraints.
    -- #5147: Don't count metas in the type of a constraint. For instance the constraint u = v : t
    -- should not stop us from generalize metas in t, since we could never solve those metas based
    -- on that constraint alone.
      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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
x)
      FindInstance MetaId
x Maybe [Candidate]
_         ->
        -- #5093: We should not generalize over metas bound by instance constraints.
        -- We keep instance constraints even if the meta is solved, to check that it could indeed
        -- be filled by instance search. If it's solved, look in the solution.
        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
      CheckDataSort{}          -> 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
    -- For blocked constant twin variables
    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)

-- | Create 'MetaInfo' in the current environment.
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
                          -- The ArgInfo is set to the right value in
                          -- the newArgsMetaCtx' function.
    }

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 ::
  (HasCallStack, MonadDebug m, ReadTCState m) =>
  MetaId -> m MetaNameSuggestion
getMetaNameSuggestion :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Char]
getMetaNameSuggestion MetaId
mi =
  MetaInfo -> [Char]
miNameSuggestion 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi

setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaNameSuggestion :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s = 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 }}

-- | Change the ArgInfo that will be used when generalizing over this
-- local meta-variable.
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 } }

-- * Query and manipulate interaction points.

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

-- | Register an interaction point during scope checking.
--   If there is no interaction id yet, create one.
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 we're given an interaction id we shouldn't look up by range.
  -- This is important when doing 'refine', since all interaction points
  -- created by the refine gets the same range.
  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
    -- If the range does not come from a file, it is not
    -- precise, so ignore it.
    forall a b. Maybe a -> b -> (a -> b) -> b
Strict.caseMaybe (Range -> Maybe RangeFile
rangeFile Range
r) (InteractionPoints -> m InteractionId
continue InteractionPoints
m) forall a b. (a -> b) -> a -> b
$ \ RangeFile
_ -> do
    -- First, try to find the interaction point by Range.
    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) {-else-} forall (m :: * -> *) a. Monad m => a -> m a
return
 where
 continue :: InteractionPoints -> m InteractionId
 continue :: InteractionPoints -> m InteractionId
continue InteractionPoints
m = do
  -- We did not find an interaction id with the same Range, so let's create one!
  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
    -- If the interaction point is already present, we keep the old ip.
    -- However, it needs to be at the same range as the new one.
    (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

-- | Find an interaction point by 'Range' by searching the whole map.
--   Issue 3000: Don't consider solved interaction points.
--
--   O(n): linear in the number of registered interaction points.

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

-- | Hook up a local meta-variable to an interaction point.
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 }
  -- The interaction point needs to be present already, we just set the meta.
  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'

-- | Mark an interaction point as solved.
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

-- | Get a list of interaction ids.
{-# 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

-- | Get all metas that correspond to unsolved interaction ids.
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 ::
  (HasCallStack, MonadDebug m, ReadTCState m) => [MetaId] -> m [Range]
getUniqueMetasRanges :: forall (m :: * -> *).
(HasCallStack, MonadDebug 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange

getUnsolvedMetas ::
  (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
getUnsolvedMetas :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedMetas = do
  [MetaId]
openMetas            <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
  [MetaId]
interactionMetas     <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
  forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges ([MetaId]
openMetas forall a. Eq a => [a] -> [a] -> [a]
List.\\ [MetaId]
interactionMetas)

getUnsolvedInteractionMetas ::
  (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas = forall (m :: * -> *).
(HasCallStack, MonadDebug 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

-- | Get all metas that correspond to unsolved interaction ids.
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

-- | Does the meta variable correspond to an interaction point?
--
--   Time: @O(log n)@ where @n@ is the number of interaction metas.
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

-- | Get the information associated to an interaction point.
{-# 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

-- | Get 'MetaId' for an interaction point.
--   Precondition: interaction point is connected.
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?)"

-- | Check whether an interaction id is already associated with a meta variable.
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

-- | Generate new meta variable.
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

-- | Generate a new meta variable with some instantiation given.
--   For instance, the instantiation could be a 'PostponedTypeCheckingProblem'.
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 }  -- fill the identifier part of the judgement
      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
                  }
  -- printing not available (import cycle)
  -- reportSDoc "tc.meta.new" 50 $ "new meta" <+> prettyTCM j'
  MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
x MetaVariable
mv
  forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x

-- | Get the 'Range' for an interaction point.
{-# 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

-- | Get the 'Range' for a local meta-variable.
getMetaRange ::
  (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Range
getMetaRange :: forall (m :: * -> *).
(HasCallStack, MonadDebug 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta

getInteractionScope ::
  (MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
   MonadTCEnv m) =>
  InteractionId -> m ScopeInfo
getInteractionScope :: forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope =
  MetaVariable -> ScopeInfo
getMetaScope forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta 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 ::
  (MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
   MonadTCEnv m, MonadTrace m) =>
  InteractionId -> m a -> m a
withInteractionId :: forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i m a
ret = do
  MetaId
m <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
  forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId MetaId
m m a
ret

withMetaId ::
  (HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
   ReadTCState m) =>
  MetaId -> m a -> m a
withMetaId :: forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId MetaId
m m a
ret = do
  MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
mv m a
ret

getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas = forall k a. Map k a -> [k]
MapS.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' LocalMetaStore TCState
stOpenMetaStore

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 l m@: register @l@ as a listener to @m@. This is done
--   when the type of l is blocked by @m@.
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 }

-- | Unregister a listener.
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 }

-- | Get the listeners for a local meta-variable.
getMetaListeners ::
  (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m [Listener]
getMetaListeners :: forall (m :: * -> *).
(HasCallStack, MonadDebug 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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m

clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
clearMetaListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
clearMetaListeners MetaId
m =
  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 }

-- | Do safe eta-expansions for meta (@SingletonRecords,Levels@).
etaExpandMetaSafe :: (MonadMetaSolver m) => MetaId -> m ()
etaExpandMetaSafe :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe = forall (m :: * -> *).
MonadMetaSolver m =>
[MetaKind] -> MetaId -> m ()
etaExpandMeta [MetaKind
SingletonRecords,MetaKind
Levels]

-- | Eta expand metavariables listening on the current meta.
etaExpandListeners :: MonadMetaSolver m => MetaId -> m ()
etaExpandListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
m = do
  [Listener]
ls <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
m
  forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
clearMetaListeners MetaId
m  -- we don't really have to do this
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (m :: * -> *). MonadMetaSolver m => Listener -> m ()
wakeupListener [Listener]
ls

-- | Wake up a meta listener and let it do its thing
wakeupListener :: MonadMetaSolver m => Listener -> m ()
  -- Andreas 2010-10-15: do not expand record mvars, lazyness needed for irrelevance
wakeupListener :: forall (m :: * -> *). MonadMetaSolver m => Listener -> m ()
wakeupListener (EtaExpand MetaId
x)         = forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
wakeupListener (CheckConstraint Int
_ ProblemConstraint
c) = do
  --reportSDoc "tc.meta.blocked" 20 $ "waking boxed constraint" <+> prettyTCM c
  forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints (ProblemConstraint
cforall a. a -> [a] -> [a]
:)
  forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

solveAwakeConstraints :: (MonadConstraint m) => m ()
solveAwakeConstraints :: forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints = forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
False

solveAwakeConstraints' :: (MonadConstraint m) => Bool -> m ()
solveAwakeConstraints' :: forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' = forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> Bool -> m ()
solveSomeAwakeConstraints (forall a b. a -> b -> a
const Bool
True)

---------------------------------------------------------------------------
-- * Freezing and unfreezing metas.
---------------------------------------------------------------------------

-- | Freeze the given meta-variables (but only if they are open) and
-- return those that were not already frozen.
freezeMetas :: MonadTCState m => LocalMetaStore -> m (Set MetaId)
freezeMetas :: forall (m :: * -> *).
MonadTCState m =>
LocalMetaStore -> m (Set MetaId)
freezeMetas LocalMetaStore
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' LocalMetaStore TCState
stOpenMetaStore 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 =>
MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
MapS.keys LocalMetaStore
ms)
  where
  freeze ::
    Monad m =>
    MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
  freeze :: forall (m :: * -> *).
Monad m =>
MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze MetaId
m = do
    LocalMetaStore
store <- forall s (m :: * -> *). MonadState s m => m s
get
    case forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m LocalMetaStore
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 (forall a. a -> Set a
Set.singleton MetaId
m)
          forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m (MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Frozen }) LocalMetaStore
store
        | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Maybe MetaVariable
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Thaw all open meta variables.
unfreezeMetas :: TCM ()
unfreezeMetas :: TCM ()
unfreezeMetas = Lens' LocalMetaStore TCState
stOpenMetaStore forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall a b k. (a -> b) -> Map k a -> Map k b
MapS.map MetaVariable -> MetaVariable
unfreeze
  where
  unfreeze :: MetaVariable -> MetaVariable
  unfreeze :: MetaVariable -> MetaVariable
unfreeze MetaVariable
mvar = MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }

isFrozen ::
  (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Bool
isFrozen :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x = do
  MetaVariable
mvar <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta 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

withFrozenMetas
  :: (MonadMetaSolver m, MonadTCState m)
  => m a -> m a
withFrozenMetas :: forall (m :: * -> *) a.
(MonadMetaSolver m, MonadTCState m) =>
m a -> m a
withFrozenMetas m a
act = do
  LocalMetaStore
openMetas <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' LocalMetaStore TCState
stOpenMetaStore
  Set MetaId
frozenMetas <- forall (m :: * -> *).
MonadTCState m =>
LocalMetaStore -> m (Set MetaId)
freezeMetas LocalMetaStore
openMetas
  a
result <- m a
act
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Set a -> [a]
Set.toList Set MetaId
frozenMetas) forall a b. (a -> b) -> a -> b
$ \MetaId
m ->
    forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv -> MetaVariable
mv { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }
  forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Unfreeze a meta and its type if this is a meta again.
--   Does not unfreeze deep occurrences of meta-variables or remote
--   meta-variables.
class UnFreezeMeta a where
  unfreezeMeta :: MonadMetaSolver m => a -> m ()

instance UnFreezeMeta MetaId where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((forall a b. (a -> b) -> a -> b
$ MetaId
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta) forall a b. (a -> b) -> a -> b
$ 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 :: * -> *). 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