{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
module Cryptol.ModuleSystem.Name (
Name(), NameInfo(..)
, NameSource(..)
, nameUnique
, nameIdent
, nameInfo
, nameLoc
, nameFixity
, nameNamespace
, asPrim
, asOrigName
, ppLocName
, Namespace(..)
, ModPath(..)
, cmpNameDisplay
, mkDeclared
, mkParameter
, toParamInstName
, asParamName
, paramModRecParam
, FreshM(..), nextUniqueM
, SupplyT(), runSupplyT
, Supply(), emptySupply, nextUnique
, PrimMap(..)
, lookupPrimDecl
, lookupPrimType
) where
import Control.DeepSeq
import qualified Data.Map as Map
import qualified Data.Monoid as M
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.Position (Range,Located(..),emptyRange)
import Cryptol.Utils.Fixity
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
data NameInfo = Declared !ModPath !NameSource
| Parameter
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
, Name -> NameInfo
nInfo :: !NameInfo
, Name -> Namespace
nNamespace :: !Namespace
, Name -> Ident
nIdent :: !Ident
, 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
$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)
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 -> String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ ModPath -> Doc
forall a. PP a => a -> Doc
pp (OrigName -> ModPath
ogModule OrigName
og)
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
ppName :: Name -> Doc
ppName :: Name -> Doc
ppName Name
nm =
case Name -> Maybe OrigName
asOrigName Name
nm of
Just OrigName
og -> OrigName -> Doc
forall a. PP a => a -> Doc
pp OrigName
og
Maybe OrigName
Nothing -> Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
nm)
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
Namespace
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nNamespace :: Namespace
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nNamespace :: Name -> Namespace
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
Namespace
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nNamespace :: Namespace
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nNamespace :: Name -> Namespace
nInfo :: Name -> NameInfo
nUnique :: Name -> Int
.. } = Bool -> Doc -> Doc
optParens (Ident -> Bool
isInfixIdent Ident
nIdent) (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 :: 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
nameNamespace :: Name -> Namespace
nameNamespace :: Name -> Namespace
nameNamespace = Name -> Namespace
nNamespace
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
Namespace
Range
NameInfo
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nNamespace :: Namespace
nInfo :: NameInfo
nUnique :: Int
nLoc :: Name -> Range
nFixity :: Name -> Maybe Fixity
nIdent :: Name -> Ident
nNamespace :: Name -> Namespace
nInfo :: Name -> NameInfo
nUnique :: Name -> Int
.. } =
case NameInfo
nInfo of
Declared (TopModule ModName
m) 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
m (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 ModPath
m NameSource
s -> Name
n { nInfo :: NameInfo
nInfo = ModPath -> NameSource -> NameInfo
Declared ((ModName -> ModName) -> ModPath -> ModPath
apPathRoot ModName -> ModName
paramInstModName ModPath
m) NameSource
s }
NameInfo
Parameter -> Name
n
asParamName :: Name -> Name
asParamName :: Name -> Name
asParamName Name
n = Name
n { nInfo :: NameInfo
nInfo = NameInfo
Parameter }
asOrigName :: Name -> Maybe OrigName
asOrigName :: Name -> Maybe OrigName
asOrigName Name
nm =
case Name -> NameInfo
nInfo Name
nm of
Declared ModPath
p NameSource
_ ->
OrigName -> Maybe OrigName
forall a. a -> Maybe a
Just OrigName :: Namespace -> ModPath -> Ident -> OrigName
OrigName { ogModule :: ModPath
ogModule = (ModName -> ModName) -> ModPath -> ModPath
apPathRoot ModName -> ModName
notParamInstModName ModPath
p
, ogNamespace :: Namespace
ogNamespace = Name -> Namespace
nNamespace Name
nm
, ogName :: Ident
ogName = Name -> Ident
nIdent Name
nm
}
NameInfo
Parameter -> Maybe OrigName
forall a. Maybe a
Nothing
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
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 #-}
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)
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)
`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
nNamespace ModPath
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 = ModPath -> NameSource -> NameInfo
Declared ModPath
m NameSource
sys
in (Name :: Int
-> NameInfo -> Namespace -> Ident -> Maybe Fixity -> Range -> Name
Name { Int
Maybe Fixity
Ident
Namespace
Range
NameInfo
nInfo :: NameInfo
nUnique :: Int
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nNamespace :: Namespace
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nNamespace :: Namespace
nInfo :: NameInfo
nUnique :: Int
.. }, Supply
s')
mkParameter :: Namespace -> Ident -> Range -> Supply -> (Name,Supply)
mkParameter :: Namespace -> Ident -> Range -> Supply -> (Name, Supply)
mkParameter Namespace
nNamespace 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 -> Namespace -> Ident -> Maybe Fixity -> Range -> Name
Name { nInfo :: NameInfo
nInfo = NameInfo
Parameter, Int
Maybe Fixity
Ident
Namespace
Range
forall a. Maybe a
nFixity :: forall a. Maybe a
nUnique :: Int
nLoc :: Range
nIdent :: Ident
nNamespace :: Namespace
nLoc :: Range
nFixity :: Maybe Fixity
nIdent :: Ident
nNamespace :: Namespace
nUnique :: Int
.. }, Supply
s')
paramModRecParam :: Name
paramModRecParam :: Name
paramModRecParam = Name :: Int
-> NameInfo -> Namespace -> 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
, nNamespace :: Namespace
nNamespace = Namespace
NSValue
}
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
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 ]
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 ]