{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Lock
  ( isTimeless
  , checkLockedVars
  , checkEarlierThan
  )
where

import Control.Monad            ( filterM, forM, forM_ )

import qualified Data.IntMap as IMap
import qualified Data.IntSet as ISet
import qualified Data.Set as Set

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Constraints () -- instance MonadConstraint TCM
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Free

import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.VarSet as VSet
import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size

checkLockedVars
  :: Term
     -- ^ term to check
  -> Type
     -- ^ its type
  -> Arg Term
     -- ^ the lock
  -> Type
     -- ^ type of the lock
  -> TCM ()
checkLockedVars :: Term -> Type -> Arg Term -> Type -> TCM ()
checkLockedVars Term
t Type
ty Arg Term
lk Type
lk_ty = Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Term -> Type -> Arg Term -> Type -> Constraint
CheckLockedVars Term
t Type
ty Arg Term
lk Type
lk_ty) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  -- Have to instantiate the lock, otherwise we might block on it even
  -- after it's been solved (e.g.: it's an interaction point, see #6528)
  -- Update (Andreas, 2023-10-23, issue #6913): need even full instantiation.
  -- Since @lk@ is typically just a variable, 'instantiateFull' is not expensive here.
  -- In #6913 it was a postulate applied to a meta, thus, 'instantiate' was not enough.
  Arg Term
lk <- Arg Term -> TCMT IO (Arg Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Arg Term
lk
  VerboseKey -> Variable -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Variable -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.lock" Variable
40 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking locked vars.."
  VerboseKey -> Variable -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Variable -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.lock" Variable
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Variable -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Variable -> m Doc -> m Doc
nest Variable
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
     [ VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"t     = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
t
     , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"ty    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
     , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"lk    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
lk
     , VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"lk_ty = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
lk_ty
     ]

  -- Strategy: compute allowed variables, check that @t@ doesn't use more.
  Maybe Variable
mi <- Term -> TCMT IO (Maybe Variable)
getLockVar (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
lk)
  Maybe Variable -> TCM () -> (Variable -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Variable
mi (TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (Term -> Type -> Arg Term -> TypeError
DoesNotMentionTicks Term
t Type
ty Arg Term
lk)) ((Variable -> TCM ()) -> TCM ()) -> (Variable -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Variable
i -> do

  Context
cxt <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  let toCheck :: [(Variable, ContextEntry)]
toCheck = [Variable] -> Context -> [(Variable, ContextEntry)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Variable
0..] (Context -> [(Variable, ContextEntry)])
-> Context -> [(Variable, ContextEntry)]
forall a b. (a -> b) -> a -> b
$ (Variable -> ContextEntry -> ContextEntry)
-> [Variable] -> Context -> Context
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Variable -> ContextEntry -> ContextEntry
forall a. Subst a => Variable -> a -> a
raise [Variable
1..] (Variable -> Context -> Context
forall a. Variable -> [a] -> [a]
take Variable
i Context
cxt)

  let fv :: VarMap
fv = IgnoreSorts -> (Term, Type) -> VarMap
forall a c t.
(IsVarSet a c, Singleton Variable c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore IgnoreSorts
IgnoreInAnnotations (Term
t,Type
ty)
  let
    rigid :: VarSet
rigid = VarMap -> VarSet
rigidVars VarMap
fv
    -- flexible = IMap.keysSet $ flexibleVars fv
    termVars :: VarSet
termVars = VarMap -> VarSet
allVars VarMap
fv -- ISet.union rigid flexible
    earlierVars :: VarSet
earlierVars = [Variable] -> VarSet
ISet.fromList [Variable
i Variable -> Variable -> Variable
forall a. Num a => a -> a -> a
+ Variable
1 .. Context -> Variable
forall a. Sized a => a -> Variable
size Context
cxt Variable -> Variable -> Variable
forall a. Num a => a -> a -> a
- Variable
1]
  if VarSet
termVars VarSet -> VarSet -> Bool
`ISet.isSubsetOf` VarSet
earlierVars then () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return () else do

  [Variable]
checked <- ([Maybe Variable] -> [Variable])
-> TCMT IO [Maybe Variable] -> TCMT IO [Variable]
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe Variable] -> [Variable]
forall a. [Maybe a] -> [a]
catMaybes (TCMT IO [Maybe Variable] -> TCMT IO [Variable])
-> (((Variable, ContextEntry) -> TCMT IO (Maybe Variable))
    -> TCMT IO [Maybe Variable])
-> ((Variable, ContextEntry) -> TCMT IO (Maybe Variable))
-> TCMT IO [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Variable, ContextEntry)]
-> ((Variable, ContextEntry) -> TCMT IO (Maybe Variable))
-> TCMT IO [Maybe Variable]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Variable, ContextEntry)]
toCheck (((Variable, ContextEntry) -> TCMT IO (Maybe Variable))
 -> TCMT IO [Variable])
-> ((Variable, ContextEntry) -> TCMT IO (Maybe Variable))
-> TCMT IO [Variable]
forall a b. (a -> b) -> a -> b
$ \ (Variable
j,ContextEntry
dom) -> do
    TCMT IO Bool
-> TCMT IO (Maybe Variable)
-> TCMT IO (Maybe Variable)
-> TCMT IO (Maybe Variable)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Type -> TCMT IO Bool
isTimeless ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom (ContextEntry -> Type) -> ContextEntry -> Type
forall a b. (a -> b) -> a -> b
$ ContextEntry
dom))
        (Maybe Variable -> TCMT IO (Maybe Variable)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Variable -> TCMT IO (Maybe Variable))
