{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Monad.MetaVars where

import Prelude hiding (null)

import Control.DeepSeq

import Control.Monad                ( (<=<), guard )
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Reader
import Control.Monad.Writer
-- Control.Monad.Fail import is redundant since GHC 8.8.1
import Control.Monad.Fail (MonadFail)

import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Foldable as Fold

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base

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

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

import Agda.Utils.Impossible

-- | Various kinds of metavariables.

data MetaKind =
    Records
    -- ^ Meta variables of record type.
  | SingletonRecords
    -- ^ Meta variables of \"hereditarily singleton\" record type.
  | Levels
    -- ^ Meta variables of level type, if type-in-type is activated.
  deriving (MetaKind -> MetaKind -> Bool
(MetaKind -> MetaKind -> Bool)
-> (MetaKind -> MetaKind -> Bool) -> Eq MetaKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MetaKind -> MetaKind -> Bool
$c/= :: MetaKind -> MetaKind -> Bool
== :: MetaKind -> MetaKind -> Bool
$c== :: MetaKind -> MetaKind -> Bool
Eq, Int -> MetaKind
MetaKind -> Int
MetaKind -> [MetaKind]
MetaKind -> MetaKind
MetaKind -> MetaKind -> [MetaKind]
MetaKind -> MetaKind -> MetaKind -> [MetaKind]
(MetaKind -> MetaKind)
-> (MetaKind -> MetaKind)
-> (Int -> MetaKind)
-> (MetaKind -> Int)
-> (MetaKind -> [MetaKind])
-> (MetaKind -> MetaKind -> [MetaKind])
-> (MetaKind -> MetaKind -> [MetaKind])
-> (MetaKind -> MetaKind -> MetaKind -> [MetaKind])
-> Enum MetaKind
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]
$cenumFromThenTo :: MetaKind -> MetaKind -> MetaKind -> [MetaKind]
enumFromTo :: MetaKind -> MetaKind -> [MetaKind]
$cenumFromTo :: MetaKind -> MetaKind -> [MetaKind]
enumFromThen :: MetaKind -> MetaKind -> [MetaKind]
$cenumFromThen :: MetaKind -> MetaKind -> [MetaKind]
enumFrom :: MetaKind -> [MetaKind]
$cenumFrom :: MetaKind -> [MetaKind]
fromEnum :: MetaKind -> Int
$cfromEnum :: MetaKind -> Int
toEnum :: Int -> MetaKind
$ctoEnum :: Int -> MetaKind
pred :: MetaKind -> MetaKind
$cpred :: MetaKind -> MetaKind
succ :: MetaKind -> MetaKind
$csucc :: MetaKind -> MetaKind
Enum, MetaKind
MetaKind -> MetaKind -> Bounded MetaKind
forall a. a -> a -> Bounded a
maxBound :: MetaKind
$cmaxBound :: MetaKind
minBound :: MetaKind
$cminBound :: MetaKind
Bounded, Int -> MetaKind -> ShowS
[MetaKind] -> ShowS
MetaKind -> [Char]
(Int -> MetaKind -> ShowS)
-> (MetaKind -> [Char]) -> ([MetaKind] -> ShowS) -> Show MetaKind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [MetaKind] -> ShowS
$cshowList :: [MetaKind] -> ShowS
show :: MetaKind -> [Char]
$cshow :: MetaKind -> [Char]
showsPrec :: Int -> MetaKind -> ShowS
$cshowsPrec :: Int -> MetaKind -> ShowS
Show)

-- | All possible metavariable kinds.

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

data KeepMetas = KeepMetas | RollBackMetas

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

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

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

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

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

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

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

-- | Switch off assignment of metas.
dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
dontAssignMetas :: forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas m a
cont = do
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta" Int
45 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"don't assign metas"
  (TCEnv -> TCEnv) -> m a -> m a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
env -> TCEnv
env { envAssignMetas :: Bool
envAssignMetas = Bool
False }) m a
cont

-- | Get the meta store.
getMetaStore :: (ReadTCState m) => m MetaStore
getMetaStore :: forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore = Lens' MetaStore TCState -> m MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' MetaStore TCState
stMetaStore

modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore MetaStore -> MetaStore
f = Lens' MetaStore TCState
stMetaStore Lens' MetaStore TCState -> (MetaStore -> MetaStore) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` MetaStore -> MetaStore
f

-- | Run a computation and record which new metas it created.
metasCreatedBy :: ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy :: forall (m :: * -> *) a. ReadTCState m => m a -> m (a, MetaStore)
metasCreatedBy m a
m = do
  -- Compute largestMeta strictly to avoid leaking memory.
  !Maybe Int
