mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-12 04:17:04 +03:00
Slight speedup in name comparison
This commit is contained in:
parent
28461e7b72
commit
98c49b875c
@ -11,6 +11,7 @@ module Cryptol.ModuleSystem.Base where
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
import Cryptol.ModuleSystem.Monad
|
||||
import Cryptol.ModuleSystem.Name (preludeName)
|
||||
import Cryptol.ModuleSystem.Env (lookupModule, LoadedModule(..)
|
||||
, meCoreLint, CoreLint(..))
|
||||
import qualified Cryptol.Eval as E
|
||||
@ -249,9 +250,6 @@ findFile path = do
|
||||
[] -> cantFindFile path
|
||||
possibleFiles paths = map (</> path) paths
|
||||
|
||||
preludeName :: P.ModName
|
||||
preludeName = P.mkModName ["Cryptol"]
|
||||
|
||||
-- | Add the prelude to the import list if it's not already mentioned.
|
||||
addPrelude :: P.Module -> P.Module
|
||||
addPrelude m
|
||||
|
@ -6,6 +6,10 @@ import Control.DeepSeq
|
||||
|
||||
import qualified Data.Text as Text
|
||||
|
||||
|
||||
preludeName :: ModName
|
||||
preludeName = mkModName ["Cryptol"]
|
||||
|
||||
type Ident = Text.Text
|
||||
|
||||
pack :: String -> Ident
|
||||
@ -30,7 +34,17 @@ data Name = Name Ident
|
||||
instance NFData Name
|
||||
|
||||
data QName = QName (Maybe ModName) Name
|
||||
deriving (Eq,Ord,Show,Generic)
|
||||
deriving (Show,Generic)
|
||||
|
||||
instance Eq QName where
|
||||
QName mb1 n1 == QName mb2 n2 = n1 == n2 && mb1 == mb2
|
||||
QName mb1 n1 /= QName mb2 n2 = n1 /= n2 && mb1 /= mb2
|
||||
|
||||
instance Ord QName where
|
||||
compare (QName mb1 n1) (QName mb2 n2) =
|
||||
case compare n1 n2 of
|
||||
EQ -> compare mb1 mb2
|
||||
r -> r
|
||||
|
||||
instance NFData QName
|
||||
|
||||
@ -46,11 +60,11 @@ mkName n = Name (pack n)
|
||||
-- XXX It would be nice to also mark this as a name that doesn't need to be
|
||||
-- resolved, if it's going to be created before renaming.
|
||||
mkPrim :: String -> QName
|
||||
mkPrim n = mkQual (ModName [pack "Cryptol"]) (Name (pack n))
|
||||
mkPrim n = mkQual preludeName (Name (pack n))
|
||||
|
||||
asPrim :: QName -> Maybe String
|
||||
asPrim (QName (Just (ModName [m])) (Name n))
|
||||
| m == pack "Cryptol" = Just (unpack n)
|
||||
asPrim (QName (Just m) (Name n))
|
||||
| m == preludeName = Just (unpack n)
|
||||
asPrim _ = Nothing
|
||||
|
||||
mkQual :: ModName -> Name -> QName
|
||||
|
@ -15,6 +15,7 @@
|
||||
module Cryptol.Prelude (writePreludeContents) where
|
||||
|
||||
import Cryptol.ModuleSystem.Monad
|
||||
import Cryptol.ModuleSystem.Name (preludeName)
|
||||
|
||||
#ifdef SELF_CONTAINED
|
||||
|
||||
@ -41,6 +42,6 @@ import Cryptol.Parser.AST as P
|
||||
|
||||
-- | If we're not self-contained, the Prelude is just missing
|
||||
writePreludeContents :: ModuleM FilePath
|
||||
writePreludeContents = moduleNotFound (P.ModName ["Cryptol"]) =<< getSearchPath
|
||||
writePreludeContents = moduleNotFound preludeName =<< getSearchPath
|
||||
|
||||
#endif
|
||||
|
@ -26,7 +26,7 @@ import Cryptol.Eval.Type(evalTF)
|
||||
import Cryptol.Eval.Value
|
||||
import Cryptol.Testing.Random (randomValue)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.ModuleSystem.Name (Ident, pack)
|
||||
import Cryptol.ModuleSystem.Name (Ident, pack, preludeName)
|
||||
|
||||
import Data.List (sortBy,transpose,genericTake,genericReplicate,genericSplitAt,genericIndex)
|
||||
import Data.Ord (comparing)
|
||||
@ -85,7 +85,7 @@ instance Bits Bool where
|
||||
|
||||
evalPrim :: Decl -> Value
|
||||
evalPrim Decl { dName = QName (Just m) (Name prim), .. }
|
||||
| m == mkModName ["Cryptol"], Just val <- Map.lookup prim primTable = val
|
||||
| m == preludeName, Just val <- Map.lookup prim primTable = val
|
||||
|
||||
evalPrim Decl { .. } =
|
||||
panic "Eval" [ "Unimplemented primitive", show dName ]
|
||||
|
@ -48,7 +48,7 @@ import Cryptol.REPL.Monad
|
||||
import Cryptol.REPL.Trie
|
||||
|
||||
import qualified Cryptol.ModuleSystem as M
|
||||
import qualified Cryptol.ModuleSystem.Base as M (preludeName)
|
||||
import qualified Cryptol.ModuleSystem.Name as M (preludeName)
|
||||
import qualified Cryptol.ModuleSystem.NamingEnv as M
|
||||
import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
|
||||
|
||||
|
@ -21,7 +21,7 @@ import Cryptol.Symbolic.Value
|
||||
import Cryptol.TypeCheck.AST (QName(..),Name(..),Decl(..),mkModName)
|
||||
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
|
||||
import Cryptol.Utils.Panic
|
||||
import Cryptol.ModuleSystem.Name (Ident, pack)
|
||||
import Cryptol.ModuleSystem.Name (Ident, pack, preludeName)
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
import qualified Data.Map as Map
|
||||
@ -37,7 +37,7 @@ traverseSnd f (x, y) = (,) x <$> f y
|
||||
|
||||
evalPrim :: Decl -> Value
|
||||
evalPrim Decl { dName = QName (Just m) (Name prim), .. }
|
||||
| m == mkModName ["Cryptol"], Just val <- Map.lookup prim primTable = val
|
||||
| m == preludeName, Just val <- Map.lookup prim primTable = val
|
||||
|
||||
evalPrim Decl { .. } =
|
||||
panic "Eval" [ "Unimplemented primitive", show dName ]
|
||||
|
@ -25,7 +25,7 @@ module Cryptol.TypeCheck.AST
|
||||
, Fixity(..)
|
||||
) where
|
||||
|
||||
import Cryptol.ModuleSystem.Name (mkQual, mkName)
|
||||
import Cryptol.ModuleSystem.Name (mkQual, mkName, preludeName)
|
||||
import Cryptol.Prims.Syntax
|
||||
import Cryptol.Parser.AST ( Name(..), Selector(..),Pragma(..), ppSelector
|
||||
, Import(..), ImportSpec(..), ExportType(..)
|
||||
@ -436,7 +436,7 @@ tBit :: Type
|
||||
tBit = TCon (TC TCBit) []
|
||||
|
||||
ePrim :: String -> Expr
|
||||
ePrim n = EVar (mkQual (mkModName ["Cryptol"]) (mkName n))
|
||||
ePrim n = EVar (mkQual preludeName (mkName n))
|
||||
|
||||
eTrue :: Expr
|
||||
eTrue = ePrim "True"
|
||||
|
Loading…
Reference in New Issue
Block a user