{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.Monad.MetaVars where

import Prelude hiding (null)

import Control.Monad.Except         ( ExceptT, MonadError )
import Control.Monad.State          ( StateT, execStateT, get, put )
import Control.Monad.Trans          ( MonadTrans, lift )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Trans.Maybe    ( MaybeT )
import Control.Monad.Reader         ( ReaderT(ReaderT), runReaderT )
import Control.Monad.Writer         ( WriterT, execWriterT, tell )

import Data.HashMap.Strict qualified as HMap
import Data.List qualified as List
import Data.Map.Strict qualified as MapS
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Foldable qualified as Fold
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.Short qualified as TS

import GHC.Stack (HasCallStack)

import Mikan.Syntax.Common
import Mikan.Syntax.Info ( MetaKind (InstanceMeta, UnificationMeta), MetaNameSuggestion )
import Mikan.Syntax.Internal
import Mikan.Syntax.Internal.MetaVars
import Mikan.Syntax.Position
import Mikan.Syntax.Scope.Base
import Mikan.Syntax.Common.Pretty (pretty, prettyShow, (<+>))

import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Monad.Builtin (HasBuiltins)
import Mikan.TypeChecking.Monad.Trace
import Mikan.TypeChecking.Monad.Closure
import Mikan.TypeChecking.Monad.Constraints (MonadConstraint(..))
import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Monad.Debug
  (MonadDebug, reportSLn, reportSDoc, __IMPOSSIBLE_VERBOSE__)
import Mikan.TypeChecking.Monad.Context
import Mikan.TypeChecking.Monad.Signature (HasConstInfo)
import Mikan.TypeChecking.Monad.State
import Mikan.TypeChecking.Substitute
import {-# SOURCE #-} Mikan.TypeChecking.Telescope

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

import Mikan.Utils.Impossible
-- import Mikan.Interaction.Errors

-- | Various classes of metavariables.

data MetaClass =
    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 (MetaClass -> MetaClass -> Bool
(MetaClass -> MetaClass -> Bool)
-> (MetaClass -> MetaClass -> Bool) -> Eq MetaClass
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaClass -> MetaClass -> Bool
== :: MetaClass -> MetaClass -> Bool
$c/= :: MetaClass -> MetaClass -> Bool
/= :: MetaClass -> MetaClass -> Bool
Eq, Int -> MetaClass
MetaClass -> Int
MetaClass -> [MetaClass]
MetaClass -> MetaClass
MetaClass -> MetaClass -> [MetaClass]
MetaClass -> MetaClass -> MetaClass -> [MetaClass]
(MetaClass -> MetaClass)
-> (MetaClass -> MetaClass)
-> (Int -> MetaClass)
-> (MetaClass -> Int)
-> (MetaClass -> [MetaClass])
-> (MetaClass -> MetaClass -> [MetaClass])
-> (MetaClass -> MetaClass -> [MetaClass])
-> (MetaClass -> MetaClass -> MetaClass -> [MetaClass])
-> Enum MetaClass
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: MetaClass -> MetaClass
succ :: MetaClass -> MetaClass
$cpred :: MetaClass -> MetaClass
pred :: MetaClass -> MetaClass
$ctoEnum :: Int -> MetaClass
toEnum :: Int -> MetaClass
$cfromEnum :: MetaClass -> Int
fromEnum :: MetaClass -> Int
$cenumFrom :: MetaClass -> [MetaClass]
enumFrom :: MetaClass -> [MetaClass]
$cenumFromThen :: MetaClass -> MetaClass -> [MetaClass]
enumFromThen :: MetaClass -> MetaClass -> [MetaClass]
$cenumFromTo :: MetaClass -> MetaClass -> [MetaClass]
enumFromTo :: MetaClass -> MetaClass -> [MetaClass]
$cenumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass]
enumFromThenTo :: MetaClass -> MetaClass -> MetaClass -> [MetaClass]
Enum, MetaClass
MetaClass -> MetaClass -> Bounded MetaClass
forall a. a -> a -> Bounded a
$cminBound :: MetaClass
minBound :: MetaClass
$cmaxBound :: MetaClass
maxBound :: MetaClass
Bounded, Int -> MetaClass -> ShowS
[MetaClass] -> ShowS
MetaClass -> String
(Int -> MetaClass -> ShowS)
-> (MetaClass -> String)
-> ([MetaClass] -> ShowS)
-> Show MetaClass
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaClass -> ShowS
showsPrec :: Int -> MetaClass -> ShowS
$cshow :: MetaClass -> String
show :: MetaClass -> String
$cshowList :: [MetaClass] -> ShowS
showList :: [MetaClass] -> ShowS
Show)

-- | All possible metavariable classes.

allMetaClasses :: [MetaClass]
allMetaClasses :: [MetaClass]
allMetaClasses = [MetaClass
forall a. Bounded a => a
minBound .. MetaClass
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' :: MetaId -> [Arg ArgName] -> Term -> m ()

  -- | Eta-expand a local meta-variable, if it is of the specified
  -- class. Don't do anything if the meta-variable is a blocked term.
  etaExpandMeta :: [MetaClass] -> 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 = m MetaId -> ReaderT r m MetaId
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m MetaId -> ReaderT r m MetaId) -> m MetaId -> ReaderT r m MetaId
forall a b. (a -> b) -> a -> b
$ MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
inst Frozen
f MetaInfo
i MetaPriority
p Permutation
perm Judgement a
j
  assignV :: CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> ReaderT r m ()
assignV CompareDirection
dir MetaId
m Args
us Term
v CompareAs
cmp = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
assignV CompareDirection
dir MetaId
m Args
us Term
v CompareAs
cmp
  assignTerm' :: MetaId -> [Arg ArgName] -> Term -> ReaderT r m ()
assignTerm' MetaId
m [Arg ArgName]
us Term
v = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg ArgName] -> Term -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg ArgName] -> Term -> m ()
assignTerm' MetaId
m [Arg ArgName]
us Term
v
  etaExpandMeta :: [MetaClass] -> MetaId -> ReaderT r m ()
etaExpandMeta [MetaClass]
k MetaId
m = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ [MetaClass] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaClass] -> MetaId -> m ()
etaExpandMeta [MetaClass]
k MetaId
m
  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> ReaderT r m ()