largestMeta <- Maybe Int -> Maybe Int
forall a. NFData a => a -> a
force (Maybe Int -> Maybe Int)
-> (MetaStore -> Maybe Int) -> MetaStore -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, MetaVariable) -> Int)
-> Maybe (Int, MetaVariable) -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, MetaVariable) -> Int
forall a b. (a, b) -> a
fst (Maybe (Int, MetaVariable) -> Maybe Int)
-> (MetaStore -> Maybe (Int, MetaVariable))
-> MetaStore
-> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaStore -> Maybe (Int, MetaVariable)
forall a. IntMap a -> Maybe (Int, a)
IntMap.lookupMax (MetaStore -> Maybe Int) -> m MetaStore -> m (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                    Lens' MetaStore TCState -> m MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
  a
a            <- m a
m
  MetaStore
ms           <- Lens' MetaStore TCState -> m MetaStore
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' MetaStore TCState
stMetaStore
  let createdMetas :: MetaStore
createdMetas = case Maybe Int
largestMeta of
        Maybe Int
Nothing          -> MetaStore
ms
        Just Int
largestMeta -> (MetaStore, MetaStore) -> MetaStore
forall a b. (a, b) -> b
snd ((MetaStore, MetaStore) -> MetaStore)
-> (MetaStore, MetaStore) -> MetaStore
forall a b. (a -> b) -> a -> b
$ Int -> MetaStore -> (MetaStore, MetaStore)
forall a. Int -> IntMap a -> (IntMap a, IntMap a)
IntMap.split Int
largestMeta MetaStore
ms
  (a, MetaStore) -> m (a, MetaStore)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
a, MetaStore
createdMetas)

-- | Lookup a meta variable.
lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupMeta' :: forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
m = Int -> MetaStore -> Maybe MetaVariable
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (MetaId -> Int
metaId MetaId
m) (MetaStore -> Maybe MetaVariable)
-> m MetaStore -> m (Maybe MetaVariable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m MetaStore
forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore

lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
lookupMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m = m MetaVariable -> m (Maybe MetaVariable) -> m MetaVariable
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaVariable
failure (m (Maybe MetaVariable) -> m MetaVariable)
-> m (Maybe MetaVariable) -> m MetaVariable
forall a b. (a -> b) -> a -> b
$ MetaId -> m (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupMeta' MetaId
m
  where failure :: m MetaVariable
failure = [Char] -> m MetaVariable
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> m MetaVariable) -> [Char] -> m MetaVariable
forall a b. (a -> b) -> a -> b
$ [Char]
"no such meta variable " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m

-- | Type of a term or sort meta.
metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
metaType :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type)
-> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Type) -> m MetaVariable -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x

-- | Update the information associated with a meta variable.
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
m MetaVariable -> MetaVariable
f = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (MetaVariable -> MetaVariable) -> Int -> MetaStore -> MetaStore
forall a. (a -> a) -> Int -> IntMap a -> IntMap a
IntMap.adjust MetaVariable -> MetaVariable
f (Int -> MetaStore -> MetaStore) -> Int -> MetaStore -> MetaStore
forall a b. (a -> b) -> a -> b
$ MetaId -> Int
metaId MetaId
m

-- | Insert a new meta variable with associated information into the meta store.
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
m MetaVariable
mv = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> MetaVariable -> MetaStore -> MetaStore
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (MetaId -> Int
metaId MetaId
m) MetaVariable
mv

getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority
getMetaPriority :: forall (m :: * -> *).
(MonadFail 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta

isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isSortMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isSortMeta MetaId
m = MetaVariable -> Bool
isSortMeta_ (MetaVariable -> Bool) -> m MetaVariable -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m

isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ :: MetaVariable -> Bool
isSortMeta_ MetaVariable
mv = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
    HasType{} -> Bool
False
    IsSort{}  -> Bool
True

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

-- | Compute the context variables that a meta should be applied to, accounting
--   for pruning.
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs :: forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVar{ mvPermutation :: MetaVariable -> Permutation
mvPermutation = Permutation
p } = do
  Args
args <- m Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
  Args -> m Args
forall (m :: * -> *) a. Monad m => a -> m a
return (Args -> m Args) -> Args -> m Args
forall a b. (a -> b) -> a -> b
$ Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (Args -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
args) Permutation
p) Args
args

-- | Given a meta, return the type applied to the current context.
getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m, HasBuiltins m)
                     => MetaId -> m Type
getMetaTypeInContext :: forall (m :: * -> *).
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m,
 HasBuiltins m) =>
MetaId -> m Type
getMetaTypeInContext MetaId
m = do
  mv :: MetaVariable
mv@MetaVar{ mvJudgement :: MetaVariable -> Judgement MetaId
mvJudgement = Judgement MetaId
j } <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  case Judgement MetaId
j of
    HasType{ jMetaType :: forall a. Judgement a -> Type
jMetaType = Type
t } -> Type -> Args -> m Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
t (Args -> m Type) -> m Args -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaVariable -> m Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
    IsSort{}                 -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__

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

