{-# 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

-- | Ensure that opaque blocks defined in the current module have
-- saturated unfolding sets.
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   <- Lens' TCState (Map OpaqueId OpaqueBlock)
-> m (Map OpaqueId OpaqueBlock)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock))
-> TCState -> f TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks
    Map QName OpaqueId
inverse <- Lens' TCState (Map QName OpaqueId) -> m (Map QName OpaqueId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Map QName OpaqueId -> f (Map QName OpaqueId))
-> TCState -> f TCState
Lens' TCState (Map QName OpaqueId)
stOpaqueIds
    OpaqueId Word64
_ ModuleNameHash
ourmod <- m OpaqueId
forall i (m :: * -> *). MonadFresh i m => m i
fresh

    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Canonical names of copied definitions:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ [(QName, QName)] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (HashMap QName QName -> [(QName, QName)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap QName QName
canonical)
    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Backcopies:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ [(QName, [QName])] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (HashMap QName [QName] -> [(QName, [QName])]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList (HashSet QName -> [QName]
forall a. HashSet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (HashSet QName -> [QName])
-> HashMap QName (HashSet QName) -> HashMap QName [QName]
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 ModuleNameHash -> ModuleNameHash -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleNameHash
ourmod
      ours :: [OpaqueBlock]
ours = (OpaqueId, OpaqueBlock) -> OpaqueBlock
forall a b. (a, b) -> b
snd ((OpaqueId, OpaqueBlock) -> OpaqueBlock)
-> [(OpaqueId, OpaqueBlock)] -> [OpaqueBlock]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((OpaqueId, OpaqueBlock) -> Bool)
-> [(OpaqueId, OpaqueBlock)] -> [(OpaqueId, OpaqueBlock)]
forall a. (a -> Bool) -> [a] -> [a]
filter (OpaqueId, OpaqueBlock) -> Bool
isOurs (Map OpaqueId OpaqueBlock -> [(OpaqueId, OpaqueBlock)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map OpaqueId OpaqueBlock
known)

    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([OpaqueBlock] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OpaqueBlock]
ours) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    () <- IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall a. a -> IO a
evaluate ((HashMap QName QName, HashMap QName (HashSet QName)) -> ()
forall a. NFData a => a -> ()
rnf (HashMap QName QName
canonical, HashMap QName (HashSet QName)
backcopies))

    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque" VerboseLevel
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
      VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Opaque blocks defined in this module:"TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
:(OpaqueBlock -> TCMT IO Doc) -> [OpaqueBlock] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map OpaqueBlock -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [OpaqueBlock]
ours

    -- Only compute transitive closure for opaque blocks declared in
    -- the current top-level module. Deserialised blocks are always
    -- closed, so this work would be redundant.
    (Map OpaqueId OpaqueBlock
blocks, Map QName OpaqueId
names) <- Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure Map OpaqueId OpaqueBlock
known Map QName OpaqueId
inverse [OpaqueBlock]
ours

    -- Associate copies with the opaque blocks of their originals. Since
    -- modules importing this one won't know how to canonicalise names
    -- we have defined, we make the work easier for them by associating
    -- copies with their original's opaque blocks.
    let names' :: Map QName OpaqueId
names' = ((QName, HashSet QName)
 -> Map QName OpaqueId -> Map QName OpaqueId)
-> Map QName OpaqueId
-> [(QName, HashSet QName)]
-> Map QName OpaqueId
forall a b. (a -> b -> b) -> b -> [a] -> b
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 (HashMap QName (HashSet QName) -> [(QName, HashSet QName)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList HashMap QName (HashSet QName)
backcopies)

    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.sat" VerboseLevel
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
      VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Saturated local opaque blocks"TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
:[ OpaqueBlock -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty OpaqueBlock
block | b :: (OpaqueId, OpaqueBlock)
b@(OpaqueId
_,OpaqueBlock
block) <- Map OpaqueId OpaqueBlock -> [(OpaqueId, OpaqueBlock)]
forall k a. Map k a -> [(k, a)]
Map.toList Map OpaqueId OpaqueBlock
blocks, (OpaqueId, OpaqueBlock) -> Bool
isOurs (OpaqueId, OpaqueBlock)
b ]

    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.sat.full" VerboseLevel
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TCMT IO Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text VerboseKey
"Saturated opaque blocks:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$ Map OpaqueId OpaqueBlock -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Map OpaqueId OpaqueBlock
blocks

    (TCState -> TCState) -> m ()
forall (m :: * -> *).
MonadTCState m =>
(TCState -> TCState) -> m ()
modifyTC' ((TCState -> TCState) -> m ()) -> (TCState -> TCState) -> m ()
forall a b. (a -> b) -> a -> b
$ \TCState
st -> TCState
st { stPostScopeState = (stPostScopeState st)
      { stPostOpaqueBlocks = blocks
      , stPostOpaqueIds    = names'
      } }

  -- Actually compute the closure.
  computeClosure
    :: Map OpaqueId OpaqueBlock
      -- Accumulates the satured opaque blocks; also contains the
      -- opaque blocks of imported modules.
    -> Map QName OpaqueId
      -- Accumulates a mapping from names to opaque blocks; also
      -- contains imported opaque names.
    -> [OpaqueBlock]
      -- List of our opaque blocks, in dependency order.
    -> m ( Map OpaqueId OpaqueBlock
         , Map QName OpaqueId
         )
  computeClosure :: Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure !Map OpaqueId OpaqueBlock
blocks !Map QName OpaqueId
names [] = (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map OpaqueId OpaqueBlock
blocks, Map QName OpaqueId
names)
  computeClosure Map OpaqueId OpaqueBlock
blocks Map QName OpaqueId
names (OpaqueBlock
block:[OpaqueBlock]
xs) = Range
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (OpaqueBlock -> Range
opaqueRange OpaqueBlock
block) (m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
 -> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId))
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
forall a b. (a -> b) -> a -> b
$ do
    let
      yell :: QName -> a -> m a
yell QName
nm a
accum = Range -> m a -> m a
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
nm) (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
        Warning -> m ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (QName -> Warning
UnfoldTransparentName QName
nm)
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
accum

      -- Add the unfolding-set of the given name to the accumulator
      -- value.
      transitive :: QName -> HashSet QName -> m (HashSet QName)
transitive QName
prenom HashSet QName
accum = m (HashSet QName) -> Maybe (m (HashSet QName)) -> m (HashSet QName)
forall a. a -> Maybe a -> a
fromMaybe (QName -> HashSet QName -> m (HashSet QName)
forall {m :: * -> *} {a}.
(MonadTrace m, MonadWarning m) =>
QName -> a -> m a
yell QName
prenom HashSet QName
accum) (Maybe (m (HashSet QName)) -> m (HashSet QName))
-> Maybe (m (HashSet QName)) -> m (HashSet QName)
forall a b. (a -> b) -> a -> b
$ do
        -- NB: If the name is a local copy, we won't yet have added the
        -- copy name to an opaque block, but we will have added the
        -- reduced name (provided it is opaque)
        let nm :: QName
nm = QName -> QName
canonise QName
prenom
        OpaqueId
id    <- QName -> Map QName OpaqueId -> Maybe OpaqueId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
nm Map QName OpaqueId
names
        OpaqueBlock
block <- OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OpaqueId
id Map OpaqueId OpaqueBlock
blocks
        m (HashSet QName) -> Maybe (m (HashSet QName))
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m (HashSet QName) -> Maybe (m (HashSet QName)))
-> (HashSet QName -> m (HashSet QName))
-> HashSet QName
-> Maybe (m (HashSet QName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet QName -> m (HashSet QName)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HashSet QName -> Maybe (m (HashSet QName)))
-> HashSet QName -> Maybe (m (HashSet QName))
forall a b. (a -> b) -> a -> b
$ HashSet QName -> HashSet QName -> HashSet QName
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HashSet.union (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block) HashSet QName
accum

    VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.opaque.copy" VerboseLevel
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"Stated unfolding clause:  " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (HashSet QName -> [QName]
forall a. HashSet a -> [a]
HashSet.toList (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block))
           , TCMT IO Doc
"with (sub)canonical names:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (QName -> QName
canonise (QName -> QName) -> [QName] -> [QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet QName -> [QName]
forall a. HashSet a -> [a]
HashSet.toList (OpaqueBlock -> HashSet QName
opaqueUnfolding OpaqueBlock
block))
           ]

    -- Compute the transitive closure: bring in names
    --
    --   ... that are defined as immediate children of the opaque block
    --   ... that are unfolded by the parent opaque block
    --   ... that are implied by each name in the unfolding clause.
    HashSet QName
closed <- (QName -> HashSet QName -> m (HashSet QName))
-> HashSet QName -> HashSet QName -> m (HashSet QName)
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
      HashSet QName -> HashSet QName -> HashSet QName
forall a. Semigroup a => a -> a -> a
<> (OpaqueBlock -> HashSet QName)
-> Maybe OpaqueBlock -> HashSet QName
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap OpaqueBlock -> HashSet QName
opaqueUnfolding (OpaqueBlock -> Maybe OpaqueId
opaqueParent OpaqueBlock
block Maybe OpaqueId
-> (OpaqueId -> Maybe OpaqueBlock) -> Maybe OpaqueBlock
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock)
-> Map OpaqueId OpaqueBlock -> OpaqueId -> Maybe OpaqueBlock
forall a b c. (a -> b -> c) -> b -> a -> c
flip OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock
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 = closed }

      -- Update the mapping from names to blocks, so that future
      -- references to names defined in our opaque block will know the
      -- right unfolding set.
      names' :: Map QName OpaqueId
