{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Lock
  ( isTimeless
  , checkLockedVars
  , checkEarlierThan
  , requireGuarded
  )
where

import Control.Monad.Reader

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

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

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

  [Variable]
checked <- ([Maybe Variable] -> [Variable])
-> TCMT IO [Maybe Variable] -> TCMT IO [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe Variable] -> [Variable]
forall a. [Maybe a] -> [a]
catMaybes (TCMT IO [Maybe Variable] -> TCMT IO [Variable])
-> (((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
    -> TCMT IO [Maybe Variable])
-> ((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
-> TCMT IO [Variable]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Variable, Dom (Name, Type))]
-> ((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
-> TCMT IO [Maybe Variable]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Variable, Dom (Name, Type))]
toCheck (((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
 -> TCMT IO [Variable])
-> ((Variable, Dom (Name, Type)) -> TCMT IO (Maybe Variable))
-> TCMT IO [Variable]
forall a b. (a -> b) -> a -> b
$ \ (Variable
j,Dom (Name, Type)
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)
-> (Dom (Name, Type) -> (Name, Type)) -> Dom (Name, Type) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom (Dom (Name, Type) -> Type) -> Dom (Name, Type) -> Type
forall a b. (a -> b) -> a -> b
$ Dom (Name, Type)
dom))
        (Maybe Variable -> TCMT IO (Maybe Variable)
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 (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
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 () -> TCM ()
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)
    Blocker -> TCM ()
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
  else do
    Term -> [Variable] -> TCM ()
forall b. Term -> [Variable] -> TCM b
notAllowedVarsError (Arg Term -> Term
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 = 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

  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 (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 -> Blocker) -> Set MetaId -> Blocker
forall a b. (a -> b) -> a -> b
$ Set MetaId
metas

  [Variable]
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 {m :: * -> *}.
(MonadFail m, MonadTCEnv m) =>
Variable -> m 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 :: Maybe Variable
mi | [Variable] -> 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 (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Variable]
is

  Maybe Variable -> TCMT IO (Maybe Variable)
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
mi

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

isTimeless :: Type -> TCM Bool
isTimeless :: Type -> TCMT IO Bool
isTimeless Type
t = do
  Type
t <- Type -> TCMT IO Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
  [Maybe QName]
timeless <- ([Char] -> TCMT IO (Maybe QName))
-> [[Char]] -> TCMT IO [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Char] -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getName' [[Char]
builtinInterval, [Char]
builtinIsOne]
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
q Elims
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> [Maybe QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
timeless -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Term
_                                -> Bool -> TCMT IO Bool
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 -> TCM b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM b) -> (Doc -> TypeError) -> Doc -> TCM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM b) -> TCM Doc -> TCM 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
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
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 -> VarSet -> TCM ()
checkEarlierThan :: Term -> VarSet -> TCM ()
checkEarlierThan Term
lk VarSet
fvs = do
  Maybe Variable
mv <- Term -> TCMT IO (Maybe Variable)
getLockVar Term
lk
  Maybe Variable -> TCM () -> (Variable -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Variable
mv (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Variable -> TCM ()) -> TCM ()) -> (Variable -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ 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
      Type
ty <- Variable -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Variable -> m Type
typeOfBV Variable
j
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Type -> TCMT IO Bool
isTimeless Type
ty) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Term -> [Variable] -> TCM ()
forall b. Term -> [Variable] -> TCM b
notAllowedVarsError Term
lk [Variable
j]