-- | Check whether all metas are instantiated.
--   Precondition: argument is a meta (in some form) or a list of metas.
class IsInstantiatedMeta a where
  isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool

instance IsInstantiatedMeta MetaId where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
m = Maybe Term -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Term -> Bool) -> m (Maybe Term) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Maybe Term)
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
m

instance IsInstantiatedMeta Term where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Term -> m Bool
isInstantiatedMeta = Term -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Term -> m Bool
loop where
   loop :: Term -> m Bool
loop Term
v =
    case Term
v of
      MetaV MetaId
x [Elim]
_  -> MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta MetaId
x
      DontCare Term
v -> Term -> m Bool
loop Term
v
      Level Level
l    -> Level -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Level
l
      Lam ArgInfo
_ Abs Term
b    -> Abs Term -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Abs Term
b
      Con ConHead
_ ConInfo
_ [Elim]
es | Just Args
vs <- [Elim] -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
es -> Args -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Args
vs
      Term
_          -> m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

instance IsInstantiatedMeta Level where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Level -> m Bool
isInstantiatedMeta (Max Integer
n [PlusLevel' Term]
ls) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = [PlusLevel' Term] -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta [PlusLevel' Term]
ls
  isInstantiatedMeta Level
_ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

instance IsInstantiatedMeta PlusLevel where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
PlusLevel' Term -> m Bool
isInstantiatedMeta (Plus Integer
n Term
l) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Term -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta Term
l
  isInstantiatedMeta PlusLevel' Term
_ = m Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

instance IsInstantiatedMeta a => IsInstantiatedMeta [a] where
  isInstantiatedMeta :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => [a] -> m Bool
isInstantiatedMeta = [m Bool] -> m Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM ([m Bool] -> m Bool) -> ([a] -> [m Bool]) -> [a] -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m Bool) -> [a] -> [m Bool]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta

instance IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Maybe a -> m Bool
isInstantiatedMeta = [a] -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta ([a] -> m Bool) -> (Maybe a -> [a]) -> Maybe a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> [a]
forall a. Maybe a -> [a]
maybeToList

instance IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Arg a -> m Bool
isInstantiatedMeta = a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta (a -> m Bool) -> (Arg a -> a) -> Arg a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> a
forall e. Arg e -> e
unArg

-- | Does not worry about raising.
instance IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) where
  isInstantiatedMeta :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
Abs a -> m Bool
isInstantiatedMeta = a -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
isInstantiatedMeta (a -> m Bool) -> (Abs a -> a) -> Abs a -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Abs a -> a
forall a. Abs a -> a
unAbs

isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
isInstantiatedMeta' :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
m = do
  MetaVariable
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  Maybe Term -> m (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> m (Maybe Term)) -> Maybe Term -> m (Maybe Term)
forall a b. (a -> b) -> a -> b
$ case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
    InstV [Arg [Char]]
tel Term
v -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ (Arg [Char] -> Term -> Term) -> Term -> [Arg [Char]] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg [Char] -> Term -> Term
mkLam Term
v [Arg [Char]]
tel
    MetaInstantiation
_           -> 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         -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
u, Term
v)
      ValueCmpOnFace Comparison
_ Term
p Type
_ Term
u Term
v -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term, Term) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
p, Term
u, Term
v)
      ElimCmp [Polarity]
_ [IsForced]
_ Type
_ Term
_ [Elim]
es [Elim]
es'   -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> ([Elim], [Elim]) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton ([Elim]
es, [Elim]
es')
      LevelCmp Comparison
_ Level
l Level
l'          -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Level -> Term
Level Level
l, Level -> Term
Level Level
l')
      UnquoteTactic Term
t Term
h Type
g      -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term, Type) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
t, Term
h, Type
g)
      SortCmp Comparison
_ Sort
s1 Sort
s2          -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId) -> (Term, Term) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)
      UnBlock MetaId
x                -> MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => a -> Set a -> Set a
Set.insert MetaId
x (Set MetaId -> Set MetaId)
-> ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId)
-> TCMT IO [Set MetaId] -> TCM (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Listener -> TCM (Set MetaId))
-> [Listener] -> TCMT IO [Set MetaId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Listener -> TCM (Set MetaId)
listenerMetas ([Listener] -> TCMT IO [Set MetaId])
-> TCMT IO [Listener] -> TCMT IO [Set MetaId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> TCMT IO [Listener]
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Listener]
getMetaListeners MetaId
x)
      FindInstance 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