names' = (QName -> Map QName OpaqueId -> Map QName OpaqueId)
-> Map QName OpaqueId -> HashSet QName -> Map QName OpaqueId
forall b a. (b -> a -> a) -> a -> HashSet b -> a
HashSet.foldr (\QName
name -> QName -> OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId
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)

    Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> [OpaqueBlock]
-> m (Map OpaqueId OpaqueBlock, Map QName OpaqueId)
computeClosure (OpaqueId
-> OpaqueBlock
-> Map OpaqueId OpaqueBlock
-> Map OpaqueId OpaqueBlock
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

  (HashMap QName QName
canonical, HashMap QName (HashSet QName)
backcopies) = [Declaration]
-> (HashMap QName QName, HashMap QName (HashSet QName))
invertDefCopies [Declaration]
moddecs
  canonise :: QName -> QName
canonise QName
name = QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
name (QName -> HashMap QName QName -> Maybe QName
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup QName
name HashMap QName QName
canonical)

  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 <- QName -> Map QName OpaqueId -> Maybe OpaqueId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
from Map QName OpaqueId
map = (QName -> Map QName OpaqueId -> Map QName OpaqueId)
-> Map QName OpaqueId -> HashSet QName -> Map QName OpaqueId
forall b a. (b -> a -> a) -> a -> HashSet b -> a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((QName -> OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId)
-> OpaqueId -> QName -> Map QName OpaqueId -> Map QName OpaqueId
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> OpaqueId -> Map QName OpaqueId -> Map QName OpaqueId
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

-- | Decide whether or not a definition is reducible. Returns 'True' if
-- the definition /can/ step.
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool

-- IgnoreAbstractMode ignores both abstract and opaque. It is used for
-- getting the original definition (for inConcreteOrAbstractMode), and
-- for "normalise ignoring abstract" interactively.
isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
isAccessibleDef TCEnv
env TCState
state Definition
defn
  | TCEnv -> AbstractMode
envAbstractMode TCEnv
env AbstractMode -> AbstractMode -> Bool
forall a. Eq a => a -> a -> Bool
== AbstractMode
IgnoreAbstractMode = Bool
True

-- Otherwise, actually apply the reducibility rules..
isAccessibleDef TCEnv
env TCState
state Definition
defn =
  let
    -- Reducibility rules for abstract definitions:
    concretise :: IsAbstract -> IsAbstract
concretise IsAbstract
def = case TCEnv -> AbstractMode
envAbstractMode TCEnv
env of
      -- Being outside an abstract block has no effect on concreteness
      AbstractMode
ConcreteMode       -> IsAbstract
def

      -- This clause is redundant with the preceding guard but GHC can't
      -- figure it out:
      AbstractMode
IgnoreAbstractMode -> IsAbstract
ConcreteDef

      AbstractMode
AbstractMode
        -- Symbols from enclosing modules will be made concrete:
        | ModuleName
current ModuleName -> ModuleName -> Bool
`isLeChildModuleOf` ModuleName
m -> IsAbstract
ConcreteDef

        -- Symbols from child modules, or unrelated modules, will keep
        -- the same concreteness:
        | Bool
otherwise                     -> IsAbstract
def
      where
        current :: ModuleName
current = ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
forall a b. (a -> b) -> a -> b
$ TCEnv -> ModuleName
envCurrentModule TCEnv
env
        m :: ModuleName
m       = ModuleName -> ModuleName
dropAnon (ModuleName -> ModuleName) -> ModuleName -> ModuleName
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 ([Name] -> ModuleName) -> [Name] -> ModuleName
forall a b. (a -> b) -> a -> b
$ (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName [Name]
ms

    -- Reducibility rule for opaque definitions: If we are operating
    -- under an unfolding block,
    clarify :: IsOpaque -> IsOpaque
clarify IsOpaque
def = case TCEnv -> Maybe OpaqueId
envCurrentOpaqueId TCEnv
env of
      Just OpaqueId
oid ->
        let
          block :: OpaqueBlock
block = OpaqueBlock -> Maybe OpaqueBlock -> OpaqueBlock
forall a. a -> Maybe a -> a
fromMaybe OpaqueBlock
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe OpaqueBlock -> OpaqueBlock)
-> Maybe OpaqueBlock -> OpaqueBlock
forall a b. (a -> b) -> a -> b
$ OpaqueId -> Map OpaqueId OpaqueBlock -> Maybe OpaqueBlock
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup OpaqueId
oid (Lens' TCState (Map OpaqueId OpaqueBlock)
-> TCState -> Map OpaqueId OpaqueBlock
forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
view (Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock))
-> TCState -> f TCState
Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks TCState
state)

          -- Then any name which is a member of the unfolding-set
          -- associated to that block will be unfolded.
          okay :: Bool
okay = Definition -> QName
defName Definition
defn QName -> HashSet QName -> Bool
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

    -- Short-circuit the map lookup for vanilla definitions
    plainDef :: Bool
plainDef = Definition -> IsAbstract
defAbstract Definition
defn IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef
            Bool -> Bool -> Bool
&& Definition -> IsOpaque
defOpaque   Definition
defn IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef

  in Bool
plainDef
  Bool -> Bool -> Bool
|| ( IsAbstract -> IsAbstract
concretise (Definition -> IsAbstract
defAbstract Definition
defn) IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef
    Bool -> Bool -> Bool
&& IsOpaque -> IsOpaque
clarify    (Definition -> IsOpaque
defOpaque Definition
defn)   IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef)

-- | Will the given 'QName' have a proper definition, or will it be
-- wrapped in an 'AbstractDefn'?
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 <- m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
  TCState
st <- m TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState
  m Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ do
    Definition
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qn
    Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ TCEnv -> TCState -> Definition -> Bool
isAccessibleDef TCEnv
env TCState
st Definition
def

type Invert = State (HashMap QName QName, HashMap QName (HashSet QName))

-- | Compute maps inverting the module applications defined in the given
-- declarations. The first returned map associates copied names to their
-- (hereditary) originals, the second map associates original names to
-- their (transitive) copies.
invertDefCopies
  :: [A.Declaration]
  -> ( HashMap QName QName
     , HashMap QName (HashSet QName)
     )
invertDefCopies :: [Declaration]
-> (HashMap QName QName, HashMap QName (HashSet QName))
invertDefCopies = (State (HashMap QName QName, HashMap QName (HashSet QName)) ()
 -> (HashMap QName QName, HashMap QName (HashSet QName))
 -> (HashMap QName QName, HashMap QName (HashSet QName)))
-> (HashMap QName QName, HashMap QName (HashSet QName))
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
-> (HashMap QName QName, HashMap QName (HashSet QName))
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (HashMap QName QName, HashMap QName (HashSet QName)) ()
-> (HashMap QName QName, HashMap QName (HashSet QName))
-> (HashMap QName QName, HashMap QName (HashSet QName))
forall s a. State s a -> s -> s
execState (HashMap QName QName, HashMap QName (HashSet QName))
forall a. Monoid a => a
mempty (State (HashMap QName QName, HashMap QName (HashSet QName)) ()
 -> (HashMap QName QName, HashMap QName (HashSet QName)))
-> ([Declaration]
    -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> [Declaration]
-> (HashMap QName QName, HashMap QName (HashSet QName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Declaration
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> [Declaration]
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Declaration
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
go where
  canon :: QName -> Invert QName
  canon :: QName -> Invert QName
canon QName
n = ((HashMap QName QName, HashMap QName (HashSet QName))
 -> Maybe QName)
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName))
     Identity
     (Maybe QName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (QName -> HashMap QName QName -> Maybe QName
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup QName
n (HashMap QName QName -> Maybe QName)
-> ((HashMap QName QName, HashMap QName (HashSet QName))
    -> HashMap QName QName)
-> (HashMap QName QName, HashMap QName (HashSet QName))
-> Maybe QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName QName, HashMap QName (HashSet QName))
-> HashMap QName QName
forall a b. (a, b) -> a
fst) StateT
  (HashMap QName QName, HashMap QName (HashSet QName))
  Identity
  (Maybe QName)
-> (Maybe QName -> Invert QName) -> Invert QName
forall a b.
StateT
  (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
-> (a
    -> StateT
         (HashMap QName QName, HashMap QName (HashSet QName)) Identity b)
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just QName
n' -> do
      QName
c <- QName -> Invert QName
canon QName
n'
      ((HashMap QName QName, HashMap QName (HashSet QName))
 -> (HashMap QName QName, HashMap QName (HashSet QName)))
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (((HashMap QName QName, HashMap QName (HashSet QName))
  -> (HashMap QName QName, HashMap QName (HashSet QName)))
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> ((HashMap QName QName, HashMap QName (HashSet QName))
    -> (HashMap QName QName, HashMap QName (HashSet QName)))
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a b. (a -> b) -> a -> b
$ \(HashMap QName QName
canon, HashMap QName (HashSet QName)
backrefs) -> (QName -> QName -> HashMap QName QName -> HashMap QName QName
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert QName
n QName
c HashMap QName QName
canon, HashMap QName (HashSet QName)
backrefs)
      QName -> Invert QName
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QName
c
    Maybe QName
Nothing -> QName -> Invert QName
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure QName
n

  copy :: QName -> QName -> Invert ()
  copy :: QName
-> QName
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
copy QName
from QName
to = do
    QName
from <- QName -> Invert QName
canon QName
from
    ((HashMap QName QName, HashMap QName (HashSet QName))
 -> (HashMap QName QName, HashMap QName (HashSet QName)))
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (((HashMap QName QName, HashMap QName (HashSet QName))
  -> (HashMap QName QName, HashMap QName (HashSet QName)))
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> ((HashMap QName QName, HashMap QName (HashSet QName))
    -> (HashMap QName QName, HashMap QName (HashSet QName)))
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a b. (a -> b) -> a -> b
$ \(HashMap QName QName
canon, HashMap QName (HashSet QName)
backrefs) ->
      ( QName -> QName -> HashMap QName QName -> HashMap QName QName
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert QName
to QName
from HashMap QName QName
canon
      , (Maybe (HashSet QName) -> Maybe (HashSet QName))
-> QName
-> HashMap QName (HashSet QName)
-> HashMap QName (HashSet QName)
forall k v.
(Eq k, Hashable k) =>
(Maybe v -> Maybe v) -> k -> HashMap k v -> HashMap k v
HashMap.alter (HashSet QName -> Maybe (HashSet QName)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HashSet QName -> Maybe (HashSet QName))
-> (Maybe (HashSet QName) -> HashSet QName)
-> Maybe (HashSet QName)
-> Maybe (HashSet QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> HashSet QName -> HashSet QName
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert QName
to (HashSet QName -> HashSet QName)
-> (Maybe (HashSet QName) -> HashSet QName)
-> Maybe (HashSet QName)
-> HashSet QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (HashSet QName) -> HashSet QName
forall m. Monoid m => Maybe m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold) QName
from HashMap QName (HashSet QName)
backrefs
      )

  go :: A.Declaration -> Invert ()
  -- Interesting case:
  go :: Declaration
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
go (A.Apply ModuleInfo
_mi Erased
_e ModuleName
_mn ModuleApplication
_app ScopeCopyInfo
info ImportDirective
_imp) =
    [(QName, List1 QName)]
-> ((QName, List1 QName)
    -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map QName (List1 QName) -> [(QName, List1 QName)]
forall k a. Map k a -> [(k, a)]
Map.toList (ScopeCopyInfo -> Map QName (List1 QName)
A.renNames ScopeCopyInfo
info)) (((QName, List1 QName)
  -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> ((QName, List1 QName)
    -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a b. (a -> b) -> a -> b
$ \(QName
from, List1 QName
tos) -> (QName
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> List1 QName
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (QName
-> QName
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
copy QName
from) List1 QName
tos

  -- Traversal:
  go (A.Mutual MutualInfo
_ [Declaration]
ds)                       = (Declaration
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> [Declaration]
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Declaration
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
go [Declaration]
ds
  go (A.Section Range
_r Erased
_e ModuleName
_mn GeneralizeTelescope
_gt [Declaration]
ds)          = (Declaration
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> [Declaration]
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Declaration
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
go [Declaration]
ds
  go (A.ScopedDecl ScopeInfo
_si [Declaration]
ds)                 = (Declaration
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> [Declaration]
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Declaration
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
go [Declaration]
ds
  go (A.RecDef DefInfo
_di QName
_qn UniverseCheck
_uc RecordDirectives
_rd DataDefParams
_ddp Type
_t [Declaration]
ds) = (Declaration
 -> State (HashMap QName QName, HashMap QName (HashSet QName)) ())
-> [Declaration]
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Declaration
-> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
go [Declaration]
ds

  -- Boring:
  go A.Axiom{}         = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.Generalize{}    = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.Field{}         = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.Primitive{}     = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.Import{}        = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.Pragma{}        = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.Open{}          = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.FunDef{}        = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.DataSig{}       = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.DataDef{}       = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.RecSig{}        = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.PatternSynDef{} = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.UnquoteDecl{}   = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.UnquoteDef{}    = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.UnquoteData{}   = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  go A.UnfoldingDecl{} = () -> State (HashMap QName QName, HashMap QName (HashSet QName)) ()
forall a.
a
-> StateT
     (HashMap QName QName, HashMap QName (HashSet QName)) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()