{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Opacity
( saturateOpaqueBlocks
, isAccessibleDef
, hasAccessibleDef
)
where
import Control.Monad.State
import Control.Exception
import Control.DeepSeq
import Control.Monad
import qualified Data.HashMap.Strict as HashMap
import qualified Data.Map.Strict as Map
import qualified Data.HashSet as HashSet
import qualified Data.List as List
import Data.HashMap.Strict (HashMap)
import Data.HashSet (HashSet)
import Data.Map.Strict (Map)
import Data.Foldable
import Data.Maybe
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Monad
import Agda.Utils.Impossible
import Agda.Utils.Monad
import Agda.Utils.Lens
saturateOpaqueBlocks
:: forall m. (MonadTCState m, ReadTCState m, MonadFresh OpaqueId m, MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m)
=> [A.Declaration]
-> m ()
saturateOpaqueBlocks :: forall (m :: * -> *).
(MonadTCState m, ReadTCState m, MonadFresh OpaqueId m,
MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m) =>
[Declaration] -> m ()
saturateOpaqueBlocks [Declaration]
moddecs = m ()
entry where
entry :: m ()
entry = do
Map OpaqueId OpaqueBlock
known <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
Map QName OpaqueId
inverse <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (Map QName OpaqueId)
stOpaqueIds
OpaqueId Word64
_ ModuleNameHash
ourmod <- forall i (m :: * -> *). MonadFresh i m => m i
fresh
HashMap QName QName
canonical <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (HashMap QName QName)
stCopiedNames
HashMap QName (HashSet QName)
backcopies <- forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC Lens' TCState (HashMap QName (HashSet QName))
stNameCopies
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Canonical names of copied definitions:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap QName QName
canonical)
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Backcopies:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall k v. HashMap k v -> [(k, v)]
HashMap.toList (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap QName (HashSet QName)
backcopies))
let
isOurs :: (OpaqueId, OpaqueBlock) -> Bool
isOurs (OpaqueId Word64
_ ModuleNameHash
mod, OpaqueBlock
_) = ModuleNameHash
mod forall a. Eq a => a -> a -> Bool
== ModuleNameHash
ourmod
canonise :: QName -> QName
canonise QName
name = forall a. a -> Maybe a -> a
fromMaybe QName
name (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup QName
name HashMap QName QName
canonical)
ours :: [OpaqueBlock]
ours = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (OpaqueId, OpaqueBlock) -> Bool
isOurs (forall k a. Map k a -> [(k, a)]
Map.toAscList Map OpaqueId OpaqueBlock
known)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OpaqueBlock]
ours) forall a b. (a -> b) -> a -> b
$ do
() <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO a
evaluate (forall a. NFData a => a -> ()
rnf (HashMap QName QName
canonical, HashMap QName (HashSet QName)
backcopies))
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Opaque blocks defined in this module:"forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [OpaqueBlock]
ours
(Map OpaqueId OpaqueBlock
blocks, Map QName OpaqueId
names) <- (QName -> QName)
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure QName -> QName
canonise Map OpaqueId OpaqueBlock
known Map QName OpaqueId
inverse [OpaqueBlock]
ours
let names' :: Map QName OpaqueId
names' = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (QName, HashSet QName) -> Map QName OpaqueId -> Map QName OpaqueId
addBackcopy Map QName OpaqueId
names (forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap QName (HashSet QName)
backcopies)
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.sat" VerboseLevel
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Saturated local opaque blocks"forall a. a -> [a] -> [a]
:[ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OpaqueBlock
block | b :: (OpaqueId, OpaqueBlock)
b@(OpaqueId
_,OpaqueBlock
block) <- forall k a. Map k a -> [(k, a)]
Map.toList Map OpaqueId OpaqueBlock
blocks, (OpaqueId, OpaqueBlock) -> Bool
isOurs (OpaqueId, OpaqueBlock)
b ]
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.sat.full" VerboseLevel
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Saturated opaque blocks:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Map OpaqueId OpaqueBlock
blocks
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC' forall a b. (a -> b) -> a -> b
$ \TCState
st -> TCState
st { stPostScopeState :: PostScopeState
stPostScopeState = (TCState -> PostScopeState
stPostScopeState TCState
st)
{ stPostOpaqueBlocks :: Map OpaqueId OpaqueBlock
stPostOpaqueBlocks = Map OpaqueId OpaqueBlock
blocks
, stPostOpaqueIds :: Map QName OpaqueId
stPostOpaqueIds = Map QName OpaqueId
names'
} }
computeClosure
:: (QName -> QName)
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m ( Map OpaqueId OpaqueBlock
, Map QName OpaqueId
)
computeClosure :: (QName -> QName)
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure QName -> QName
canonise !Map OpaqueId OpaqueBlock
blocks !Map QName OpaqueId
names [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map OpaqueId OpaqueBlock
blocks, Map QName OpaqueId
names)
computeClosure QName -> QName
canonise Map OpaqueId OpaqueBlock
blocks Map QName OpaqueId
names (OpaqueBlock
block:[OpaqueBlock]
xs) = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (OpaqueBlock -> Range
opaqueRange OpaqueBlock
block) forall a b. (a -> b) -> a -> b
$ do
let
yell :: QName -> a -> m a
yell QName
nm a
accum = forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (forall a. HasRange a => a -> Range
getRange QName
nm) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (QName -> Warning
UnfoldTransparentName QName
nm)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
accum
transitive :: QName -> HashSet QName -> m (HashSet QName)
transitive QName
prenom HashSet QName
accum = forall a. a -> Maybe a -> a
fromMaybe (forall {m :: * -> *} {a}.
(MonadTrace m, MonadWarning m) =>
QName -> a -> m a
yell QName
prenom HashSet QName
accum) forall a b. (a -> b) -> a -> b
$ do
let nm :: QName
nm = QName -> QName
canonise QName
prenom
OpaqueId
id <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
nm Map QName OpaqueId
names
OpaqueBlock
block <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OpaqueId
id Map OpaqueId OpaqueBlock
blocks
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block) HashSet QName
accum
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"Stated unfolding clause: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. HashSet a -> [a]
HashSet.toList (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block))
, TCMT IO Doc
"with (sub)canonical names:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> QName
canonise forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
HashSet.toList (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block))
]
HashSet QName
closed <- forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM QName -> HashSet QName -> m (HashSet QName)
transitive
( OpaqueBlock -> HashSet QName
opaqueDecls OpaqueBlock
block
forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap OpaqueBlock -> HashSet QName
opaqueUnfolding (OpaqueBlock -> Maybe OpaqueId
opaqueParent OpaqueBlock
block forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Map OpaqueId OpaqueBlock
blocks)
)
(OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block)
let
block' :: OpaqueBlock
block' = OpaqueBlock
block { opaqueUnfolding :: HashSet QName
opaqueUnfolding = HashSet QName
closed }
names' :: Map QName OpaqueId
names' = forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr (\QName
name -> forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
name (OpaqueBlock -> OpaqueId
opaqueId OpaqueBlock
block)) Map QName OpaqueId
names
(OpaqueBlock -> HashSet QName
opaqueDecls OpaqueBlock
block)
(QName -> QName)
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure QName -> QName
canonise (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (OpaqueBlock -> OpaqueId
opaqueId OpaqueBlock
block) OpaqueBlock
block' Map OpaqueId OpaqueBlock
blocks) Map QName OpaqueId
names' [OpaqueBlock]
xs
addBackcopy :: (QName, HashSet QName) -> Map QName OpaqueId -> Map QName OpaqueId
addBackcopy :: (QName, HashSet QName) -> Map QName OpaqueId -> Map QName OpaqueId
addBackcopy (QName
from, HashSet QName
prop) Map QName OpaqueId
map
| Just OpaqueId
id <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
from Map QName OpaqueId
map = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert OpaqueId
id) Map QName OpaqueId
map HashSet QName
prop
| Bool
otherwise = Map QName OpaqueId
map
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
isAccessibleDef TCEnv
env TCState
state Definition
defn
| TCEnv -> AbstractMode
envAbstractMode TCEnv
env forall a. Eq a => a -> a -> Bool
== AbstractMode
IgnoreAbstractMode = Bool
True
isAccessibleDef TCEnv
env TCState
state Definition
defn =
let
concretise :: IsAbstract -> IsAbstract
concretise IsAbstract
def = case TCEnv -> AbstractMode
envAbstractMode TCEnv
env of
AbstractMode
ConcreteMode -> IsAbstract
def
AbstractMode
IgnoreAbstractMode -> IsAbstract
ConcreteDef
AbstractMode
AbstractMode
| ModuleName
current ModuleName -> ModuleName -> Bool
`isLeChildModuleOf` ModuleName
m -> IsAbstract
ConcreteDef
| Bool
otherwise -> IsAbstract
def
where
current :: ModuleName
current = ModuleName -> ModuleName
dropAnon forall a b. (a -> b) -> a -> b
$ TCEnv -> ModuleName
envCurrentModule TCEnv
env
m :: ModuleName
m = ModuleName -> ModuleName
dropAnon forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule (Definition -> QName
defName Definition
defn)
dropAnon :: ModuleName -> ModuleName
dropAnon (MName [Name]
ms) = [Name] -> ModuleName
MName forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd forall a. IsNoName a => a -> Bool
isNoName [Name]
ms
clarify :: IsOpaque -> IsOpaque
clarify IsOpaque
def = case TCEnv -> Maybe OpaqueId
envCurrentOpaqueId TCEnv
env of
Just OpaqueId
oid ->
let
block :: OpaqueBlock
block = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OpaqueId
oid (forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
view Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks TCState
state)
okay :: Bool
okay = Definition -> QName
defName Definition
defn forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block
in if Bool
okay then IsOpaque
TransparentDef else IsOpaque
def
Maybe OpaqueId
Nothing -> IsOpaque
def
plainDef :: Bool
plainDef = Definition -> IsAbstract
defAbstract Definition
defn forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef
Bool -> Bool -> Bool
&& Definition -> IsOpaque
defOpaque Definition
defn forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef
in Bool
plainDef
Bool -> Bool -> Bool
|| ( IsAbstract -> IsAbstract
concretise (Definition -> IsAbstract
defAbstract Definition
defn) forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef
Bool -> Bool -> Bool
&& IsOpaque -> IsOpaque
clarify (Definition -> IsOpaque
defOpaque Definition
defn) forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef)
hasAccessibleDef
:: (ReadTCState m, MonadTCEnv m, HasConstInfo m) => QName -> m Bool
hasAccessibleDef :: forall (m :: * -> *).
(ReadTCState m, MonadTCEnv m, HasConstInfo m) =>
QName -> m Bool
hasAccessibleDef QName
qn = do
TCEnv
env <- forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
TCState
st <- forall (m :: * -> *). ReadTCState m => m TCState
getTCState
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TCEnv -> TCState -> Definition -> Bool
isAccessibleDef TCEnv
env TCState
st Definition
def