-- |
-- 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.Position (Range,Located(..),emptyRange)
import           Cryptol.Utils.Fixity
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
  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 lexically.
cmpNameLexical :: Name -> Name -> Ordering
cmpNameLexical :: Name -> Name -> Ordering
cmpNameLexical Name
l Name
r =
  case (Name -> NameInfo
nameInfo Name
l, Name -> NameInfo
nameInfo Name
r) of

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

    (NameInfo
Parameter,NameInfo
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 ModName
nsl NameSource
_,NameInfo
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))
    (NameInfo
Parameter,Declared ModName
nsr NameSource
_) -> 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 NameDisp
disp Name
l Name
r =
  case (Name -> NameInfo
nameInfo Name
l, Name -> NameInfo
nameInfo Name
r) of

    (Declared ModName
nsl NameSource
_, Declared ModName
nsr NameSource
_) -> -- 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
            Ordering
EQ  -> Name -> Name -> Ordering
cmpName Name
l Name
r
            Ordering
cmp -> Ordering
cmp

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

    (Declared ModName
nsl NameSource
_,NameInfo
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
            Ordering
EQ  -> Ordering
GT
            Ordering
cmp -> Ordering
cmp

    (NameInfo
Parameter,Declared ModName
nsr NameSource
_) ->
      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
            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)

  -- 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 (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 { Int
Maybe Fixity
Ident
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nInfo :: Name -> NameInfo
nUnique :: Name -> Int
.. } =
  case NameInfo
nInfo of

    Declared ModName
m NameSource
_ -> (NameDisp -> Doc) -> Doc
withNameDisp ((NameDisp -> Doc) -> Doc) -> (NameDisp -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \NameDisp
disp ->
      case ModName -> Ident -> NameDisp -> NameFormat
getNameFormat ModName
m Ident
nIdent NameDisp
disp of
        Qualified ModName
m' -> ModName -> Doc
ppQual ModName
m' Doc -> Doc -> Doc
<.> Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
nIdent
        NameFormat
UnQualified  ->               Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
nIdent
        NameFormat
NotInScope   -> ModName -> Doc
ppQual ModName
m  Doc -> Doc -> Doc
<.> Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
nIdent -- XXX: only when not in scope?
      where
      ppQual :: ModName -> Doc
ppQual ModName
mo = if ModName
mo ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
exprModName then Doc
empty else ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
mo Doc -> Doc -> Doc
<.> String -> Doc
text String
"::"

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

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 n :: Name
n @ Name { Int
Maybe Fixity
Ident
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nInfo :: Name -> NameInfo
nUnique :: Name -> Int
.. }
    | Ident -> Bool
isInfixIdent Ident
nIdent = 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 Ident
nIdent ]

  ppPrefixName :: Name -> Doc
ppPrefixName n :: Name
n @ Name { Int
Maybe Fixity
Ident
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nInfo :: Name -> NameInfo
nUnique :: Name -> Int
.. } = 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 Name
n = Located Name -> Doc
forall a. PP a => a -> Doc
pp Located :: 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 PrimIdent
asPrim :: Name -> Maybe PrimIdent
asPrim Name { Int
Maybe Fixity
Ident
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nInfo :: Name -> NameInfo
nUnique :: Name -> Int
.. } =
  case NameInfo
nInfo of
    Declared ModName
p NameSource
_ -> 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
p (Text -> PrimIdent) -> Text -> PrimIdent
forall a b. (a -> b) -> a -> b
$ Ident -> Text
identText Ident
nIdent
    NameInfo
_            -> Maybe PrimIdent
forall a. Maybe a
Nothing

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

asParamName :: Name -> Name
asParamName :: Name -> Name
asParamName 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 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 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 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 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 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 (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 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

instance Monad m => Functor (SupplyT m) where
  fmap :: (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 (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 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 #-}

  SupplyT m (a -> b)
f <*> :: 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 (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 #-}

  SupplyT m a
m >>= :: 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 (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 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 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 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 #-}

instance MonadFix m => MonadFix (SupplyT m) where
  mfix :: (a -> SupplyT m a) -> SupplyT m a
mfix 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 Int
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 Int
n) = Supply
s' Supply -> (Int, Supply) -> (Int, Supply)
`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 :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name,Supply)
mkDeclared :: ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared ModName
m NameSource
sys Ident
nIdent Maybe Fixity
nFixity Range
nLoc Supply
s =
  let (Int
nUnique,Supply
s') = Supply -> (Int, Supply)
nextUnique Supply
s
      nInfo :: NameInfo
nInfo        = ModName -> NameSource -> NameInfo
Declared ModName
m NameSource
sys
   in (Name :: Int -> NameInfo -> Ident -> Maybe Fixity -> Range -> Name
Name { Int
Maybe Fixity
Ident
Range
NameInfo
nInfo :: NameInfo
nUnique :: Int
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nInfo :: NameInfo
nUnique :: Int
.. }, Supply
s')

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

paramModRecParam :: Name
paramModRecParam :: Name
paramModRecParam = Name :: 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 String
"$modParams"
                        , nLoc :: Range
nLoc    = Range
emptyRange
                        , nUnique :: Int
nUnique = Int
0x01
                        }

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

instance Semigroup PrimMap where
  PrimMap
x <> :: PrimMap -> PrimMap -> PrimMap
<> PrimMap
y = PrimMap :: Map PrimIdent Name -> Map PrimIdent Name -> PrimMap
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
primTypes :: Map PrimIdent Name
primDecls :: Map PrimIdent Name
primTypes :: PrimMap -> Map PrimIdent Name
primDecls :: PrimMap -> 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
primTypes :: Map PrimIdent Name
primDecls :: Map PrimIdent Name
primTypes :: PrimMap -> Map PrimIdent Name
primDecls :: PrimMap -> 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 ]