content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  {-# LANGUAGE NondecreasingIndentation #-}
  
  module Agda.TypeChecking.Lock
    ( isTimeless
    , checkLockedVars
    , checkEarlierThan
    )
  where
  
  import Prelude hiding (null)
  import qualified Prelude as Prelude
  
  import qualified Data.IntMap as IMap
  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 VarSet
  import Agda.Utils.VarSet (VarSet)
  import Agda.Utils.Functor
  import Agda.Utils.Maybe
  import Agda.Utils.Monad
  import Agda.Utils.Null
  import Agda.Utils.Size
  
  checkLockedVars ::
       Term
       -- ^ term to check
    -> Type
       -- ^ its type
    -> Arg Term
       -- ^ the lock
    -> Type
       -- ^ type of the lock
    -> TCM ()
  checkLockedVars t ty lk lk_ty = 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 <- instantiateFull lk
    catchConstraint (CheckLockedVars t ty lk lk_ty) do
  
    reportSDoc "tc.term.lock" 40 $ "Checking locked vars.."
    reportSDoc "tc.term.lock" 45 $ nest 2 $ vcat
       [ text "t     = " <+> prettyTCM t
       , text "ty    = " <+> prettyTCM ty
       , text "lk    = " <+> prettyTCM lk
       , text "lk_ty = " <+> prettyTCM lk_ty
       ]
    reportSDoc "tc.term.lock" 80 $ 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)) $ \ i -> do
  
    cxt <- getContext
  
    let fv = freeVarsIgnore IgnoreInAnnotations (t,ty)
    let
      rigid = rigidVars fv
      -- flexible = IMap.keysSet $ flexibleVars fv
      termVars = allVars fv -- ISet.union rigid flexible
      earlierVars = VarSet.range i (size cxt)
    if termVars `VarSet.isSubsetOf` earlierVars then return () else do
  
    let toCheck = zip [0..] $ zipWith raise [1..] (take i cxt)
    checked <- fmap catMaybes . forM toCheck $ \ (j,ce) -> do
      ifM (isTimeless (ctxEntryType ce))
          (return $ Just j)
          (return $ Nothing)
  
    let allowedVars = VarSet.union earlierVars (VarSet.fromList checked)
  
    if termVars `VarSet.isSubsetOf` allowedVars then return () else do
    let
      illegalVars = rigid `VarSet.difference` allowedVars
      -- flexVars = flexibleVars fv
      -- blockingMetas = map (`lookupVarMap` flexVars) (ISet.toList $ termVars ISet.\\ allowedVars)
    if 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 (VarSet.toAscList illegalVars)) lk i
      -- List1.fromList is guarded by not (null illegalVars)
  
  
  -- | Precondition: 'Term' is fully instantiated.
  getLockVar :: Term -> TCMT IO (Maybe Int)
  getLockVar lk = do
    let
      fv = freeVarsIgnore IgnoreInAnnotations lk
      flex = flexibleVars fv
  
      isLock i = fmap (getLock . domInfo) (domOfBV i) <&> \case
        IsLock{} -> True
        IsNotLock{} -> False
  
    unless (IMap.null flex) $ do
      let metas = Set.unions $ map (foldrMetaSet Set.insert Set.empty) $ IMap.elems flex
      patternViolation $ unblockOnAnyMeta 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 <- filterM isLock $ VarSet.toAscList $ rigidVars 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 | Prelude.null is   = Nothing
           | otherwise = Just $ maximum is
  
    pure mi
  
  isTimeless :: Type -> TCM Bool
  isTimeless t = do
    t <- abortIfBlocked t
    timeless <- mapM getName' [builtinInterval, builtinIsOne]
    case unEl t of
      Def q _ | Just q `elem` timeless -> return True
      _                                -> return 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 -> VarSet -> TCM Bool
  checkEarlierThan lk fvs = do
    getLockVar lk >>= \case
      Nothing -> return True
      Just i  -> allM (isTimeless <=< typeOfBV) $ filter (<= i) $ VarSet.toAscList fvs
  