    {-# 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)
      => m ()
    saturateOpaqueBlocks :: forall (m :: * -> *).
    (MonadTCState m, ReadTCState m, MonadFresh OpaqueId m,
     MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m) =>
    m ()
    saturateOpaqueBlocks = m ()
    entry where
      entry :: m ()
    entry = do
        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
        inverse <- useTC stOpaqueIds
        OpaqueId _ ourmod <- fresh

        canonical <- useTC stCopiedNames
        backcopies <- useTC stNameCopies

        reportSDoc "tc.opaque.copy" 45 $ "Canonical names of copied definitions:" $+$ pretty (HashMap.toList canonical)
        reportSDoc "tc.opaque.copy" 45 $ "Backcopies:" $+$ pretty (HashMap.toList (toList <$> backcopies))

        let
          isOurs (OpaqueId Word64
    _ ModuleNameHash
    mod, OpaqueBlock
    _) = ModuleNameHash
    mod ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleNameHash
    ourmod
          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)
          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)

        () <- liftIO $ evaluate (rnf (canonical, backcopies))

        reportSDoc "tc.opaque" 30 $ vcat $
          text "Opaque blocks defined in this module:":map pretty 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.
        (blocks, names) <- computeClosure canonise known inverse 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' = ((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)

        reportSDoc "tc.opaque.sat" 30 $ vcat $
          text "Saturated local opaque blocks":[ pretty block | b@(_,block) <- Map.toList blocks, isOurs b ]

        reportSDoc "tc.opaque.sat.full" 50 $ text "Saturated opaque blocks:" $+$ pretty blocks

        modifyTC' $ \TCState
    st -> TCState
    st { stPostScopeState = (stPostScopeState st)
          { stPostOpaqueBlocks = blocks
          , stPostOpaqueIds    = names'
          } }

      -- Actually compute the closure.
      computeClosure
        :: (QName -> QName)
        -> 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 :: (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 [] = (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 QName -> QName
    canonise 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
            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
            block <- Map.lookup id blocks
            pure . pure $ HashSet.union (opaqueUnfolding block) 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.
        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 { 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' = (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)

        computeClosure canonise (Map.insert (opaqueId block) block' blocks) names' 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 <- 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
      env <- m TCEnv
    forall (m :: * -> *). MonadTCEnv m => m TCEnv
    askTC
      st <- getTCState
      ignoreAbstractMode $ do
        def <- getConstInfo qn
        pure $ isAccessibleDef env st def