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

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

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

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

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

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

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


import           Cryptol.Parser.Name (PName)
import qualified Cryptol.Parser.Name as PName
import           Cryptol.Parser.Position (Range,Located(..))
import           Cryptol.Utils.Fixity
import           Cryptol.Utils.Ident
import           Cryptol.Utils.Panic
import           Cryptol.Utils.PP

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

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

                 , Name -> NameInfo
nInfo :: !NameInfo

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

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


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


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

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



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

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

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

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

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

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

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

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



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

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

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

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

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


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

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

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

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

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

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

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

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

-- | Compute a `PName` for the definition site corresponding to the given
-- `Name`.   Usually this is an unqualified name, but names that come
-- from module parameters are qualified with the corresponding parameter name.
nameToDefPName :: Name -> PName
nameToDefPName :: Name -> PName
nameToDefPName Name
n =
  case Name -> NameInfo
nInfo Name
n of
    GlobalName NameSource
_ OrigName
og -> OrigName -> PName
PName.origNameToDefPName OrigName
og
    LocalName Namespace
_ Ident
txt -> Ident -> PName
PName.mkUnqual Ident
txt

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

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

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

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

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


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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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


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

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

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

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

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

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

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

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

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

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

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

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