{-# 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.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 :: Term -> Type'' Term Term -> Arg Term -> Type'' Term Term -> TCM ()
checkLockedVars Term
t Type'' Term Term
ty Arg Term
lk Type'' Term Term
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 <- Arg Term -> TCMT IO (Arg Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Arg Term
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)) $ \ Int
i -> do

  cxt <- TCMT IO (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext

  let fv = (Term, Type'' Term Term) -> VarMap
forall t. Free t => t -> VarMap
freeVarMapIgnoreAnn (Term
t,Type'' Term Term
ty)
  let
    rigid = VarMap -> VarSet
rigidVars VarMap
fv
    -- flexible = IMap.keysSet $ flexibleVars fv
    termVars = VarMap -> VarSet
allVars VarMap
fv -- ISet.union rigid flexible
    earlierVars = Int -> Int -> VarSet
VarSet.range Int
i (Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
cxt)
  if termVars `VarSet.isSubsetOf` earlierVars then return () else do

  let toCheck = [Int] -> [ContextEntry] -> [(Int, ContextEntry)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([ContextEntry] -> [(Int, ContextEntry)])
-> [ContextEntry] -> [(Int, ContextEntry)]
forall a b. (a -> b) -> a -> b
$ (Int -> ContextEntry -> ContextEntry)
-> [Int] -> [ContextEntry] -> [ContextEntry]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> ContextEntry -> ContextEntry
forall a. Subst a => Int -> a -> a
raise [Int
1..] ([ContextEntry] -> [ContextEntry])
-> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> a -> b
$ Int -> Context' ContextEntry -> [ContextEntry]
cxTake Int
i Context' ContextEntry
cxt
  checked <- fmap catMaybes . forM toCheck $ \ (Int
j,ContextEntry
ce) -> do
    TCMT IO Bool
-> TCMT IO (Maybe Int)
-> TCMT IO (Maybe Int)
-> TCMT IO (Maybe Int)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Type'' Term Term -> TCMT IO Bool
isTimeless (ContextEntry -> Type'' Term Term
ctxEntryType ContextEntry
ce))
        (Maybe Int -> TCMT IO (Maybe Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> TCMT IO (Maybe Int))
-> Maybe Int -> TCMT IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int
forall a. a -> Maybe a
Just Int
j)
        (Maybe Int -> TCMT IO (Maybe Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> TCMT IO (Maybe Int))
-> Maybe Int -> TCMT IO (Maybe Int)
forall a b. (a -> b) -> a -> b
$ Maybe Int
forall a. Maybe a
Nothing)

  let allowedVars = VarSet -> VarSet -> VarSet
VarSet.union VarSet
earlierVars ([Int] -> VarSet
VarSet.fromList [Int]
checked)

  if termVars `VarSet.isSubsetOf` allowedVars then return () else do
  let
    illegalVars = VarSet
rigid VarSet -> VarSet -> VarSet
`VarSet.difference` VarSet
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 :: Term -> TCMT IO (Maybe Int)
getLockVar Term
lk = do
  let
    fv :: VarMap
fv = Term -> VarMap
forall t. Free t => t -> VarMap
freeVarMapIgnoreAnn Term
lk
    flex :: IntMap MetaSet
flex = VarMap -> IntMap MetaSet
flexibleVars VarMap
fv

    isLock :: Int -> f Bool
isLock Int
i = (Dom' Term (Type'' Term Term) -> Lock)
-> f (Dom' Term (Type'' Term Term)) -> 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'' Term Term) -> ArgInfo)
-> Dom' Term (Type'' Term Term)
-> Lock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Type'' Term Term) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo) (Int -> f (Dom' Term (Type'' Term Term))
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Dom' Term (Type'' Term Term))
domOfBV Int
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 <- (Int -> TCMT IO Bool) -> [Int] -> TCMT IO [Int]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Int -> TCMT IO Bool
forall {f :: * -> *}. (MonadDebug f, MonadTCEnv f) => Int -> f Bool
isLock ([Int] -> TCMT IO [Int]) -> [Int] -> TCMT IO [Int]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Int]
VarSet.toAscList (VarSet -> [Int]) -> VarSet -> [Int]
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 | [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [Int]
is   = Maybe Int
forall a. Maybe a
Nothing
         | Bool
otherwise = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
is

  pure mi

isTimeless :: Type -> TCM Bool
isTimeless :: Type'' Term Term -> TCMT IO Bool
isTimeless Type'' Term Term
t = do
  t <- Type'' Term Term -> TCMT IO (Type'' Term Term)
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type'' Term Term
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 -> VarSet -> TCM Bool
checkEarlierThan :: Term -> VarSet -> TCMT IO Bool
checkEarlierThan Term
lk VarSet
fvs = do
  Term -> TCMT IO (Maybe Int)
getLockVar Term
lk TCMT IO (Maybe Int) -> (Maybe Int -> 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 Int
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just Int
i  -> (Int -> TCMT IO Bool) -> [Int] -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
allM (Type'' Term Term -> TCMT IO Bool
isTimeless (Type'' Term Term -> TCMT IO Bool)
-> (Int -> TCMT IO (Type'' Term Term)) -> Int -> TCMT IO Bool
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Int -> TCMT IO (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV) ([Int] -> TCMT IO Bool) -> [Int] -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ VarSet -> [Int]
VarSet.toAscList VarSet
fvs