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

    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE RankNTypes #-}
    -- for the instances of RunM and BaseM
    {-# LANGUAGE UndecidableInstances #-}

    module Cryptol.ModuleSystem.Name (
        -- * Names
        Name(), NameInfo(..)
      , NameSource(..)
      , nameUnique
      , nameIdent
      , mapNameIdent
      , nameInfo
      , nameLoc
      , nameFixity
      , nameNamespace
      , asPrim
      , asOrigName
      , nameModPath
      , nameModPathMaybe
      , nameTopModule
      , nameTopModuleMaybe
      , ppLocName
      , Namespace(..)
      , ModPath(..)
      , cmpNameDisplay

        -- ** Creation
      , mkDeclared
      , mkLocal
      , asLocal
      , mkModParam

        -- ** Unique Supply
      , FreshM(..), nextUniqueM
      , SupplyT(), runSupplyT, runSupply
      , Supply(), emptySupply, nextUnique
      , freshNameFor

        -- ** PrimMap
      , PrimMap(..)
      , lookupPrimDecl
      , lookupPrimType
      ) where

    import           Control.DeepSeq
    import qualified Data.Map as Map
    import qualified Data.Monoid as M
    import           Data.Functor.Identity(runIdentity)
    import           GHC.Generics (Generic)
    import           MonadLib
    import           Prelude ()
    import           Prelude.Compat
    import qualified Data.Text as Text
    import           Data.Char(isAlpha,toUpper)

    import           Cryptol.Parser.Position (Range,Located(..))
    import           Cryptol.Utils.Fixity
    import           Cryptol.Utils.Ident
    import           Cryptol.Utils.Panic
    import           Cryptol.Utils.PP

    data NameInfo = GlobalName NameSource OrigName
                  | LocalName Namespace Ident
                    deriving ((forall x. NameInfo -> Rep NameInfo x)
    -> (forall x. Rep NameInfo x -> NameInfo) -> Generic NameInfo
    forall x. Rep NameInfo x -> NameInfo
    forall x. NameInfo -> Rep NameInfo x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. NameInfo -> Rep NameInfo x
    from :: forall x. NameInfo -> Rep NameInfo x
    $cto :: forall x. Rep NameInfo x -> NameInfo
    to :: forall x. Rep NameInfo x -> NameInfo
    Generic, NameInfo -> ()
    (NameInfo -> ()) -> NFData NameInfo
    forall a. (a -> ()) -> NFData a
    $crnf :: NameInfo -> ()
    rnf :: NameInfo -> ()
    NFData, Int -> NameInfo -> ShowS
    [NameInfo] -> ShowS
    NameInfo -> String
    (Int -> NameInfo -> ShowS)
    -> (NameInfo -> String) -> ([NameInfo] -> ShowS) -> Show NameInfo
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> NameInfo -> ShowS
    showsPrec :: Int -> NameInfo -> ShowS
    $cshow :: NameInfo -> String
    show :: NameInfo -> String
    $cshowList :: [NameInfo] -> ShowS
    showList :: [NameInfo] -> ShowS
    Show)

    -- Names -----------------------------------------------------------------------
    data Name = Name { Name -> Int
    nUnique :: {-# UNPACK #-} !Int
                       -- ^ INVARIANT: this field uniquely identifies a name for one
                       -- session with the Cryptol library. Names are unique to
                       -- their binding site.

                     , Name -> NameInfo
    nInfo :: !NameInfo

                     , Name -> Maybe Fixity
    nFixity :: !(Maybe Fixity)
                       -- ^ The associativity and precedence level of
                       --   infix operators.  'Nothing' indicates an
                       --   ordinary prefix operator.

                     , Name -> Range
    nLoc :: !Range
                       -- ^ Where this name was defined
                     } deriving ((forall x. Name -> Rep Name x)
    -> (forall x. Rep Name x -> Name) -> Generic Name
    forall x. Rep Name x -> Name
    forall x. Name -> Rep Name x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Name -> Rep Name x
    from :: forall x. Name -> Rep Name x
    $cto :: forall x. Rep Name x -> Name
    to :: forall x. Rep Name x -> Name
    Generic, Name -> ()
    (Name -> ()) -> NFData Name
    forall a. (a -> ()) -> NFData a
    $crnf :: Name -> ()
    rnf :: Name -> ()
    NFData, Int -> Name -> ShowS
    [Name] -> ShowS
    Name -> String
    (Int -> Name -> ShowS)
    -> (Name -> String) -> ([Name] -> ShowS) -> Show Name
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Name -> ShowS
    showsPrec :: Int -> Name -> ShowS
    $cshow :: Name -> String
    show :: Name -> String
    $cshowList :: [Name] -> ShowS
    showList :: [Name] -> ShowS
    Show)

    data NameSource = SystemName | UserName
                        deriving ((forall x. NameSource -> Rep NameSource x)
    -> (forall x. Rep NameSource x -> NameSource) -> Generic NameSource
    forall x. Rep NameSource x -> NameSource
    forall x. NameSource -> Rep NameSource x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. NameSource -> Rep NameSource x
    from :: forall x. NameSource -> Rep NameSource x
    $cto :: forall x. Rep NameSource x -> NameSource
    to :: forall x. Rep NameSource x -> NameSource
    Generic, NameSource -> ()
    (NameSource -> ()) -> NFData NameSource
    forall a. (a -> ()) -> NFData a
    $crnf :: NameSource -> ()
    rnf :: NameSource -> ()
    NFData, Int -> NameSource -> ShowS
    [NameSource] -> ShowS
    NameSource -> String
    (Int -> NameSource -> ShowS)
    -> (NameSource -> String)
    -> ([NameSource] -> ShowS)
    -> Show NameSource
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> NameSource -> ShowS
    showsPrec :: Int -> NameSource -> ShowS
    $cshow :: NameSource -> String
    show :: NameSource -> String
    $cshowList :: [NameSource] -> ShowS
    showList :: [NameSource] -> ShowS
    Show, NameSource -> NameSource -> Bool
    (NameSource -> NameSource -> Bool)
    -> (NameSource -> NameSource -> Bool) -> Eq NameSource
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: NameSource -> NameSource -> Bool
    == :: NameSource -> NameSource -> Bool
    $c/= :: NameSource -> NameSource -> Bool
    /= :: NameSource -> NameSource -> Bool
    Eq)

    instance Eq Name where
      Name
    a == :: Name -> Name -> Bool
    == Name
    b = Name -> Name -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Name
    a Name
    b Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ
      Name
    a /= :: Name -> Name -> Bool
    /= Name
    b = Name -> Name -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Name
    a Name
    b Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Ordering
    EQ

    instance Ord Name where
      compare :: Name -> Name -> Ordering
    compare Name
    a Name
    b = Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Name -> Int
    nUnique Name
    a) (Name -> Int
    nUnique Name
    b)

    -- | Compare two names by the way they would be displayed.
    -- This is used to order names nicely when showing what's in scope
    cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
    cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
    cmpNameDisplay NameDisp
    disp Name
    l Name
    r =
      case (Name -> Maybe OrigName
    asOrigName Name
    l, Name -> Maybe OrigName
    asOrigName Name
    r) of

        (Just OrigName
    ogl, Just OrigName
    ogr) -> -- XXX: uses system name info?
           case Text -> Text -> Ordering
    cmpText (OrigName -> Text
    fmtPref OrigName
    ogl) (OrigName -> Text
    fmtPref OrigName
    ogr) of
             Ordering
    EQ  -> Name -> Name -> Ordering
    cmpName Name
    l Name
    r
             Ordering
    cmp -> Ordering
    cmp

        (Maybe OrigName
    Nothing,Maybe OrigName
    Nothing) -> Name -> Name -> Ordering
    cmpName Name
    l Name
    r

        (Just OrigName
    ogl,Maybe OrigName
    Nothing) ->
           case Text -> Text -> Ordering
    cmpText (OrigName -> Text
    fmtPref OrigName
    ogl) (Ident -> Text
    identText (Name -> Ident
    nameIdent Name
    r)) of
             Ordering
    EQ  -> Ordering
    GT
             Ordering
    cmp -> Ordering
    cmp

        (Maybe OrigName
    Nothing,Just OrigName
    ogr) ->
           case Text -> Text -> Ordering
    cmpText (Ident -> Text
    identText (Name -> Ident
    nameIdent Name
    l)) (OrigName -> Text
    fmtPref OrigName
    ogr) of
             Ordering
    EQ  -> Ordering
    LT
             Ordering
    cmp -> Ordering
    cmp

      where
      cmpName :: Name -> Name -> Ordering
    cmpName Name
    xs Name
    ys  = Ident -> Ident -> Ordering
    cmpIdent (Name -> Ident
    nameIdent Name
    xs) (Name -> Ident
    nameIdent Name
    ys)
      cmpIdent :: Ident -> Ident -> Ordering
    cmpIdent Ident
    xs Ident
    ys = Text -> Text -> Ordering
    cmpText (Ident -> Text
    identText Ident
    xs) (Ident -> Text
    identText Ident
    ys)

          --- let pfxl = fmtModName nsl (getNameFormat nsl (nameIdent l) disp)
      fmtPref :: OrigName -> Text
    fmtPref OrigName
    og = case OrigName -> NameDisp -> NameFormat
    getNameFormat OrigName
    og NameDisp
    disp of
                     NameFormat
    UnQualified -> Text
    ""
                     Qualified ModName
    q -> ModName -> Text
    modNameToText ModName
    q
                     NameFormat
    NotInScope  ->
                        let m :: Text
    m = String -> Text
    Text.pack (Doc -> String
    forall a. Show a => a -> String
    show (ModPath -> Doc
    forall a. PP a => a -> Doc
    pp (OrigName -> ModPath
    ogModule OrigName
    og)))
                        in
                        case OrigName -> OrigSource
    ogSource OrigName
    og of
                          FromModParam Ident
    q  -> Text
    m Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> Text
    "::" Text -> Text -> Text
    forall a. Semigroup a => a -> a -> a
    <> String -> Text
    Text.pack (Doc -> String
    forall a. Show a => a -> String
    show (Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    q))
                          OrigSource
    _ -> Text
    m

      -- Note that this assumes that `xs` is `l` and `ys` is `r`
      cmpText :: Text -> Text -> Ordering
    cmpText Text
    xs Text
    ys =
        case (Text -> Bool
    Text.null Text
    xs, Text -> Bool
    Text.null Text
    ys) of
          (Bool
    True,Bool
    True)   -> Ordering
    EQ
          (Bool
    True,Bool
    False)  -> Ordering
    LT
          (Bool
    False,Bool
    True)  -> Ordering
    GT
          (Bool
    False,Bool
    False) -> (Int, Maybe Int, Text) -> (Int, Maybe Int, Text) -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Maybe Int -> Text -> (Int, Maybe Int, Text)
    forall {b}. b -> Text -> (Int, b, Text)
    cmp (Name -> Maybe Int
    fx Name
    l) Text
    xs) (Maybe Int -> Text -> (Int, Maybe Int, Text)
    forall {b}. b -> Text -> (Int, b, Text)
    cmp (Name -> Maybe Int
    fx Name
    r) Text
    ys)
            where
            fx :: Name -> Maybe Int
    fx Name
    a = Fixity -> Int
    fLevel (Fixity -> Int) -> Maybe Fixity -> Maybe Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> Maybe Fixity
    nameFixity Name
    a
            cmp :: b -> Text -> (Int, b, Text)
    cmp b
    a Text
    cs = (Char -> Int
    ordC (HasCallStack => Text -> Int -> Char
    Text -> Int -> Char
    Text.index Text
    cs Int
    0), b
    a, Text
    cs)
            ordC :: Char -> Int
    ordC Char
    a | Char -> Bool
    isAlpha Char
    a  = Char -> Int
    forall a. Enum a => a -> Int
    fromEnum (Char -> Char
    toUpper Char
    a)
                   | Char
    a Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '_'   = Int
    1
                   | Bool
    otherwise  = Int
    0

    -- | Figure out how the name should be displayed, by referencing the display
    -- function in the environment. NOTE: this function doesn't take into account
    -- the need for parentheses.
    ppName :: Name -> Doc
    ppName :: Name -> Doc
    ppName Name
    nm =
      case Name -> NameInfo
    nInfo Name
    nm of
        GlobalName NameSource
    _ OrigName
    og -> OrigName -> Doc
    forall a. PP a => a -> Doc
    pp OrigName
    og
        LocalName Namespace
    _ Ident
    i   -> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    i
      Doc -> Doc -> Doc
    <.>
      (PPCfg -> Doc) -> Doc
    withPPCfg \PPCfg
    cfg ->
        if PPCfg -> Bool
    ppcfgShowNameUniques PPCfg
    cfg then Doc
    "_" Doc -> Doc -> Doc
    <.> Int -> Doc
    int (Name -> Int
    nameUnique Name
    nm)
                                    else Doc
    forall a. Monoid a => a
    mempty

    instance PP Name where
      ppPrec :: Int -> Name -> Doc
    ppPrec Int
    _ = Name -> Doc
    forall a. PPName a => a -> Doc
    ppPrefixName

    instance PPName Name where
      ppNameFixity :: Name -> Maybe Fixity
    ppNameFixity Name
    n = Name -> Maybe Fixity
    nameFixity Name
    n

      ppInfixName :: Name -> Doc
    ppInfixName Name
    n
        | Ident -> Bool
    isInfixIdent (Name -> Ident
    nameIdent Name
    n) = Name -> Doc
    ppName Name
    n
        | Bool
    otherwise           = String -> [String] -> Doc
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Name" [ String
    "Non-infix name used infix"
                                             , Ident -> String
    forall a. Show a => a -> String
    show (Name -> Ident
    nameIdent Name
    n) ]

      ppPrefixName :: Name -> Doc
    ppPrefixName Name
    n = Bool -> Doc -> Doc
    optParens (Ident -> Bool
    isInfixIdent (Name -> Ident
    nameIdent Name
    n)) (Name -> Doc
    ppName Name
    n)

    -- | Pretty-print a name with its source location information.
    ppLocName :: Name -> Doc
    ppLocName :: Name -> Doc
    ppLocName Name
    n = Located Name -> Doc
    forall a. PP a => a -> Doc
    pp Located { srcRange :: Range
    srcRange = Name -> Range
    nameLoc Name
    n, thing :: Name
    thing = Name
    n }

    nameUnique :: Name -> Int
    nameUnique :: Name -> Int
    nameUnique  = Name -> Int
    nUnique

    nameInfo :: Name -> NameInfo
    nameInfo :: Name -> NameInfo
    nameInfo = Name -> NameInfo
    nInfo

    nameIdent :: Name -> Ident
    nameIdent :: Name -> Ident
    nameIdent Name
    n = case Name -> NameInfo
    nInfo Name
    n of
                    GlobalName NameSource
    _ OrigName
    og -> OrigName -> Ident
    ogName OrigName
    og
                    LocalName Namespace
    _ Ident
    i   -> Ident
    i

    mapNameIdent :: (Ident -> Ident) -> Name -> Name
    mapNameIdent :: (Ident -> Ident) -> Name -> Name
    mapNameIdent Ident -> Ident
    f Name
    n =
      Name
    n { nInfo :: NameInfo
    nInfo =
            case Name -> NameInfo
    nInfo Name
    n of
              GlobalName NameSource
    x OrigName
    og -> NameSource -> OrigName -> NameInfo
    GlobalName NameSource
    x OrigName
    og { ogName :: Ident
    ogName = Ident -> Ident
    f (OrigName -> Ident
    ogName OrigName
    og) }
              LocalName Namespace
    x Ident
    i   -> Namespace -> Ident -> NameInfo
    LocalName Namespace
    x (Ident -> Ident
    f Ident
    i)
        }

    nameNamespace :: Name -> Namespace
    nameNamespace :: Name -> Namespace
    nameNamespace Name
    n = case Name -> NameInfo
    nInfo Name
    n of
                        GlobalName NameSource
    _ OrigName
    og -> OrigName -> Namespace
    ogNamespace OrigName
    og
                        LocalName Namespace
    ns Ident
    _  -> Namespace
    ns

    nameLoc :: Name -> Range
    nameLoc :: Name -> Range
    nameLoc  = Name -> Range
    nLoc

    nameFixity :: Name -> Maybe Fixity
    nameFixity :: Name -> Maybe Fixity
    nameFixity = Name -> Maybe Fixity
    nFixity

    -- | Primtiives must be in a top level module, at least for now.
    asPrim :: Name -> Maybe PrimIdent
    asPrim :: Name -> Maybe PrimIdent
    asPrim Name
    n =
      case Name -> NameInfo
    nInfo Name
    n of
        GlobalName NameSource
    _ OrigName
    og
          | TopModule ModName
    m <- OrigName -> ModPath
    ogModule OrigName
    og, Bool -> Bool
    not (OrigName -> Bool
    ogFromModParam OrigName
    og) ->
            PrimIdent -> Maybe PrimIdent
    forall a. a -> Maybe a
    Just (PrimIdent -> Maybe PrimIdent) -> PrimIdent -> Maybe PrimIdent
    forall a b. (a -> b) -> a -> b
    $ ModName -> Text -> PrimIdent
    PrimIdent ModName
    m (Text -> PrimIdent) -> Text -> PrimIdent
    forall a b. (a -> b) -> a -> b
    $ Ident -> Text
    identText (Ident -> Text) -> Ident -> Text
    forall a b. (a -> b) -> a -> b
    $ OrigName -> Ident
    ogName OrigName
    og

        NameInfo
    _ -> Maybe PrimIdent
    forall a. Maybe a
    Nothing

    asOrigName :: Name -> Maybe OrigName
    asOrigName :: Name -> Maybe OrigName
    asOrigName Name
    n =
      case Name -> NameInfo
    nInfo Name
    n of
        GlobalName NameSource
    _ OrigName
    og -> OrigName -> Maybe OrigName
    forall a. a -> Maybe a
    Just OrigName
    og
        LocalName {}    -> Maybe OrigName
    forall a. Maybe a
    Nothing

    -- | Get the module path for the given name.
    nameModPathMaybe :: Name -> Maybe ModPath
    nameModPathMaybe :: Name -> Maybe ModPath
    nameModPathMaybe Name
    n = OrigName -> ModPath
    ogModule (OrigName -> ModPath) -> Maybe OrigName -> Maybe ModPath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> Maybe OrigName
    asOrigName Name
    n

    -- | Get the module path for the given name.
    -- The name should be a top-level name.
    nameModPath :: Name -> ModPath
    nameModPath :: Name -> ModPath
    nameModPath Name
    n =
      case Name -> Maybe ModPath
    nameModPathMaybe Name
    n of
        Just ModPath
    p  -> ModPath
    p
        Maybe ModPath
    Nothing -> String -> [String] -> ModPath
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "nameModPath" [ String
    "Not a top-level name: ", Name -> String
    forall a. Show a => a -> String
    show Name
    n ]

    -- | Get the name of the top-level module that introduced this name.
    nameTopModuleMaybe :: Name -> Maybe ModName
    nameTopModuleMaybe :: Name -> Maybe ModName
    nameTopModuleMaybe = (ModPath -> ModName) -> Maybe ModPath -> Maybe ModName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ModPath -> ModName
    topModuleFor (Maybe ModPath -> Maybe ModName)
    -> (Name -> Maybe ModPath) -> Name -> Maybe ModName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Maybe ModPath
    nameModPathMaybe

    -- | Get the name of the top-level module that introduced this name.
    -- Works only for top-level names (i.e., that have original names)
    nameTopModule :: Name -> ModName
    nameTopModule :: Name -> ModName
    nameTopModule = ModPath -> ModName
    topModuleFor (ModPath -> ModName) -> (Name -> ModPath) -> Name -> ModName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> ModPath
    nameModPath

    -- Name Supply -----------------------------------------------------------------

    class Monad m => FreshM m where
      liftSupply :: (Supply -> (a,Supply)) -> m a

    instance FreshM m => FreshM (ExceptionT i m) where
      liftSupply :: forall a. (Supply -> (a, Supply)) -> ExceptionT i m a
    liftSupply Supply -> (a, Supply)
    f = m a -> ExceptionT i m a
    forall (m :: * -> *) a. Monad m => m a -> ExceptionT i m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ((Supply -> (a, Supply)) -> m a
    forall a. (Supply -> (a, Supply)) -> m a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance (M.Monoid i, FreshM m) => FreshM (WriterT i m) where
      liftSupply :: forall a. (Supply -> (a, Supply)) -> WriterT i m a
    liftSupply Supply -> (a, Supply)
    f = m a -> WriterT i m a
    forall (m :: * -> *) a. Monad m => m a -> WriterT i m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ((Supply -> (a, Supply)) -> m a
    forall a. (Supply -> (a, Supply)) -> m a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance FreshM m => FreshM (ReaderT i m) where
      liftSupply :: forall a. (Supply -> (a, Supply)) -> ReaderT i m a
    liftSupply Supply -> (a, Supply)
    f = m a -> ReaderT i m a
    forall (m :: * -> *) a. Monad m => m a -> ReaderT i m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ((Supply -> (a, Supply)) -> m a
    forall a. (Supply -> (a, Supply)) -> m a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance FreshM m => FreshM (StateT i m) where
      liftSupply :: forall a. (Supply -> (a, Supply)) -> StateT i m a
    liftSupply Supply -> (a, Supply)
    f = m a -> StateT i m a
    forall (m :: * -> *) a. Monad m => m a -> StateT i m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ((Supply -> (a, Supply)) -> m a
    forall a. (Supply -> (a, Supply)) -> m a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance Monad m => FreshM (SupplyT m) where
      liftSupply :: forall a. (Supply -> (a, Supply)) -> SupplyT m a
    liftSupply Supply -> (a, Supply)
    f = StateT Supply m a -> SupplyT m a
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT (StateT Supply m a -> SupplyT m a)
    -> StateT Supply m a -> SupplyT m a
    forall a b. (a -> b) -> a -> b
    $
        do Supply
    s <- StateT Supply m Supply
    forall (m :: * -> *) i. StateM m i => m i
    get
           let (a
    a,Supply
    s') = Supply -> (a, Supply)
    f Supply
    s
           Supply -> StateT Supply m ()
    forall (m :: * -> *) i. StateM m i => i -> m ()
    set (Supply -> StateT Supply m ()) -> Supply -> StateT Supply m ()
    forall a b. (a -> b) -> a -> b
    $! Supply
    s'
           a -> StateT Supply m a
    forall a. a -> StateT Supply m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    -- | A monad for easing the use of the supply.
    newtype SupplyT m a = SupplyT { forall (m :: * -> *) a. SupplyT m a -> StateT Supply m a
    unSupply :: StateT Supply m a }

    runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a,Supply)
    runSupplyT :: forall (m :: * -> *) a.
    Monad m =>
    Supply -> SupplyT m a -> m (a, Supply)
    runSupplyT Supply
    s (SupplyT StateT Supply m a
    m) = Supply -> StateT Supply m a -> m (a, Supply)
    forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
    runStateT Supply
    s StateT Supply m a
    m

    runSupply :: Supply -> (forall m. FreshM m => m a) -> (a,Supply)
    runSupply :: forall a.
    Supply -> (forall (m :: * -> *). FreshM m => m a) -> (a, Supply)
    runSupply Supply
    s forall (m :: * -> *). FreshM m => m a
    m = Identity (a, Supply) -> (a, Supply)
    forall a. Identity a -> a
    runIdentity (Supply -> SupplyT Identity a -> Identity (a, Supply)
    forall (m :: * -> *) a.
    Monad m =>
    Supply -> SupplyT m a -> m (a, Supply)
    runSupplyT Supply
    s SupplyT Identity a
    forall (m :: * -> *). FreshM m => m a
    m)

    instance Monad m => Functor (SupplyT m) where
      fmap :: forall a b. (a -> b) -> SupplyT m a -> SupplyT m b
    fmap a -> b
    f (SupplyT StateT Supply m a
    m) = StateT Supply m b -> SupplyT m b
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT ((a -> b) -> StateT Supply m a -> StateT Supply m b
    forall a b. (a -> b) -> StateT Supply m a -> StateT Supply m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f StateT Supply m a
    m)
      {-# INLINE fmap #-}

    instance Monad m => Applicative (SupplyT m) where
      pure :: forall a. a -> SupplyT m a
    pure a
    x = StateT Supply m a -> SupplyT m a
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT (a -> StateT Supply m a
    forall a. a -> StateT Supply m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x)
      {-# INLINE pure #-}

      SupplyT m (a -> b)
    f <*> :: forall a b. SupplyT m (a -> b) -> SupplyT m a -> SupplyT m b
    <*> SupplyT m a
    g = StateT Supply m b -> SupplyT m b
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT (SupplyT m (a -> b) -> StateT Supply m (a -> b)
    forall (m :: * -> *) a. SupplyT m a -> StateT Supply m a
    unSupply SupplyT m (a -> b)
    f StateT Supply m (a -> b) -> StateT Supply m a -> StateT Supply m b
    forall a b.
    StateT Supply m (a -> b) -> StateT Supply m a -> StateT Supply m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> SupplyT m a -> StateT Supply m a
    forall (m :: * -> *) a. SupplyT m a -> StateT Supply m a
    unSupply SupplyT m a
    g)
      {-# INLINE (<*>) #-}

    instance Monad m => Monad (SupplyT m) where
      return :: forall a. a -> SupplyT m a
    return = a -> SupplyT m a
    forall a. a -> SupplyT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      {-# INLINE return #-}

      SupplyT m a
    m >>= :: forall a b. SupplyT m a -> (a -> SupplyT m b) -> SupplyT m b
    >>= a -> SupplyT m b
    f = StateT Supply m b -> SupplyT m b
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT (SupplyT m a -> StateT Supply m a
    forall (m :: * -> *) a. SupplyT m a -> StateT Supply m a
    unSupply SupplyT m a
    m StateT Supply m a -> (a -> StateT Supply m b) -> StateT Supply m b
    forall a b.
    StateT Supply m a -> (a -> StateT Supply m b) -> StateT Supply m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= SupplyT m b -> StateT Supply m b
    forall (m :: * -> *) a. SupplyT m a -> StateT Supply m a
    unSupply (SupplyT m b -> StateT Supply m b)
    -> (a -> SupplyT m b) -> a -> StateT Supply m b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SupplyT m b
    f)
      {-# INLINE (>>=) #-}

    instance MonadT SupplyT where
      lift :: forall (m :: * -> *) a. Monad m => m a -> SupplyT m a
    lift m a
    m = StateT Supply m a -> SupplyT m a
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT (m a -> StateT Supply m a
    forall (m :: * -> *) a. Monad m => m a -> StateT Supply m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift m a
    m)

    instance BaseM m n => BaseM (SupplyT m) n where
      inBase :: forall a. n a -> SupplyT m a
    inBase n a
    m = StateT Supply m a -> SupplyT m a
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT (n a -> StateT Supply m a
    forall a. n a -> StateT Supply m a
    forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
    inBase n a
    m)
      {-# INLINE inBase #-}

    instance RunM m (a,Supply) r => RunM (SupplyT m) a (Supply -> r) where
      runM :: SupplyT m a -> Supply -> r
    runM (SupplyT StateT Supply m a
    m) Supply
    s = StateT Supply m a -> Supply -> r
    forall (m :: * -> *) a r. RunM m a r => m a -> r
    runM StateT Supply m a
    m Supply
    s
      {-# INLINE runM #-}

    -- | Retrieve the next unique from the supply.
    nextUniqueM :: FreshM m => m Int
    nextUniqueM :: forall (m :: * -> *). FreshM m => m Int
    nextUniqueM  = (Supply -> (Int, Supply)) -> m Int
    forall a. (Supply -> (a, Supply)) -> m a
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (Int, Supply)
    nextUnique

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

    -- | This should only be used once at library initialization, and threaded
    -- through the rest of the session.  The supply is started at 0x1000 to leave us
    -- plenty of room for names that the compiler needs to know about (wired-in
    -- constants).
    emptySupply :: Supply
    emptySupply :: Supply
    emptySupply  = Int -> Supply
    Supply Int
    0x1000
    -- For one such name, see paramModRecParam
    -- XXX: perhaps we should simply not have such things
    -- XXX: do we have these anymore?

    nextUnique :: Supply -> (Int,Supply)
    nextUnique :: Supply -> (Int, Supply)
    nextUnique (Supply Int
    n) = Supply
    s' Supply -> (Int, Supply) -> (Int, Supply)
    forall a b. a -> b -> b
    `seq` (Int
    n,Supply
    s')
      where
      s' :: Supply
    s' = Int -> Supply
    Supply (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)

    -- Name Construction -----------------------------------------------------------

    -- | Make a new name for a declaration.
    mkDeclared ::
      Namespace -> ModPath -> NameSource -> Ident -> Maybe Fixity -> Range ->
      Supply -> (Name,Supply)
    mkDeclared :: Namespace
    -> ModPath
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    mkDeclared Namespace
    ns ModPath
    m NameSource
    sys Ident
    ident Maybe Fixity
    fixity Range
    loc Supply
    s = (Name
    name, Supply
    s')
      where
      (Int
    u,Supply
    s') = Supply -> (Int, Supply)
    nextUnique Supply
    s
      name :: Name
    name = Name { nUnique :: Int
    nUnique   = Int
    u
                  , nFixity :: Maybe Fixity
    nFixity   = Maybe Fixity
    fixity
                  , nLoc :: Range
    nLoc      = Range
    loc
                  , nInfo :: NameInfo
    nInfo     = NameSource -> OrigName -> NameInfo
    GlobalName
                                  NameSource
    sys
                                  OrigName
                                    { ogNamespace :: Namespace
    ogNamespace = Namespace
    ns
                                    , ogModule :: ModPath
    ogModule    = ModPath
    m
                                    , ogName :: Ident
    ogName      = Ident
    ident
                                    , ogSource :: OrigSource
    ogSource    = OrigSource
    FromDefinition
                                    }
                  }

    -- | Make a new parameter name.
    mkLocal :: Namespace -> Ident -> Range -> Supply -> (Name,Supply)
    mkLocal :: Namespace -> Ident -> Range -> Supply -> (Name, Supply)
    mkLocal Namespace
    ns Ident
    ident Range
    loc Supply
    s = (Name
    name, Supply
    s')
      where
      (Int
    u,Supply
    s')  = Supply -> (Int, Supply)
    nextUnique Supply
    s
      name :: Name
    name    = Name { nUnique :: Int
    nUnique = Int
    u
                     , nLoc :: Range
    nLoc    = Range
    loc
                     , nFixity :: Maybe Fixity
    nFixity = Maybe Fixity
    forall a. Maybe a
    Nothing
                     , nInfo :: NameInfo
    nInfo   = Namespace -> Ident -> NameInfo
    LocalName Namespace
    ns Ident
    ident
                     }

    {- | Make a local name derived from the given name.
    This is a bit questionable,
    but it is used by the translation to SAW Core -}
    asLocal :: Namespace -> Name -> Name
    asLocal :: Namespace -> Name -> Name
    asLocal Namespace
    ns Name
    x =
      case Name -> NameInfo
    nameInfo Name
    x of
        GlobalName NameSource
    _ OrigName
    og -> Name
    x { nInfo :: NameInfo
    nInfo = Namespace -> Ident -> NameInfo
    LocalName Namespace
    ns (OrigName -> Ident
    ogName OrigName
    og) }
        LocalName {}    -> Name
    x

    mkModParam ::
      ModPath {- ^ Module containing the parameter -} ->
      Ident   {- ^ Name of the module parameter    -} ->
      Range   {- ^ Location                        -} ->
      Name    {- ^ Name in the signature           -} ->
      Supply -> (Name, Supply)
    mkModParam :: ModPath -> Ident -> Range -> Name -> Supply -> (Name, Supply)
    mkModParam ModPath
    own Ident
    pname Range
    rng Name
    n Supply
    s = (Name
    name, Supply
    s')
      where
      (Int
    u,Supply
    s') = Supply -> (Int, Supply)
    nextUnique Supply
    s
      name :: Name
    name = Name { nUnique :: Int
    nUnique = Int
    u
                  , nInfo :: NameInfo
    nInfo   = NameSource -> OrigName -> NameInfo
    GlobalName
                                NameSource
    UserName
                                OrigName
                                  { ogModule :: ModPath
    ogModule    = ModPath
    own
                                  , ogName :: Ident
    ogName      = Name -> Ident
    nameIdent Name
    n
                                  , ogNamespace :: Namespace
    ogNamespace = Name -> Namespace
    nameNamespace Name
    n
                                  , ogSource :: OrigSource
    ogSource    = Ident -> OrigSource
    FromModParam Ident
    pname
                                  }
                  , nFixity :: Maybe Fixity
    nFixity = Name -> Maybe Fixity
    nFixity Name
    n
                  , nLoc :: Range
    nLoc    = Range
    rng
                  }

    -- | This is used when instantiating functors
    freshNameFor :: ModPath -> Name -> Supply -> (Name,Supply)
    freshNameFor :: ModPath -> Name -> Supply -> (Name, Supply)
    freshNameFor ModPath
    mpath Name
    x Supply
    s = (Name
    newName, Supply
    s1)
      where
      (Int
    u,Supply
    s1) = Supply -> (Int, Supply)
    nextUnique Supply
    s
      newName :: Name
    newName =
        Name
    x { nUnique :: Int
    nUnique = Int
    u
          , nInfo :: NameInfo
    nInfo =
              case Name -> NameInfo
    nInfo Name
    x of
                GlobalName NameSource
    src OrigName
    og -> NameSource -> OrigName -> NameInfo
    GlobalName NameSource
    src OrigName
    og { ogModule :: ModPath
    ogModule = ModPath
    mpath
                                                       , ogSource :: OrigSource
    ogSource = OrigSource
    FromFunctorInst }
                LocalName {} -> String -> [String] -> NameInfo
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "freshNameFor" [String
    "Unexpected local",Name -> String
    forall a. Show a => a -> String
    show Name
    x]
          }

    -- Prim Maps -------------------------------------------------------------------

    -- | A mapping from an identifier defined in some module to its real name.
    data PrimMap = PrimMap { PrimMap -> Map PrimIdent Name
    primDecls :: Map.Map PrimIdent Name
                           , PrimMap -> Map PrimIdent Name
    primTypes :: Map.Map PrimIdent Name
                           } deriving (Int -> PrimMap -> ShowS
    [PrimMap] -> ShowS
    PrimMap -> String
    (Int -> PrimMap -> ShowS)
    -> (PrimMap -> String) -> ([PrimMap] -> ShowS) -> Show PrimMap
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PrimMap -> ShowS
    showsPrec :: Int -> PrimMap -> ShowS
    $cshow :: PrimMap -> String
    show :: PrimMap -> String
    $cshowList :: [PrimMap] -> ShowS
    showList :: [PrimMap] -> ShowS
    Show, (forall x. PrimMap -> Rep PrimMap x)
    -> (forall x. Rep PrimMap x -> PrimMap) -> Generic PrimMap
    forall x. Rep PrimMap x -> PrimMap
    forall x. PrimMap -> Rep PrimMap x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PrimMap -> Rep PrimMap x
    from :: forall x. PrimMap -> Rep PrimMap x
    $cto :: forall x. Rep PrimMap x -> PrimMap
    to :: forall x. Rep PrimMap x -> PrimMap
    Generic, PrimMap -> ()
    (PrimMap -> ()) -> NFData PrimMap
    forall a. (a -> ()) -> NFData a
    $crnf :: PrimMap -> ()
    rnf :: PrimMap -> ()
    NFData)

    instance Semigroup PrimMap where
      PrimMap
    x <> :: PrimMap -> PrimMap -> PrimMap
    <> PrimMap
    y = PrimMap { primDecls :: Map PrimIdent Name
    primDecls = Map PrimIdent Name -> Map PrimIdent Name -> Map PrimIdent Name
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (PrimMap -> Map PrimIdent Name
    primDecls PrimMap
    x) (PrimMap -> Map PrimIdent Name
    primDecls PrimMap
    y)
                       , primTypes :: Map PrimIdent Name
    primTypes = Map PrimIdent Name -> Map PrimIdent Name -> Map PrimIdent Name
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (PrimMap -> Map PrimIdent Name
    primTypes PrimMap
    x) (PrimMap -> Map PrimIdent Name
    primTypes PrimMap
    y)
                       }

    lookupPrimDecl, lookupPrimType :: PrimIdent -> PrimMap -> Name

    -- | It's assumed that we're looking things up that we know already exist, so
    -- this will panic if it doesn't find the name.
    lookupPrimDecl :: PrimIdent -> PrimMap -> Name
    lookupPrimDecl PrimIdent
    name PrimMap { Map PrimIdent Name
    primDecls :: PrimMap -> Map PrimIdent Name
    primTypes :: PrimMap -> Map PrimIdent Name
    primDecls :: Map PrimIdent Name
    primTypes :: Map PrimIdent Name
    .. } = Name -> PrimIdent -> Map PrimIdent Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    forall {a}. a
    err PrimIdent
    name Map PrimIdent Name
    primDecls
      where
      err :: a
    err = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.ModuleSystem.Name.lookupPrimDecl"
            [ String
    "Unknown declaration: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ PrimIdent -> String
    forall a. Show a => a -> String
    show PrimIdent
    name
            , Map PrimIdent Name -> String
    forall a. Show a => a -> String
    show Map PrimIdent Name
    primDecls ]

    -- | It's assumed that we're looking things up that we know already exist, so
    -- this will panic if it doesn't find the name.
    lookupPrimType :: PrimIdent -> PrimMap -> Name
    lookupPrimType PrimIdent
    name PrimMap { Map PrimIdent Name
    primDecls :: PrimMap -> Map PrimIdent Name
    primTypes :: PrimMap -> Map PrimIdent Name
    primDecls :: Map PrimIdent Name
    primTypes :: Map PrimIdent Name
    .. } = Name -> PrimIdent -> Map PrimIdent Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    forall {a}. a
    err PrimIdent
    name Map PrimIdent Name
    primTypes
      where
      err :: a
    err = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.ModuleSystem.Name.lookupPrimType"
            [ String
    "Unknown type: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ PrimIdent -> String
    forall a. Show a => a -> String
    show PrimIdent
    name
            , Map PrimIdent Name -> String
    forall a. Show a => a -> String
    show Map PrimIdent Name
    primTypes ]