updateMetaVar MetaId
m MetaVariable -> MetaVariable
f = m () -> ReaderT r m ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT r m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ()) -> m () -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m MetaVariable -> MetaVariable
f
  speculateMetas :: ReaderT r m () -> ReaderT r m KeepMetas -> ReaderT r m ()
speculateMetas ReaderT r m ()
fallback ReaderT r m KeepMetas
m = (r -> m ()) -> ReaderT r m ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m ()) -> ReaderT r m ()) -> (r -> m ()) -> ReaderT r m ()
forall a b. (a -> b) -> a -> b
$ \r
x -> m () -> m KeepMetas -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
m () -> m KeepMetas -> m ()
speculateMetas (ReaderT r m () -> r -> m ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m ()
fallback r
x) (ReaderT r m KeepMetas -> r -> m KeepMetas
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT r m KeepMetas
m r
x)

-- | Switch off assignment of metas.
dontAssignMetas :: (MonadTCEnv m, MonadDebug m) => m a -> m a
dontAssignMetas :: forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
dontAssignMetas m a
cont = do
  String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta" Int
45 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"don't assign metas"
  (TCEnv -> TCEnv) -> m a -> m a
forall a. (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
eAssignMetas 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
  h <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
  return (\MetaId
m -> ModuleNameHash
h ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
/= MetaId -> ModuleNameHash
metaModule MetaId
m)

-- | 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 = Lens' TCState MetaId -> m MetaId
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (MetaId -> f MetaId) -> TCState -> f TCState
Lens' TCState MetaId
stFreshMetaId

-- | 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
  !nextMeta <- m MetaId
forall (m :: * -> *). ReadTCState m => m MetaId
nextLocalMeta
  a         <- m
  os        <- created stOpenMetaStore   nextMeta
  ss        <- created stSolvedMetaStore nextMeta
  return (a, LocalMetaStores { openMetas = os, solvedMetas = ss })
  where
  created :: Lens' TCState LocalMetaStore -> MetaId -> m LocalMetaStore
  created :: Lens' TCState LocalMetaStore -> MetaId -> m LocalMetaStore
created Lens' TCState LocalMetaStore
store MetaId
next = do
    ms <- Getter TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
Getter TCState LocalMetaStore
store
    return $ case MapS.splitLookup next ms of
      (LocalMetaStore
_, Maybe MetaVariable
Nothing, LocalMetaStore
ms) -> LocalMetaStore
ms
      (LocalMetaStore
_, Just MetaVariable
m,  LocalMetaStore
ms) -> MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
next MetaVariable
m LocalMetaStore
ms

-- | Find information about the given local meta-variable, if any.
{-# SPECIALIZE lookupLocalMeta' :: MetaId -> TCM (Maybe MetaVariable) #-}
lookupLocalMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m = do
  tc <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  case MapS.lookup m (tc ^. stSolvedMetaStore) of
    mv :: Maybe MetaVariable
mv@Just{} -> Maybe MetaVariable -> m (Maybe MetaVariable)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe MetaVariable
mv
    Maybe MetaVariable
Nothing   -> Maybe MetaVariable -> m (Maybe MetaVariable)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe MetaVariable -> m (Maybe MetaVariable))
-> Maybe MetaVariable -> m (Maybe MetaVariable)
forall a b. (a -> b) -> a -> b
$! MetaId -> LocalMetaStore -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m (TCState
tc TCState
-> Getting LocalMetaStore TCState LocalMetaStore -> LocalMetaStore
forall s a. s -> Getting a s a -> a
^. Getting LocalMetaStore TCState LocalMetaStore
Lens' TCState LocalMetaStore
stOpenMetaStore)

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

{-# SPECIALIZE lookupLocalMeta :: MetaId -> TCM MetaVariable #-}
lookupLocalMeta ::
  (HasCallStack, MonadDebug m, ReadTCState m) =>
  MetaId -> m MetaVariable
lookupLocalMeta :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m =
  m MetaVariable -> m (Maybe MetaVariable) -> m MetaVariable
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (String -> m MetaVariable
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
err) (m (Maybe MetaVariable) -> m MetaVariable)
-> m (Maybe MetaVariable) -> m MetaVariable
forall a b. (a -> b) -> a -> b
$ MetaId -> m (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
  where
  err :: String
err = String
"no such local meta-variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
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.

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

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

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

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

{-# INLINE getMetaType #-}
-- | The type of a term or sort meta-variable.
getMetaType :: ReadTCState m => MetaId -> m Type
getMetaType :: forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
x = do
  t <- Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype)
-> m (Judgement MetaId) -> m Teletype
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Judgement MetaId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
x
  pure $! teleApply t []

-- | 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
  mv <- MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
m
  case mv of
    Maybe MetaVariable
Nothing -> do
      mv <- MetaId -> TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
      case mv of
        Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> String -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__
                     (String
"Meta-variable not found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
m)
        Just{}  -> String -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__
                     (String
"Attempt to update remote meta-variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
m)
    Just MetaVariable
mv -> do
      let mv' :: MetaVariable
mv'    = MetaVariable -> MetaVariable
f MetaVariable
mv
          insert :: ASetter' TCState LocalMetaStore -> TCM ()
insert = (ASetter' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m MetaVariable
mv')
          delete :: ASetter' TCState LocalMetaStore -> TCM ()
delete = (ASetter' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` MetaId -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> Map k a -> Map k a
MapS.delete MetaId
m)
      case ( MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv)
           , MetaInstantiation -> Bool
isOpenMeta (MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv')
           ) of
        (Bool
True,  Bool
True)  -> ASetter' TCState LocalMetaStore -> TCM ()
insert ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stOpenMetaStore
        (Bool
False, Bool
False) -> ASetter' TCState LocalMetaStore -> TCM ()
insert ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stSolvedMetaStore
        (Bool
True,  Bool
False) -> do
          ASetter' TCState LocalMetaStore -> TCM ()
delete ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stOpenMetaStore
          ASetter' TCState LocalMetaStore -> TCM ()
insert ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stSolvedMetaStore
        (Bool
False, Bool
True)  -> TCM ()
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) = ASetter' TCState LocalMetaStore -> TCM ()
insert ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stOpenMetaStore
  | Bool
otherwise                       = ASetter' TCState LocalMetaStore -> TCM ()
insert ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stSolvedMetaStore
  where
  insert :: ASetter' TCState LocalMetaStore -> TCM ()
insert = (ASetter' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m MetaVariable
mv)

{-# INLINE getMetaPriority #-}
-- | 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 (MetaVariable -> MetaPriority)
-> (MetaId -> m MetaVariable) -> MetaId -> m MetaPriority
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta

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

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

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

-- | If a meta variable is still open, what is its kind?
--
metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
metaInstantiationToMetaKind :: MetaInstantiation -> MetaKind
metaInstantiationToMetaKind = \case
  OpenMeta MetaKind
k                     -> MetaKind
k
  InstV{}                        -> MetaKind
forall a. Null a => a
empty
  BlockedConst{}                 -> MetaKind
forall a. Null a => a
empty
  PostponedTypeCheckingProblem{} -> MetaKind
forall a. Null a => a
empty

{-# SPECIALIZE getMetaContextArgs :: MetaVariable -> TCM Args #-}
-- | 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 <- m Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  return $ permute (takeP (length args) p) args

{-# SPECIALIZE getMetaTypeInContext :: MetaId -> TCM Type #-}
-- | Given a local meta-variable, return the type applied to the
-- current context.
getMetaTypeInContext ::
  (HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m) =>
  MetaId -> m Type
getMetaTypeInContext :: forall (m :: * -> *).
(HasBuiltins m, HasCallStack, MonadDebug m, MonadReduce m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m = do
  mv@MetaVar{ mvJudgement = j } <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
  case j of
    HasType{ jMetaType :: forall a. Judgement a -> Teletype
jMetaType = Teletype
t } -> HasCallStack => Teletype -> Args -> Type
Teletype -> Args -> Type
teleApply Teletype
t (Args -> Type) -> m Args -> m Type
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> MetaVariable -> m Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
    IsSort{}                 -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# SPECIALIZE isGeneralizableMeta :: MetaId -> TCM DoGeneralize #-}
-- | 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 =
  Arg DoGeneralize -> DoGeneralize
forall e. Arg e -> e
unArg (Arg DoGeneralize -> DoGeneralize)
-> (MetaVariable -> Arg DoGeneralize)
-> MetaVariable
-> DoGeneralize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaInfo -> Arg DoGeneralize)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Arg DoGeneralize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> DoGeneralize) -> m MetaVariable -> m DoGeneralize
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x

{-# INLINE isInstantiatedMeta #-}
-- | Check whether all metas are instantiated.
isInstantiatedMeta :: (ReadTCState m) => MetaId -> m Bool
isInstantiatedMeta :: forall (m :: * -> *). ReadTCState m => MetaId -> m Bool
isInstantiatedMeta MetaId
m = do
  MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m m MetaInstantiation -> (MetaInstantiation -> Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    InstV {} -> Bool
True
    MetaInstantiation
_ -> Bool
False

{-# SPECIALIZE isInstantiatedMeta' :: MetaId -> TCM (Maybe Term) #-}
isInstantiatedMeta' :: (ReadTCState m) => MetaId -> m (Maybe Term)
isInstantiatedMeta' :: forall (m :: * -> *). ReadTCState m => MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
m = do
  inst <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
  return $ case inst of
    InstV Instantiation
inst -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Arg ArgName -> Term -> Term) -> Term -> [Arg ArgName] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg ArgName -> Term -> Term
mkLam (Instantiation -> Term
instBody Instantiation
inst) (Instantiation -> [Arg ArgName]
instTel Instantiation
inst)
    MetaInstantiation
_          -> Maybe Term
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         -> (Term, Term) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Term
u, Term
v)
      ValueCmpOnFace Comparison
_ Term
p Type
_ Term
u Term
v -> (Term, Term, Term) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Term
p, Term
u, Term
v)
      ElimCmp [Polarity]
_ [IsForced]
_ Type
_ Term
_ Elims
es Elims
es'   -> (Elims, Elims) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Elims
es, Elims
es')
      LevelCmp Comparison
_ Level
l Level
l'          -> (Term, Term) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Level -> Term
Level Level
l, Level -> Term
Level Level
l')
      UnquoteTactic Term
t Term
h Type
g      -> (Term, Term, Type) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Term
t, Term
h, Type
g)
      SortCmp Comparison
_ Sort
s1 Sort
s2          -> (Term, Term) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)
      UnBlock MetaId
x                -> MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => a -> Set a -> Set a
Set.insert MetaId
x (Set MetaId -> Set MetaId)
-> ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId)
-> TCMT IO [Set MetaId] -> TCM (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Listener -> TCM (Set MetaId))
-> [Listener] -> TCMT IO [Set MetaId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Listener -> TCM (Set MetaId)
listenerMetas ([Listener] -> TCMT IO [Set MetaId])
-> TCMT IO [Listener] -> TCMT IO [Set MetaId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO [Listener]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
x)
      FindInstance Range
_ 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.
        TCMT IO (Maybe Term)
-> TCM (Set MetaId)
-> (Term -> TCM (Set MetaId))
-> TCM (Set MetaId)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (MetaId -> TCMT IO (Maybe Term)
forall (m :: * -> *). ReadTCState m => MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
x) (Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
x) ((Term -> TCM (Set MetaId)) -> TCM (Set MetaId))
-> (Term -> TCM (Set MetaId)) -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId))
-> (Term -> Set MetaId) -> Term -> TCM (Set MetaId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> Set MetaId) -> Term -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Term -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton
      ResolveInstanceHead{}    -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      IsEmpty{}                -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckFunDef{}            -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      HasPTSRule{}             -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckDataSort{}          -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckMetaInst MetaId
x          -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckType Type
t              -> Type -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas Type
t
  where
    -- For blocked constant twin variables
    listenerMetas :: Listener -> TCM (Set MetaId)
listenerMetas EtaExpand{}           = Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Set a
Set.empty
    listenerMetas (CheckConstraint Int
_ ProblemConstraint
c) = Constraint -> TCM (Set MetaId)
constraintMetas (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c)

    gatherMetas :: AllMetas t => t -> TCM (Set MetaId)
    gatherMetas :: forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas = (MetaId -> TCM (Set MetaId)) -> t -> TCM (Set MetaId)
forall m. Monoid m => (MetaId -> m) -> t -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> TCM (Set MetaId)
makeSingle

    makeSingle :: MetaId -> TCM (Set MetaId)
    makeSingle :: MetaId -> TCM (Set MetaId)
makeSingle MetaId
m = MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m TCMT IO MetaInstantiation
-> (MetaInstantiation -> TCM (Set MetaId)) -> TCM (Set MetaId)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      InstV Instantiation
i -> Term -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Term -> TCM (Set MetaId)) -> Term -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ Instantiation -> Term
instBody Instantiation
i
      OpenMeta MetaKind