-> Maybe Variable -> TCMT IO (Maybe Variable)
forall a b. (a -> b) -> a -> b
$ Variable -> Maybe Variable
forall a. a -> Maybe a
Just Variable
j)
        (Maybe Variable -> TCMT IO (Maybe Variable)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Variable -> TCMT IO (Maybe Variable))
-> Maybe Variable -> TCMT IO (Maybe Variable)
forall a b. (a -> b) -> a -> b
$ Maybe Variable
forall a. Maybe a
Nothing)

  let allowedVars :: VarSet
allowedVars = VarSet -> VarSet -> VarSet
ISet.union VarSet
earlierVars ([Variable] -> VarSet
ISet.fromList [Variable]
checked)

  if VarSet
termVars VarSet -> VarSet -> Bool
`ISet.isSubsetOf` VarSet
allowedVars then () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return () else do
  let
    illegalVars :: VarSet
illegalVars = VarSet
rigid VarSet -> VarSet -> VarSet
ISet.\\ VarSet
allowedVars
    -- flexVars = flexibleVars fv
    -- blockingMetas = map (`lookupVarMap` flexVars) (ISet.toList $ termVars ISet.\\ allowedVars)
  if VarSet -> Bool
ISet.null VarSet
illegalVars then  -- only flexible vars are infringing
    -- TODO: be more precise about which metas
    -- flexVars = flexibleVars fv
    -- blockingMetas = map (`lookupVarMap` flexVars) (ISet.toList $ termVars ISet.\\ allowedVars)
    Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
  else
    TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> NonEmpty Variable -> Arg Term -> Variable -> TypeError
ReferencesFutureVariables Term
t ([Item (NonEmpty Variable)] -> NonEmpty Variable
forall l. IsList l => [Item l] -> l
List1.fromList (VarSet -> [Variable]
ISet.toList VarSet
illegalVars)) Arg Term
lk Variable
i
    -- List1.fromList is guarded by not (null illegalVars)


-- | Precondition: 'Term' is fully instantiated.
getLockVar :: Term -> TCMT IO (Maybe Int)
getLockVar :: Term -> TCMT IO (Maybe Variable)
getLockVar Term
lk = do
  let
    fv :: VarMap
fv = IgnoreSorts -> Term -> VarMap
forall a c t.
(IsVarSet a c, Singleton Variable c, Free t) =>
IgnoreSorts -> t -> c
freeVarsIgnore IgnoreSorts
IgnoreInAnnotations Term
lk
    flex :: IntMap MetaSet
flex = VarMap -> IntMap MetaSet
flexibleVars VarMap
fv

    isLock :: Variable -> f Bool
isLock Variable
i = (ContextEntry -> Lock) -> f ContextEntry -> f Lock
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> Lock
forall a. LensLock a => a -> Lock
getLock (ArgInfo -> Lock)
-> (ContextEntry -> ArgInfo) -> ContextEntry -> Lock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo) (Variable -> f ContextEntry
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Variable -> m ContextEntry
lookupBV Variable
i) f Lock -> (Lock -> Bool) -> f Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      IsLock{} -> Bool
True
      IsNotLock{} -> Bool
