{-# 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.
  lk <- Arg Term -> TCMT IO (Arg Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Arg Term
lk
  reportSDoc "tc.term.lock" 40 $ "Checking locked vars.."
  reportSDoc "tc.term.lock" 50 $ nest 2 $ vcat
     [ text "t     = " <+> pretty t
     , text "ty    = " <+> pretty ty
     , text "lk    = " <+> pretty lk
     , text "lk_ty = " <+> pretty lk_ty
     ]

  -- Strategy: compute allowed variables, check that @t@ doesn't use more.
  mi <- getLockVar (unArg lk)
  caseMaybe mi (typeError (DoesNotMentionTicks t ty lk)) $ \ Variable
i -> do

  cxt <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  let 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 = 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 = VarMap -> VarSet
rigidVars VarMap
fv
    -- flexible = IMap.keysSet $ flexibleVars fv
    termVars = VarMap -> VarSet
allVars VarMap
fv -- ISet.union rigid flexible
    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 termVars `ISet.isSubsetOf` earlierVars then return () else do

  checked <- fmap catMaybes . forM toCheck $ \ (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 -> VarSet -> VarSet
ISet.union VarSet
earlierVars ([Variable] -> VarSet
ISet.fromList [Variable]
checked)

  if termVars `ISet.isSubsetOf` allowedVars then return () else do
  let
    illegalVars = VarSet
rigid VarSet -> VarSet -> VarSet
ISet.\\ VarSet
allowedVars
    -- flexVars = flexibleVars fv
    -- blockingMetas = map (`lookupVarMap` flexVars) (ISet.toList $ termVars ISet.\\ allowedVars)
  if ISet.null 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)
    patternViolation alwaysUnblock
  else
    typeError $ ReferencesFutureVariables t (List1.fromList (ISet.toList illegalVars)) lk 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.

  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 | [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

  pure mi

isTimeless :: Type -> TCM Bool
isTimeless :: Type -> TCMT IO Bool
isTimeless Type
t = do
  t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  timeless <- mapM getName' [builtinInterval, builtinIsOne]
  case unEl 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 -> TCMT IO b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO b) -> (Doc -> TypeError) -> Doc -> TCMT IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO b) -> TCM Doc -> TCMT IO 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
  mv <- Term -> TCMT IO (Maybe Variable)
getLockVar Term
lk
  caseMaybe mv (return ()) $ \ 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
      ty <- Variable -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Variable -> m Type
typeOfBV Variable
j
      unlessM (isTimeless ty) $
        notAllowedVarsError lk [j]