GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

Split out exports specs; add some parsing for functor instances.

Browse Source
This commit is contained in:
Iavor Diatchki 2017-10-02 15:01:45 -07:00
parent 7135284f80
commit 498b99cda3
9 changed files with 117 additions and 71 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol.cabal
View File

@ -110,6 +110,7 @@ library
Cryptol.ModuleSystem.Name,
Cryptol.ModuleSystem.NamingEnv,
Cryptol.ModuleSystem.Renamer,
Cryptol.ModuleSystem.Exports,
Cryptol.ModuleSystem.InstantiateModule,
Cryptol.TypeCheck,

61
src/Cryptol/ModuleSystem/Exports.hs Normal file
View File

@ -0,0 +1,61 @@
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.ModuleSystem.Exports where
import Data.Set(Set)
import qualified Data.Set as Set
import Data.Foldable(fold)
import Control.DeepSeq(NFData)
import GHC.Generics (Generic)
import Cryptol.Parser.AST
import Cryptol.Parser.Names
modExports :: Ord name => Module name -> ExportSpec name
modExports m = fold (concat [ exportedNames d | d <- mDecls m ])
where
names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ]
exportedNames (Decl td) = map exportBind (names namesD td)
++ map exportType (names tnamesD td)
exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt)
exportedNames (Include {}) = []
exportedNames (DParameterFun {}) = []
exportedNames (DParameterType {}) = []
exportedNames (DParameterConstraint {}) = []
data ExportSpec name = ExportSpec { eTypes :: Set name
, eBinds :: Set name
} deriving (Show, Generic)
instance NFData name => NFData (ExportSpec name)
instance Ord name => Monoid (ExportSpec name) where
mempty = ExportSpec { eTypes = mempty, eBinds = mempty }
mappend l r = ExportSpec { eTypes = mappend (eTypes l) (eTypes r)
, eBinds = mappend (eBinds l) (eBinds r)
}
-- | Add a binding name to the export list, if it should be exported.
exportBind :: Ord name => TopLevel name -> ExportSpec name
exportBind n
| tlExport n == Public = mempty { eBinds = Set.singleton (tlValue n) }
| otherwise = mempty
-- | Add a type synonym name to the export list, if it should be exported.
exportType :: Ord name => TopLevel name -> ExportSpec name
exportType n
| tlExport n == Public = mempty { eTypes = Set.singleton (tlValue n) }
| otherwise = mempty
-- | Check to see if a binding is exported.
isExportedBind :: Ord name => name -> ExportSpec name -> Bool
isExportedBind n = Set.member n . eBinds
-- | Check to see if a type synonym is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool
isExportedType n = Set.member n . eTypes

10
src/Cryptol/ModuleSystem/InstantiateModule.hs
View File

@ -12,7 +12,7 @@ import qualified Data.Map as Map
import MonadLib(Id,ReaderT,runReaderT,runId,ask)
import Cryptol.ModuleSystem.Name
import qualified Cryptol.Parser.AST as P
import Cryptol.ModuleSystem.Exports(ExportSpec(..))
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst(listSubst, apSubst)
import Cryptol.Utils.Ident(ModName)
@ -265,10 +265,10 @@ instance Inst UserTC where
inst env (UserTC x t) = UserTC y t
where y = Map.findWithDefault x x (tyNameMap env)
instance Inst (P.ExportSpec Name) where
inst env es = P.ExportSpec { eTypes = Set.map instT (P.eTypes es)
, eBinds = Set.map instV (P.eBinds es)
}
instance Inst (ExportSpec Name) where
inst env es = ExportSpec { eTypes = Set.map instT (eTypes es)
, eBinds = Set.map instV (eBinds es)
}
where instT x = Map.findWithDefault x x (tyNameMap env)
instV x = Map.findWithDefault x x (funNameMap env)

14
src/Cryptol/Parser.y
View File

@ -154,16 +154,10 @@ import Paths_cryptol
vmodule :: { Module PName }
: 'module' modName 'where' 'v{' vmod_body 'v}'
{ let (is,ts) = $5 in Module $2 is ts }
| 'v{' vmod_body 'v}'
{ let { (is,ts) = $2
-- XXX make a location from is and ts
; modName = Located { srcRange = emptyRange
, thing = mkModName ["Main"]
}
} in Module modName is ts }
: 'module' modName 'where' 'v{' vmod_body 'v}' { mkModule $2 $5 }
| 'module' modName '=' modName 'where' 'v{' vmod_body 'v}'
{ mkModuleInstance $2 $4 $7 }
| 'v{' vmod_body 'v}' { mkAnonymousModule $2 }
vmod_body :: { ([Located Import], [TopDecl PName]) }
: vimports 'v;' vtop_decls { (reverse $1, reverse $3) }

52
src/Cryptol/Parser/AST.hs
View File

