-- |
-- 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 ]