{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Lock
  ( isTimeless
  , checkLockedVars
  , checkEarlierThan
  , requireGuarded
  )
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.Interaction.Options ( optGuarded )

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute.Class
import Agda.TypeChecking.Free

import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.VarSet as VSet

import Agda.Utils.Impossible

requireGuarded :: String -> TCM ()
requireGuarded :: [Char] -> TCM ()
requireGuarded [Char]
s = do
  Bool
guarded <- PragmaOptions -> Bool
optGuarded forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
guarded forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Missing option --guarded " forall a. [a] -> [a] -> [a]
++ [Char]
s


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 = 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) forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Variable -> TCM Doc -> m ()
reportSDoc [Char]
"tc.term.lock" Variable
40 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking locked vars.."
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Variable -> TCM Doc -> m ()
reportSDoc [Char]
"tc.term.lock" Variable
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Variable -> m Doc -> m Doc
nest Variable
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
     [ forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"t     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
t
     , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"ty    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
     , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"lk    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
lk
     , forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"lk_ty = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 (forall e. Arg e -> e
unArg Arg Term
lk)
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Variable
mi (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \ Variable
i -> do

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

  let fv :: VarMap
fv = 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
iforall a. Num a => a -> a -> a
+Variable
1 .. forall a. Sized a => a -> Variable
size Context
cxt forall a. Num a => a -> a -> a
- Variable
1]
  if VarSet
termVars VarSet -> VarSet -> Bool
`ISet.isSubsetOf` VarSet
earlierVars then forall (m :: * -> *) a. Monad m => a -> m a
return () else do

  [Variable]
checked <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Variable, ContextEntry)]
toCheck forall a b. (a -> b) -> a -> b
$ \ (Variable
j,ContextEntry
dom) -> do
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Type -> TCMT IO Bool
isTimeless (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ ContextEntry
dom))
        (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Variable
j)
        (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 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)
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
  else do
    forall b. Term -> [Variable] -> TCM b
notAllowedVarsError (forall e. Arg e -> e
unArg Arg Term
lk) (VarSet -> [Variable]
ISet.toList VarSet
illegalVars)


getLockVar :: Term -> TCMT IO (Maybe Int)
getLockVar :: Term -> TCMT IO (Maybe Variable)
getLockVar Term
lk = do
  let
    fv :: VarMap
fv = 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

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. IntMap a -> Bool
IMap.null IntMap MetaSet
flex) forall a b. (a -> b) -> a -> b
$ do
    let metas :: Set MetaId
metas = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. (MetaId -> a -> a) -> a -> MetaSet -> a
foldrMetaSet forall a. Ord a => a -> Set a -> Set a
Set.insert forall a. Set a
Set.empty) forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [a]
IMap.elems IntMap MetaSet
flex
    forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation forall a b. (a -> b) -> a -> b
$ Set MetaId -> Blocker
unblockOnAnyMeta forall a b. (a -> b) -> a -> b
$ Set MetaId
metas

  [Variable]
is <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM forall {m :: * -> *}.
(MonadFail m, MonadTCEnv m) =>
Variable -> m Bool
isLock forall a b. (a -> b) -> a -> b
$ VarSet -> [Variable]
ISet.toList 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 | forall (t :: * -> *) a. Foldable t => t a -> Bool
Prelude.null [Variable]
is   = forall a. Maybe a
Nothing
         | Bool
otherwise = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Variable]
is

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe Variable
mi

  where
   isLock :: Variable -> m Bool
isLock Variable
i = do
     Lock
islock <- forall a. LensLock a => a -> Lock
getLock forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> ArgInfo
domInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Variable -> m ContextEntry
lookupBV Variable
i
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Lock
islock forall a. Eq a => a -> a -> Bool
== Lock
IsLock

isTimeless :: Type -> TCM Bool
isTimeless :: Type -> TCMT IO Bool
isTimeless Type
t = do
  Type
t <- forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  [Maybe QName]
timeless <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getName' [[Char]
builtinInterval, [Char]
builtinIsOne]
  case forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
q Elims
_ | forall a. a -> Maybe a
Just QName
q forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
timeless -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Term
_                                -> 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
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError 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"
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
lk forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a b. (a -> b) -> [a] -> [b]
map Variable -> Term
var forall a b. (a -> b) -> a -> b
$ [Variable]
is))

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