{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Cryptol.ModuleSystem.Name (
Name(), NameInfo(..)
, NameSource(..)
, nameUnique
, nameIdent
, mapNameIdent
, nameInfo
, nameLoc
, nameFixity
, nameNamespace
, nameToDefPName
, asPrim
, asOrigName
, nameModPath
, nameModPathMaybe
, nameTopModule
, nameTopModuleMaybe
, ppLocName
, Namespace(..)
, ModPath(..)
, cmpNameDisplay
, mkDeclared
, mkLocal
, asLocal
, mkModParam
, FreshM(..), nextUniqueM
, SupplyT(), runSupplyT, runSupply
, Supply(), emptySupply, nextUnique
, freshNameFor
, 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)
data Name = Name { Name -> Int
nUnique :: {-# UNPACK #-} !Int
, Name -> NameInfo
nInfo :: !NameInfo
, Name -> Maybe Fixity
nFixity :: !(Maybe Fixity)
, Name -> Range
nLoc :: !Range
} 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)
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) ->
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)
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
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
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)
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
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
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
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
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 ]
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
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
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
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 #-}
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)
emptySupply :: Supply
emptySupply :: Supply
emptySupply = Int -> Supply
Supply Int
0x1000
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)
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
}
}
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
}
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 ->
Ident ->
Range ->
Name ->
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
}
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]
}
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
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 ]
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 ]