_ -> Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
m
      BlockedConst Term
t ->
        -- Jesper, 2025-05-13: We should really look into the
        -- (blocked) solution here but doing so triggers a
        -- regression in the standard library that I'm too tired
        -- to deal with (see test/Succeed/Issue7876b.agda).
        -- Set.insert m <$> gatherMetas t
        Set MetaId -> TCM (Set MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
m
      PostponedTypeCheckingProblem Closure TypeCheckingProblem
clos -> MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => a -> Set a -> Set a
Set.insert MetaId
m (Set MetaId -> Set MetaId) -> TCM (Set MetaId) -> TCM (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeCheckingProblem -> TCM (Set MetaId)
tcProblemMetas (Closure TypeCheckingProblem -> TypeCheckingProblem
forall a. Closure a -> a
clValue Closure TypeCheckingProblem
clos)

    tcProblemMetas :: TypeCheckingProblem -> TCM (Set MetaId)
    tcProblemMetas :: TypeCheckingProblem -> TCM (Set MetaId)
tcProblemMetas = \case
      CheckExpr Comparison
_ Expr
_ Type
ty -> Type -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas Type
ty
      CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
_ Type
ty1 Type
ty2 ArgsCheckState CheckedTarget -> TCM Term
_ -> (Type, Type) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Type
ty1, Type
ty2)
      CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type
ty1 Int
_ Term
u Type
ty2 PrincipalArgTypeMetas
patm -> (Term, Type, Type, PrincipalArgTypeMetas) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Term
u, Type
ty1, Type
ty2, PrincipalArgTypeMetas
patm)
      DisambiguateConstructor ConstructorDisambiguationData