@ -45,8 +45,6 @@ module Cryptol.Parser.AST
, BindDef(..), LBindDef
, Pragma(..)
, ExportType(..)
, ExportSpec(..), exportBind, exportType
, isExportedBind, isExportedType
, TopLevel(..)
, Import(..), ImportSpec(..)
, Newtype(..)
@ -80,7 +78,6 @@ import Cryptol.Utils.Ident
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import qualified Data.Set as Set
import Data.List(intersperse)
import Data.Bits(shiftR)
import Data.Maybe (catMaybes)
@ -108,10 +105,14 @@ type LString = Located String
newtype Program name = Program [TopDecl name]
deriving (Show)
data Module name = Module { mName :: Located ModName
, mImports :: [Located Import]
, mDecls :: [TopDecl name]
} deriving (Show, Generic, NFData)
-- | A parsed module.
data Module name = Module
{ mName :: Located ModName -- ^ Name of the module
, mInstance :: !(Maybe (Located ModName)) -- ^ Functor to instantiate
-- (if this is a functor instnaces)
, mImports :: [Located Import] -- ^ Imports for the module
, mDecls :: [TopDecl name] -- ^ Declartions for the module
} deriving (Show, Generic, NFData)
modRange :: Module name -> Range
@ -261,36 +262,6 @@ data TopLevel a = TopLevel { tlExport :: ExportType
deriving (Show, Generic, NFData, Functor, Foldable, Traversable)
data ExportSpec name = ExportSpec { eTypes :: Set.Set name
, eBinds :: Set.Set name
} deriving (Show, Generic, NFData)
instance Ord name => Monoid (ExportSpec name) where
mempty = ExportSpec { eTypes = mempty, eBinds = mempty }
mappend l r = ExportSpec { eTypes = mappend (eTypes l) (eTypes r)
, eBinds = mappend (eBinds l) (eBinds r)
}
-- | Add a binding name to the export list, if it should be exported.
exportBind :: Ord name => TopLevel name -> ExportSpec name
exportBind n
| tlExport n == Public = mempty { eBinds = Set.singleton (tlValue n) }
| otherwise = mempty
-- | Check to see if a binding is exported.
isExportedBind :: Ord name => name -> ExportSpec name -> Bool
isExportedBind n = Set.member n . eBinds
-- | Add a type synonym name to the export list, if it should be exported.
exportType :: Ord name => TopLevel name -> ExportSpec name
exportType n
| tlExport n == Public = mempty { eTypes = Set.singleton (tlValue n) }
| otherwise = mempty
-- | Check to see if a type synonym is exported.
isExportedType :: Ord name => name -> ExportSpec name -> Bool
isExportedType n = Set.member n . eTypes
-- | Infromation about the representation of a numeric constant.
data NumInfo = BinLit Int -- ^ n-digit binary literal
| OctLit Int -- ^ n-digit octal literal
@ -927,9 +898,10 @@ instance NoPos (Program name) where
noPos (Program x) = Program (noPos x)
instance NoPos (Module name) where
noPos m = Module { mName = mName m
, mImports = noPos (mImports m)
, mDecls = noPos (mDecls m)
noPos m = Module { mName = mName m
, mInstance = mInstance m
, mImports = noPos (mImports m)
, mDecls = noPos (mDecls m)
}
instance NoPos (TopDecl name) where

13
src/Cryptol/Parser/Names.hs
View File

@ -18,19 +18,6 @@ import qualified Data.Set as Set
import Data.Foldable (fold)
modExports :: Ord name => Module name -> ExportSpec name
modExports m = fold (concat [ exportedNames d | d <- mDecls m ])
where
names by td = [ td { tlValue = thing n } | n <- fst (by (tlValue td)) ]
exportedNames (Decl td) = map exportBind (names namesD td)
++ map exportType (names tnamesD td)
exportedNames (TDNewtype nt) = map exportType (names tnamesNT nt)
exportedNames (Include {}) = []
exportedNames (DParameterFun {}) = []
exportedNames (DParameterType {}) = []
exportedNames (DParameterConstraint {}) = []
-- | The names defined by a newtype.
tnamesNT :: Newtype name -> ([Located name], ())
tnamesNT x = ([ nName x ], ())

30
src/Cryptol/Parser/ParserUtils.hs
View File

@ -479,3 +479,33 @@ arithIdent = mkIdent (S.pack "Arith")
finIdent = mkIdent (S.pack "fin")
cmpIdent = mkIdent (S.pack "Cmp")
signedCmpIdent = mkIdent (S.pack "SignedCmp")
-- | Make an ordinary module
mkModule :: Located ModName ->
([Located Import], [TopDecl PName]) ->
Module PName
mkModule nm (is,ds) = Module { mName = nm
, mInstance = Nothing
, mImports = is
, mDecls = ds
}
-- | Make an unnamed module---gets the name @Main@.
mkAnonymousModule :: ([Located Import], [TopDecl PName]) ->
Module PName
mkAnonymousModule = mkModule Located { srcRange = emptyRange
, thing = mkModName [T.pack "Main"]
}
-- | Make a module which defines a functor instance.
mkModuleInstance :: Located ModName ->
Located ModName ->
([Located Import], [TopDecl PName]) ->
Module PName
mkModuleInstance nm fun (is,ds) =
Module { mName = nm
, mInstance = Just fun
, mImports = is
, mDecls = ds
}

5
src/Cryptol/TypeCheck/AST.hs
View File

@ -29,11 +29,12 @@ module Cryptol.TypeCheck.AST
) where
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Exports(ExportSpec(..)
, isExportedBind, isExportedType)
import Cryptol.Prims.Syntax
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Import(..), ImportSpec(..), ExportType(..)
, ExportSpec(..), isExportedBind
, isExportedType, Fixity(..))
, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type

2
src/Cryptol/TypeCheck/Infer.hs
View File

@ -18,7 +18,7 @@ module Cryptol.TypeCheck.Infer where
import Cryptol.ModuleSystem.Name (asPrim,lookupPrimDecl)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Parser.Names as P
import qualified Cryptol.ModuleSystem.Exports as P
import Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp)
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Solve