{-# 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 = 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
Arg Term
lk <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Arg Term
lk
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Variable -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.term.lock" Variable
40 forall a b. (a -> b) -> a -> b
$ TCM Doc
"Checking locked vars.."
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Variable -> TCM Doc -> m ()
reportSDoc VerboseKey
"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 => VerboseKey -> m Doc
text VerboseKey
"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 => VerboseKey -> m Doc
text VerboseKey
"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 => VerboseKey -> m Doc
text VerboseKey
"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 => VerboseKey -> m Doc
text VerboseKey
"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
]
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.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (Term -> Type -> Arg Term -> TypeError
DoesNotMentionTicks Term
t Type
ty Arg Term
lk)) 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
termVars :: VarSet
termVars = VarMap -> VarSet
allVars VarMap
fv
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 -> TCM 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
if VarSet -> Bool
ISet.null VarSet
illegalVars then
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
else
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Term -> NonEmpty Variable -> Arg Term -> Variable -> TypeError
ReferencesFutureVariables Term
t (forall l. IsList l => [Item l] -> l
List1.fromList (VarSet -> [Variable]
ISet.toList VarSet
illegalVars)) Arg Term
lk Variable
i
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
isLock :: Variable -> m Bool
isLock Variable
i = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Variable -> m ContextEntry
lookupBV Variable
i) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
IsLock{} -> Bool
True
IsNotLock{} -> Bool
False
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 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
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 (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Variable
mi
isTimeless :: Type -> TCM Bool
isTimeless :: Type -> TCM 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 :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' [BuiltinId
builtinInterval, BuiltinId
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 -> VSet.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 -> TCM Bool
isTimeless Type
ty) forall a b. (a -> b) -> a -> b
$
forall b. Term -> [Variable] -> TCM b
notAllowedVarsError Term
lk [Variable
j]