False

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (IntMap MetaSet -> Bool
forall a. IntMap a -> Bool
IMap.null IntMap MetaSet
flex) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let metas :: Set MetaId
metas = [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId) -> [Set MetaId] -> Set MetaId
forall a b. (a -> b) -> a -> b
$ (MetaSet -> Set MetaId) -> [MetaSet] -> [Set MetaId]
forall a b. (a -> b) -> [a] -> [b]
map ((MetaId -> Set MetaId -> Set MetaId)
-> Set MetaId -> MetaSet -> Set MetaId
forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => a -> Set a -> Set a
Set.insert Set MetaId
forall a. Set a
Set.empty) ([MetaSet] -> [Set MetaId]) -> [MetaSet] -> [Set MetaId]
forall a b. (a -> b) -> a -> b
$ IntMap MetaSet -> [MetaSet]
forall a. IntMap a -> [a]
IMap.elems IntMap MetaSet
flex
    Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCM ()) -> Blocker -> TCM ()
forall a b. (a -> b) -> a -> b
$ Set MetaId -> Blocker
unblockOnAnyMeta Set MetaId
metas
      -- Andreas, 2023-10-23, issue #6913:
      -- We should not block on solved metas, so we need @lk@ to be fully instantiated,
      -- otherwise it may mention solved metas which end up here.

  [Variable]
is <- (Variable -> TCMT IO Bool) -> [Variable] -> TCMT IO [Variable]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Variable -> TCMT IO Bool
forall {f :: * -> *}.
(MonadFail f, MonadTCEnv f) =>
Variable -> f Bool
isLock ([Variable] -> TCMT IO [Variable])
-> [Variable] -> TCMT IO [Variable]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Variable]
ISet.toList (VarSet -> [Variable]) -> VarSet -> [Variable]
forall a b. (a -> b) -> a -> b
$ VarMap -> VarSet
rigidVars VarMap
fv

  -- Out of the lock variables that appear in @lk@ the one in the
  -- left-most position in the context is what will determine the
  -- available context for the head.
  let mi :: Maybe Variable
mi | [Variable] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [Variable]
is   = Maybe Variable
forall a. Maybe a
Nothing
         | Bool
otherwise = Variable -> Maybe Variable
forall a. a -> Maybe a
Just (Variable -> Maybe Variable) -> Variable -> Maybe Variable
forall a b. (a -> b) -> a -> b
$ [Variable] -> Variable
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Variable]
is

  Maybe Variable -> TCMT IO (Maybe Variable)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Variable
mi

isTimeless :: Type -> TCM Bool
isTimeless :: Type -> TCMT IO Bool
isTimeless Type
t = do
  Type
t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  [Maybe QName]
timeless <- (BuiltinId -> TCMT IO (Maybe QName))
-> [BuiltinId] -> TCMT IO [Maybe QName]
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 BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' [BuiltinId
builtinInterval, BuiltinId
builtinIsOne]
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
q Elims
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> [Maybe QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
timeless -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Term
_                                -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

notAllowedVarsError :: Term -> [Int] -> TCM b
notAllowedVarsError :: forall b. Term -> [Variable] -> TCM b
notAllowedVarsError Term
lk [Variable]
is = do
        TypeError -> TCM b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM b) -> (Doc -> TypeError) -> Doc -> TCM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM b) -> TCM Doc -> TCM b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
         (TCM Doc
"The following vars are not allowed in a later value applied to"
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
lk TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM ((Variable -> Term) -> [Variable] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Term
var ([Variable] -> [Term]) -> [Variable] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Variable]
is))

checkEarlierThan :: Term -> VSet.VarSet -> TCM ()
checkEarlierThan :: Term -> VarSet -> TCM ()
checkEarlierThan Term
lk VarSet
fvs = do
  Maybe Variable
mv <- Term -> TCMT IO (Maybe Variable)
getLockVar Term
lk
  Maybe Variable -> TCM () -> (Variable -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Variable
mv (() -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Variable -> TCM ()) -> TCM ()) -> (Variable -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Variable
i -> do
    let problems :: [Variable]
problems = (Variable -> Bool) -> [Variable] -> [Variable]
forall a. (a -> Bool) -> [a] -> [a]
filter (Variable -> Variable -> Bool
forall a. Ord a => a -> a -> Bool
<= Variable
i) ([Variable] -> [Variable]) -> [Variable] -> [Variable]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Variable]
VSet.toList VarSet
fvs
    [Variable] -> (Variable -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Variable]
problems ((Variable -> TCM ()) -> TCM ()) -> (Variable -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Variable
j -> do
      Type
ty <- Variable -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Variable -> m Type
typeOfBV Variable
j
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Type -> TCMT IO Bool
isTimeless Type
ty) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Term -> [Variable] -> TCM ()
forall b. Term -> [Variable] -> TCM b
notAllowedVarsError Term
lk [Variable
j]