x) (Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. 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 (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 t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton
      IsEmpty{}                -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckFunDef{}            -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckSizeLtSat{}         -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      HasBiggerSort{}          -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      HasPTSRule{}             -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckMetaInst MetaId
x          -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
      CheckLockedVars Term
a Type
b Arg Term
c Type
d  -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCM (Set MetaId)) -> Set MetaId -> TCM (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (MetaId -> Set MetaId)
-> (Term, Type, Arg Term, Type) -> Set MetaId
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton (Term
a, Type
b, Arg Term
c, Type
d)
      UsableAtModality{}       -> Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Monoid a => a
mempty
  where
    -- For blocked constant twin variables
    listenerMetas :: Listener -> TCM (Set MetaId)
listenerMetas EtaExpand{}           = Set MetaId -> TCM (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Set a
Set.empty
    listenerMetas (CheckConstraint 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)

-- | 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
  Range
r        <- m Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange
  Closure Range
cl       <- Range -> m (Closure Range)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Range
r
  DoGeneralize
gen      <- Lens' DoGeneralize TCEnv -> m DoGeneralize
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' DoGeneralize TCEnv
eGeneralizeMetas
  Modality
modality <- Lens' Modality TCEnv -> m Modality
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Modality TCEnv
eModality
  MetaInfo -> m MetaInfo
forall (m :: * -> *) a. Monad m => a -> m a
return MetaInfo
    { miClosRange :: Closure Range
miClosRange       = Closure Range
cl
    , miModality :: Modality
miModality        = Modality
modality
    , miMetaOccursCheck :: RunMetaOccursCheck
miMetaOccursCheck = RunMetaOccursCheck
b
    , miNameSuggestion :: [Char]
miNameSuggestion  = [Char]
""
    , miGeneralizable :: Arg DoGeneralize
miGeneralizable   = DoGeneralize -> Arg DoGeneralize
forall a. a -> Arg a
defaultArg DoGeneralize
gen
                          -- The ArgInfo is set to the right value in
                          -- the newArgsMetaCtx' function.
    }

setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
setValueMetaName :: forall (m :: * -> *). MonadMetaSolver m => Term -> [Char] -> m ()
setValueMetaName Term
v [Char]
s = do
  case Term
v of
    MetaV MetaId
mi [Elim]
_ -> MetaId -> [Char] -> m ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s
    Term
u          -> do
      [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.name" Int
70 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
        [Char]
"cannot set meta name; newMeta returns " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Show a => a -> [Char]
show Term
u
      () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
getMetaNameSuggestion :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m [Char]
getMetaNameSuggestion MetaId
mi = MetaInfo -> [Char]
miNameSuggestion (MetaInfo -> [Char])
-> (MetaVariable -> MetaInfo) -> MetaVariable -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> [Char]) -> m MetaVariable -> m [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi

setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaNameSuggestion :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> [Char] -> m ()
setMetaNameSuggestion MetaId
mi [Char]
s = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Char] -> Bool
forall a. Null a => a -> Bool
null [Char]
s Bool -> Bool -> Bool
|| [Char] -> Bool
forall a. Underscore a => a -> Bool
isUnderscore [Char]
s) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.name" Int
20 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"setting name of meta " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
mi [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" to " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s
  MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
mi ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mvar ->
    MetaVariable
mvar { mvInfo :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar) { miNameSuggestion :: [Char]
miNameSuggestion = [Char]
s }}

-- | Change the ArgInfo that will be used when generalizing over this meta.
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 :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)
        { miGeneralizable :: Arg DoGeneralize
miGeneralizable = ArgInfo -> Arg DoGeneralize -> Arg DoGeneralize
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
i (MetaInfo -> Arg DoGeneralize
miGeneralizable (MetaVariable -> MetaInfo
mvInfo MetaVariable
mv)) } }

updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange :: 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 :: MetaInfo
mvInfo = (MetaVariable -> MetaInfo
mvInfo MetaVariable
mvar) { miMetaOccursCheck :: RunMetaOccursCheck
miMetaOccursCheck = RunMetaOccursCheck
b } }

-- * Query and manipulate interaction points.

class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
  freshInteractionId :: m InteractionId
  default freshInteractionId
    :: (MonadTrans t, MonadInteractionPoints n, t n ~ m)
    => m InteractionId
  freshInteractionId = n InteractionId -> t n InteractionId
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 ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (n () -> m ())
-> ((InteractionPoints -> InteractionPoints) -> n ())
-> (InteractionPoints -> InteractionPoints)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoints -> InteractionPoints) -> n ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints

instance MonadInteractionPoints m => MonadInteractionPoints (IdentityT m)
instance MonadInteractionPoints m => MonadInteractionPoints (ReaderT r m)
instance MonadInteractionPoints m => MonadInteractionPoints (StateT s m)

instance MonadInteractionPoints TCM where
  freshInteractionId :: TCM InteractionId
