GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-17 01:41:09 +03:00
Code Issues Projects Releases Wiki Activity

Implement :focus

Browse Source
This commit is contained in:
Eric Mertens 2024-07-08 17:41:06 -07:00
parent b2ce8200cd
commit 72902bddf3
16 changed files with 213 additions and 81 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
bench/Main.hs
View File

@ -138,7 +138,7 @@ ceval cd name path expr =
menv <- M.initialModuleEnv
(eres, _) <- M.runModuleM (evOpts,menv) $ withLib $ do
m <- M.loadModuleByPath path
M.setFocusedModule (T.mName m)
M.setFocusedModule (P.ImpTop (T.mName m))
let Right pexpr = P.parseExpr expr
(_, texpr, _) <- M.checkExpr pexpr
return texpr
@ -160,7 +160,7 @@ seval cd name path expr =
menv <- M.initialModuleEnv
(eres, _) <- M.runModuleM (evOpts,menv) $ withLib $ do
m <- M.loadModuleByPath path
M.setFocusedModule (T.mName m)
M.setFocusedModule (P.ImpTop (T.mName m))
let Right pexpr = P.parseExpr expr
(_, texpr, _) <- M.checkExpr pexpr
return texpr

2
cryptol-remote-api/cryptol-eval-server/Main.hs
View File

@ -77,7 +77,7 @@ main = customMain initMod initMod initMod initMod description buildApp
case res of
Left err -> die err
Right (m, menv') ->
do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (tcTopEntitytName (snd m)))
do res' <- fst <$> runModuleM minp{ minpModuleEnv = menv' } (setFocusedModule (P.ImpTop (tcTopEntitytName (snd m))))
case res' of
Left err -> die err
Right (_, menv'') -> pure menv''

2
cryptol/Main.hs
View File

