{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.DeadCode (eliminateDeadCode) where

import Control.Monad ((<$!>))
import Control.Monad.Trans

import Data.Maybe
import Data.Monoid (All(..))
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Map.Strict as MapS
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap

import Agda.Interaction.Options

import qualified Agda.Syntax.Abstract as A

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Names
import Agda.Syntax.Scope.Base

import qualified Agda.Benchmarking as Bench
import qualified Agda.TypeChecking.Monad.Benchmark as Bench

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce

import Agda.Utils.Impossible
import Agda.Utils.Lens

import Agda.Utils.HashTable (HashTable)
import qualified Agda.Utils.HashTable as HT

-- | Run before serialisation to remove any definitions and
-- meta-variables that are not reachable from the module's public
-- interface.
--
-- Things that are reachable only from warnings are removed.

eliminateDeadCode ::
     Map ModuleName a
       -- ^ Exported modules whose telescopes should not be mutilated by the dead-code removal.
  -> BuiltinThings PrimFun
  -> DisplayForms
  -> Signature
  -> LocalMetaStore
  -> TCM (DisplayForms, Signature, RemoteMetaStore)
eliminateDeadCode :: forall a.
Map ModuleName a
-> BuiltinThings PrimFun
-> DisplayForms
-> Signature
-> LocalMetaStore
-> TCM (DisplayForms, Signature, RemoteMetaStore)
eliminateDeadCode Map ModuleName a
publicModules BuiltinThings PrimFun
bs DisplayForms
disp Signature
sig LocalMetaStore
ms = Account (BenchPhase (TCMT IO))
-> TCM (DisplayForms, Signature, RemoteMetaStore)
-> TCM (DisplayForms, Signature, RemoteMetaStore)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.DeadCode] (TCM (DisplayForms, Signature, RemoteMetaStore)
 -> TCM (DisplayForms, Signature, RemoteMetaStore))
-> TCM (DisplayForms, Signature, RemoteMetaStore)
-> TCM (DisplayForms, Signature, RemoteMetaStore)
forall a b. (a -> b) -> a -> b
$ do
  !PatternSynDefns
patsyn <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
  !Set QName
