{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Lock
( isTimeless
, checkLockedVars
, checkEarlierThan
)
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.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Constraints ()
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
-> Type
-> Arg Term
-> Type
-> 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
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
]
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
termVars = VarMap -> VarSet
allVars VarMap
fv
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
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)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom (ContextEntry -> Type) -> ContextEntry -> Type
forall a b. (a -> b) -> a -> b
$ ContextEntry
dom))
(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
if ISet.null illegalVars then
patternViolation alwaysUnblock
else
typeError $ ReferencesFutureVariables t (List1.fromList (ISet.toList illegalVars)) lk i
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 = (ContextEntry -> Lock) -> f ContextEntry -> 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)
-> (ContextEntry -> ArgInfo) -> ContextEntry -> Lock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo) (Variable -> f ContextEntry
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Variable -> m ContextEntry
lookupBV 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 (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 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
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 :: * -> *}.
(MonadFail 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
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
notAllowedVarsError :: Term -> [Int] -> TCM b
notAllowedVarsError :: forall b. Term -> [Variable] -> TCM b
notAllowedVarsError Term
lk [Variable]
is = do
TypeError -> TCMT IO b
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO b) -> (Doc -> TypeError) -> Doc -> TCMT IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO b) -> TCM Doc -> TCMT IO 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
forall (m :: * -> *). MonadPretty m => Term -> 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
forall (m :: * -> *). MonadPretty m => [Term] -> 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 -> VSet.VarSet -> TCM ()
checkEarlierThan :: Term -> VarSet -> TCM ()
checkEarlierThan Term
lk VarSet
fvs = do
mv <- Term -> TCMT IO (Maybe Variable)
getLockVar Term
lk
caseMaybe mv (return ()) $ \ 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
ty <- Variable -> TCMT IO Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Variable -> m Type
typeOfBV Variable
j
unlessM (isTimeless ty) $
notAllowedVarsError lk [j]