@ -292,7 +292,7 @@ setupREPL opts = do
-- we tried, instead of the Prelude
REPL.setEditPath l
REPL.setLoadedMod REPL.LoadedModule
{ REPL.lName = Nothing
{ REPL.lFocus = Nothing
, REPL.lPath = InFile l
}
_ -> io $ putStrLn "Only one file may be loaded at the command line."

17
src/Cryptol/ModuleSystem.hs
View File

@ -30,6 +30,9 @@ module Cryptol.ModuleSystem (
, getPrimMap
, renameVar
, renameType
, setFocusedModule
, Base.renameImpNameInCurrentEnv
, impNameTopModule
-- * Interfaces
, Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)
@ -45,7 +48,7 @@ import qualified Cryptol.Eval.Concrete as Concrete
import Cryptol.ModuleSystem.Env
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Monad
import Cryptol.ModuleSystem.Name (Name,PrimMap)
import Cryptol.ModuleSystem.Name (Name,PrimMap,nameTopModule)
import qualified Cryptol.ModuleSystem.Renamer as R
import qualified Cryptol.ModuleSystem.Base as Base
import qualified Cryptol.Parser.AST as P
@ -76,7 +79,7 @@ loadModuleByPath path minp = do
runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
unloadModule ((InFile path ==) . lmFilePath)
m <- Base.loadModuleByPath True path
setFocusedModule (T.tcTopEntitytName m)
setFocusedModule (P.ImpTop (T.tcTopEntitytName m))
return (InFile path,m)
-- | Load the given parsed module.
@ -86,7 +89,7 @@ loadModuleByName n minp = do
runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
unloadModule ((n ==) . lmName)
(path,m') <- Base.loadModuleFrom False (FromModule n)
setFocusedModule (T.tcTopEntitytName m')
setFocusedModule (P.ImpTop (T.tcTopEntitytName m'))
return (path,m')
-- | Parse and typecheck a module, but don't evaluate or change the environment.
@ -155,3 +158,11 @@ getFileDependencies f env = runModuleM env (Base.findDepsOf (InFile f))
getModuleDependencies :: M.ModName -> ModuleCmd (ModulePath, FileInfo)
getModuleDependencies m env = runModuleM env (Base.findDepsOfModule m)
--------------------------------------------------------------------------------
-- ImpName utilities
impNameTopModule :: P.ImpName Name -> M.ModName
impNameTopModule impName =
case impName of
P.ImpTop m -> m
P.ImpNested n -> nameTopModule n

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

@ -81,7 +81,7 @@ import qualified Cryptol.Backend.FFI.Error as FFI
import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
, preludeReferenceName, interactiveName, modNameChunks
, modNameToNormalModName )
, modNameToNormalModName, Namespace(NSModule) )
import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
@ -118,6 +118,21 @@ rename modName env m = do
renameModule :: P.Module PName -> ModuleM R.RenamedModule
renameModule m = rename (thing (mName m)) mempty (R.renameModule m)
renameImpNameInCurrentEnv :: P.ImpName PName -> ModuleM (P.ImpName Name)
renameImpNameInCurrentEnv (P.ImpTop top) =
do ok <- isLoaded top
if ok then
pure (P.ImpTop top)
else
fail ("Top-level module not loaded: " ++ show (pp top))
renameImpNameInCurrentEnv (P.ImpNested pname) =
do env <- getFocusedEnv
case R.lookupListNS NSModule pname (mctxNames env) of
[] -> do
fail ("Undefined submodule name: " ++ show (pp pname))
_:_:_ -> do
fail ("Ambiguous submodule name: " ++ show (pp pname))
[name] -> pure (P.ImpNested name)
-- NoPat -----------------------------------------------------------------------

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

@ -25,7 +25,7 @@ import Cryptol.Eval (EvalEnv)
import qualified Cryptol.IR.FreeVars as T
import Cryptol.ModuleSystem.Fingerprint
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name (Name,NameInfo(..),Supply,emptySupply,nameInfo)
import Cryptol.ModuleSystem.Name (Name,NameInfo(..),Supply,emptySupply,nameInfo,nameTopModuleMaybe)
import qualified Cryptol.ModuleSystem.NamingEnv as R
import Cryptol.Parser.AST
import qualified Cryptol.TypeCheck as T
@ -58,6 +58,7 @@ import Prelude.Compat
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.PP(pp)
import Cryptol.TypeCheck.AST (Submodule(smIface))
-- Module Environment ----------------------------------------------------------
@ -84,7 +85,7 @@ data ModuleEnv = ModuleEnv
, meFocusedModule :: Maybe ModName
, meFocusedModule :: Maybe (ImpName Name)
-- ^ The "current" module. Used to decide how to print names, for example.
, meSearchPath :: [FilePath]
@ -195,7 +196,7 @@ initialModuleEnv = do
focusModule :: ModName -> ModuleEnv -> Maybe ModuleEnv
focusModule n me = do
guard (isLoaded n (meLoadedModules me))
return me { meFocusedModule = Just n }
return me { meFocusedModule = Just (ImpTop n) }
-- | Get a list of all the loaded modules. Each module in the
-- resulting list depends only on other modules that precede it.
@ -273,9 +274,28 @@ instance Monoid ModContext where
}
modContextOf :: ImpName Name -> ModuleEnv -> Maybe ModContext
modContextOf (ImpNested name) me =
do mname <- nameTopModuleMaybe name
lm <- lookupModule mname me
sm <- Map.lookup name (T.mSubmodules (lmModule lm)) -- TODO: support uninstantiated functors
let
localNames = T.smInScope sm
modContextOf :: ModName -> ModuleEnv -> Maybe ModContext
modContextOf mname me =
-- XXX: do we want only public ones here?
loadedDecls = map (ifDefines . lmInterface)
$ getLoadedModules (meLoadedModules me)
pure ModContext
{ mctxParams = NoParams
, mctxExported = ifsPublic (smIface sm)
, mctxDecls = mconcat (ifDefines (lmInterface lm) : loadedDecls)
, mctxNames = localNames
, mctxNameDisp = R.toNameDisp localNames
}
-- TODO: support focusing inside a submodule signature to support browsing?
modContextOf (ImpTop mname) me =
do lm <- lookupModule mname me
let localIface = lmInterface lm
localNames = lmNamingEnv lm

28
src/Cryptol/ModuleSystem/Interface.hs
View File

@ -10,6 +10,7 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Safe #-}
module Cryptol.ModuleSystem.Interface (
Iface
@ -26,6 +27,7 @@ module Cryptol.ModuleSystem.Interface (
, filterIfaceDecls
, ifaceDeclsNames
, ifaceOrigNameMap
, ifaceNameToModuleMap
) where
import Data.Set(Set)
@ -45,8 +47,9 @@ import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident (ModName, OrigName(..))
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Fixity(Fixity)
import Cryptol.Parser.AST(Pragma)
import Cryptol.Parser.AST(Pragma, ImpName(..))
import Cryptol.TypeCheck.Type
import Data.Maybe (maybeToList)
type Iface = IfaceG ModName
@ -56,7 +59,7 @@ data IfaceG name = Iface
, ifParams :: FunctorParams -- ^ Module parameters, if any
, ifDefines :: IfaceDecls -- ^ All things defines in the module
-- (includes nested definitions)
} deriving (Show, Generic, NFData)
} deriving (Show, Generic, NFData, Functor)
-- | Remove the name of a module. This is useful for dealing with collections
-- of modules, as in `Map (ImpName Name) (IfaceG ())`.
@ -75,7 +78,7 @@ data IfaceNames name = IfaceNames
, ifsDefines :: Set Name -- ^ Things defined in this module
, ifsPublic :: Set Name -- ^ Subset of `ifsDefines` that is public
, ifsDoc :: !(Maybe Text) -- ^ Documentation
} deriving (Show, Generic, NFData)
} deriving (Show, Generic, NFData, Functor)
-- | Is this interface for a functor.
ifaceIsFunctor :: IfaceG name -> Bool
@ -232,9 +235,18 @@ ifaceOrigNameMap ifa = Map.unionsWith Map.union (here : nested)
(concatMap conNames (Map.elems (ifNominalTypes decls)))
where conNames = map fst . nominalTypeConTypes
-- | For every name in the interface compute the direct module that defines it.
-- This does not traverse into functors or interfaces.
ifaceNameToModuleMap :: Iface -> Map Name (ImpName Name)
ifaceNameToModuleMap iface = go (ImpTop <$> ifNames iface)
where
theModules = ifModules (ifDefines iface)
go :: IfaceNames (ImpName Name) -> Map Name (ImpName Name)
go names =
Map.fromSet (\_ -> ifsName names) (ifsDefines names) <>
Map.unions
[ go (ImpNested <$> modu)
| childName <- Set.toList (ifsNested names)
, modu <- maybeToList (Map.lookup childName theModules)
]

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

