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

Checkpoint: functional top-level signatures?

Browse Source
This commit is contained in:
Iavor Diatchki 2022-06-08 10:26:21 -07:00
parent e08548dff0
commit 5f816c8ef5
23 changed files with 319 additions and 200 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Cryptol/ModuleSystem.hs
View File

@ -62,21 +62,21 @@ findModule :: P.ModName -> ModuleCmd ModulePath
findModule n env = runModuleM env (Base.findModule n)
-- | Load the module contained in the given file.
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.TCTopEntity)
loadModuleByPath path minp =
runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do
unloadModule ((InFile path ==) . lmFilePath)
m <- Base.loadModuleByPath path
setFocusedModule (T.mName m)
setFocusedModule (T.tcTopEntitytName m)
return (InFile path,m)
-- | Load the given parsed module.
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.TCTopEntity)
loadModuleByName n minp =
runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do
unloadModule ((n ==) . lmName)
(path,m') <- Base.loadModuleFrom False (FromModule n)
setFocusedModule (T.mName m')
setFocusedModule (T.tcTopEntitytName m')
return (path,m')
-- Extended Environments -------------------------------------------------------

117
src/Cryptol/ModuleSystem/Base.hs
View File

@ -44,8 +44,9 @@ import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..))
import Cryptol.ModuleSystem.Env (lookupModule
, LoadedModuleG(..), lmModule, lmInterface
import Cryptol.ModuleSystem.Env ( lookupModule
, lookupTCEntity
, LoadedModuleG(..), lmInterface
, meCoreLint, CoreLint(..)
, ModContext(..)
, ModulePath(..), modulePathLabel)
@ -67,7 +68,7 @@ import qualified Cryptol.TypeCheck.Sanity as TcSanity
import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
, preludeReferenceName, interactiveName, modNameChunks
, notParamInstModName, isParamInstModName )
, notParamInstModName )
import Cryptol.Utils.PP (pretty)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
@ -153,10 +154,10 @@ parseModule path = do
Left err -> moduleParseError path err
-- Modules ---------------------------------------------------------------------
-- Top Level Modules and Signatures ----------------------------------------------
-- | Load a module by its path.
loadModuleByPath :: FilePath -> ModuleM T.Module
loadModuleByPath :: FilePath -> ModuleM T.TCTopEntity
loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
let fileName = takeFileName path
foundPath <- findFile fileName
@ -172,23 +173,23 @@ loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
-- whether it's already been loaded
path' <- io (canonicalizePath foundPath)
case lookupModule n env of
case lookupTCEntity n env of
-- loadModule will calculate the canonical path again
Nothing -> doLoadModule False (FromModule n) (InFile foundPath) fp pm
Just lm
| path' == loaded -> return (lmModule lm)
| path' == loaded -> return (lmData lm)
| otherwise -> duplicateModuleName n path' loaded
where loaded = lmModuleId lm
-- | Load a module, unless it was previously loaded.
loadModuleFrom ::
Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.Module)
Bool {- ^ quiet mode -} -> ImportSource -> ModuleM (ModulePath,T.TCTopEntity)
loadModuleFrom quiet isrc =
do let n = importedModule isrc
mb <- getLoadedMaybe n
case mb of
Just m -> return (lmFilePath m, lmModule m)
Just m -> return (lmFilePath m, lmData m)
Nothing ->
do path <- findModule n
errorInFile path $
@ -203,34 +204,34 @@ doLoadModule ::
ModulePath ->
Fingerprint ->
P.Module PName ->
ModuleM T.Module
ModuleM T.TCTopEntity
doLoadModule quiet isrc path fp pm0 =
loading isrc $
do let pm = addPrelude pm0
loadDeps pm
let what = case P.mDef pm of
P.SignatureModule {} -> "signature"
_ -> "module"
unless quiet $ withLogger logPutStrLn
("Loading module " ++ pretty (P.thing (P.mName pm)))
("Loading " ++ what ++ " " ++ pretty (P.thing (P.mName pm)))
(nameEnv,tcmod) <- checkModule isrc path pm
tcm <- optionalInstantiate tcmod
(nameEnv,tcm) <- checkModule isrc path pm
-- extend the eval env, unless a functor.
tbl <- Concrete.primTable <$> getEvalOptsAction
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
callStacks <- getCallStacks
let ?callStacks = callStacks
unless (T.isParametrizedModule tcm)
$ modifyEvalEnv (E.moduleEnv Concrete tcm)
loadedModule path fp nameEnv tcm
case tcm of
T.TCTopModule m | not (T.isParametrizedModule m) ->
modifyEvalEnv (E.moduleEnv Concrete m)
_ -> pure ()
loadedModule path fp nameEnv tcm
return tcm
where
optionalInstantiate tcm
| isParamInstModName (importedModule isrc) =
failedToParameterizeModDefs (T.mName tcm)
| otherwise = return tcm
@ -279,20 +280,21 @@ findModule n = do
-- | Discover a file. This is distinct from 'findModule' in that we
-- assume we've already been given a particular file name.
findFile :: FilePath -> ModuleM FilePath
findFile path | isAbsolute path = do
-- No search path checking for absolute paths
b <- io (doesFileExist path)
if b then return path else cantFindFile path
findFile path = do
paths <- getSearchPath
loop (possibleFiles paths)
where
loop paths = case paths of
path':rest -> do
b <- io (doesFileExist path')
if b then return (normalise path') else loop rest
[] -> cantFindFile path
possibleFiles paths = map (</> path) paths
findFile path
| isAbsolute path =
do -- No search path checking for absolute paths
b <- io (doesFileExist path)
if b then return path else cantFindFile path
| otherwise =
do paths <- getSearchPath
loop (possibleFiles paths)
where
loop paths = case paths of
path' : rest ->
do b <- io (doesFileExist path')
if b then return (normalise path') else loop rest
[] -> cantFindFile path
possibleFiles paths = map (</> path) paths
-- | Add the prelude to the import list if it's not already mentioned.
addPrelude :: P.Module PName -> P.Module PName
@ -420,20 +422,13 @@ getPrimMap =
Nothing -> panic "Cryptol.ModuleSystem.Base.getPrimMap"
[ "Unable to find the prelude" ]
-- | Load a module, be it a normal module or a functor instantiation.
checkModule ::
ImportSource -> ModulePath -> P.Module PName ->
ModuleM (R.NamingEnv, T.Module)
checkModule isrc path m = checkSingleModule T.tcModule isrc path m
-- | Typecheck a single module.
checkSingleModule ::
Act (P.Module Name) T.Module {- ^ how to check -} ->
ImportSource {- ^ why are we loading this -} ->
ModulePath {- path -} ->
P.Module PName {- ^ module to check -} ->
ModuleM (R.NamingEnv,T.Module)
checkSingleModule how isrc path m = do
checkModule ::
ImportSource {- ^ why are we loading this -} ->
ModulePath {- path -} ->
P.Module PName {- ^ module to check -} ->
ModuleM (R.NamingEnv,T.TCTopEntity)
checkModule isrc path m = do
-- check that the name of the module matches expectations
let nm = importedModule isrc
@ -475,21 +470,22 @@ checkSingleModule how isrc path m = do
else getPrimMap
-- typecheck
let act = TCAction { tcAction = how
, tcLinter = moduleLinter (P.thing (P.mName m))
let act = TCAction { tcAction = T.tcModule
, tcLinter = tcTopEntitytLinter (P.thing (P.mName m))
, tcPrims = prims }
tcm0 <- typecheck act (R.rmModule renMod) mempty (R.rmImported renMod)
tcm <- typecheck act (R.rmModule renMod) mempty (R.rmImported renMod)
let tcm = tcm0 -- fromMaybe tcm0 (addModParams tcm0)
rewMod <- liftSupply (`rewModule` tcm)
rewMod <- case tcm of
T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo)
T.TCTopSignature {} -> pure tcm
pure (R.rmInScope renMod,rewMod)
data TCLinter o = TCLinter
{ lintCheck ::
o -> T.InferInput -> Either (Range, TcSanity.Error) [TcSanity.ProofObligation]
o -> T.InferInput ->
Either (Range, TcSanity.Error) [TcSanity.ProofObligation]
, lintModule :: Maybe P.ModName
}
@ -524,6 +520,17 @@ moduleLinter m = TCLinter
, lintModule = Just m
}
tcTopEntitytLinter :: P.ModName -> TCLinter T.TCTopEntity
tcTopEntitytLinter m = TCLinter
{ lintCheck = \m' i -> case m' of
T.TCTopModule mo ->
lintCheck (moduleLinter m) mo i
T.TCTopSignature {} -> Right []
-- XXX: what can we lint about a signature
, lintModule = Just m
}
type Act i o = i -> T.InferInput -> IO (T.InferOutput o)
data TCAction i o = TCAction

3
src/Cryptol/ModuleSystem/Binds.hs
View File

@ -15,6 +15,7 @@ module Cryptol.ModuleSystem.Binds
, newModParam
, InModule(..)
, ifaceToMod
, ifaceSigToMod
, modToMap
, defsOf
) where
@ -150,7 +151,7 @@ topModuleDefs m =
case mDef m of
NormalModule ds -> TopMod mname <$> declsToMod (Just (TopModule mname)) ds
FunctorInstance f as _ -> pure (TopInst mname (thing f) as)
SignatureModule s -> TopSig mname <$> sigToMod (TopModule mname) s
SignatureModule s -> TopMod mname <$> sigToMod (TopModule mname) s
where
mname = thing (mName m)

42
src/Cryptol/ModuleSystem/Env.hs
View File

@ -35,6 +35,7 @@ import Control.Monad (guard,mplus)
import qualified Control.Exception as X
import Data.Function (on)
import Data.Set(Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Semigroup
@ -303,9 +304,22 @@ data LoadedModules = LoadedModules
} deriving (Show, Generic, NFData)
getLoadedEntities ::
LoadedModules -> Map ModName (Either LoadedSignature LoadedModule)
getLoadedEntities lm =
Map.fromList $ [ (lmName x, Right x) | x <- lmLoadedModules lm ] ++
[ (lmName x, Right x) | x <- lmLoadedParamModules lm ] ++
[ (lmName x, Left x) | x <- lmLoadedSignatures lm ]
getLoadedModules :: LoadedModules -> [LoadedModule]
getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x
getLoadedNames :: LoadedModules -> Set ModName
getLoadedNames lm = Set.fromList
$ map lmName (lmLoadedModules lm)
++ map lmName (lmLoadedParamModules lm)
++ map lmName (lmLoadedSignatures lm)
instance Semigroup LoadedModules where
l <> r = LoadedModules
{ lmLoadedModules = List.unionBy ((==) `on` lmName)
@ -365,12 +379,22 @@ type LoadedSignature = LoadedModuleG T.ModParamNames
-- | Has this module been loaded already.
isLoaded :: ModName -> LoadedModules -> Bool
isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)
isLoaded mn lm = mn `Set.member` getLoadedNames lm
-- | Is this a loaded parameterized module.
isLoadedParamMod :: ModName -> LoadedModules -> Bool
isLoadedParamMod mn ln = any ((mn ==) . lmName) (lmLoadedParamModules ln)
lookupTCEntity :: ModName -> ModuleEnv -> Maybe (LoadedModuleG T.TCTopEntity)
lookupTCEntity m env =
case lookupModule m env of
Just lm -> pure lm { lmData = T.TCTopModule (lmModule lm) }
Nothing ->
do lm <- lookupSignature m env
pure lm { lmData = T.TCTopSignature m (lmData lm) }
-- | Try to find a previously loaded module
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules
@ -381,6 +405,22 @@ lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature
lookupSignature mn me =
List.find ((mn ==) . lmName) (lmLoadedSignatures (meLoadedModules me))
addLoadedSignature ::
ModulePath -> String -> Fingerprint -> R.NamingEnv ->
ModName -> T.ModParamNames ->
LoadedModules -> LoadedModules
addLoadedSignature path ident fp nameEnv nm si lm
| isLoaded nm lm = lm
| otherwise = lm { lmLoadedSignatures = loaded : lmLoadedSignatures lm }
where
loaded = LoadedModule
{ lmName = nm
, lmFilePath = path
, lmModuleId = ident
, lmNamingEnv = nameEnv
, lmData = si
, lmFingerprint = fp
}
-- | Add a freshly loaded module. If it was previously loaded, then
-- the new version is ignored.

39
src/Cryptol/ModuleSystem/Monad.hs
View File

@ -19,6 +19,7 @@ import Cryptol.Eval (EvalEnv,EvalOpts(..))
import qualified Cryptol.Backend.Monad as E
import Cryptol.ModuleSystem.Env
import qualified Cryptol.ModuleSystem.Env as MEnv
import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
@ -45,7 +46,6 @@ import Control.Exception (IOException)
import Data.ByteString (ByteString)
import Data.Function (on)
import Data.Map (Map)
import Data.Maybe (isJust)
import Data.Text.Encoding.Error (UnicodeException)
import MonadLib
import System.Directory (canonicalizePath)
@ -426,13 +426,17 @@ modifyModuleEnv f = ModuleT $ do
env <- get
set $! f env
getLoadedMaybe :: P.ModName -> ModuleM (Maybe LoadedModule)
getLoadedMaybe :: P.ModName -> ModuleM (Maybe (LoadedModuleG T.TCTopEntity))
getLoadedMaybe mn = ModuleT $
do env <- get
return (lookupModule mn env)
return (lookupTCEntity mn env)
-- | This checks if the given name is loaded---it might refer to either
-- a module or a signature.
isLoaded :: P.ModName -> ModuleM Bool
isLoaded mn = isJust <$> getLoadedMaybe mn
isLoaded mn =
do env <- ModuleT get
pure (MEnv.isLoaded mn (meLoadedModules env))
loadingImport :: Located P.Import -> ModuleM a -> ModuleM a
loadingImport = loading . FromImport
@ -466,16 +470,15 @@ getImportSource = ModuleT $ do
is : _ -> return is
_ -> return (FromModule noModuleName)
getIface :: P.ModName -> ModuleM Iface
getIface mn = ($ mn) <$> getIfaces
getIfaces :: ModuleM (P.ModName -> Iface)
getIfaces = doLookup <$> ModuleT get
getIfaces :: ModuleM (Map P.ModName (Either T.ModParamNames Iface))
getIfaces = toMap <$> ModuleT get
where
doLookup env = \mn ->
case lookupModule mn env of
Just lm -> lmInterface lm
Nothing -> panic "ModuleSystem" ["Interface not available", show (pp mn)]
toMap env = cvt <$> getLoadedEntities (meLoadedModules env)
cvt ent =
case ent of
Left sig -> Left (lmData sig)
Right mo -> Right (lmdInterface (lmData mo))
getLoaded :: P.ModName -> ModuleM T.Module
getLoaded mn = ModuleT $
@ -528,15 +531,19 @@ unloadModule rm = ModuleT $ do
set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
loadedModule ::
ModulePath -> Fingerprint -> NamingEnv -> T.Module -> ModuleM ()
ModulePath -> Fingerprint -> NamingEnv -> T.TCTopEntity -> ModuleM ()
loadedModule path fp nameEnv m = ModuleT $ do
env <- get
ident <- case path of
InFile p -> unModuleT $ io (canonicalizePath p)
InMem l _ -> pure l
set $! env { meLoadedModules = addLoadedModule path ident fp nameEnv m
(meLoadedModules env) }
let newLM = case m of
T.TCTopModule mo -> addLoadedModule path ident fp nameEnv mo
T.TCTopSignature x s ->
addLoadedSignature path ident fp nameEnv x s
set $! env { meLoadedModules = newLM (meLoadedModules env) }
modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
modifyEvalEnv f = ModuleT $ do

13
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -140,7 +140,7 @@ renameModule m0 =
mapM_ recordError errs
-- Step 3: resolve imports
extern <- getExternalMods
extern <- getExternal
resolvedMods <- liftSupply (resolveImports extern defs)
let pathToName = Map.fromList [ (Nested (nameModPath x) (nameIdent x), x)
@ -183,7 +183,7 @@ renameTopDecls m ds0 =
mapM_ recordError errs
-- Step 3: resolve imports
extern <- getExternalMods
extern <- getExternal
resolvedMods <- liftSupply (resolveImports extern (TopMod m defs))
let pathToName = Map.fromList [ (Nested (nameModPath x) (nameIdent x), x)
@ -276,7 +276,10 @@ checkFunctorArgs args =
mkInstMap :: Maybe Range -> Map Name Name -> ImpName Name -> ImpName Name ->
RenameM (Map Name Name)
mkInstMap checkFun acc0 ogname iname =
do (onames,osubs) <- lookupDefinesAndSubs checkFun ogname
do case checkFun of
Nothing -> pure ()
Just r -> checkIsModule r ogname AFunctor
(onames,osubs) <- lookupDefinesAndSubs ogname
inames <- lookupDefines iname
let mp = zipByTextName onames inames
subs = [ (ImpNested k, ImpNested v)
@ -557,6 +560,10 @@ doModParam mp =
sigName' <-
case thing sigName of
ImpTop t -> pure (ImpTop t)
-- XXX: should we record a dpendency here?
-- Not sure what the dependencies are for..
-- Not sure what the dependencies are for..
ImpNested n ->
do nm <- resolveName NameUse NSModule n
case modPathCommon me (nameModPath nm) of

161
src/Cryptol/ModuleSystem/Renamer/Monad.hs
View File

@ -23,12 +23,14 @@ import MonadLib hiding (mapM, mapM_)
import Prelude ()
import Prelude.Compat
import Cryptol.Utils.PP(pp)
import Cryptol.Utils.Panic(panic)
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.NamingEnv
import Cryptol.ModuleSystem.Binds
import Cryptol.ModuleSystem.Interface
import Cryptol.Parser.AST
import Cryptol.TypeCheck.AST(ModParamNames)
import Cryptol.Parser.Position
import Cryptol.Utils.Ident(modPathCommon,OrigName(..))
@ -44,16 +46,19 @@ data RenamerInfo = RenamerInfo
{ renSupply :: Supply -- ^ Use to make new names
, renContext :: ModPath -- ^ We are renaming things in here
, renEnv :: NamingEnv -- ^ This is what's in scope
, renIfaces :: ModName -> Iface
, renIfaces :: Map ModName (Either ModParamNames Iface)
-- ^ External modules
}
newtype RenameM a = RenameM { unRenameM :: ReaderT RO (StateT RW Lift) a }
data RO = RO
{ roLoc :: Range
, roNames :: NamingEnv
, roIfaces :: ModName -> Iface
, roCurMod :: ModPath -- ^ Current module we are working on
{ roLoc :: Range
, roNames :: NamingEnv
, roExternal :: Map ModName (Maybe Iface, Map (ImpName Name) (Mod ()))
-- ^ Externally loaded modules. `Mod` is defined in 'Cryptol.Renamer.Binds'.
, roCurMod :: ModPath -- ^ Current module we are working on
, roNestedMods :: Map ModPath Name
{- ^ Maps module paths to the actual name for it. This is used
@ -167,7 +172,7 @@ runRenamer info m = (res, warns)
ro = RO { roLoc = emptyRange
, roNames = renEnv info
, roIfaces = renIfaces info
, roExternal = Map.mapWithKey toModMap (renIfaces info)
, roCurMod = renContext info
, roNestedMods = Map.empty
, roResolvedModules = mempty
@ -178,6 +183,12 @@ runRenamer info m = (res, warns)
res | Set.null (rwErrors rw) = Right (a,rwSupply rw)
| otherwise = Left (Set.toList (rwErrors rw))
toModMap t ent =
case ent of
Left ps -> (Nothing, Map.singleton (ImpTop t) (ifaceSigToMod ps))
Right i -> (Just i, modToMap (ImpTop t) (ifaceToMod i) mempty)
setCurMod :: ModPath -> RenameM a -> RenameM a
setCurMod mpath (RenameM m) =
@ -395,6 +406,35 @@ warnUnused m0 env rw =
sys == UserName && m == m0 && nm `Set.notMember` oldNames
LocalName {} -> True
getExternal :: RenameM (ImpName Name -> Mod ())
getExternal =
do mp <- roExternal <$> RenameM ask
pure \nm -> let mb = do t <- case nm of
ImpTop t -> pure t
ImpNested x -> nameTopModuleMaybe x
(_,mp1) <- Map.lookup t mp
Map.lookup nm mp1
in case mb of
Just m -> m
Nothing -> panic "getExternal"
["Missing external name", show (pp nm) ]
getExternalMod :: ImpName Name -> RenameM (Mod ())
getExternalMod nm = ($ nm) <$> getExternal
-- | Returns `Nothing` if the name does not refer to a module (i.e., it is a sig)
getTopModuleIface :: ImpName Name -> RenameM (Maybe Iface)
getTopModuleIface nm =
do mp <- roExternal <$> RenameM ask
let t = case nm of
ImpTop t' -> t'
ImpNested x -> nameTopModule x
case Map.lookup t mp of
Just (mb, _) -> pure mb
Nothing -> panic "getTopModuleIface"
["Missing external module", show (pp nm) ]
{- | Record an import:
* record external dependency if the name refers to an external import
* record an error if the imported thing is a functor
@ -407,54 +447,25 @@ recordImport r i =
case rmodKind loc of
AModule -> pure ()
k -> recordError (ModuleKindMismatch r i AModule k)
Nothing
| Just topName <- case i of
ImpTop m -> Just m
ImpNested n -> nameTopModuleMaybe n
-> do let iface = roIfaces ro topName
RenameM $ sets_ \s ->
s { rwExternalDeps = ifPublic iface <>
rwExternalDeps s }
when (ifaceIsFunctor iface)
(recordError (ModuleKindMismatch r i AModule AFunctor))
-- XXX: This could be a signature, but we don't have top
-- signature interfaces.
-- This may happen if encoutnered an error (e.g., undefined name)
| otherwise -> pure ()
Nothing ->
do mb <- getTopModuleIface i
case mb of
Nothing -> recordError (ModuleKindMismatch r i AModule ASignature)
Just iface
| ifaceIsFunctor iface ->
recordError (ModuleKindMismatch r i AModule AFunctor)
| otherwise ->
RenameM $ sets_ \s -> s { rwExternalDeps = ifPublic iface <>
rwExternalDeps s }
-- XXX: Maybe we'd want to cache some of the conversion to Mod?
-- | This gives the loaded *external* modules.
-- XXX: For now, this does *not* include top-level signatures, as we have no
-- interface type for them yet.
getExternalModsMaybe :: RenameM (ImpName Name -> Maybe (Mod ()))
getExternalModsMaybe =
do getIf <- RenameM (roIfaces <$> ask)
pure \nm ->
case nm of
ImpTop m -> Just (ifaceToMod (getIf m))
ImpNested n ->
do top <- nameTopModuleMaybe n
let mp = modToMap (ImpTop top) (ifaceToMod (getIf top)) Map.empty
Map.lookup nm mp
getExternalMods :: RenameM (ImpName Name -> Mod ())
getExternalMods =
do f <- getExternalModsMaybe
pure \x -> case f x of
Just a -> a
Nothing -> panic "getExternalMods"
[ "Module not loaded", show x ]
-- | Lookup a name either in the locally resolved thing or in an external module
lookupModuleThing :: ImpName Name -> RenameM (Either ResolvedLocal (Mod ()))
lookupModuleThing nm =
do ro <- RenameM ask
case Map.lookup nm (roResolvedModules ro) of
Just loc -> pure (Left loc)
Nothing ->
do loaded <- getExternalMods
pure (Right (loaded nm))
Nothing -> Right <$> getExternalMod nm
lookupDefines :: ImpName Name -> RenameM NamingEnv
lookupDefines nm =
@ -465,48 +476,22 @@ lookupDefines nm =
checkIsModule :: Range -> ImpName Name -> ModKind -> RenameM ()
checkIsModule r nm expect =
do ro <- RenameM ask
actual <- case Map.lookup nm (roResolvedModules ro) of
Just loc -> pure (rmodKind loc)
Nothing ->
do loaded <- getExternalMods
pure (modKind (loaded nm))
do thing <- lookupModuleThing nm
let actual = case thing of
Left rmod -> rmodKind rmod
Right mo -> modKind mo
unless (actual == expect)
(recordError (ModuleKindMismatch r nm expect actual))
lookupDefinesAndSubs ::
Maybe Range -> ImpName Name -> RenameM (NamingEnv, Set Name)
lookupDefinesAndSubs checkFun nm =
do ro <- RenameM ask
case Map.lookup nm (roResolvedModules ro) of
Just loc ->
do case checkFun of
Just r ->
case rmodKind loc of
AFunctor -> pure ()
k -> recordError (ModuleKindMismatch r nm AFunctor k)
Nothing -> pure ()
pure (rmodDefines loc, rmodNested loc)
Nothing ->
do mb <- ($ nm) <$> getExternalModsMaybe
case mb of
Nothing -> pure ( mempty, Set.empty )
Just m ->
do case checkFun of
Just r ->
case modKind m of
AFunctor -> pure ()
k -> recordError (ModuleKindMismatch r nm AFunctor k)
Nothing -> pure ()
pure ( modDefines m
, Set.unions [ Map.keysSet (modMods m)
, Map.keysSet (modInstances m)
]
)
lookupDefinesAndSubs :: ImpName Name -> RenameM (NamingEnv, Set Name)
lookupDefinesAndSubs nm =
do thing <- lookupModuleThing nm
pure case thing of
Left rmod -> ( rmodDefines rmod, rmodNested rmod)
Right m ->
( modDefines m
, Set.unions [ Map.keysSet (modMods m)
, Map.keysSet (modInstances m)
]
)

12
src/Cryptol/Parser.y
View File

@ -84,7 +84,7 @@ import Paths_cryptol
'if' { Located $$ (Token (KW KW_if ) _)}
'then' { Located $$ (Token (KW KW_then ) _)}
'else' { Located $$ (Token (KW KW_else ) _)}
'signature' { Located $$ (Token (KW KW_signature) _)}
'interface' { Located $$ (Token (KW KW_interface) _)}
'x' { Located $$ (Token (KW KW_x) _)}
'down' { Located $$ (Token (KW KW_down) _)}
'by' { Located $$ (Token (KW KW_by) _)}
@ -168,7 +168,8 @@ import Paths_cryptol
top_module :: { [Module PName] }
: 'module' module_def { mkTopMods $2 }
| 'v{' vmod_body 'v}' { [mkAnonymousModule $2] }
| 'interface' 'module' modName 'where' 'v{' sig_body 'v}'
{ mkTopSig $3 $6 }
module_def :: { Module PName }
@ -288,8 +289,8 @@ vtop_decl :: { [TopDecl PName] }
-- currently that odcumentation is just discarded
sig_def :: { (Located PName, Signature PName) }
: 'signature' name 'where' 'v{' sig_body 'v}'
{ ($2, $5) }
: 'interface' 'submodule' name 'where' 'v{' sig_body 'v}'
{ ($3, $6) }
sig_body :: { Signature PName }
: par_decls { mkSignature [] $1 }
@ -299,7 +300,7 @@ sig_body :: { Signature PName }
mod_param_decl :: { ModParam PName }
: mbDoc
'import' 'signature'
'import' 'interface'
impName mbAs { ModParam { mpSignature = $4
, mpAs = fmap thing $5
, mpName = mkModParamName $4 $5
@ -845,6 +846,7 @@ smodName :: { Located ModName }
modName :: { Located ModName }
: smodName { $1 }
| 'module' smodName { $2 }
| '`' smodName { fmap paramInstModName $2 }

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

@ -250,7 +250,7 @@ data TopDecl name =
| DModule (TopLevel (NestedModule name)) -- ^ @submodule M where ...@
| DImport (Located (ImportG (ImpName name))) -- ^ @import X@
| DModParam (ModParam name) -- ^ @import signature X ...@
| DModParam (ModParam name) -- ^ @import interface X ...@
deriving (Show, Generic, NFData)
data ModuleInstanceArgs name =
@ -291,8 +291,6 @@ data Decl name = DSignature [Located name] (Schema name)
-- | A type parameter for a module.
-- This is used in the OLD module system, as well as in signatures of
-- the NEW module system.
data ParameterType name = ParameterType
{ ptName :: Located name -- ^ name of type parameter
, ptKind :: Kind -- ^ kind of parameter
@ -302,8 +300,6 @@ data ParameterType name = ParameterType
} deriving (Eq,Show,Generic,NFData)
-- | A value parameter for a module.
-- This is used in the OLD module system, as well as in signatures of
-- the NEW module system.
data ParameterFun name = ParameterFun
{ pfName :: Located name -- ^ name of value parameter
, pfSchema :: Schema name -- ^ schema for parameter
@ -312,13 +308,15 @@ data ParameterFun name = ParameterFun
} deriving (Eq,Show,Generic,NFData)
{- | Module signatures (aka types of functor arguments)
This is part of the NEW module system.
{- | Interface Modules (aka types of functor arguments)
Note that the names *defined* in a signature are only really used in the
other members of a signature. When a signature is "imported" as a functor
parameter these names are instantiated to new names, because there could
be multiple paramers using the same signature. -}
IMPORTANT: Interface Modules are a language construct and are different from
the notion of "interface" in the Cyrptol implementation.
Note that the names *defined* in an interface module are only really used in the
other members of the interface module. When an interface module is "imported"
as a functor parameter these names are instantiated to new names,
because there could be multiple paramers using the same interface. -}
data Signature name = Signature
{ sigImports :: ![Located (ImportG (ImpName name))]
-- ^ Add things in scope
@ -329,11 +327,11 @@ data Signature name = Signature
{- | A module parameter declaration.
> import signature A
> import signature A as B
> import interface A
> import interface A as B
The name of the parameter is derived from the `as` clause. If there
is no `as` clause then it is derived from the name of the signature.
is no `as` clause then it is derived from the name of the interface module.
If there is no `as` clause, then the type/value parameters are unqualified,
and otherwise they are qualified.

6
src/Cryptol/Parser/Layout.hs
View File

@ -64,7 +64,11 @@ layout isMod ts0
| let t = head ts0
rng = srcRange t
blockCol = max 1 (col (from rng)) -- see startImplicitBlock
, isMod && tokenType (thing t) /= KW KW_module =
implictMod = case map (tokenType . thing) ts0 of
KW KW_module : _ -> False
KW KW_interface : KW KW_module : _ -> False
_ -> True
, isMod && implictMod =
virt rng VCurlyL : go [ Virtual blockCol ] blockCol True ts0
| otherwise =

2
src/Cryptol/Parser/Lexer.x
View File

@ -104,6 +104,7 @@ $white+ { emit $ White Space }
"include" { emit $ KW KW_include }
"module" { emit $ KW KW_module }
"submodule" { emit $ KW KW_submodule }
"interface" { emit $ KW KW_interface }
"newtype" { emit $ KW KW_newtype }
"pragma" { emit $ KW KW_pragma }
"property" { emit $ KW KW_property }
@ -118,7 +119,6 @@ $white+ { emit $ White Space }
"newtype" { emit $ KW KW_newtype }
"down" { emit $ KW KW_down }
"by" { emit $ KW KW_by }
"signature" { emit $ KW KW_signature }
"infixl" { emit $ KW KW_infixl }
"infixr" { emit $ KW KW_infixr }

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

@ -954,6 +954,13 @@ mkTopMods mo =
_ -> [mo]
mkTopSig :: Located ModName -> Signature PName -> [Module PName]
mkTopSig nm sig =
[ Module { mName = nm
, mDef = SignatureModule sig
}
]
-- XXX: This is wrong.
-- The signautre should go outside of the functor that uses it.
mkModBody :: [TopDecl PName] -> [TopDecl PName]

2
src/Cryptol/Parser/Token.hs
View File

@ -50,7 +50,7 @@ data TokenKW = KW_else
| KW_primitive
| KW_parameter
| KW_constraint
| KW_signature
| KW_interface
| KW_Prop
| KW_by
| KW_down

8
src/Cryptol/REPL/Command.hs
View File

@ -1150,10 +1150,14 @@ loadCmd path
}
loadHelper (M.loadModuleByPath path)
loadHelper :: M.ModuleCmd (M.ModulePath,T.Module) -> REPL ()
loadHelper :: M.ModuleCmd (M.ModulePath,T.TCTopEntity) -> REPL ()
loadHelper how =
do clearLoadedMod
(path,m) <- liftModuleCmd how
(path,ent) <- liftModuleCmd how
m <- case ent of
T.TCTopModule mo -> pure mo
T.TCTopSignature {} -> raise CannotLoadASignature
whenDebug (rPutStrLn (dump m))
setLoadedMod LoadedModule
{ lName = Just (T.mName m)

3
src/Cryptol/REPL/Monad.hs
View File

@ -15,6 +15,7 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.REPL.Monad (
-- * REPL Monad
@ -328,6 +329,7 @@ data REPLException
| TooWide WordTooWide
| Unsupported Unsupported
| ModuleSystemError NameDisp M.ModuleError
| CannotLoadASignature
| EvalPolyError T.Schema
| TypeNotTestable T.Type
| EvalInParamModule [M.Name]
@ -367,6 +369,7 @@ instance PP REPLException where
SBVException e -> text "SBV exception:" $$ text (show e)
SBVPortfolioException e -> text "SBV exception:" $$ text (show e)
W4Exception e -> text "What4 exception:" $$ text (show e)
CannotLoadASignature -> "Cannot load signatures"
-- | Raise an exception.
raise :: REPLException -> REPL a

4
src/Cryptol/Symbolic/SBV.hs
View File

@ -298,7 +298,9 @@ prepareQuery ::
ProverCommand ->
M.ModuleT IO (Either String ([FinType], SBV.Symbolic SBV.SVal))
prepareQuery evo ProverCommand{..} =
do ds <- do (_mp, m) <- M.loadModuleFrom True (M.FromModule preludeReferenceName)
do ds <- do (_mp, ent) <- M.loadModuleFrom True (M.FromModule preludeReferenceName)
let m = tcTopEntityToModule ent
let decls = mDecls m
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (M.genIface m)))
let ds = Map.fromList [ (prelPrim (identText (M.nameIdent nm)), EWhere (EVar nm) decls) | nm <- nms ]

3
src/Cryptol/Symbolic/What4.hs
View File

@ -333,7 +333,8 @@ prepareQuery sym ProverCommand { .. } = do
do let lPutStrLn = M.withLogger logPutStrLn
when pcVerbose (lPutStrLn "Simulating...")
ds <- do (_mp, m) <- M.loadModuleFrom True (M.FromModule preludeReferenceName)
ds <- do (_mp, ent) <- M.loadModuleFrom True (M.FromModule preludeReferenceName)
let m = tcTopEntityToModule ent
let decls = mDecls m
let nms = fst <$> Map.toList (M.ifDecls (M.ifPublic (M.genIface m)))
let ds = Map.fromList [ (prelPrim (identText (M.nameIdent nm)), EWhere (EVar nm) decls) | nm <- nms ]

2
src/Cryptol/TypeCheck.hs
View File

@ -55,7 +55,7 @@ import Cryptol.Utils.Panic(panic)
tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
tcModule :: P.Module Name -> InferInput -> IO (InferOutput TCTopEntity)
tcModule m inp = runInferM inp (inferTopModule m)
tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))

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

@ -28,6 +28,8 @@ module Cryptol.TypeCheck.AST
, module Cryptol.TypeCheck.Type
) where
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
import Cryptol.Parser.Position(Located,Range,HasLoc(..))
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Interface
@ -37,7 +39,6 @@ import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Import
, ImportG(..), ImportSpec(..), ExportType(..)
, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
import Cryptol.Utils.RecordMap
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
@ -53,6 +54,25 @@ import qualified Data.IntMap as IntMap
import Data.Text (Text)
data TCTopEntity =
TCTopModule (ModuleG ModName)
| TCTopSignature ModName ModParamNames
deriving (Show, Generic, NFData)
tcTopEntitytName :: TCTopEntity -> ModName
tcTopEntitytName ent =
case ent of
TCTopModule m -> mName m
TCTopSignature m _ -> m
-- | Panics if the entity is not a module
tcTopEntityToModule :: TCTopEntity -> Module
tcTopEntityToModule ent =
case ent of
TCTopModule m -> m
TCTopSignature {} -> panic "tcTopEntityToModule" [ "Not a module" ]
-- | A Cryptol module.
data ModuleG mname =
Module { mName :: !mname

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

@ -64,7 +64,7 @@ import Control.Monad(zipWithM,unless,foldM,forM_,mplus)
inferTopModule :: P.Module Name -> InferM Module
inferTopModule :: P.Module Name -> InferM TCTopEntity
inferTopModule m =
case P.mDef m of
P.NormalModule ds ->
@ -80,6 +80,12 @@ inferTopModule m =
Just mo -> pure mo
Nothing -> panic "inferModule" ["Didnt' get a module"]
P.SignatureModule sig ->
do newTopSignatureScope (thing (P.mName m))
checkSignature sig
endTopSignature
-- | Construct a Prelude primitive in the parsed AST.

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

@ -32,7 +32,7 @@ doFunctorInst ::
{- ^ Instantitation. These is the renaming for the functor that arises from
generativity (i.e., it is something that will make the names "fresh").
-} ->
InferM (Maybe Module)
InferM (Maybe TCTopEntity)
doFunctorInst m f as inst =
inRange (srcRange m)
do mf <- lookupFunctor (thing f)

22
src/Cryptol/TypeCheck/Monad.hs
View File

@ -214,6 +214,7 @@ data ScopeName = ExternalScope
| LocalScope
| SubModule Name
| SignatureScope Name (Maybe Text) -- ^ The Text is docs
| TopSignatureScope P.ModName
| MTopModule P.ModName
-- | Read-only component of the monad.
@ -900,6 +901,9 @@ newSignatureScope x doc =
do updScope \o -> o { mNested = Set.insert x (mNested o) }
newScope (SignatureScope x doc)
newTopSignatureScope :: ModName -> InferM ()
newTopSignatureScope x = newScope (TopSignatureScope x)
{- | Start a new submodule scope. The imports and exports are just used
to initialize an empty module. As we type check declarations they are
added to this module's scope. -}
@ -972,12 +976,12 @@ endSubmodule =
_ -> panic "endSubmodule" [ "Not a submodule" ]
endModule :: InferM Module
endModule :: InferM TCTopEntity
endModule =
IM $ sets \rw ->
case iScope rw of
[ x ] | MTopModule m <- mName x ->
( x { mName = m, mDecls = reverse (mDecls x) }
( TCTopModule x { mName = m, mDecls = reverse (mDecls x) }
, rw { iScope = [] }
)
_ -> panic "endModule" [ "Not a single top module" ]
@ -1005,6 +1009,20 @@ endSignature =
}
_ -> panic "endSignature" [ "Not a signature scope" ]
endTopSignature :: InferM TCTopEntity
endTopSignature =
IM $ sets \rw ->
case iScope rw of
[ x ] | TopSignatureScope m <- mName x ->
( TCTopSignature m ModParamNames
{ mpnTypes = mParamTypes x
, mpnConstraints = mParamConstraints x
, mpnFuns = mParamFuns x
, mpnDoc = Nothing
}
, rw { iScope = [] }
)
_ -> panic "endTopSignature" [ "Not a top-level signature" ]

7
src/Cryptol/TypeCheck/Subst.hs
View File

@ -434,3 +434,10 @@ instance TVars Module where
apSubst su m =
let !decls' = apSubst su (mDecls m)
in m { mDecls = decls' }
-- WARNING: This applies the substitution only to the declarations in modules.
instance TVars TCTopEntity where
apSubst su ent =
case ent of
TCTopModule m -> TCTopModule (apSubst su m)
TCTopSignature {} -> ent