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

    {-# LANGUAGE Trustworthy #-}

    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE RecordWildCards #-}
    -- for the instances of RunM and BaseM
    {-# LANGUAGE UndecidableInstances #-}

    module Cryptol.ModuleSystem.Name (
        -- * Names
        Name(), NameInfo(..)
      , NameSource(..)
      , nameUnique
      , nameIdent
      , nameInfo
      , nameLoc
      , nameFixity
      , asPrim
      , cmpNameLexical
      , cmpNameDisplay
      , ppLocName

        -- ** Creation
      , mkDeclared
      , mkParameter
      , toParamInstName
      , asParamName
      , paramModRecParam

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

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

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

    import           Control.DeepSeq
    import           Control.Monad.Fix (MonadFix(mfix))
    import qualified Data.Map as Map
    import qualified Data.Monoid as M
    import           Data.Ord (comparing)
    import qualified Data.Text as Text
    import           Data.Char(isAlpha,toUpper)
    import           GHC.Generics (Generic)
    import           MonadLib
    import           Prelude ()
    import           Prelude.Compat

    -- Names -----------------------------------------------------------------------
    -- | Information about the binding site of the name.
    data NameInfo = Declared !ModName !NameSource
                    -- ^ This name refers to a declaration from this module
                  | Parameter
                    -- ^ This name is a parameter (function or type)
                    deriving (NameInfo -> NameInfo -> Bool
    (NameInfo -> NameInfo -> Bool)
    -> (NameInfo -> NameInfo -> Bool) -> Eq NameInfo
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: NameInfo -> NameInfo -> Bool
    $c/= :: NameInfo -> NameInfo -> Bool
    == :: NameInfo -> NameInfo -> Bool
    $c== :: NameInfo -> NameInfo -> Bool
    Eq, 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
    showList :: [NameInfo] -> ShowS
    $cshowList :: [NameInfo] -> ShowS
    show :: NameInfo -> String
    $cshow :: NameInfo -> String
    showsPrec :: Int -> NameInfo -> ShowS
    $cshowsPrec :: Int -> NameInfo -> ShowS
    Show, (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
    $cto :: forall x. Rep NameInfo x -> NameInfo
    $cfrom :: forall x. NameInfo -> Rep NameInfo x
    Generic, NameInfo -> ()
    (NameInfo -> ()) -> NFData NameInfo
    forall a. (a -> ()) -> NFData a
    rnf :: NameInfo -> ()
    $crnf :: NameInfo -> ()
    NFData)

    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
                       -- ^ Information about the origin of this name.

                     , Name -> Ident
    nIdent :: !Ident
                       -- ^ The name of the identifier

                     , 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
    $cto :: forall x. Rep Name x -> Name
    $cfrom :: forall x. Name -> Rep Name x
    Generic, Name -> ()
    (Name -> ()) -> NFData Name
    forall a. (a -> ()) -> NFData a
    rnf :: Name -> ()
    $crnf :: 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
    showList :: [Name] -> ShowS
    $cshowList :: [Name] -> ShowS
    show :: Name -> String
    $cshow :: Name -> String
    showsPrec :: Int -> Name -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep NameSource x -> NameSource
    $cfrom :: forall x. NameSource -> Rep NameSource x
    Generic, NameSource -> ()
    (NameSource -> ()) -> NFData NameSource
    forall a. (a -> ()) -> NFData a
    rnf :: NameSource -> ()
    $crnf :: 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
    showList :: [NameSource] -> ShowS
    $cshowList :: [NameSource] -> ShowS
    show :: NameSource -> String
    $cshow :: NameSource -> String
    showsPrec :: Int -> NameSource -> ShowS
    $cshowsPrec :: Int -> NameSource -> ShowS
    Show, NameSource -> NameSource -> Bool
    (NameSource -> NameSource -> Bool)
    -> (NameSource -> NameSource -> Bool) -> Eq NameSource
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: NameSource -> NameSource -> Bool
    $c/= :: NameSource -> NameSource -> Bool
    == :: NameSource -> NameSource -> Bool
    $c== :: NameSource -> NameSource -> Bool
    Eq)

    instance Eq Name where
      a :: Name
    a == :: Name -> Name -> Bool
    == b :: 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
      a :: Name
    a /= :: Name -> Name -> Bool
    /= b :: 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 a :: Name
    a b :: 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 lexically.
    cmpNameLexical :: Name -> Name -> Ordering
    cmpNameLexical :: Name -> Name -> Ordering
    cmpNameLexical l :: Name
    l r :: Name
    r =
      case (Name -> NameInfo
    nameInfo Name
    l, Name -> NameInfo
    nameInfo Name
    r) of

        (Declared nsl :: ModName
    nsl _,Declared nsr :: ModName
    nsr _) ->
          case ModName -> ModName -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare ModName
    nsl ModName
    nsr of
            EQ  -> (Name -> Ident) -> Name -> Name -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing Name -> Ident
    nameIdent Name
    l Name
    r
            cmp :: Ordering
    cmp -> Ordering
    cmp

        (Parameter,Parameter) -> (Name -> Ident) -> Name -> Name -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing Name -> Ident
    nameIdent Name
    l Name
    r

        (Declared nsl :: ModName
    nsl _,Parameter) -> Text -> Text -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (ModName -> Text
    modNameToText ModName
    nsl)
                                              (Ident -> Text
    identText (Name -> Ident
    nameIdent Name
    r))
        (Parameter,Declared nsr :: ModName
    nsr _) -> Text -> Text -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Ident -> Text
    identText (Name -> Ident
    nameIdent Name
    l))
                                              (ModName -> Text
    modNameToText ModName
    nsr)

    -- | Compare two names by the way they would be displayed.
    cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
    cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
    cmpNameDisplay disp :: NameDisp
    disp l :: Name
    l r :: Name
    r =
      case (Name -> NameInfo
    nameInfo Name
    l, Name -> NameInfo
    nameInfo Name
    r) of

        (Declared nsl :: ModName
    nsl _, Declared nsr :: ModName
    nsr _) -> -- XXX: uses system name info?
          let pfxl :: Text
    pfxl = ModName -> NameFormat -> Text
    fmtModName ModName
    nsl (ModName -> Ident -> NameDisp -> NameFormat
    getNameFormat ModName
    nsl (Name -> Ident
    nameIdent Name
    l) NameDisp
    disp)
              pfxr :: Text
    pfxr = ModName -> NameFormat -> Text
    fmtModName ModName
    nsr (ModName -> Ident -> NameDisp -> NameFormat
    getNameFormat ModName
    nsr (Name -> Ident
    nameIdent Name
    r) NameDisp
    disp)
           in case Text -> Text -> Ordering
    cmpText Text
    pfxl Text
    pfxr of
                EQ  -> Name -> Name -> Ordering
    cmpName Name
    l Name
    r
                cmp :: Ordering
    cmp -> Ordering
    cmp

        (Parameter,Parameter) -> Name -> Name -> Ordering
    cmpName Name
    l Name
    r

        (Declared nsl :: ModName
    nsl _,Parameter) ->
          let pfxl :: Text
    pfxl = ModName -> NameFormat -> Text
    fmtModName ModName
    nsl (ModName -> Ident -> NameDisp -> NameFormat
    getNameFormat ModName
    nsl (Name -> Ident
    nameIdent Name
    l) NameDisp
    disp)
           in case Text -> Text -> Ordering
    cmpText Text
    pfxl (Ident -> Text
    identText (Name -> Ident
    nameIdent Name
    r)) of
                EQ  -> Ordering
    GT
                cmp :: Ordering
    cmp -> Ordering
    cmp

        (Parameter,Declared nsr :: ModName
    nsr _) ->
          let pfxr :: Text
    pfxr = ModName -> NameFormat -> Text
    fmtModName ModName
    nsr (ModName -> Ident -> NameDisp -> NameFormat
    getNameFormat ModName
    nsr (Name -> Ident
    nameIdent Name
    r) NameDisp
    disp)
           in case Text -> Text -> Ordering
    cmpText (Ident -> Text
    identText (Name -> Ident
    nameIdent Name
    l)) Text
    pfxr of
                EQ  -> Ordering
    LT
                cmp :: Ordering
    cmp -> Ordering
    cmp

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

      -- Note that this assumes that `xs` is `l` and `ys` is `r`
      cmpText :: Text -> Text -> Ordering
    cmpText xs :: Text
    xs ys :: Text
    ys =
        case (Text -> Bool
    Text.null Text
    xs, Text -> Bool
    Text.null Text
    ys) of
          (True,True)   -> Ordering
    EQ
          (True,False)  -> Ordering
    LT
          (False,True)  -> Ordering
    GT
          (False,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 a :: 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 a :: b
    a cs :: Text
    cs = (Char -> Int
    ordC (Text -> Int -> Char
    Text.index Text
    cs 0), b
    a, Text
    cs)
            ordC :: Char -> Int
    ordC a :: 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
    == '_'   = 1
                   | Bool
    otherwise  = 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 parenthesis.
    ppName :: Name -> Doc
    ppName :: Name -> Doc
    ppName Name { .. } =
      case NameInfo
    nInfo of

        Declared m :: ModName
    m _ -> (NameDisp -> Doc) -> Doc
    withNameDisp ((NameDisp -> Doc) -> Doc) -> (NameDisp -> Doc) -> Doc
    forall a b. (a -> b) -> a -> b
    $ \disp :: NameDisp
    disp ->
          case ModName -> Ident -> NameDisp -> NameFormat
    getNameFormat ModName
    m Ident
    nIdent NameDisp
    disp of
            Qualified m' :: ModName
    m' -> ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    m' Doc -> Doc -> Doc
    <.> String -> Doc
    text "::" Doc -> Doc -> Doc
    <.> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    nIdent
            UnQualified  ->                         Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    nIdent
            NotInScope   -> ModName -> Doc
    forall a. PP a => a -> Doc
    pp ModName
    m  Doc -> Doc -> Doc
    <.> String -> Doc
    text "::" Doc -> Doc -> Doc
    <.> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    nIdent

        Parameter -> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    nIdent

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

    instance PPName Name where
      ppNameFixity :: Name -> Maybe (Assoc, Int)
    ppNameFixity n :: Name
    n = (Fixity -> (Assoc, Int)) -> Maybe Fixity -> Maybe (Assoc, Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\(Fixity a :: Assoc
    a i :: Int
    i) -> (Assoc
    a,Int
    i)) (Maybe Fixity -> Maybe (Assoc, Int))
    -> Maybe Fixity -> Maybe (Assoc, Int)
    forall a b. (a -> b) -> a -> b
    $ Name -> Maybe Fixity
    nameFixity Name
    n

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

      ppPrefixName :: Name -> Doc
    ppPrefixName n :: Name
    n @ Name { .. } = Bool -> Doc -> Doc
    optParens (Ident -> Bool
    isInfixIdent Ident
    nIdent) (Name -> Doc
    ppName Name
    n)

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

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

    nameIdent :: Name -> Ident
    nameIdent :: Name -> Ident
    nameIdent  = Name -> Ident
    nIdent

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

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

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

    asPrim :: Name -> Maybe Ident
    asPrim :: Name -> Maybe Ident
    asPrim Name { .. } =
      case NameInfo
    nInfo of
        Declared p :: ModName
    p _ | ModName
    p ModName -> ModName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModName
    preludeName -> Ident -> Maybe Ident
    forall a. a -> Maybe a
    Just Ident
    nIdent
        _ -> Maybe Ident
    forall a. Maybe a
    Nothing

    toParamInstName :: Name -> Name
    toParamInstName :: Name -> Name
    toParamInstName n :: Name
    n =
      case Name -> NameInfo
    nInfo Name
    n of
        Declared m :: ModName
    m s :: NameSource
    s -> Name
    n { nInfo :: NameInfo
    nInfo = ModName -> NameSource -> NameInfo
    Declared (ModName -> ModName
    paramInstModName ModName
    m) NameSource
    s }
        Parameter   -> Name
    n

    asParamName :: Name -> Name
    asParamName :: Name -> Name
    asParamName n :: Name
    n = Name
    n { nInfo :: NameInfo
    nInfo = NameInfo
    Parameter }

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

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

    instance FreshM m => FreshM (ExceptionT i m) where
      liftSupply :: (Supply -> (a, Supply)) -> ExceptionT i m a
    liftSupply f :: Supply -> (a, Supply)
    f = 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 (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 :: (Supply -> (a, Supply)) -> WriterT i m a
    liftSupply f :: Supply -> (a, Supply)
    f = 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 (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance FreshM m => FreshM (ReaderT i m) where
      liftSupply :: (Supply -> (a, Supply)) -> ReaderT i m a
    liftSupply f :: Supply -> (a, Supply)
    f = 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 (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance FreshM m => FreshM (StateT i m) where
      liftSupply :: (Supply -> (a, Supply)) -> StateT i m a
    liftSupply f :: Supply -> (a, Supply)
    f = 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 (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply Supply -> (a, Supply)
    f)

    instance Monad m => FreshM (SupplyT m) where
      liftSupply :: (Supply -> (a, Supply)) -> SupplyT m a
    liftSupply f :: 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
    a,s' :: 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 (m :: * -> *) a. Monad m => a -> m a
    return a
    a

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

    runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a,Supply)
    runSupplyT :: Supply -> SupplyT m a -> m (a, Supply)
    runSupplyT s :: Supply
    s (SupplyT m :: 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

    instance Monad m => Functor (SupplyT m) where
      fmap :: (a -> b) -> SupplyT m a -> SupplyT m b
    fmap f :: a -> b
    f (SupplyT m :: 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 (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 :: a -> SupplyT m a
    pure x :: 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 (f :: * -> *) a. Applicative f => a -> f a
    pure a
    x)
      {-# INLINE pure #-}

      f :: SupplyT m (a -> b)
    f <*> :: SupplyT m (a -> b) -> SupplyT m a -> SupplyT m b
    <*> g :: 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 (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 :: a -> SupplyT m a
    return = a -> SupplyT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      {-# INLINE return #-}

      m :: SupplyT m a
    m >>= :: SupplyT m a -> (a -> SupplyT m b) -> SupplyT m b
    >>= f :: 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 (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 :: m a -> SupplyT m a
    lift m :: 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 (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 :: n a -> SupplyT m a
    inBase m :: 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 (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 m :: StateT Supply m a
    m) s :: 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 #-}

    instance MonadFix m => MonadFix (SupplyT m) where
      mfix :: (a -> SupplyT m a) -> SupplyT m a
    mfix f :: a -> SupplyT m a
    f = StateT Supply m a -> SupplyT m a
    forall (m :: * -> *) a. StateT Supply m a -> SupplyT m a
    SupplyT ((a -> StateT Supply m a) -> StateT Supply m a
    forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
    mfix (SupplyT m a -> StateT Supply m a
    forall (m :: * -> *) a. SupplyT m a -> StateT Supply m a
    unSupply (SupplyT m a -> StateT Supply m a)
    -> (a -> SupplyT m a) -> a -> StateT Supply m a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> SupplyT m a
    f))

    -- | Retrieve the next unique from the supply.
    nextUniqueM :: FreshM m => m Int
    nextUniqueM :: m Int
    nextUniqueM  = (Supply -> (Int, Supply)) -> m Int
    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
    showList :: [Supply] -> ShowS
    $cshowList :: [Supply] -> ShowS
    show :: Supply -> String
    $cshow :: Supply -> String
    showsPrec :: Int -> Supply -> ShowS
    $cshowsPrec :: Int -> 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
    $cto :: forall x. Rep Supply x -> Supply
    $cfrom :: forall x. Supply -> Rep Supply x
    Generic, Supply -> ()
    (Supply -> ()) -> NFData Supply
    forall a. (a -> ()) -> NFData a
    rnf :: Supply -> ()
    $crnf :: 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 0x1000
    -- For one such name, see paramModRecParam
    -- XXX: perhaps we should simply not have such things, but that's the way
    -- for now.

    nextUnique :: Supply -> (Int,Supply)
    nextUnique :: Supply -> (Int, Supply)
    nextUnique (Supply n :: 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
    + 1)

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

    -- | Make a new name for a declaration.
    mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name,Supply)
    mkDeclared :: ModName
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    mkDeclared m :: ModName
    m sys :: NameSource
    sys nIdent :: Ident
    nIdent nFixity :: Maybe Fixity
    nFixity nLoc :: Range
    nLoc s :: Supply
    s =
      let (nUnique :: Int
    nUnique,s' :: Supply
    s') = Supply -> (Int, Supply)
    nextUnique Supply
    s
          nInfo :: NameInfo
    nInfo        = ModName -> NameSource -> NameInfo
    Declared ModName
    m NameSource
    sys
       in ($WName :: Int -> NameInfo -> Ident -> Maybe Fixity -> Range -> Name
    Name { .. }, Supply
    s')

    -- | Make a new parameter name.
    mkParameter :: Ident -> Range -> Supply -> (Name,Supply)
    mkParameter :: Ident -> Range -> Supply -> (Name, Supply)
    mkParameter nIdent :: Ident
    nIdent nLoc :: Range
    nLoc s :: Supply
    s =
      let (nUnique :: Int
    nUnique,s' :: Supply
    s') = Supply -> (Int, Supply)
    nextUnique Supply
    s
          nFixity :: Maybe a
    nFixity      = Maybe a
    forall a. Maybe a
    Nothing
       in ($WName :: Int -> NameInfo -> Ident -> Maybe Fixity -> Range -> Name
    Name { nInfo :: NameInfo
    nInfo = NameInfo
    Parameter, .. }, Supply
    s')

    paramModRecParam :: Name
    paramModRecParam :: Name
    paramModRecParam = $WName :: Int -> NameInfo -> Ident -> Maybe Fixity -> Range -> Name
    Name { nInfo :: NameInfo
    nInfo = NameInfo
    Parameter
                            , nFixity :: Maybe Fixity
    nFixity = Maybe Fixity
    forall a. Maybe a
    Nothing
                            , nIdent :: Ident
    nIdent  = String -> Ident
    packIdent "$modParams"
                            , nLoc :: Range
    nLoc    = Range
    emptyRange
                            , nUnique :: Int
    nUnique = 0x01
                            }

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

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

    lookupPrimDecl, lookupPrimType :: Ident -> 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 :: Ident -> PrimMap -> Name
    lookupPrimDecl name :: Ident
    name PrimMap { .. } = Name -> Ident -> Map Ident Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    forall a. a
    err Ident
    name Map Ident Name
    primDecls
      where
      err :: a
    err = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.ModuleSystem.Name.lookupPrimDecl"
            [ "Unknown declaration: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Ident -> String
    forall a. Show a => a -> String
    show Ident
    name
            , Map Ident Name -> String
    forall a. Show a => a -> String
    show Map Ident 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 :: Ident -> PrimMap -> Name
    lookupPrimType name :: Ident
    name PrimMap { .. } = Name -> Ident -> Map Ident Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    forall a. a
    err Ident
    name Map Ident Name
    primTypes
      where
      err :: a
    err = String -> [String] -> a
    forall a. HasCallStack => String -> [String] -> a
    panic "Cryptol.ModuleSystem.Name.lookupPrimType"
            [ "Unknown type: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Ident -> String
    forall a. Show a => a -> String
    show Ident
    name
            , Map Ident Name -> String
    forall a. Show a => a -> String
    show Map Ident Name
    primTypes ]