    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

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

    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
    ce) -> 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 (ContextEntry -> Type
    ctxEntryType ContextEntry
    ce))
            (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 = (Dom' Term Type -> Lock) -> f (Dom' Term Type) -> 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)
    -> (Dom' Term Type -> ArgInfo) -> Dom' Term Type -> Lock
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term Type -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo) (Variable -> f (Dom' Term Type)
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Variable -> m (Dom' Term Type)
    domOfBV 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    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 :: * -> *}.
    (MonadDebug 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

    -- | If the first argument is a lock variable, check that all variables in the given set
    --   are either earlier than this variable or are timeless.
    --
    checkEarlierThan :: Term -> VSet.VarSet -> TCM Bool
    checkEarlierThan :: Term -> VarSet -> TCMT IO Bool
    checkEarlierThan Term
    lk VarSet
    fvs = do
      Term -> TCMT IO (Maybe Variable)
    getLockVar Term
    lk TCMT IO (Maybe Variable)
    -> (Maybe Variable -> TCMT IO Bool) -> TCMT IO Bool
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Maybe Variable
    Nothing -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Just Variable
    i  -> (Variable -> TCMT IO Bool) -> [Variable] -> TCMT IO Bool
    forall (f :: * -> *) (m :: * -> *) a.
    (Foldable f, Monad m) =>
    (a -> m Bool) -> f a -> m Bool
    allM (Type -> TCMT IO Bool
    isTimeless (Type -> TCMT IO Bool)
    -> (Variable -> TCMT IO Type) -> Variable -> TCMT IO Bool
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Variable -> TCMT IO Type
    forall (m :: * -> *).
    (MonadDebug m, MonadTCEnv m) =>
    Variable -> m Type
    typeOfBV) ([Variable] -> TCMT IO Bool) -> [Variable] -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ (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