cdd ConHead -> TCM Term
_ -> Type -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Type -> TCM (Set MetaId)) -> Type -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ ConstructorDisambiguationData -> Type
bcdType ConstructorDisambiguationData
cdd
      DoQuoteTerm Comparison
_ Term
u Type
ty -> (Term, Type) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Term
u, Type
ty)
      CheckWithApp     Comparison
_ Type
ty WithAppHead
_ QName
_ Elims
as List1 Expr
_ -> (Type, Elims) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Type
ty, Elims
as)
      CheckWithAppHead Comparison
_ Type
ty Expr
_ Term
as List1 Expr
_   -> (Type, Term) -> TCM (Set MetaId)
forall t. AllMetas t => t -> TCM (Set MetaId)
gatherMetas (Type
ty, Term
as)

-- | Create 'MetaInfo' in the current environment.
createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo :: forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo = RunMetaOccursCheck -> m MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
RunMetaOccursCheck

createMetaInfo'
  :: (MonadTCEnv m, ReadTCState m)
  => RunMetaOccursCheck -> m MetaInfo
createMetaInfo' :: forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b = do
  r        <- m Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange
  cl       <- buildClosure r
  gen      <- viewTC eGeneralizeMetas
  return MetaInfo
    { miClosRange       = cl
    , miMetaOccursCheck = b
    , miNameSuggestion  = ""
    , miGeneralizable   = defaultArg gen
      -- The ArgInfo is set to the right value in createGenValue.
    }

setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
setValueMetaName :: forall (m :: * -> *). MonadMetaSolver m => Term -> ArgName -> m ()
setValueMetaName Term
v ArgName
s = do
  case Term
v of
    MetaV MetaId
mi Elims
_ -> MetaId -> ArgName -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
mi ArgName
s
    Term
u          -> do
      String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta.name" Int
70 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$
        String
"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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

getMetaNameSuggestion ::
  (HasCallStack, MonadDebug m, ReadTCState m) =>
  MetaId -> m MetaNameSuggestion
getMetaNameSuggestion :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion MetaId
mi =
  MetaInfo -> ArgName
miNameSuggestion (MetaInfo -> ArgName)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> ArgName) -> m MetaVariable -> m ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi

setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaNameSuggestion :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
mi ArgName
s = Bool -> m () -> m ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (ArgName -> Bool
forall a. Null a => a -> Bool
null ArgName
s Bool -> Bool -> Bool
|| ArgName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore ArgName
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 String
"tc.meta.name" Int
20 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$
    String
"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]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArgName -> String
TS.unpack ArgName
s
  MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
    MetaVariable
mvar { mvInfo = (mvInfo mvar) { miNameSuggestion = s }}

-- | 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 = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
  MetaVariable
mv { mvInfo = (mvInfo mv)
        { miGeneralizable = setArgInfo i (miGeneralizable (mvInfo mv)) } }

updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mi Range
r = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi (Range -> MetaVariable -> MetaVariable
forall a. SetRange a => Range -> a -> a
setRange Range
r)

setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck :: forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck MetaId
mi RunMetaOccursCheck
b = MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
  MetaVariable
mvar { mvInfo = (mvInfo mvar) { miMetaOccursCheck = b } }

-- * 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 = n InteractionId -> t n InteractionId
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId

  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
  default modifyInteractionPoints
    :: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
    => (InteractionPoints -> InteractionPoints) -> m ()
  modifyInteractionPoints = n () -> m ()
n () -> t n ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n () -> m ())
-> ((InteractionPoints -> InteractionPoints) -> n ())
-> (InteractionPoints -> InteractionPoints)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoints -> InteractionPoints) -> n ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints

