    -- |
    -- Module      :  Cryptol.ModuleSystem.Interface
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE Safe #-}
    module Cryptol.ModuleSystem.Interface (
        Iface
      , IfaceG(..)
      , IfaceDecls(..)
      , IfaceDecl(..)
      , IfaceNames(..)
      , ifModName

      , emptyIface
      , ifacePrimMap
      , ifaceForgetName
      , ifaceIsFunctor
      , filterIfaceDecls
      , ifaceDeclsNames
      , ifaceOrigNameMap
      ) where

    import           Data.Set(Set)
    import qualified Data.Set as Set
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import           Data.Semigroup
    import           Data.Text (Text)

    import GHC.Generics (Generic)
    import Control.DeepSeq

    import Prelude ()
    import Prelude.Compat

    import Cryptol.ModuleSystem.Name
    import Cryptol.Utils.Ident (ModName, OrigName(..))
    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.Fixity(Fixity)
    import Cryptol.Parser.AST(Pragma)
    import Cryptol.TypeCheck.Type

    type Iface = IfaceG ModName

    -- | The interface repersenting a typecheck top-level module.
    data IfaceG name = Iface
      { forall name. IfaceG name -> IfaceNames name
    ifNames     :: IfaceNames name    -- ^ Info about names in this module
      , forall name. IfaceG name -> FunctorParams
    ifParams    :: FunctorParams      -- ^ Module parameters, if any
      , forall name. IfaceG name -> IfaceDecls
    ifDefines   :: IfaceDecls         -- ^ All things defines in the module
                                          -- (includes nested definitions)
      } deriving (Int -> IfaceG name -> ShowS
    [IfaceG name] -> ShowS
    IfaceG name -> String
    (Int -> IfaceG name -> ShowS)
    -> (IfaceG name -> String)
    -> ([IfaceG name] -> ShowS)
    -> Show (IfaceG name)
    forall name. Show name => Int -> IfaceG name -> ShowS
    forall name. Show name => [IfaceG name] -> ShowS
    forall name. Show name => IfaceG name -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall name. Show name => Int -> IfaceG name -> ShowS
    showsPrec :: Int -> IfaceG name -> ShowS
    $cshow :: forall name. Show name => IfaceG name -> String
    show :: IfaceG name -> String
    $cshowList :: forall name. Show name => [IfaceG name] -> ShowS
    showList :: [IfaceG name] -> ShowS
    Show, (forall x. IfaceG name -> Rep (IfaceG name) x)
    -> (forall x. Rep (IfaceG name) x -> IfaceG name)
    -> Generic (IfaceG name)
    forall x. Rep (IfaceG name) x -> IfaceG name
    forall x. IfaceG name -> Rep (IfaceG name) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall name x. Rep (IfaceG name) x -> IfaceG name
    forall name x. IfaceG name -> Rep (IfaceG name) x
    $cfrom :: forall name x. IfaceG name -> Rep (IfaceG name) x
    from :: forall x. IfaceG name -> Rep (IfaceG name) x
    $cto :: forall name x. Rep (IfaceG name) x -> IfaceG name
    to :: forall x. Rep (IfaceG name) x -> IfaceG name
    Generic, IfaceG name -> ()
    (IfaceG name -> ()) -> NFData (IfaceG name)
    forall name. NFData name => IfaceG name -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall name. NFData name => IfaceG name -> ()
    rnf :: IfaceG name -> ()
    NFData)

    -- | Remove the name of a module.  This is useful for dealing with collections
    -- of modules, as in `Map (ImpName Name) (IfaceG ())`.
    ifaceForgetName :: IfaceG name -> IfaceG ()
    ifaceForgetName :: forall name. IfaceG name -> IfaceG ()
    ifaceForgetName IfaceG name
    i = IfaceG name
    i { ifNames :: IfaceNames ()
    ifNames = IfaceNames ()
    newNames }
      where newNames :: IfaceNames ()
    newNames = (IfaceG name -> IfaceNames name
    forall name. IfaceG name -> IfaceNames name
    ifNames IfaceG name
    i) { ifsName :: ()
    ifsName = () }

    -- | Access the name of a module.
    ifModName :: IfaceG name -> name
    ifModName :: forall name. IfaceG name -> name
    ifModName = IfaceNames name -> name
    forall name. IfaceNames name -> name
    ifsName (IfaceNames name -> name)
    -> (IfaceG name -> IfaceNames name) -> IfaceG name -> name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IfaceG name -> IfaceNames name
    forall name. IfaceG name -> IfaceNames name
    ifNames

    -- | Information about the names in a module.
    data IfaceNames name = IfaceNames
      { forall name. IfaceNames name -> name
    ifsName     :: name       -- ^ Name of this submodule
      , forall name. IfaceNames name -> Set Name
    ifsNested   :: Set Name   -- ^ Things nested in this module
      , forall name. IfaceNames name -> Set Name
    ifsDefines  :: Set Name   -- ^ Things defined in this module
      , forall name. IfaceNames name -> Set Name
    ifsPublic   :: Set Name   -- ^ Subset of `ifsDefines` that is public
      , forall name. IfaceNames name -> Maybe Text
    ifsDoc      :: !(Maybe Text) -- ^ Documentation
      } deriving (Int -> IfaceNames name -> ShowS
    [IfaceNames name] -> ShowS
    IfaceNames name -> String
    (Int -> IfaceNames name -> ShowS)
    -> (IfaceNames name -> String)
    -> ([IfaceNames name] -> ShowS)
    -> Show (IfaceNames name)
    forall name. Show name => Int -> IfaceNames name -> ShowS
    forall name. Show name => [IfaceNames name] -> ShowS
    forall name. Show name => IfaceNames name -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall name. Show name => Int -> IfaceNames name -> ShowS
    showsPrec :: Int -> IfaceNames name -> ShowS
    $cshow :: forall name. Show name => IfaceNames name -> String
    show :: IfaceNames name -> String
    $cshowList :: forall name. Show name => [IfaceNames name] -> ShowS
    showList :: [IfaceNames name] -> ShowS
    Show, (forall x. IfaceNames name -> Rep (IfaceNames name) x)
    -> (forall x. Rep (IfaceNames name) x -> IfaceNames name)
    -> Generic (IfaceNames name)
    forall x. Rep (IfaceNames name) x -> IfaceNames name
    forall x. IfaceNames name -> Rep (IfaceNames name) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall name x. Rep (IfaceNames name) x -> IfaceNames name
    forall name x. IfaceNames name -> Rep (IfaceNames name) x
    $cfrom :: forall name x. IfaceNames name -> Rep (IfaceNames name) x
    from :: forall x. IfaceNames name -> Rep (IfaceNames name) x
    $cto :: forall name x. Rep (IfaceNames name) x -> IfaceNames name
    to :: forall x. Rep (IfaceNames name) x -> IfaceNames name
    Generic, IfaceNames name -> ()
    (IfaceNames name -> ()) -> NFData (IfaceNames name)
    forall name. NFData name => IfaceNames name -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall name. NFData name => IfaceNames name -> ()
    rnf :: IfaceNames name -> ()
    NFData)

    -- | Is this interface for a functor.
    ifaceIsFunctor :: IfaceG name -> Bool
    ifaceIsFunctor :: forall name. IfaceG name -> Bool
    ifaceIsFunctor = Bool -> Bool
    not (Bool -> Bool) -> (IfaceG name -> Bool) -> IfaceG name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FunctorParams -> Bool
    forall k a. Map k a -> Bool
    Map.null (FunctorParams -> Bool)
    -> (IfaceG name -> FunctorParams) -> IfaceG name -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IfaceG name -> FunctorParams
    forall name. IfaceG name -> FunctorParams
    ifParams

    emptyIface :: ModName -> Iface
    emptyIface :: ModName -> Iface
    emptyIface ModName
    nm = Iface
      { ifNames :: IfaceNames ModName
    ifNames   = IfaceNames { ifsName :: ModName
    ifsName    = ModName
    nm
                               , ifsDefines :: Set Name
    ifsDefines = Set Name
    forall a. Monoid a => a
    mempty
                               , ifsPublic :: Set Name
    ifsPublic  = Set Name
    forall a. Monoid a => a
    mempty
                               , ifsNested :: Set Name
    ifsNested  = Set Name
    forall a. Monoid a => a
    mempty
                               , ifsDoc :: Maybe Text
    ifsDoc     = Maybe Text
    forall a. Maybe a
    Nothing
                               }
      , ifParams :: FunctorParams
    ifParams  = FunctorParams
    forall a. Monoid a => a
    mempty
      , ifDefines :: IfaceDecls
    ifDefines = IfaceDecls
    forall a. Monoid a => a
    mempty
      }

    -- | Declarations in a module.  Note that this includes things from nested
    -- modules, but not things from nested functors, which are in `ifFunctors`.
    data IfaceDecls = IfaceDecls
      { IfaceDecls -> Map Name TySyn
    ifTySyns        :: Map.Map Name TySyn
      , IfaceDecls -> Map Name Newtype
    ifNewtypes      :: Map.Map Name Newtype
      , IfaceDecls -> Map Name AbstractType
    ifAbstractTypes :: Map.Map Name AbstractType
      , IfaceDecls -> Map Name IfaceDecl
    ifDecls         :: Map.Map Name IfaceDecl
      , IfaceDecls -> Map Name (IfaceNames Name)
    ifModules       :: !(Map.Map Name (IfaceNames Name))
      , IfaceDecls -> Map Name ModParamNames
    ifSignatures    :: !(Map.Map Name ModParamNames)
      , IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors      :: !(Map.Map Name (IfaceG Name))
        {- ^ XXX: Maybe arg info?
        Also, with the current implementation we aim to complete remove functors
        by essentially inlining them.  To achieve this with just interfaces
        we'd have to store here the entire module, not just its interface.
        At the moment we work around this by passing all loaded modules to the
        type checker, so it looks up functors there, instead of in the interfaces,
        but we'd need to change this if we want better support for separate
        compilation. -}

      } deriving (Int -> IfaceDecls -> ShowS
    [IfaceDecls] -> ShowS
    IfaceDecls -> String
    (Int -> IfaceDecls -> ShowS)
    -> (IfaceDecls -> String)
    -> ([IfaceDecls] -> ShowS)
    -> Show IfaceDecls
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IfaceDecls -> ShowS
    showsPrec :: Int -> IfaceDecls -> ShowS
    $cshow :: IfaceDecls -> String
    show :: IfaceDecls -> String
    $cshowList :: [IfaceDecls] -> ShowS
    showList :: [IfaceDecls] -> ShowS
    Show, (forall x. IfaceDecls -> Rep IfaceDecls x)
    -> (forall x. Rep IfaceDecls x -> IfaceDecls) -> Generic IfaceDecls
    forall x. Rep IfaceDecls x -> IfaceDecls
    forall x. IfaceDecls -> Rep IfaceDecls x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. IfaceDecls -> Rep IfaceDecls x
    from :: forall x. IfaceDecls -> Rep IfaceDecls x
    $cto :: forall x. Rep IfaceDecls x -> IfaceDecls
    to :: forall x. Rep IfaceDecls x -> IfaceDecls
    Generic, IfaceDecls -> ()
    (IfaceDecls -> ()) -> NFData IfaceDecls
    forall a. (a -> ()) -> NFData a
    $crnf :: IfaceDecls -> ()
    rnf :: IfaceDecls -> ()
    NFData)

    filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
    filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
    filterIfaceDecls Name -> Bool
    p IfaceDecls
    ifs = IfaceDecls
      { ifTySyns :: Map Name TySyn
    ifTySyns        = Map Name TySyn -> Map Name TySyn
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name TySyn
    ifTySyns IfaceDecls
    ifs)
      , ifNewtypes :: Map Name Newtype
    ifNewtypes      = Map Name Newtype -> Map Name Newtype
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    ifs)
      , ifAbstractTypes :: Map Name AbstractType
    ifAbstractTypes = Map Name AbstractType -> Map Name AbstractType
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name AbstractType
    ifAbstractTypes IfaceDecls
    ifs)
      , ifDecls :: Map Name IfaceDecl
    ifDecls         = Map Name IfaceDecl -> Map Name IfaceDecl
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name IfaceDecl
    ifDecls IfaceDecls
    ifs)
      , ifModules :: Map Name (IfaceNames Name)
    ifModules       = Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name (IfaceNames Name)
    ifModules IfaceDecls
    ifs)
      , ifFunctors :: Map Name (IfaceG Name)
    ifFunctors      = Map Name (IfaceG Name) -> Map Name (IfaceG Name)
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors IfaceDecls
    ifs)
      , ifSignatures :: Map Name ModParamNames
    ifSignatures    = Map Name ModParamNames -> Map Name ModParamNames
    forall a. Map Name a -> Map Name a
    filterMap (IfaceDecls -> Map Name ModParamNames
    ifSignatures IfaceDecls
    ifs)
      }
      where
      filterMap :: Map.Map Name a -> Map.Map Name a
      filterMap :: forall a. Map Name a -> Map Name a
    filterMap = (Name -> a -> Bool) -> Map Name a -> Map Name a
    forall k a. (k -> a -> Bool) -> Map k a -> Map k a
    Map.filterWithKey (\Name
    k a
    _ -> Name -> Bool
    p Name
    k)

    ifaceDeclsNames :: IfaceDecls -> Set Name
    ifaceDeclsNames :: IfaceDecls -> Set Name
    ifaceDeclsNames IfaceDecls
    i = [Set Name] -> Set Name
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [ Map Name TySyn -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name TySyn
    ifTySyns IfaceDecls
    i)
                                   , Map Name Newtype -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    i)
                                   , Map Name AbstractType -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name AbstractType
    ifAbstractTypes IfaceDecls
    i)
                                   , Map Name IfaceDecl -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name IfaceDecl
    ifDecls IfaceDecls
    i)
                                   , Map Name (IfaceNames Name) -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name (IfaceNames Name)
    ifModules IfaceDecls
    i)
                                   , Map Name (IfaceG Name) -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors IfaceDecls
    i)
                                   , Map Name ModParamNames -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map Name ModParamNames
    ifSignatures IfaceDecls
    i)
                                   ]

    instance Semigroup IfaceDecls where
      IfaceDecls
    l <> :: IfaceDecls -> IfaceDecls -> IfaceDecls
    <> IfaceDecls
    r = IfaceDecls
        { ifTySyns :: Map Name TySyn
    ifTySyns   = Map Name TySyn -> Map Name TySyn -> Map Name TySyn
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (IfaceDecls -> Map Name TySyn
    ifTySyns IfaceDecls
    l)   (IfaceDecls -> Map Name TySyn
    ifTySyns IfaceDecls
    r)
        , ifNewtypes :: Map Name Newtype
    ifNewtypes = Map Name Newtype -> Map Name Newtype -> Map Name Newtype
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    l) (IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    r)
        , ifAbstractTypes :: Map Name AbstractType
    ifAbstractTypes = Map Name AbstractType
    -> Map Name AbstractType -> Map Name AbstractType
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (IfaceDecls -> Map Name AbstractType
    ifAbstractTypes IfaceDecls
    l) (IfaceDecls -> Map Name AbstractType
    ifAbstractTypes IfaceDecls
    r)
        , ifDecls :: Map Name IfaceDecl
    ifDecls    = Map Name IfaceDecl -> Map Name IfaceDecl -> Map Name IfaceDecl
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (IfaceDecls -> Map Name IfaceDecl
    ifDecls IfaceDecls
    l)    (IfaceDecls -> Map Name IfaceDecl
    ifDecls IfaceDecls
    r)
        , ifModules :: Map Name (IfaceNames Name)
    ifModules  = Map Name (IfaceNames Name)
    -> Map Name (IfaceNames Name) -> Map Name (IfaceNames Name)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (IfaceDecls -> Map Name (IfaceNames Name)
    ifModules IfaceDecls
    l)  (IfaceDecls -> Map Name (IfaceNames Name)
    ifModules IfaceDecls
    r)
        , ifFunctors :: Map Name (IfaceG Name)
    ifFunctors = Map Name (IfaceG Name)
    -> Map Name (IfaceG Name) -> Map Name (IfaceG Name)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors IfaceDecls
    l) (IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors IfaceDecls
    r)
        , ifSignatures :: Map Name ModParamNames
    ifSignatures = IfaceDecls -> Map Name ModParamNames
    ifSignatures IfaceDecls
    l Map Name ModParamNames
    -> Map Name ModParamNames -> Map Name ModParamNames
    forall a. Semigroup a => a -> a -> a
    <> IfaceDecls -> Map Name ModParamNames
    ifSignatures IfaceDecls
    r
        }

    instance Monoid IfaceDecls where
      mempty :: IfaceDecls
    mempty      = IfaceDecls
                      { ifTySyns :: Map Name TySyn
    ifTySyns = Map Name TySyn
    forall a. Monoid a => a
    mempty
                      , ifNewtypes :: Map Name Newtype
    ifNewtypes = Map Name Newtype
    forall a. Monoid a => a
    mempty
                      , ifAbstractTypes :: Map Name AbstractType
    ifAbstractTypes = Map Name AbstractType
    forall a. Monoid a => a
    mempty
                      , ifDecls :: Map Name IfaceDecl
    ifDecls = Map Name IfaceDecl
    forall a. Monoid a => a
    mempty
                      , ifModules :: Map Name (IfaceNames Name)
    ifModules = Map Name (IfaceNames Name)
    forall a. Monoid a => a
    mempty
                      , ifFunctors :: Map Name (IfaceG Name)
    ifFunctors = Map Name (IfaceG Name)
    forall a. Monoid a => a
    mempty
                      , ifSignatures :: Map Name ModParamNames
    ifSignatures = Map Name ModParamNames
    forall a. Monoid a => a
    mempty
                      }
      mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls
    mappend = IfaceDecls -> IfaceDecls -> IfaceDecls
    forall a. Semigroup a => a -> a -> a
    (<>)
      mconcat :: [IfaceDecls] -> IfaceDecls
    mconcat [IfaceDecls]
    ds  = IfaceDecls
        { ifTySyns :: Map Name TySyn
    ifTySyns   = [Map Name TySyn] -> Map Name TySyn
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name TySyn) -> [IfaceDecls] -> [Map Name TySyn]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name TySyn
    ifTySyns   [IfaceDecls]
    ds)
        , ifNewtypes :: Map Name Newtype
    ifNewtypes = [Map Name Newtype] -> Map Name Newtype
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name Newtype)
    -> [IfaceDecls] -> [Map Name Newtype]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name Newtype
    ifNewtypes [IfaceDecls]
    ds)
        , ifAbstractTypes :: Map Name AbstractType
    ifAbstractTypes = [Map Name AbstractType] -> Map Name AbstractType
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name AbstractType)
    -> [IfaceDecls] -> [Map Name AbstractType]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name AbstractType
    ifAbstractTypes [IfaceDecls]
    ds)
        , ifDecls :: Map Name IfaceDecl
    ifDecls    = [Map Name IfaceDecl] -> Map Name IfaceDecl
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name IfaceDecl)
    -> [IfaceDecls] -> [Map Name IfaceDecl]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name IfaceDecl
    ifDecls    [IfaceDecls]
    ds)
        , ifModules :: Map Name (IfaceNames Name)
    ifModules  = [Map Name (IfaceNames Name)] -> Map Name (IfaceNames Name)
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name (IfaceNames Name))
    -> [IfaceDecls] -> [Map Name (IfaceNames Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name (IfaceNames Name)
    ifModules [IfaceDecls]
    ds)
        , ifFunctors :: Map Name (IfaceG Name)
    ifFunctors = [Map Name (IfaceG Name)] -> Map Name (IfaceG Name)
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name (IfaceG Name))
    -> [IfaceDecls] -> [Map Name (IfaceG Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors [IfaceDecls]
    ds)
        , ifSignatures :: Map Name ModParamNames
    ifSignatures = [Map Name ModParamNames] -> Map Name ModParamNames
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ((IfaceDecls -> Map Name ModParamNames)
    -> [IfaceDecls] -> [Map Name ModParamNames]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceDecls -> Map Name ModParamNames
    ifSignatures [IfaceDecls]
    ds)
        }

    data IfaceDecl = IfaceDecl
      { IfaceDecl -> Name
    ifDeclName    :: !Name          -- ^ Name of thing
      , IfaceDecl -> Schema
    ifDeclSig     :: Schema         -- ^ Type
      , IfaceDecl -> Bool
    ifDeclIsPrim   :: !Bool
      , IfaceDecl -> [Pragma]
    ifDeclPragmas :: [Pragma]       -- ^ Pragmas
      , IfaceDecl -> Bool
    ifDeclInfix   :: Bool           -- ^ Is this an infix thing
      , IfaceDecl -> Maybe Fixity
    ifDeclFixity  :: Maybe Fixity   -- ^ Fixity information
      , IfaceDecl -> Maybe Text
    ifDeclDoc     :: Maybe Text     -- ^ Documentation
      } deriving (Int -> IfaceDecl -> ShowS
    [IfaceDecl] -> ShowS
    IfaceDecl -> String
    (Int -> IfaceDecl -> ShowS)
    -> (IfaceDecl -> String)
    -> ([IfaceDecl] -> ShowS)
    -> Show IfaceDecl
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> IfaceDecl -> ShowS
    showsPrec :: Int -> IfaceDecl -> ShowS
    $cshow :: IfaceDecl -> String
    show :: IfaceDecl -> String
    $cshowList :: [IfaceDecl] -> ShowS
    showList :: [IfaceDecl] -> ShowS
    Show, (forall x. IfaceDecl -> Rep IfaceDecl x)
    -> (forall x. Rep IfaceDecl x -> IfaceDecl) -> Generic IfaceDecl
    forall x. Rep IfaceDecl x -> IfaceDecl
    forall x. IfaceDecl -> Rep IfaceDecl x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. IfaceDecl -> Rep IfaceDecl x
    from :: forall x. IfaceDecl -> Rep IfaceDecl x
    $cto :: forall x. Rep IfaceDecl x -> IfaceDecl
    to :: forall x. Rep IfaceDecl x -> IfaceDecl
    Generic, IfaceDecl -> ()
    (IfaceDecl -> ()) -> NFData IfaceDecl
    forall a. (a -> ()) -> NFData a
    $crnf :: IfaceDecl -> ()
    rnf :: IfaceDecl -> ()
    NFData)

    -- | Produce a PrimMap from an interface.
    --
    -- NOTE: the map will expose /both/ public and private names.
    -- NOTE: this is a bit misnamed, as it is used to resolve known names
    -- that Cryptol introduces (e.g., during type checking).  These
    -- names need not be primitives.   A better way to do this in the future
    -- might be to use original names instead (see #1522).
    ifacePrimMap :: Iface -> PrimMap
    ifacePrimMap :: Iface -> PrimMap
    ifacePrimMap = IfaceDecls -> PrimMap
    ifaceDeclsPrimMap (IfaceDecls -> PrimMap)
    -> (Iface -> IfaceDecls) -> Iface -> PrimMap
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Iface -> IfaceDecls
    forall name. IfaceG name -> IfaceDecls
    ifDefines

    ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
    ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
    ifaceDeclsPrimMap IfaceDecls { Map Name AbstractType
    Map Name Newtype
    Map Name TySyn
    Map Name ModParamNames
    Map Name IfaceDecl
    Map Name (IfaceNames Name)
    Map Name (IfaceG Name)
    ifFunctors :: IfaceDecls -> Map Name (IfaceG Name)
    ifTySyns :: IfaceDecls -> Map Name TySyn
    ifNewtypes :: IfaceDecls -> Map Name Newtype
    ifAbstractTypes :: IfaceDecls -> Map Name AbstractType
    ifDecls :: IfaceDecls -> Map Name IfaceDecl
    ifModules :: IfaceDecls -> Map Name (IfaceNames Name)
    ifSignatures :: IfaceDecls -> Map Name ModParamNames
    ifTySyns :: Map Name TySyn
    ifNewtypes :: Map Name Newtype
    ifAbstractTypes :: Map Name AbstractType
    ifDecls :: Map Name IfaceDecl
    ifModules :: Map Name (IfaceNames Name)
    ifSignatures :: Map Name ModParamNames
    ifFunctors :: Map Name (IfaceG Name)
    .. } =
      PrimMap { primDecls :: Map PrimIdent Name
    primDecls = [(PrimIdent, Name)] -> Map PrimIdent Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Name)]
    newtypes [(PrimIdent, Name)] -> [(PrimIdent, Name)] -> [(PrimIdent, Name)]
    forall a. [a] -> [a] -> [a]
    ++ [(PrimIdent, Name)]
    exprs)
              , primTypes :: Map PrimIdent Name
    primTypes = [(PrimIdent, Name)] -> Map PrimIdent Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Name)]
    newtypes [(PrimIdent, Name)] -> [(PrimIdent, Name)] -> [(PrimIdent, Name)]
    forall a. [a] -> [a] -> [a]
    ++ [(PrimIdent, Name)]
    types)
              }
      where
      entry :: Name -> (PrimIdent, Name)
    entry Name
    n = case Name -> Maybe PrimIdent
    asPrim Name
    n of
                  Just PrimIdent
    pid -> (PrimIdent
    pid,Name
    n)
                  Maybe PrimIdent
    Nothing ->
                    String -> [String] -> (PrimIdent, Name)
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "ifaceDeclsPrimMap"
                              [ String
    "Top level name not declared in a module?"
                              , Name -> String
    forall a. Show a => a -> String
    show Name
    n ]

      newtypes :: [(PrimIdent, Name)]
    newtypes = (Name -> (PrimIdent, Name)) -> [Name] -> [(PrimIdent, Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> (PrimIdent, Name)
    entry (Map Name Newtype -> [Name]
    forall k a. Map k a -> [k]
    Map.keys Map Name Newtype
    ifNewtypes)
      exprs :: [(PrimIdent, Name)]
    exprs    = (Name -> (PrimIdent, Name)) -> [Name] -> [(PrimIdent, Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> (PrimIdent, Name)
    entry (Map Name IfaceDecl -> [Name]
    forall k a. Map k a -> [k]
    Map.keys Map Name IfaceDecl
    ifDecls)
      types :: [(PrimIdent, Name)]
    types    = (Name -> (PrimIdent, Name)) -> [Name] -> [(PrimIdent, Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> (PrimIdent, Name)
    entry (Map Name TySyn -> [Name]
    forall k a. Map k a -> [k]
    Map.keys Map Name TySyn
    ifTySyns)

    -- | Given an interface computing a map from original names to actual names,
    -- grouped by namespace.
    ifaceOrigNameMap :: IfaceG name -> Map Namespace (Map OrigName Name)
    ifaceOrigNameMap :: forall name. IfaceG name -> Map Namespace (Map OrigName Name)
    ifaceOrigNameMap IfaceG name
    ifa = (Map OrigName Name -> Map OrigName Name -> Map OrigName Name)
    -> [Map Namespace (Map OrigName Name)]
    -> Map Namespace (Map OrigName Name)
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    (a -> a -> a) -> f (Map k a) -> Map k a
    Map.unionsWith Map OrigName Name -> Map OrigName Name -> Map OrigName Name
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (Map Namespace (Map OrigName Name)
    here Map Namespace (Map OrigName Name)
    -> [Map Namespace (Map OrigName Name)]
    -> [Map Namespace (Map OrigName Name)]
    forall a. a -> [a] -> [a]
    : [Map Namespace (Map OrigName Name)]
    nested)
      where
      here :: Map Namespace (Map OrigName Name)
    here        = [(Namespace, Map OrigName Name)]
    -> Map Namespace (Map OrigName Name)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Namespace, Map OrigName Name)]
     -> Map Namespace (Map OrigName Name))
    -> [(Namespace, Map OrigName Name)]
    -> Map Namespace (Map OrigName Name)
    forall a b. (a -> b) -> a -> b
    $
                      [ (Namespace
    NSValue, Set Name -> Map OrigName Name
    toMap Set Name
    vaNames) | Bool -> Bool
    not (Set Name -> Bool
    forall a. Set a -> Bool
    Set.null Set Name
    vaNames) ] [(Namespace, Map OrigName Name)]
    -> [(Namespace, Map OrigName Name)]
    -> [(Namespace, Map OrigName Name)]
    forall a. [a] -> [a] -> [a]
    ++
                      [ (Namespace
    NSType,  Set Name -> Map OrigName Name
    toMap Set Name
    tyNames) | Bool -> Bool
    not (Set Name -> Bool
    forall a. Set a -> Bool
    Set.null Set Name
    tyNames) ] [(Namespace, Map OrigName Name)]
    -> [(Namespace, Map OrigName Name)]
    -> [(Namespace, Map OrigName Name)]
    forall a. [a] -> [a] -> [a]
    ++
                      [ (Namespace
    NSValue, Set Name -> Map OrigName Name
    toMap Set Name
    moNames) | Bool -> Bool
    not (Set Name -> Bool
    forall a. Set a -> Bool
    Set.null Set Name
    moNames) ]

      nested :: [Map Namespace (Map OrigName Name)]
    nested      = (IfaceG Name -> Map Namespace (Map OrigName Name))
    -> [IfaceG Name] -> [Map Namespace (Map OrigName Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map IfaceG Name -> Map Namespace (Map OrigName Name)
    forall name. IfaceG name -> Map Namespace (Map OrigName Name)
    ifaceOrigNameMap (Map Name (IfaceG Name) -> [IfaceG Name]
    forall k a. Map k a -> [a]
    Map.elems (IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors IfaceDecls
    decls))

      toMap :: Set Name -> Map OrigName Name
    toMap Set Name
    names = [(OrigName, Name)] -> Map OrigName Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList
                      [ (OrigName
    og,Name
    x) | Name
    x <- Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList Set Name
    names, Just OrigName
    og <- [ Name -> Maybe OrigName
    asOrigName Name
    x ] ]

      decls :: IfaceDecls
    decls       = IfaceG name -> IfaceDecls
    forall name. IfaceG name -> IfaceDecls
    ifDefines IfaceG name
    ifa
      from :: (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map k a
    f      = Map k a -> Set k
    forall k a. Map k a -> Set k
    Map.keysSet (IfaceDecls -> Map k a
    f IfaceDecls
    decls)
      tyNames :: Set Name
    tyNames     = [Set Name] -> Set Name
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [ (IfaceDecls -> Map Name TySyn) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name TySyn
    ifTySyns, (IfaceDecls -> Map Name Newtype) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name Newtype
    ifNewtypes, (IfaceDecls -> Map Name AbstractType) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name AbstractType
    ifAbstractTypes ]
      moNames :: Set Name
    moNames     = [Set Name] -> Set Name
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [ (IfaceDecls -> Map Name (IfaceNames Name)) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name (IfaceNames Name)
    ifModules, (IfaceDecls -> Map Name ModParamNames) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name ModParamNames
    ifSignatures, (IfaceDecls -> Map Name (IfaceG Name)) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name (IfaceG Name)
    ifFunctors ]
      vaNames :: Set Name
    vaNames     = [Set Name] -> Set Name
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [ Set Name
    newtypeCons, (IfaceDecls -> Map Name IfaceDecl) -> Set Name
    forall {k} {a}. (IfaceDecls -> Map k a) -> Set k
    from IfaceDecls -> Map Name IfaceDecl
    ifDecls ]
      newtypeCons :: Set Name
    newtypeCons = [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ((Newtype -> Name) -> [Newtype] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Newtype -> Name
    ntConName (Map Name Newtype -> [Newtype]
    forall k a. Map k a -> [a]
    Map.elems (IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    decls)))