@ -577,13 +577,16 @@ getEvalOpts =
getNominalTypes :: ModuleM (Map T.Name T.NominalType)
getNominalTypes = ModuleT (loadedNominalTypes <$> get)
getFocusedModule :: ModuleM (Maybe P.ModName)
getFocusedModule :: ModuleM (Maybe (P.ImpName T.Name))
getFocusedModule = ModuleT (meFocusedModule `fmap` get)
setFocusedModule :: P.ModName -> ModuleM ()
setFocusedModule n = ModuleT $ do
setFocusedModule :: P.ImpName T.Name -> ModuleM ()
setFocusedModule = setMaybeFocusedModule . Just
setMaybeFocusedModule :: Maybe (P.ImpName T.Name) -> ModuleM ()
setMaybeFocusedModule mb = ModuleT $ do
me <- get
set $! me { meFocusedModule = Just n }
set $! me { meFocusedModule = mb }
getSearchPath :: ModuleM [FilePath]
getSearchPath = ModuleT (meSearchPath `fmap` get)

1
src/Cryptol/ModuleSystem/Name.hs
View File

@ -276,7 +276,6 @@ nameTopModuleMaybe = fmap topModuleFor . nameModPathMaybe
nameTopModule :: Name -> ModName
nameTopModule = topModuleFor . nameModPath
-- Name Supply -----------------------------------------------------------------
class Monad m => FreshM m where

8
src/Cryptol/Parser.y
View File