public <- (AbstractName -> QName) -> Set AbstractName -> Set QName
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic AbstractName -> QName
anameName (Set AbstractName -> Set QName)
-> (ScopeInfo -> Set AbstractName) -> ScopeInfo -> Set QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> Set AbstractName
publicNames (ScopeInfo -> Set QName)
-> TCMT IO ScopeInfo -> TCMT IO (Set QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  !Bool
save   <- PragmaOptions -> Bool
optSaveMetas (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  !HashMap QName Definition
defs   <- if Bool
save then HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Signature
sig Signature
-> Lens' Signature (HashMap QName Definition)
-> HashMap QName Definition
forall o i. o -> Lens' o i -> i
^. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions)
                     else Account (BenchPhase (TCMT IO))
-> TCMT IO (HashMap QName Definition)
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.DeadCode, BenchPhase (TCMT IO)
Phase
Bench.DeadCodeInstantiateFull]
                          ((Definition -> TCMT IO Definition)
-> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> HashMap QName a -> f (HashMap QName b)
traverse (\Definition
x -> Definition -> TCMT IO Definition
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Definition
x) (Signature
sig Signature
-> Lens' Signature (HashMap QName Definition)
-> HashMap QName Definition
forall o i. o -> Lens' o i -> i
^. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions))

  -- #2921: Eliminating definitions with attached COMPILE pragmas results in
  -- the pragmas not being checked. Simple solution: don't eliminate these.
  -- #6022 (Andreas, 2022-09-30): Eliminating cubical primitives can lead to crashes.
   -- Simple solution: retain all primitives (shouldn't be many).
  let hasCompilePragma :: Definition -> Bool
hasCompilePragma = Bool -> Bool
not (Bool -> Bool) -> (Definition -> Bool) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map [Char] [CompilerPragma] -> Bool
forall k a. Map k a -> Bool
MapS.null (Map [Char] [CompilerPragma] -> Bool)
-> (Definition -> Map [Char] [CompilerPragma])
-> Definition
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Map [Char] [CompilerPragma]
defCompiledRep
      isPrimitive :: Defn -> Bool
isPrimitive = \case
        Primitive{}     -> Bool
True
        PrimitiveSort{} -> Bool
True
        Defn
_ -> Bool
False
      extraRootsFilter :: (a, Definition) -> Maybe a
extraRootsFilter (a
name, Definition
def)
        | Definition -> Bool
hasCompilePragma Definition
def Bool -> Bool -> Bool
|| Defn -> Bool
isPrimitive (Definition -> Defn
theDef Definition
def) = a -> Maybe a
forall a. a -> Maybe a
Just a
name
        | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing
      extraRoots :: Set QName
extraRoots =
        [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList ([QName] -> Set QName) -> [QName] -> Set QName
forall a b. (a -> b) -> a -> b
$ ((QName, Definition) -> Maybe QName)
-> [(QName, Definition)] -> [QName]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (QName, Definition) -> Maybe QName
forall {a}. (a, Definition) -> Maybe a
extraRootsFilter ([(QName, Definition)] -> [QName])
-> [(QName, Definition)] -> [QName]
forall a b. (a -> b) -> a -> b
$ HashMap QName Definition -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList HashMap QName Definition
defs

      rootSections :: [Section]
rootSections = Sections -> [Section]
forall k a. Map k a -> [a]
Map.elems (Sections -> [Section]) -> Sections -> [Section]
forall a b. (a -> b) -> a -> b
$ (Signature
sig Signature -> Lens' Signature Sections -> Sections
forall o i. o -> Lens' o i -> i
^. (Sections -> f Sections) -> Signature -> f Signature
Lens' Signature Sections
sigSections) Sections -> Map ModuleName a -> Sections
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.intersection` Map ModuleName a
publicModules
      rootNames :: Set QName
rootNames = Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
public Set QName
extraRoots
      rootMetas :: Set MetaId
rootMetas =
        if Bool -> Bool
not Bool
save then Set MetaId
forall a. Set a
Set.empty else (BuiltinThings PrimFun, Sections, RewriteRuleMap, DisplayForms)
-> Set MetaId
forall a m. (NamesIn a, Collection MetaId m) => a -> m
metasIn
          ( BuiltinThings PrimFun
bs
          , Signature
sig Signature -> Lens' Signature Sections -> Sections
forall o i. o -> Lens' o i -> i
^. (Sections -> f Sections) -> Signature -> f Signature
Lens' Signature Sections
sigSections
          , Signature
sig Signature -> Lens' Signature RewriteRuleMap -> RewriteRuleMap
forall o i. o -> Lens' o i -> i
^. (RewriteRuleMap -> f RewriteRuleMap) -> Signature -> f Signature
Lens' Signature RewriteRuleMap
sigRewriteRules
          , (QName -> [LocalDisplayForm] -> Bool)
-> DisplayForms -> DisplayForms
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\QName
x [LocalDisplayForm]
_ -> QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
rootNames) DisplayForms
disp
          )

  (!Set QName
rns, !Set MetaId
rms) <- Account (BenchPhase (TCMT IO))
-> TCMT IO (Set QName, Set MetaId)
-> TCMT IO (Set QName, Set MetaId)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.DeadCode, BenchPhase (TCMT IO)
Phase
Bench.DeadCodeReachable] (TCMT IO (Set QName, Set MetaId)
 -> TCMT IO (Set QName, Set MetaId))
-> TCMT IO (Set QName, Set MetaId)
-> TCMT IO (Set QName, Set MetaId)
forall a b. (a -> b) -> a -> b
$ IO (Set QName, Set MetaId) -> TCMT IO (Set QName, Set MetaId)
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Set QName, Set MetaId) -> TCMT IO (Set QName, Set MetaId))
-> IO (Set QName, Set MetaId) -> TCMT IO (Set QName, Set MetaId)
forall a b. (a -> b) -> a -> b
$
                    [Section]
-> Set QName
-> Set MetaId
-> PatternSynDefns
-> DisplayForms
-> HashMap QName Definition
-> LocalMetaStore
-> IO (Set QName, Set MetaId)
reachableFrom [Section]
rootSections Set QName
rootNames Set MetaId
rootMetas PatternSynDefns
patsyn DisplayForms
disp HashMap QName Definition
defs LocalMetaStore
ms

  let !dead :: Set QName
dead  = [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList (HashMap QName Definition -> [QName]
forall k v. HashMap k v -> [k]
HMap.keys HashMap QName Definition
defs) Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set QName
rns
      !valid :: LocalDisplayForm -> Bool
valid = All -> Bool
getAll (All -> Bool)
-> (LocalDisplayForm -> All) -> LocalDisplayForm -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> All) -> LocalDisplayForm -> All
forall a m. (NamesIn a, Monoid m) => (QName -> m) -> a -> m
namesIn' (Bool -> All
All (Bool -> All) -> (QName -> Bool) -> QName -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set QName
dead))  -- no used name is dead
      !defs' :: HashMap QName Definition
defs' = (Definition -> Definition)
-> HashMap QName Definition -> HashMap QName Definition
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ( \ Definition
d -> Definition
d { defDisplay = filter valid (defDisplay d) } )
               (HashMap QName Definition -> HashMap QName Definition)
-> HashMap QName Definition -> HashMap QName Definition
forall a b. (a -> b) -> a -> b
$ (QName -> Definition -> Bool)
-> HashMap QName Definition -> HashMap QName Definition
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HMap.filterWithKey (\ QName
x Definition
_ -> QName -> Set QName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member QName
x Set QName
rns) HashMap QName Definition
defs
      !disp' :: DisplayForms
disp' = ([LocalDisplayForm] -> Bool) -> DisplayForms -> DisplayForms
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool)
-> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LocalDisplayForm] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (DisplayForms -> DisplayForms) -> DisplayForms -> DisplayForms
forall a b. (a -> b) -> a -> b
$ ([LocalDisplayForm] -> [LocalDisplayForm])
-> DisplayForms -> DisplayForms
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ((LocalDisplayForm -> Bool)
-> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
valid) DisplayForms
disp
      !ms' :: RemoteMetaStore
ms'   = [(MetaId, RemoteMetaVariable)] -> RemoteMetaStore
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(MetaId, RemoteMetaVariable)] -> RemoteMetaStore)
-> [(MetaId, RemoteMetaVariable)] -> RemoteMetaStore
forall a b. (a -> b) -> a -> b
$
                ((MetaId, MetaVariable) -> Maybe (MetaId, RemoteMetaVariable))
-> [(MetaId, MetaVariable)] -> [(MetaId, RemoteMetaVariable)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
                  (\(MetaId
m, MetaVariable
mv) ->
                    if Bool -> Bool
not (MetaId -> Set MetaId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member MetaId
m Set MetaId
rms)
                    then Maybe (MetaId, RemoteMetaVariable)
forall a. Maybe a
Nothing
                    else (MetaId, RemoteMetaVariable) -> Maybe (MetaId, RemoteMetaVariable)
forall a. a -> Maybe a
Just (MetaId
m, MetaVariable -> RemoteMetaVariable
remoteMetaVariable MetaVariable
mv)) ([(MetaId, MetaVariable)] -> [(MetaId, RemoteMetaVariable)])
-> [(MetaId, MetaVariable)] -> [(MetaId, RemoteMetaVariable)]
forall a b. (a -> b) -> a -> b
$
                LocalMetaStore -> [(MetaId, MetaVariable)]
forall k a. Map k a -> [(k, a)]
MapS.toList LocalMetaStore
ms

  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.dead" Int
10 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"Removed " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (HashMap QName Definition -> Int
forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs Int -> Int -> Int
forall a. Num a => a -> a -> a
- HashMap QName Definition -> Int
forall k v. HashMap k v -> Int
HMap.size HashMap QName Definition
defs') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
" unused definitions and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (LocalMetaStore -> Int
forall k a. Map k a -> Int
MapS.size LocalMetaStore
ms Int -> Int -> Int
forall a. Num a => a -> a -> a
- RemoteMetaStore -> Int
forall k v. HashMap k v -> Int
HMap.size RemoteMetaStore
ms') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
" unused meta-variables."
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.dead" Int
90 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    [Char]
"Removed the following definitions from the signature:" [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
:
    (QName -> [Char]) -> [QName] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"- " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> (QName -> [Char]) -> QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) (Set QName -> [QName]
forall a. Set a -> [a]
Set.toList Set QName
dead)
  let !sig' :: Signature
sig' = Lens' Signature (HashMap QName Definition)
-> LensSet Signature (HashMap QName Definition)
forall o i. Lens' o i -> LensSet o i
set (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' Signature (HashMap QName Definition)
sigDefinitions HashMap QName Definition
defs' Signature
sig
  (DisplayForms, Signature, RemoteMetaStore)
-> TCM (DisplayForms, Signature, RemoteMetaStore)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (DisplayForms
disp', Signature
sig', RemoteMetaStore
ms')

reachableFrom ::
     [Section]      -- ^ Root modules.
  -> Set QName      -- ^ Root names.
  -> Set MetaId     -- ^ Root metas.
  -> A.PatternSynDefns
  -> DisplayForms
  -> Definitions
  -> LocalMetaStore
  -> IO (Set QName, Set MetaId)
reachableFrom :: [Section]
-> Set QName
-> Set MetaId
-> PatternSynDefns
-> DisplayForms
-> HashMap QName Definition
-> LocalMetaStore
-> IO (Set QName, Set MetaId)
reachableFrom [Section]
sections Set QName
ids Set MetaId
ms PatternSynDefns
psyns DisplayForms
disp HashMap QName Definition
defs LocalMetaStore
insts = do

  !HashTable QName ()
seenNames <- IO (HashTable QName ())
forall k v. IO (HashTable k v)
HT.empty :: IO (HashTable QName ())
  !HashTable MetaId ()
seenMetas <- IO (HashTable MetaId ())
forall k v. IO (HashTable k v)
HT.empty :: IO (HashTable MetaId ())

  let goName :: QName -> IO ()
      goName :: QName -> IO ()
goName !QName
x = HashTable QName () -> QName -> IO (Maybe ())
forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
HT.lookup HashTable QName ()
seenNames QName
x IO (Maybe ()) -> (Maybe () -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just ()
_ ->
          () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Maybe ()
Nothing -> do
          HashTable QName () -> QName -> () -> IO ()
forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
HT.insert HashTable QName ()
seenNames QName
x ()
          Maybe Definition -> IO ()
forall a. NamesIn a => a -> IO ()
go (QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x HashMap QName Definition
defs)
          Maybe PSyn -> IO ()
forall a. NamesIn a => a -> IO ()
go (PatternSynDefn -> PSyn
PSyn (PatternSynDefn -> PSyn) -> Maybe PatternSynDefn -> Maybe PSyn
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> QName -> PatternSynDefns -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup QName
x PatternSynDefns
psyns)
          Maybe [LocalDisplayForm] -> IO ()
forall a. NamesIn a => a -> IO ()
go (QName -> DisplayForms -> Maybe [LocalDisplayForm]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
x DisplayForms
disp)

      goMeta :: MetaId -> IO ()
      goMeta :: MetaId -> IO ()
goMeta !MetaId
m = HashTable MetaId () -> MetaId -> IO (Maybe ())
forall k v.
(Eq k, Hashable k) =>
HashTable k v -> k -> IO (Maybe v)
HT.lookup HashTable MetaId ()
seenMetas MetaId
m IO (Maybe ()) -> (Maybe () -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just ()
_ ->
          () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Maybe ()
Nothing -> do
          HashTable MetaId () -> MetaId -> () -> IO ()
forall k v. (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
HT.insert HashTable MetaId ()
seenMetas MetaId
m ()
          case MetaId -> LocalMetaStore -> Maybe MetaVariable
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup MetaId
m LocalMetaStore
insts of
            Maybe MetaVariable
Nothing -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Just MetaVariable
mv -> Term -> IO ()
forall a. NamesIn a => a -> IO ()
go (Instantiation -> Term
instBody (MetaVariable -> Instantiation
theInstantiation MetaVariable
mv))

      go :: NamesIn a => a -> IO ()
      go :: forall a. NamesIn a => a -> IO ()
go = (Either QName MetaId -> IO ()) -> a -> IO ()
forall m. Monoid m => (Either QName MetaId -> m) -> a -> m
forall a m.
(NamesIn a, Monoid m) =>
(Either QName MetaId -> m) -> a -> m
namesAndMetasIn' ((QName -> IO ())
-> (MetaId -> IO ()) -> Either QName MetaId -> IO ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either QName -> IO ()
goName MetaId -> IO ()
goMeta)
      {-# INLINE go #-}

  [Section] -> IO ()
forall a. NamesIn a => a -> IO ()
go [Section]
sections
  (QName -> IO ()) -> Set QName -> IO ()
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap QName -> IO ()
goName Set QName
ids
  (MetaId -> IO ()) -> Set MetaId -> IO ()
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap MetaId -> IO ()
goMeta Set MetaId
ms
  !Set QName
ids' <- HashTable QName () -> IO (Set QName)
forall k v. Ord k => HashTable k v -> IO (Set k)
HT.keySet HashTable QName ()
seenNames
  !Set MetaId
ms'  <- HashTable MetaId () -> IO (Set MetaId)
forall k v. Ord k => HashTable k v -> IO (Set k)
HT.keySet HashTable MetaId ()
seenMetas
  (Set QName, Set MetaId) -> IO (Set QName, Set MetaId)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set QName
ids', Set MetaId
ms')


-- | Returns the instantiation.
--
-- Precondition: The instantiation must be of the form @'InstV' inst@.

theInstantiation :: MetaVariable -> Instantiation
theInstantiation :: MetaVariable -> Instantiation
theInstantiation MetaVariable
mv = case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
  InstV Instantiation
inst                     -> Instantiation
inst
  Open{}                         -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
  OpenInstance{}                 -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
  BlockedConst{}                 -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__
  PostponedTypeCheckingProblem{} -> Instantiation
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Converts from 'MetaVariable' to 'RemoteMetaVariable'.
--
-- Precondition: The instantiation must be of the form @'InstV' inst@.

remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
remoteMetaVariable :: MetaVariable -> RemoteMetaVariable
remoteMetaVariable MetaVariable
mv = RemoteMetaVariable
  { rmvInstantiation :: Instantiation
rmvInstantiation = MetaVariable -> Instantiation
theInstantiation MetaVariable
mv
  , rmvModality :: Modality
rmvModality      = MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality MetaVariable
mv
  , rmvJudgement :: Judgement MetaId
rmvJudgement     = MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
  }