freshInteractionId = TCM InteractionId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM ()
modifyInteractionPoints InteractionPoints -> InteractionPoints
f = Lens' InteractionPoints TCState
stInteractionPoints Lens' InteractionPoints TCState
-> (InteractionPoints -> InteractionPoints) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` InteractionPoints -> InteractionPoints
f

-- | Register an interaction point during scope checking.
--   If there is no interaction id yet, create one.
registerInteractionPoint
  :: forall m. MonadInteractionPoints m
  => Bool -> Range -> Maybe Nat -> m InteractionId
registerInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Int -> m InteractionId
registerInteractionPoint Bool
preciseRange Range
r Maybe Int
maybeId = do
  InteractionPoints
m <- Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
  -- If we're given an interaction id we shouldn't look up by range.
  -- This is important when doing 'refine', since all interaction points
  -- created by the refine gets the same range.
  if Bool -> Bool
not Bool
preciseRange Bool -> Bool -> Bool
|| Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
maybeId then InteractionPoints -> m InteractionId
continue InteractionPoints
m else do
    -- If the range does not come from a file, it is not
    -- precise, so ignore it.
    Maybe AbsolutePath
-> m InteractionId
-> (AbsolutePath -> m InteractionId)
-> m InteractionId
forall a b. Maybe a -> b -> (a -> b) -> b
Strict.caseMaybe (Range -> Maybe AbsolutePath
rangeFile Range
r) (InteractionPoints -> m InteractionId
continue InteractionPoints
m) ((AbsolutePath -> m InteractionId) -> m InteractionId)
-> (AbsolutePath -> m InteractionId) -> m InteractionId
forall a b. (a -> b) -> a -> b
$ \ AbsolutePath
_ -> 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 (m :: * -> *) a. Monad m => a -> m a
return
 where
 continue :: InteractionPoints -> m InteractionId
 continue :: InteractionPoints -> m InteractionId
continue InteractionPoints
m = do
  -- We did not find an interaction id with the same Range, so let's create one!
  InteractionId
ii <- case Maybe Int
maybeId of
    Just Int
i  -> InteractionId -> m InteractionId
forall (m :: * -> *) a. Monad m => a -> m a
return (InteractionId -> m InteractionId)
-> InteractionId -> m InteractionId
forall a b. (a -> b) -> a -> b
$ Int -> InteractionId
InteractionId Int
i
    Maybe Int
Nothing -> m InteractionId
forall (m :: * -> *). MonadInteractionPoints m => m InteractionId
freshInteractionId
  let ip :: InteractionPoint
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 }
  case (InteractionId
 -> InteractionPoint -> InteractionPoint -> InteractionPoint)
-> InteractionId
-> InteractionPoint
-> InteractionPoints
-> (Maybe InteractionPoint, InteractionPoints)
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
old) InteractionId
ii InteractionPoint
ip InteractionPoints
m of
    -- If the interaction point is already present, we keep the old ip.
    -- However, it needs to be at the same range as the new one.
    (Just InteractionPoint
ip0, InteractionPoints
_)
       | InteractionPoint -> Range
ipRange InteractionPoint
ip Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= InteractionPoint -> Range
ipRange InteractionPoint
ip0 -> m InteractionId
forall a. HasCallStack => a
__IMPOSSIBLE__
       | Bool
otherwise                 -> InteractionId -> m InteractionId
forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
ii
    (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 (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 (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Range -> Bool
forall a. Null a => a -> Bool
null Range
r
  [InteractionId] -> Maybe InteractionId
forall a. [a] -> Maybe a
listToMaybe ([InteractionId] -> Maybe InteractionId)
-> [InteractionId] -> Maybe InteractionId
forall a b. (a -> b) -> a -> b
$ ((InteractionId, InteractionPoint) -> Maybe InteractionId)
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange ([(InteractionId, InteractionPoint)] -> [InteractionId])
-> [(InteractionId, InteractionPoint)] -> [InteractionId]
forall a b. (a -> b) -> a -> b
$ InteractionPoints -> [(InteractionId, InteractionPoint)]
forall k v. BiMap k v -> [(k, v)]
BiMap.toList InteractionPoints
m
  where
    sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
    sameRange :: (InteractionId, InteractionPoint) -> Maybe InteractionId
sameRange (InteractionId
ii, InteractionPoint Range
r' Maybe MetaId
_ Bool
False IPClause
_) | 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

-- | Hook up meta variable to interaction point.
connectInteractionPoint
  :: MonadInteractionPoints m
  => InteractionId -> MetaId -> m ()
connectInteractionPoint :: forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> MetaId -> m ()
connectInteractionPoint InteractionId
ii MetaId
mi = do
  IPClause
ipCl <- (TCEnv -> IPClause) -> m IPClause
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> IPClause
envClause
  InteractionPoints
m <- Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
  let ip :: InteractionPoint
ip = InteractionPoint { 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 }
  -- The interaction point needs to be present already, we just set the meta.
  case (InteractionId
 -> InteractionPoint -> InteractionPoint -> InteractionPoint)
-> InteractionId
-> InteractionPoint
-> InteractionPoints
-> (Maybe InteractionPoint, InteractionPoints)
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(k -> v -> v -> v) -> k -> v -> BiMap k v -> (Maybe v, BiMap k v)
BiMap.insertLookupWithKey (\ InteractionId
key InteractionPoint
new InteractionPoint
old -> InteractionPoint
new { ipRange :: Range
ipRange = InteractionPoint -> Range
ipRange InteractionPoint
old }) InteractionId
ii InteractionPoint
ip InteractionPoints
m of
    (Maybe InteractionPoint
Nothing, InteractionPoints
_) -> 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 :: Bool
ipSolved = Bool
True }) InteractionId
ii

-- | Get a list of interaction ids.
{-# SPECIALIZE getInteractionPoints :: TCM [InteractionId] #-}
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionPoints :: forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints = InteractionPoints -> [InteractionId]
forall k v. BiMap k v -> [k]
BiMap.keys (InteractionPoints -> [InteractionId])
-> m InteractionPoints -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints

-- | Get all metas that correspond to unsolved interaction ids.
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas =
  (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' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints

getUniqueMetasRanges :: (MonadFail m, ReadTCState m) => [MetaId] -> m [Range]
getUniqueMetasRanges :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
[MetaId] -> m [Range]
getUniqueMetasRanges = ([Range] -> [Range]) -> m [Range] -> m [Range]
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)
mapM MetaId -> m Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange

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

getUnsolvedInteractionMetas :: (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas :: forall (m :: * -> *). (MonadFail m, ReadTCState m) => m [Range]
getUnsolvedInteractionMetas = [MetaId] -> m [Range]
forall (m :: * -> *).
(MonadFail 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' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
  where f :: (t, InteractionPoint) -> Maybe (t, MetaId)
f (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' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints

-- | Get the information associated to an interaction point.
{-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
lookupInteractionPoint
  :: (MonadFail m, ReadTCState m, MonadError TCErr m)
  => InteractionId -> m InteractionPoint
lookupInteractionPoint :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii =
  m InteractionPoint
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m InteractionPoint
err (m (Maybe InteractionPoint) -> m InteractionPoint)
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$ InteractionId -> InteractionPoints -> Maybe InteractionPoint
forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup InteractionId
ii (InteractionPoints -> Maybe InteractionPoint)
-> m InteractionPoints -> m (Maybe InteractionPoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints
  where
    err :: m InteractionPoint
err  = [Char] -> m InteractionPoint
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> m InteractionPoint) -> [Char] -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$ [Char]
"no such interaction point: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Show a => a -> [Char]
show InteractionId
ii

-- | Get 'MetaId' for an interaction point.
--   Precondition: interaction point is connected.
lookupInteractionId
  :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
  => InteractionId -> m MetaId
lookupInteractionId :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii = m MetaId -> m (Maybe MetaId) -> m MetaId
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM m MetaId
err2 (m (Maybe MetaId) -> m MetaId) -> m (Maybe MetaId) -> m MetaId
forall a b. (a -> b) -> a -> b
$ InteractionPoint -> Maybe MetaId
ipMeta (InteractionPoint -> Maybe MetaId)
-> m InteractionPoint -> m (Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  where
    err2 :: m MetaId
err2 = TypeError -> m MetaId
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m MetaId) -> TypeError -> m MetaId
forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$ [Char]
"No type nor action available for hole " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow InteractionId
ii [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
". Possible cause: the hole has not been reached during type checking (do you see yellow?)"

-- | Check whether an interaction id is already associated with a meta variable.
lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
lookupInteractionMeta :: forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii = InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ InteractionId
ii (InteractionPoints -> Maybe MetaId)
-> m InteractionPoints -> m (Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' InteractionPoints TCState -> m InteractionPoints
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' InteractionPoints TCState
stInteractionPoints

lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
lookupInteractionMeta_ 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 (m :: * -> *) a.
MonadMetaSolver m =>
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> m MetaId
newMeta' MetaInstantiation
Open

-- | Generate a new meta variable with some instantiation given.
--   For instance, the instantiation could be a 'PostponedTypeCheckingProblem'.
newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation ->
               Judgement a -> TCM MetaId
newMetaTCM' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMetaTCM' MetaInstantiation
inst Frozen
frozen MetaInfo
mi MetaPriority
p Permutation
perm Judgement a
j = do
  MetaId
x <- TCM MetaId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  let j' :: Judgement MetaId
j' = Judgement a
j { jMetaId :: MetaId
jMetaId = MetaId
x }  -- fill the identifier part of the judgement
      mv :: MetaVariable
mv = MetaVar{ mvInfo :: MetaInfo
mvInfo             = MetaInfo
mi
                  , mvPriority :: MetaPriority
mvPriority         = MetaPriority
p
                  , mvPermutation :: Permutation
mvPermutation      = Permutation
perm
                  , mvJudgement :: Judgement MetaId
mvJudgement        = Judgement MetaId
j'
                  , mvInstantiation :: MetaInstantiation
mvInstantiation    = MetaInstantiation
inst
                  , mvListeners :: Set Listener
mvListeners        = Set Listener
forall a. Set a
Set.empty
                  , mvFrozen :: Frozen
mvFrozen           = Frozen
frozen
                  , mvTwin :: Maybe MetaId
mvTwin             = Maybe MetaId
forall a. Maybe a
Nothing
                  }
  -- printing not available (import cycle)
  -- reportSDoc "tc.meta.new" 50 $ "new meta" <+> prettyTCM j'
  MetaId -> MetaVariable -> TCM ()
insertMetaVar MetaId
x MetaVariable
mv
  MetaId -> TCM MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x

-- | Get the 'Range' for an interaction point.
{-# SPECIALIZE getInteractionRange :: InteractionId -> TCM Range #-}
getInteractionRange
  :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m)
  => InteractionId -> m Range
getInteractionRange :: forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange = InteractionPoint -> Range
ipRange (InteractionPoint -> Range)
-> (InteractionId -> m InteractionPoint)
-> InteractionId
-> m Range
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint

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

getInteractionScope
  :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)
  => InteractionId -> m ScopeInfo
getInteractionScope :: forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope = MetaVariable -> ScopeInfo
getMetaScope (MetaVariable -> ScopeInfo)
-> (MetaId -> m MetaVariable) -> MetaId -> m ScopeInfo
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta (MetaId -> m ScopeInfo)
-> (InteractionId -> m MetaId) -> InteractionId -> m ScopeInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< InteractionId -> m MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId

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

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

withInteractionId
  :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m)
  => InteractionId -> m a -> m a
withInteractionId :: forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i m a
ret = do
  MetaId
m <- InteractionId -> m MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
  MetaId -> m a -> m a
forall (m :: * -> *) a.
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaId -> m a -> m a
withMetaId MetaId
m m a
ret

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

getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
getMetaVariables :: forall (m :: * -> *).
ReadTCState m =>
(MetaVariable -> Bool) -> m [MetaId]
getMetaVariables MetaVariable -> Bool
p = do
  MetaStore
store <- m MetaStore
forall (m :: * -> *). ReadTCState m => m MetaStore
getMetaStore
  [MetaId] -> m [MetaId]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Int -> MetaId
MetaId Int
i | (Int
i, MetaVariable
mv) <- MetaStore -> [(Int, MetaVariable)]
forall a. IntMap a -> [(Int, a)]
IntMap.assocs MetaStore
store, MetaVariable -> Bool
p MetaVariable
mv ]

getOpenMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas = (MetaVariable -> Bool) -> m [MetaId]
forall (m :: * -> *).
ReadTCState m =>
(MetaVariable -> Bool) -> m [MetaId]
getMetaVariables (MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool)
-> (MetaVariable -> MetaInstantiation) -> MetaVariable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInstantiation
mvInstantiation)

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

-- | @listenToMeta l m@: register @l@ as a listener to @m@. This is done
--   when the type of l is blocked by @m@.
listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
listenToMeta :: forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta Listener
l MetaId
m =
  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 Listener
mvListeners = Listener -> Set Listener -> Set Listener
forall a. Ord a => a -> Set a -> Set a
Set.insert Listener
l (Set Listener -> Set Listener) -> Set Listener -> Set Listener
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Set Listener
mvListeners MetaVariable
mv }

-- | 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 Listener
mvListeners = Listener -> Set Listener -> Set Listener
forall a. Ord a => a -> Set a -> Set a
Set.delete Listener
l (Set Listener -> Set Listener) -> Set Listener -> Set Listener
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Set Listener
mvListeners MetaVariable
mv }

-- | Get the listeners to a meta.
getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
getMetaListeners :: forall (m :: * -> *).
(MonadFail 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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m

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

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

-- | Freeze the given meta-variables and return those that were not
--   already frozen.
freezeMetas :: MetaStore -> TCM IntSet
freezeMetas :: MetaStore -> TCM IntSet
freezeMetas MetaStore
ms =
  WriterT IntSet (TCMT IO) () -> TCM IntSet
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT (WriterT IntSet (TCMT IO) () -> TCM IntSet)
-> WriterT IntSet (TCMT IO) () -> TCM IntSet
forall a b. (a -> b) -> a -> b
$
  Lens' MetaStore TCState
-> (MetaStore -> WriterT IntSet (TCMT IO) MetaStore)
-> WriterT IntSet (TCMT IO) ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> m a) -> m ()
modifyTCLensM Lens' MetaStore TCState
stMetaStore ((MetaStore -> WriterT IntSet (TCMT IO) MetaStore)
 -> WriterT IntSet (TCMT IO) ())
-> (MetaStore -> WriterT IntSet (TCMT IO) MetaStore)
-> WriterT IntSet (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
  StateT MetaStore (WriterT IntSet (TCMT IO)) ()
-> MetaStore -> WriterT IntSet (TCMT IO) MetaStore
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT ((Int -> StateT MetaStore (WriterT IntSet (TCMT IO)) ())
-> [Int] -> StateT MetaStore (WriterT IntSet (TCMT IO)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Int -> StateT MetaStore (WriterT IntSet (TCMT IO)) ()
forall (m :: * -> *).
Monad m =>
Int -> StateT MetaStore (WriterT IntSet m) ()
freeze ([Int] -> StateT MetaStore (WriterT IntSet (TCMT IO)) ())
-> [Int] -> StateT MetaStore (WriterT IntSet (TCMT IO)) ()
forall a b. (a -> b) -> a -> b
$ MetaStore -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys MetaStore
ms)
  where
  freeze :: Monad m => Int -> StateT MetaStore (WriterT IntSet m) ()
  freeze :: forall (m :: * -> *).
Monad m =>
Int -> StateT MetaStore (WriterT IntSet m) ()
freeze Int
m = do
    MetaStore
store <- StateT MetaStore (WriterT IntSet m) MetaStore
forall s (m :: * -> *). MonadState s m => m s
get
    case Int -> MetaStore -> Maybe MetaVariable
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
m MetaStore
store of
      Just MetaVariable
mvar
        | MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
/= Frozen
Frozen -> do
          WriterT IntSet m () -> StateT MetaStore (WriterT IntSet m) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT IntSet m () -> StateT MetaStore (WriterT IntSet m) ())
-> WriterT IntSet m () -> StateT MetaStore (WriterT IntSet m) ()
forall a b. (a -> b) -> a -> b
$ IntSet -> WriterT IntSet m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Int -> IntSet
IntSet.singleton Int
m)
          MetaStore -> StateT MetaStore (WriterT IntSet m) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (MetaStore -> StateT MetaStore (WriterT IntSet m) ())
-> MetaStore -> StateT MetaStore (WriterT IntSet m) ()
forall a b. (a -> b) -> a -> b
$ Int -> MetaVariable -> MetaStore -> MetaStore
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
m (MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Frozen }) MetaStore
store
        | Bool
otherwise -> () -> StateT MetaStore (WriterT IntSet m) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Maybe MetaVariable
Nothing -> StateT MetaStore (WriterT IntSet m) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Thaw all meta variables.
unfreezeMetas :: TCM ()
unfreezeMetas :: TCM ()
unfreezeMetas = (MetaStore -> MetaStore) -> TCM ()
modifyMetaStore ((MetaStore -> MetaStore) -> TCM ())
-> (MetaStore -> MetaStore) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (MetaVariable -> MetaVariable) -> MetaStore -> MetaStore
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map MetaVariable -> MetaVariable
unfreeze
  where
  unfreeze :: MetaVariable -> MetaVariable
  unfreeze :: MetaVariable -> MetaVariable
unfreeze MetaVariable
mvar = MetaVariable
mvar { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }

isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isFrozen :: forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x = do
  MetaVariable
mvar <- MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
x
  Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Frozen
mvFrozen MetaVariable
mvar Frozen -> Frozen -> Bool
forall a. Eq a => a -> a -> Bool
== Frozen
Frozen

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

instance UnFreezeMeta MetaId where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
unfreezeMeta MetaId
x = do
    MetaId -> (MetaVariable -> MetaVariable) -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> (MetaVariable -> MetaVariable) -> m ()
updateMetaVar MetaId
x ((MetaVariable -> MetaVariable) -> m ())
-> (MetaVariable -> MetaVariable) -> m ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv -> MetaVariable
mv { mvFrozen :: Frozen
mvFrozen = Frozen
Instantiable }
    Type -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta (Type -> m ()) -> m Type -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
x

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

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

instance UnFreezeMeta Sort where
  unfreezeMeta :: forall (m :: * -> *). MonadMetaSolver m => Sort -> m ()
unfreezeMeta (MetaS MetaId
x [Elim]
_)   = MetaId -> m ()
forall a (m :: * -> *).
(UnFreezeMeta a, MonadMetaSolver m) =>
a -> m ()
unfreezeMeta MetaId
x
  unfreezeMeta Sort
_             = () -> m ()
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 ()
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 ()
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 ()
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 ()
unfreezeMeta