@ -19,6 +19,7 @@ module Cryptol.Parser
, parseRepl, parseReplWith
, parseSchema, parseSchemaWith
, parseModName, parseHelpName
, parseImpName
, ParseError(..), ppError
, Layout(..)
, Config(..), defaultConfig
@ -155,6 +156,7 @@ import Paths_cryptol
%name repl repl
%name schema schema
%name modName modName
%name impName impName
%name helpName help_name
%tokentype { Located Token }
%monad { ParseM }
@ -945,6 +947,12 @@ parseModName txt =
Right a -> Just (thing a)
Left _ -> Nothing
parseImpName :: String -> Maybe (ImpName PName)
parseImpName txt =
case parseString defaultConfig { cfgModuleScope = False } impName txt of
Right a -> Just (thing a)
Left _ -> Nothing
parseHelpName :: String -> Maybe PName
parseHelpName txt =
case parseString defaultConfig { cfgModuleScope = False } helpName txt of

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

@ -63,6 +63,8 @@ import Cryptol.REPL.Browse
import Cryptol.REPL.Help
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Interface as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M
@ -74,7 +76,7 @@ import Cryptol.ModuleSystem.Fingerprint(fingerprintHexString)
import Cryptol.Backend.FloatHelpers as FP
import qualified Cryptol.Backend.Monad as E
import qualified Cryptol.Backend.SeqMap as E
import Cryptol.Eval.Concrete( Concrete(..) )
import Cryptol.Backend.Concrete ( Concrete(..) )
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Env as E
import Cryptol.Eval.FFI
@ -86,7 +88,7 @@ import Cryptol.Testing.Random
import qualified Cryptol.Testing.Random as TestR
import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
,parseModName,parseHelpName)
,parseModName,parseHelpName,parseImpName)
import Cryptol.Parser.Position (Position(..),Range(..),HasLoc(..))
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Error as T
@ -330,6 +332,9 @@ commandList =
, CommandDescr [ ":m", ":module" ] ["[ MODULE ]"] (FilenameArg moduleCmd)
"Load a module by its name."
""
, CommandDescr [ ":f", ":focus" ] ["[ MODULE ]"] (ModNameArg focusCmd)
"Focus name scope inside a loaded module."
""
, CommandDescr [ ":w", ":writeByteArray" ] ["FILE", "EXPR"] (FileExprArg writeFileCmd)
"Write data of type 'fin n => [n][8]' to a file."
""
@ -1241,7 +1246,7 @@ editCmd path =
mbL <- getLoadedMod
if not (null path)
then do when (isNothing mbL)
$ setLoadedMod LoadedModule { lName = Nothing
$ setLoadedMod LoadedModule { lFocus = Nothing
, lPath = M.InFile path }
doEdit path
else case msum [ M.InFile <$> mbE, lPath <$> mbL ] of
@ -1301,13 +1306,49 @@ moduleCmd modString
case mpath of
M.InFile file ->
do setEditPath file
setLoadedMod LoadedModule { lName = Just m, lPath = mpath }
setLoadedMod LoadedModule { lFocus = Just (P.ImpTop m), lPath = mpath }
loadHelper (M.loadModuleByPath file)
M.InMem {} -> loadHelper (M.loadModuleByName m)
Nothing ->
do rPutStrLn "Invalid module name."
pure emptyCommandResult { crSuccess = False }
focusCmd :: String -> REPL CommandResult
focusCmd modString
| null modString =
do mb <- getLoadedMod
case mb of
Nothing -> pure ()
Just lm ->
case lName lm of
Nothing -> pure ()
Just name -> do
let top = P.ImpTop name
liftModuleCmd (`M.runModuleM` M.setFocusedModule top)
setLoadedMod lm { lFocus = Just top }
pure emptyCommandResult
| otherwise =
case parseImpName modString of
Nothing ->
do rPutStrLn "Invalid module name."
pure emptyCommandResult { crSuccess = False }
Just pimpName -> do
impName <- liftModuleCmd (setFocusedModuleCmd pimpName)
mb <- getLoadedMod
case mb of
Nothing -> pure ()
Just lm -> setLoadedMod lm { lFocus = Just impName }
pure emptyCommandResult
setFocusedModuleCmd :: P.ImpName P.PName -> M.ModuleCmd (P.ImpName T.Name)
setFocusedModuleCmd pimpName i = M.runModuleM i $
do impName <- M.renameImpNameInCurrentEnv pimpName
M.setFocusedModule impName
pure impName
loadPrelude :: REPL ()
loadPrelude = void $ moduleCmd $ show $ pp M.preludeName
@ -1317,7 +1358,7 @@ loadCmd path
-- when `:load`, the edit and focused paths become the parameter
| otherwise = do setEditPath path
setLoadedMod LoadedModule { lName = Nothing
setLoadedMod LoadedModule { lFocus = Nothing
, lPath = M.InFile path
}
loadHelper (M.loadModuleByPath path)
@ -1329,7 +1370,7 @@ loadHelper how =
whenDebug (rPutStrLn (dump ent))
setLoadedMod LoadedModule
{ lName = Just (T.tcTopEntitytName ent)
{ lFocus = Just (P.ImpTop (T.tcTopEntitytName ent))
, lPath = path
}
-- after a successful load, the current module becomes the edit target
@ -1379,12 +1420,13 @@ browseCmd input
rPrint (browseModContext BrowseInScope fe)
pure emptyCommandResult
| otherwise =
case parseModName input of
case parseImpName input of
Nothing -> do
rPutStrLn "Invalid module name"
pure emptyCommandResult { crSuccess = False }
Just m -> do
mb <- M.modContextOf m <$> getModuleEnv
Just pimpName -> do
impName <- liftModuleCmd (`M.runModuleM` M.renameImpNameInCurrentEnv pimpName)
mb <- M.modContextOf impName <$> getModuleEnv
case mb of
Nothing -> do
rPutStrLn ("Module " ++ show input ++ " is not loaded")
@ -2044,8 +2086,8 @@ captureLog m = do
pure (output, result)
-- | Check all the code blocks in a given docstring.
checkDocString :: T.Text -> REPL [[SubcommandResult]]
checkDocString str =
checkDocString :: P.ImpName T.Name -> T.Text -> REPL [[SubcommandResult]]
checkDocString impName str =
case extractCodeBlocks str of
Left e -> do
pure [[SubcommandResult
@ -2053,8 +2095,11 @@ checkDocString str =
, srResult = emptyCommandResult { crSuccess = False }
, srLog = e
}]]
Right bs -> do
traverse checkBlock bs
Right bs ->
Ex.bracket
(liftModuleCmd (`M.runModuleM` (M.getFocusedModule <* M.setFocusedModule impName)))
(\mb -> liftModuleCmd (`M.runModuleM` M.setMaybeFocusedModule mb))
(\_ -> traverse checkBlock bs)
-- | Check all of the docstrings in the given module.
--
@ -2064,8 +2109,8 @@ checkDocString str =
checkDocStrings :: M.LoadedModule -> REPL [[SubcommandResult]]
checkDocStrings m = do
let dat = M.lmdModule (M.lmData m)
let ds = T.gatherModuleDocstrings dat
concat <$> traverse checkDocString ds
let ds = T.gatherModuleDocstrings (M.ifaceNameToModuleMap (M.lmInterface m)) dat
concat <$> traverse (uncurry checkDocString) ds
-- | Evaluate all the docstrings in the specified module.
--
@ -2114,8 +2159,11 @@ checkDocStringsCmd input
forM_ results $ \result ->
forM_ result $ \line -> do
rPutStrLn ""
rPutStrLn (T.unpack (srInput line))
rPutStr (srLog line)
rPutStrLn ("Successes: " ++ show successes ++ " Failures: " ++ show failures)
rPutStrLn ""
rPutStrLn ("Successes: " ++ show successes ++ ", Failures: " ++ show failures)
pure emptyCommandResult { crSuccess = failures == 0 }

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

@ -48,7 +48,7 @@ module Cryptol.REPL.Monad (
, getTypeNames
, getPropertyNames
, getModNames
, LoadedModule(..), getLoadedMod, setLoadedMod, clearLoadedMod
, LoadedModule(..), lName, getLoadedMod, setLoadedMod, clearLoadedMod
, setEditPath, getEditPath, clearEditPath
, setSearchPath, prependSearchPath
, getPrompt
@ -147,10 +147,13 @@ import Prelude.Compat
-- | This indicates what the user would like to work on.
data LoadedModule = LoadedModule
{ lName :: Maybe P.ModName -- ^ Working on this module.
, lPath :: M.ModulePath -- ^ Working on this file.
{ lFocus :: Maybe (P.ImpName T.Name) -- ^ Working on this module.
, lPath :: M.ModulePath -- ^ Working on this file.
}
lName :: LoadedModule -> Maybe P.ModName
lName lm = M.impNameTopModule <$> lFocus lm
-- | REPL RW Environment.
data RW = RW
{ eLoadedMod :: Maybe LoadedModule
@ -234,14 +237,16 @@ mkPrompt rw
detailedPrompt = id False
modLn =
case lName =<< eLoadedMod rw of
case lFocus =<< eLoadedMod rw of
Nothing -> show (pp I.preludeName)
Just m
| M.isLoadedParamMod m loaded -> modName ++ "(parameterized)"
| M.isLoadedInterface m loaded -> modName ++ "(interface)"
| M.isLoadedParamMod top loaded -> modName ++ "(parameterized)"
| M.isLoadedInterface top loaded -> modName ++ "(interface)"
| otherwise -> modName
where modName = pretty m
loaded = M.meLoadedModules (eModuleEnv rw)
where
top = M.impNameTopModule m
modName = pretty m
loaded = M.meLoadedModules (eModuleEnv rw)
withFocus =
case eLoadedMod rw of
@ -501,7 +506,7 @@ getEvalOptsAction = REPL $ \rwRef -> pure $
clearLoadedMod :: REPL ()
clearLoadedMod = do modifyRW_ (\rw -> rw { eLoadedMod = upd <$> eLoadedMod rw })
updateREPLTitle
where upd x = x { lName = Nothing }
where upd x = x { lFocus = Nothing }
-- | Set the name of the currently focused file, loaded via @:r@.
setLoadedMod :: LoadedModule -> REPL ()

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

@ -110,7 +110,7 @@ data ModuleG mname =
, mTySyns :: Map Name TySyn
, mNominalTypes :: Map Name NominalType
, mDecls :: [DeclGroup]
, mSubmodules :: Map Name (IfaceNames Name)
, mSubmodules :: Map Name Submodule
, mSignatures :: !(Map Name ModParamNames)
, mInScope :: NamingEnv
@ -118,6 +118,11 @@ data ModuleG mname =
-- Submodule in-scope information is in 'mSubmodules'.
} deriving (Show, Generic, NFData)
data Submodule = Submodule
{ smIface :: IfaceNames Name
, smInScope :: NamingEnv
} deriving (Show, Generic, NFData)
emptyModule :: mname -> ModuleG mname
emptyModule nm =
Module
@ -524,29 +529,25 @@ instance PP (WithNames TCTopEntity) where
TCTopSignature n ps ->
hang ("interface module" <+> pp n <+> "where") 2 (pp ps)
gatherModuleDocstrings :: Module -> [Text]
gatherModuleDocstrings m =
map snd $
sortBy (comparing fst) $
gatherModuleDocstrings' m { mName = start }
gatherModuleDocstrings' :: ModuleG Position -> [(Position, Text)]
gatherModuleDocstrings' m =
cat [(mName m, mDoc m)] ++
cat [(mName m, mpnDoc (mpParameters param)) | (_, param) <- Map.assocs (mParams m)] ++
cat [(pos n, mtpDoc param) | (n, param) <- Map.assocs (mParamTypes m)] ++
cat [(pos n, mvpDoc param) | (n, param) <- Map.assocs (mParamFuns m)] ++
cat [(pos n, tsDoc t) | (n, t) <- Map.assocs (mTySyns m)] ++
cat [(pos n, ntDoc t) | (n, t) <- Map.assocs (mNominalTypes m)] ++
cat [(pos (dName d), dDoc d) | g <- mDecls m, d <- groupDecls g] ++
cat [(pos n, ifsDoc s) | (n, s) <- Map.assocs (mSubmodules m)] ++
cat [(pos n, mpnDoc s) | (n, s) <- Map.assocs (mSignatures m)] ++
[doc | m' <- Map.elems (mFunctors m), doc <- gatherModuleDocstrings' (mapModName pos m')]
-- functor parameters don't have a *name*, so we associate them with their module for now
gatherModuleDocstrings ::
Map Name (ImpName Name) ->
Module ->
[(ImpName Name, Text)]
gatherModuleDocstrings nameToModule m =
cat [(ImpTop (mName m), mDoc m)] ++
-- mParams m
-- mParamTypes m
-- mParamFuns m
cat [(lookupModuleName n, tsDoc t) | (n, t) <- Map.assocs (mTySyns m)] ++
cat [(lookupModuleName n, ntDoc t) | (n, t) <- Map.assocs (mNominalTypes m)] ++
cat [(lookupModuleName (dName d), dDoc d) | g <- mDecls m, d <- groupDecls g] ++
cat [(ImpNested n, ifsDoc (smIface s)) | (n, s) <- Map.assocs (mSubmodules m)] ++
cat [(ImpTop (mName m), mpnDoc s) | s <- Map.elems (mSignatures m)]
where
pos = from . nameLoc
mapModName f md = md { mName = f (mName md) }
cat :: [(Position, Maybe Text)] -> [(Position, Text)]
cat :: [(a, Maybe Text)] -> [(a, Text)]
cat entries = [(p, d) | (p, Just d) <- entries]
lookupModuleName n =
case Map.lookup n nameToModule of
Just x -> x
Nothing -> panic "gatherModuleDocstrings" ["No owning module for name:", show (pp n)]

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

@ -51,7 +51,8 @@ genModDefines m =
where
nestedInSet = Set.unions . map inNested . Set.toList
inNested x = case Map.lookup x (mSubmodules m) of
Just y -> ifsDefines y `Set.union` nestedInSet (ifsNested y)
Just y -> ifsDefines iface `Set.union` nestedInSet (ifsNested iface)
where iface = smIface y
Nothing -> Set.empty -- must be signature or a functor
genIface :: ModuleG name -> IfaceG name
@ -71,7 +72,7 @@ genIfaceWithNames names m =
, d <- groupDecls dg
, let qn = dName d
]
, ifModules = mSubmodules m
, ifModules = smIface <$> mSubmodules m
, ifSignatures = mSignatures m
, ifFunctors = genIface <$> mFunctors m
}

6
src/Cryptol/TypeCheck/ModuleInstance.hs
View File

@ -63,6 +63,12 @@ instance ModuleInstance name => ModuleInstance (ImpName name) where
ImpTop t -> ImpTop t
ImpNested n -> ImpNested (moduleInstance n)
instance ModuleInstance Submodule where
moduleInstance x = Submodule
{ smInScope = moduleInstance (smInScope x)
, smIface = moduleInstance (smIface x)
}
instance ModuleInstance (ModuleG name) where
moduleInstance m =
Module { mName = mName m

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

@ -852,7 +852,7 @@ lookupModule iname =
do localMods <- getScope mSubmodules
case Map.lookup m localMods of
Just names ->
do n <- genIfaceWithNames names <$> getCurDecls
do n <- genIfaceWithNames (smIface names) <$> getCurDecls
pure (If.ifaceForgetName n)
Nothing ->
@ -1057,7 +1057,10 @@ endSubmodule =
, mSignatures = add mSignatures
, mSubmodules = if isFun
then mSubmodules y
else Map.insert m (genIfaceNames x1)
else let sm = Submodule
{ smIface = genIfaceNames x1
, smInScope = mInScope x }
in Map.insert m sm
(mSubmodules x <> mSubmodules y)
, mFunctors = if isFun
then Map.insert m x1 (mFunctors y)
@ -1183,7 +1186,7 @@ addSignatures :: Map Name ModParamNames -> InferM ()
addSignatures mp =
updScope \r -> r { mSignatures = Map.union mp (mSignatures r) }
addSubmodules :: Map Name (If.IfaceNames Name) -> InferM ()
addSubmodules :: Map Name Submodule -> InferM ()
addSubmodules mp =
updScope \r -> r { mSubmodules = Map.union mp (mSubmodules r) }