instance MonadInteractionPoints m => MonadInteractionPoints (ExceptT e m)
instance MonadInteractionPoints m => MonadInteractionPoints (MaybeT m)
instance MonadInteractionPoints m => MonadInteractionPoints (IdentityT m)
instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)
instance MonadInteractionPoints m => MonadInteractionPoints (StateT s m)
instance (MonadInteractionPoints m, Monoid w) => MonadInteractionPoints (WriterT w m)

instance MonadInteractionPoints TCM where
  -- TODO: does the pure mode happen?
  freshInteractionId :: TCM InteractionId
freshInteractionId =
    TCM InteractionId -> TCM InteractionId -> TCM InteractionId
forall a. TCM a -> TCM a -> TCM a
ifImpureConv TCM InteractionId
forall i (m :: * -> *). MonadFresh i m => m i
fresh (Blocker -> TCM InteractionId
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock)
  -- TODO: does the pure mode happen?
  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
f =
    TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv ((InteractionPoints -> Identity InteractionPoints)
-> TCState -> Identity TCState
Lens' TCState InteractionPoints
stInteractionPoints ((InteractionPoints -> Identity InteractionPoints)
 -> TCState -> Identity TCState)
-> (InteractionPoints -> InteractionPoints) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` InteractionPoints -> InteractionPoints
f) (Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock)

-- | 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
  m <- Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
  -- If 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 not preciseRange || isJust maybeId then continue m else do
    -- If the range does not come from a file, it is not
    -- precise, so ignore it.
    Strict.caseMaybe (rangeFile r) (continue m) $ \ RangeFile
_ -> do
    -- First, try to find the interaction point by Range.
    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) {-else-} InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
 where
 continue :: InteractionPoints -> m InteractionId
 continue :: InteractionPoints -> m InteractionId
continue InteractionPoints
m = do
  -- We did not find an interaction id with the same Range, so let's create one!
  ii <- case Maybe Int
maybeId of
    Just Int
i  -> InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (InteractionId -> m InteractionId)
-> InteractionId -> m InteractionId
forall a b. (a -> b) -> a -> b
$ Int -> InteractionId
InteractionId Int
i
    Maybe Int
Nothing -> m InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
  let ip = InteractionPoint { ipRange :: Range
ipRange = Range
r, ipMeta :: Maybe MetaId
ipMeta = Maybe MetaId
forall a. Maybe a
Nothing, ipSolved :: Bool
ipSolved = Bool
False, ipClause :: IPClause
ipClause = IPClause
IPNoClause, ipBoundary :: IPBoundary
ipBoundary = Map (IntMap Bool) Term -> IPBoundary
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary Map (IntMap Bool) Term
forall a. Monoid a => a
mempty }
  case BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
old) ii ip m of
    -- 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 Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= InteractionPoint -> Range
ipRange InteractionPoint
ip0 -> m InteractionId
forall a. HasCallStack => a
__IMPOSSIBLE__
       | Bool
otherwise                 -> InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
    (Maybe InteractionPoint
Nothing, InteractionPoints
m') -> do
      (InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints (InteractionPoints -> InteractionPoints -> InteractionPoints
forall a b. a -> b -> a
const InteractionPoints
m')
      InteractionId -> m InteractionId
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii

-- | 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
  Bool -> Maybe ()
forall b (m :: * -> *). (IsBool b, MonadPlus m) => b -> m ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Range -> Bool
forall a. Null a => a -> Bool
null Range
r
  [InteractionId] -> Maybe InteractionId
forall a. [a] -> Maybe a
listToMaybe ([InteractionId] -> Maybe InteractionId)
-> [InteractionId] -> Maybe InteractionId
forall a b. (a -> b) -> a -> b
$ ((InteractionId, InteractionPoint) -> Maybe InteractionId)
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange ([(InteractionId, InteractionPoint)] -> [InteractionId])
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> b) -> a -> b
$ InteractionPoints -> [(InteractionId, InteractionPoint)]
forall k v. BiMap k v -> [(k, v)]
BiMap.toList InteractionPoints
m
  where
    sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
    sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange (InteractionId
ii, InteractionPoint Range
r' Maybe MetaId
_ Bool
False IPClause
_ IPBoundary
_) | Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
r' = InteractionId -> Maybe InteractionId
forall a. a -> Maybe a
Just InteractionId
ii
    sameRange (InteractionId, InteractionPoint)
_ = Maybe InteractionId
forall a. Maybe a
Nothing

{-# INLINABLE connectInteractionPoint #-}
-- | 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
  ipCl <- Lens' TCEnv IPClause -> m IPClause
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (IPClause -> f IPClause) -> TCEnv -> f TCEnv
Lens' TCEnv IPClause
eClause
  m <- useR stInteractionPoints
  let ip = InteractionPoint { ipRange :: Range
ipRange = Range
forall a. HasCallStack => a
__IMPOSSIBLE__, ipMeta :: Maybe MetaId
ipMeta = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
mi, ipSolved :: Bool
ipSolved = Bool
False, ipClause :: IPClause
ipClause = IPClause
ipCl, ipBoundary :: IPBoundary
ipBoundary = Map (IntMap Bool) Term -> IPBoundary
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary Map (IntMap Bool) Term
forall a. Monoid a => a
mempty }
  -- The interaction point needs to be present already, we just set the meta.
  case BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
new { ipRange = ipRange old }) ii ip m of
    (Maybe InteractionPoint
Nothing, InteractionPoints
_) -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Just InteractionPoint
_, InteractionPoints
m') -> (InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoints -> InteractionPoints) -> m ())
-> (InteractionPoints -> InteractionPoints) -> m ()
forall a b. (a -> b) -> a -> b
$ InteractionPoints -> InteractionPoints -> InteractionPoints
forall a b. a -> b -> a
const InteractionPoints
m'

-- | Mark an interaction point as solved.
removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
removeInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii =
  (InteractionPoints -> InteractionPoints) -> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoints -> InteractionPoints) -> m ())
-> (InteractionPoints -> InteractionPoints) -> m ()
forall a b. (a -> b) -> a -> b
$ (InteractionPoint -> Maybe InteractionPoint)
-> InteractionId -> InteractionPoints -> InteractionPoints
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> Maybe v) -> k -> BiMap k v -> BiMap k v
BiMap.update (\ InteractionPoint
ip -> InteractionPoint -> Maybe InteractionPoint
forall a. a -> Maybe a
Just InteractionPoint
ip{ ipSolved = True }) InteractionId
ii

-- | Get a list of unsolved interaction ids.
{-# SPECIALIZE getInteractionPoints :: TCM [InteractionId] #-}
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionPoints :: forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints =
  ((InteractionId, InteractionPoint) -> InteractionId)
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, InteractionPoint) -> InteractionId
forall a b. (a, b) -> a
fst ([(InteractionId, InteractionPoint)] -> [InteractionId])
-> (InteractionPoints -> [(InteractionId, InteractionPoint)])
-> InteractionPoints
-> [InteractionId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, InteractionPoint) -> Bool)
-> [(InteractionId, InteractionPoint)]
-> [(InteractionId, InteractionPoint)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((InteractionId, InteractionPoint) -> Bool)
-> (InteractionId, InteractionPoint)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved (InteractionPoint -> Bool)
-> ((InteractionId, InteractionPoint) -> InteractionPoint)
-> (InteractionId, InteractionPoint)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId, InteractionPoint) -> InteractionPoint
forall a b. (a, b) -> b
snd) ([(InteractionId, InteractionPoint)]
 -> [(InteractionId, InteractionPoint)])
-> (InteractionPoints -> [(InteractionId, InteractionPoint)])
-> InteractionPoints
-> [(InteractionId, InteractionPoint)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoints -> [(InteractionId, InteractionPoint)]
forall k v. BiMap k v -> [(k, v)]
BiMap.toList (InteractionPoints -> [InteractionId])
-> m InteractionPoints -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
  -- The following alternative will not include the unreachable IPs
  -- (e.g. test/interaction/Issue2807).
  -- This might lead to a wrong numbering of ?s.
  -- map fst <$> getInteractionIdsAndMetas

-- | Get all metas that correspond to unsolved interaction ids.
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas =
  (InteractionPoint -> Maybe MetaId)
-> [InteractionPoint] -> [MetaId]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe InteractionPoint -> Maybe MetaId
ipMeta ([InteractionPoint] -> [MetaId])
-> (InteractionPoints -> [InteractionPoint])
-> InteractionPoints
-> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoint -> Bool)
-> [InteractionPoint] -> [InteractionPoint]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (InteractionPoint -> Bool) -> InteractionPoint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved) ([InteractionPoint] -> [InteractionPoint])
-> (InteractionPoints -> [InteractionPoint])
-> InteractionPoints
-> [InteractionPoint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoints -> [InteractionPoint]
forall k v. BiMap k v -> [v]
BiMap.elems (InteractionPoints -> [MetaId])
-> m InteractionPoints -> m [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints

getUniqueMetasRanges ::
  (HasCallStack, MonadDebug m, ReadTCState m) => [MetaId] -> m [Range]
getUniqueMetasRanges :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges = ([Range] -> [Range]) -> m [Range] -> m [Range]
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Range -> Range) -> [Range] -> [Range]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn Range -> Range
forall a. a -> a
id) (m [Range] -> m [Range])
-> ([MetaId] -> m [Range]) -> [MetaId] -> m [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> m Range) -> [MetaId] -> m [Range]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM MetaId -> m Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange

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

getUnsolvedInteractionMetas ::
  (HasCallStack, MonadDebug m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
m [Range]
getUnsolvedInteractionMetas = [MetaId] -> m [Range]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges ([MetaId] -> m [Range]) -> m [MetaId] -> m [Range]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas

-- | Get all metas that correspond to unsolved interaction ids.
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId,MetaId)]
getInteractionIdsAndMetas :: forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas =
  ((InteractionId, InteractionPoint)
 -> Maybe (InteractionId, MetaId))
-> [(InteractionId, InteractionPoint)] -> [(InteractionId, MetaId)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe (InteractionId, MetaId)
forall {t}. (t, InteractionPoint) -> Maybe (t, MetaId)
f ([(InteractionId, InteractionPoint)] -> [(InteractionId, MetaId)])
-> (InteractionPoints -> [(InteractionId, InteractionPoint)])
-> InteractionPoints
-> [(InteractionId, MetaId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, InteractionPoint) -> Bool)
-> [(InteractionId, InteractionPoint)]
-> [(InteractionId, InteractionPoint)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((InteractionId, InteractionPoint) -> Bool)
-> (InteractionId, InteractionPoint)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint -> Bool
ipSolved (InteractionPoint -> Bool)
-> ((InteractionId, InteractionPoint) -> InteractionPoint)
-> (InteractionId, InteractionPoint)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId, InteractionPoint) -> InteractionPoint
forall a b. (a, b) -> b
snd) ([(InteractionId, InteractionPoint)]
 -> [(InteractionId, InteractionPoint)])
-> (InteractionPoints -> [(InteractionId, InteractionPoint)])
-> InteractionPoints
-> [(InteractionId, InteractionPoint)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoints -> [(InteractionId, InteractionPoint)]
forall k v. BiMap k v -> [(k, v)]
BiMap.toList (InteractionPoints -> [(InteractionId, MetaId)])
-> m InteractionPoints -> m [(InteractionId, MetaId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints
  where f :: (t, InteractionPoint) -> Maybe (t, MetaId)
f (t
ii, InteractionPoint
ip) = (t
ii,) (MetaId -> (t, MetaId)) -> Maybe MetaId -> Maybe (t, MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionPoint -> Maybe MetaId
ipMeta InteractionPoint
ip

-- | 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 = Tag InteractionPoint -> InteractionPoints -> Maybe InteractionId
forall v k. Ord (Tag v) => Tag v -> BiMap k v -> Maybe k
BiMap.invLookup Tag InteractionPoint
MetaId
x (InteractionPoints -> Maybe InteractionId)
-> m InteractionPoints -> m (Maybe InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints

-- | 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 (InteractionPoints -> Maybe MetaId)
-> m InteractionPoints -> m (Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState InteractionPoints -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints

lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ InteractionId
ii InteractionPoints
m = InteractionPoint -> Maybe MetaId
ipMeta (InteractionPoint -> Maybe MetaId)
-> Maybe InteractionPoint -> Maybe MetaId
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> InteractionPoints -> Maybe InteractionPoint
forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup InteractionId
ii InteractionPoints
m

-- | 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 = MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
forall (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' (MetaKind -> MetaInstantiation
OpenMeta MetaKind
UnificationMeta)

-- | 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
  x <- TCM MetaId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  let j' = Judgement a
j { jMetaId = x }  -- fill the identifier part of the judgement
      mv = MetaVar{ mvInfo :: MetaInfo
mvInfo             = MetaInfo
mi
                  , mvPriority :: MetaPriority
mvPriority         = MetaPriority
p
                  , mvPermutation :: Permutation
mvPermutation      = Permutation
perm
                  , mvJudgement :: Judgement MetaId
mvJudgement        = Judgement MetaId
j'
                  , mvInstantiation :: MetaInstantiation
mvInstantiation    = MetaInstantiation
inst
                  , mvListeners :: Set Listener
mvListeners        = Set Listener
forall a. Set a
Set.empty
                  , mvFrozen :: Frozen
mvFrozen           = Frozen
frozen
                  , mvTwin :: Maybe MetaId
mvTwin             = Maybe MetaId
forall a. Maybe a
Nothing
                  , mvError :: Bool
mvError            = Bool
False
                  }
  -- printing not available (import cycle)
  -- reportSDoc "tc.meta.new" 50 $ "new meta" <+> prettyTCM j'
  insertMetaVar x mv
  return x

-- | 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 = MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange (MetaVariable -> Range)
-> (MetaId -> m MetaVariable) -> MetaId -> m Range
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta


withMetaInfo' :: (MonadTrace m) => MetaVariable -> m a -> m a
withMetaInfo' :: forall (m :: * -> *) a. MonadTrace m => MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
mv = Closure Range -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Closure Range -> m a -> m a
withMetaInfo (MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)

withMetaInfo :: (MonadTrace m) => Closure Range -> m a -> m a
withMetaInfo :: forall (m :: * -> *) a. MonadTrace m => Closure Range -> m a -> m a
withMetaInfo Closure Range
mI m a
cont = Closure Range -> (Range -> m a) -> m a
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure Range
mI ((Range -> m a) -> m a) -> (Range -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \ Range
r ->
  Range -> m a -> m a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r m a
cont


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

getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas = LocalMetaStore -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys (LocalMetaStore -> [MetaId])
-> (LocalMetaStore -> LocalMetaStore) -> LocalMetaStore -> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaVariable -> Bool) -> LocalMetaStore -> LocalMetaStore
forall a k. (a -> Bool) -> Map k a -> Map k a
MapS.filter (Bool -> Bool
not (Bool -> Bool) -> (MetaVariable -> Bool) -> MetaVariable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Bool
mvError) (LocalMetaStore -> [MetaId]) -> m LocalMetaStore -> m [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore

isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta :: MetaInstantiation -> Bool
isOpenMeta OpenMeta{}                     = Bool
True
isOpenMeta BlockedConst{}                 = Bool
True
isOpenMeta PostponedTypeCheckingProblem{} = Bool
True
isOpenMeta InstV{}                        = Bool
False

-- | @listenToMeta 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 =
  MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners = Set.insert l $ mvListeners mv }

-- | Unregister a listener.
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
unlistenToMeta Listener
l MetaId
m =
  MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners = Set.delete l $ mvListeners mv }

-- | 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 = Set Listener -> [Listener]
forall a. Set a -> [a]
Set.toList (Set Listener -> [Listener])
-> (MetaVariable -> Set Listener) -> MetaVariable -> [Listener]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Set Listener
mvListeners (MetaVariable -> [Listener]) -> m MetaVariable -> m [Listener]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m

clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
clearMetaListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
clearMetaListeners MetaId
m =
  MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
m ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \MetaVariable
mv -> MetaVariable
mv { mvListeners = Set.empty }

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

-- | Eta expand metavariables listening on the current meta.
etaExpandListeners :: MonadMetaSolver m => MetaId -> m ()
etaExpandListeners :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
m = do
  ls <- MetaId -> m [Listener]
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
m
  clearMetaListeners m  -- we don't really have to do this
  mapM_ wakeupListener 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
  -- ncf 2026-05-10: this is no longer needed but doesn't hurt?
wakeupListener :: forall (m :: * -> *). MonadMetaSolver m => Listener -> m ()
wakeupListener (EtaExpand MetaId
x)         = MetaId -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandMetaSafe MetaId
x
wakeupListener (CheckConstraint Int
_ ProblemConstraint
c) = do
  --reportSDoc "tc.meta.blocked" 20 $ "waking boxed constraint" <+> prettyTCM c
  (Constraints -> Constraints) -> m ()
forall (m :: * -> *).
MonadConstraint m =>
(Constraints -> Constraints) -> m ()
modifyAwakeConstraints (ProblemConstraint
cProblemConstraint -> Constraints -> Constraints
forall a. a -> [a] -> [a]
:)
  m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

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

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

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

{-# SPECIALIZE freezeMetas :: [MetaId] -> TCM (Set MetaId) #-}
-- | Freeze the given meta-variables (but only if they are open) and
-- return those that were not already frozen.
freezeMetas :: forall m t. (MonadTCState m, ReadTCState m, Traversable t) => t MetaId -> m (Set MetaId)
freezeMetas :: forall (m :: * -> *) (t :: * -> *).
(MonadTCState m, ReadTCState m, Traversable t) =>
t MetaId -> m (Set MetaId)
freezeMetas =
  WriterT (Set MetaId) m () -> m (Set MetaId)
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT (Set MetaId) m () -> m (Set MetaId))
-> (t MetaId -> WriterT (Set MetaId) m ())
-> t MetaId
-> m (Set MetaId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCState LocalMetaStore
-> (LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
-> WriterT (Set MetaId) m ()
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
Lens' TCState a -> (a -> m a) -> m ()
modifyingTCM (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore ((LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
 -> WriterT (Set MetaId) m ())
-> (t MetaId
    -> LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
-> t MetaId
-> WriterT (Set MetaId) m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT LocalMetaStore (WriterT (Set MetaId) m) ()
-> LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (StateT LocalMetaStore (WriterT (Set MetaId) m) ()
 -> LocalMetaStore -> WriterT (Set MetaId) m LocalMetaStore)
-> (t MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> t MetaId
-> LocalMetaStore
-> WriterT (Set MetaId) m LocalMetaStore
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> t MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze
    -- For efficiency, this modifies the 'LocalMetaStore' in 'stOpenMetaStore'
    -- in a local state and writes this store back to TCState in the end
    -- with the accumulated changes.
  where
  freeze :: MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
  freeze :: MetaId -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
freeze MetaId
m = do
    store <- StateT LocalMetaStore (WriterT (Set MetaId) m) LocalMetaStore
forall s (m :: * -> *). MonadState s m => m s
get
    whenJust (MapS.lookup m store) \ MetaVariable
mvar -> do
      Bool
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
== Frozen
Frozen) do
        WriterT (Set MetaId) m ()
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall (m :: * -> *) a. Monad m => m a -> StateT LocalMetaStore m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT (Set MetaId) m ()
 -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> WriterT (Set MetaId) m ()
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a b. (a -> b) -> a -> b
$ Set MetaId -> WriterT (Set MetaId) m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Set MetaId -> WriterT (Set MetaId) m ())
-> Set MetaId -> WriterT (Set MetaId) m ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
m
        LocalMetaStore -> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (LocalMetaStore
 -> StateT LocalMetaStore (WriterT (Set MetaId) m) ())
-> LocalMetaStore
-> StateT LocalMetaStore (WriterT (Set MetaId) m) ()
forall a b. (a -> b) -> a -> b
$ MetaId -> MetaVariable -> LocalMetaStore -> LocalMetaStore
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert MetaId
m (MetaVariable
mvar { mvFrozen = Frozen }) LocalMetaStore
store

-- | Thaw all open meta variables.
unfreezeMetas :: TCM ()
unfreezeMetas :: TCM ()
unfreezeMetas = do
  String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.meta" Int
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"unfreezing ALL metas"
  ASetter' TCState LocalMetaStore
Lens' TCState LocalMetaStore
stOpenMetaStore ASetter' TCState LocalMetaStore
-> (LocalMetaStore -> LocalMetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` (MetaVariable -> MetaVariable) -> LocalMetaStore -> LocalMetaStore
forall a b k. (a -> b) -> Map k a -> Map k b
MapS.map MetaVariable -> MetaVariable
unfreeze_

unfreeze_ :: MetaVariable -> MetaVariable
unfreeze_ :: MetaVariable -> MetaVariable
unfreeze_ = \ MetaVariable
mvar -> MetaVariable
mvar { mvFrozen = Instantiable }

{-# SPECIALIZE isFrozen :: MetaId -> TCM Bool #-}
isFrozen ::
  (HasCallStack, MonadDebug m, ReadTCState m) => MetaId -> m Bool
isFrozen :: forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x = do
  mvar <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
  return $ mvFrozen mvar == Frozen

-- | Temporarily freeze all open metas (from 'stOpenMetaStore')
--   and unfreeze exactly those that were frozen in the first step.
withFrozenMetas ::
    (MonadMetaSolver m, MonadTCState m)
  => m a -> m a
withFrozenMetas :: forall (m :: * -> *) a.
(MonadMetaSolver m, MonadTCState m) =>
m a -> m a
withFrozenMetas m a
act = do
  openMetas <- LocalMetaStore -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys (LocalMetaStore -> [MetaId]) -> m LocalMetaStore -> m [MetaId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState LocalMetaStore -> m LocalMetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (LocalMetaStore -> f LocalMetaStore) -> TCState -> f TCState
Lens' TCState LocalMetaStore
stOpenMetaStore
  frozenMetas <- freezeMetas openMetas
  result <- act
  mapM_ (`updateMetaVar` unfreeze_) frozenMetas
  return 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 = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (((MetaId -> Bool) -> MetaId -> Bool
forall a b. (a -> b) -> a -> b
$ MetaId
x) ((MetaId -> Bool) -> Bool) -> m (MetaId -> Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (MetaId -> Bool)
forall (m :: * -> *). ReadTCState m => m (MetaId -> Bool)
isRemoteMeta) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    String -> Int -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.meta" Int
50 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc
"unfreezing meta" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
x MetaVariable -> MetaVariable
unfreeze_
    Type -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
unfreezeMeta (Type -> m ()) -> m Type -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
x
{-# SPECIALIZE unfreezeMeta :: MetaId -> TCM () #-}

instance UnFreezeMeta Type where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Type -> m ()
unfreezeMeta (El Sort
s Term
t) = Sort -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta Sort
s m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta Term
t

instance UnFreezeMeta Term where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta (MetaV MetaId
x Elims
_)   = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x
  unfreezeMeta (Sort Sort
s)      = Sort -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta Sort
s
  unfreezeMeta (Level Level
l)     = Level -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Level -> m ()
unfreezeMeta Level
l
  unfreezeMeta (DontCare Term
t)  = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta Term
t
  unfreezeMeta (Lam ArgInfo
_ Abs Term
v)     = Abs Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Abs Term -> m ()
unfreezeMeta Abs Term
v
  unfreezeMeta Term
_             = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance UnFreezeMeta Sort where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta (MetaS MetaId
x Elims
_)   = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x
  unfreezeMeta Sort
_             = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance UnFreezeMeta Level where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Level -> m ()
unfreezeMeta (Max Integer
_ [PlusLevel' Term]
ls)      = [PlusLevel' Term] -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[PlusLevel' Term] -> m ()
unfreezeMeta [PlusLevel' Term]
ls

instance UnFreezeMeta PlusLevel where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => PlusLevel' Term -> m ()
unfreezeMeta (Plus Integer
_ Term
a)    = Term -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => Term -> m ()
unfreezeMeta Term
a

instance UnFreezeMeta a => UnFreezeMeta [a] where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => [a] -> m ()
unfreezeMeta = (a -> m ()) -> [a] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ a -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => a -> m ()
unfreezeMeta

instance UnFreezeMeta a => UnFreezeMeta (Abs a) where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Abs a -> m ()
unfreezeMeta = (a -> m ()) -> Abs a -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ a -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
forall (m :: * -> *). MonadMetaSolver m => a -> m ()
unfreezeMeta