From 72902bddf3c681aeb87066c8caa15f8e9556b1a7 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Mon, 8 Jul 2024 17:41:06 -0700 Subject: [PATCH] Implement :focus --- bench/Main.hs | 4 +- .../cryptol-eval-server/Main.hs | 2 +- cryptol/Main.hs | 2 +- src/Cryptol/ModuleSystem.hs | 17 +++- src/Cryptol/ModuleSystem/Base.hs | 17 +++- src/Cryptol/ModuleSystem/Env.hs | 30 +++++-- src/Cryptol/ModuleSystem/Interface.hs | 30 ++++--- src/Cryptol/ModuleSystem/Monad.hs | 11 ++- src/Cryptol/ModuleSystem/Name.hs | 1 - src/Cryptol/Parser.y | 8 ++ src/Cryptol/REPL/Command.hs | 80 +++++++++++++++---- src/Cryptol/REPL/Monad.hs | 23 +++--- src/Cryptol/TypeCheck/AST.hs | 51 ++++++------ src/Cryptol/TypeCheck/Interface.hs | 5 +- src/Cryptol/TypeCheck/ModuleInstance.hs | 6 ++ src/Cryptol/TypeCheck/Monad.hs | 9 ++- 16 files changed, 214 insertions(+), 82 deletions(-) diff --git a/bench/Main.hs b/bench/Main.hs index 761c3c5c4..7457587c7 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -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 diff --git a/cryptol-remote-api/cryptol-eval-server/Main.hs b/cryptol-remote-api/cryptol-eval-server/Main.hs index aa1048b05..5016aff33 100644 --- a/cryptol-remote-api/cryptol-eval-server/Main.hs +++ b/cryptol-remote-api/cryptol-eval-server/Main.hs @@ -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'' diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 425cb06ba..85beccf28 100644 --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -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." diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index 81f7cbae0..6845b51d2 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index ae1461fe6..6f050d9b0 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -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 ----------------------------------------------------------------------- diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 3f033babd..49a9899f5 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -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 diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index adc63513d..92b65a6f0 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -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) + ] diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index c4350e9f8..78d939d53 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -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) diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index aff8e3468..fc865ad56 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -276,7 +276,6 @@ nameTopModuleMaybe = fmap topModuleFor . nameModPathMaybe nameTopModule :: Name -> ModName nameTopModule = topModuleFor . nameModPath - -- Name Supply ----------------------------------------------------------------- class Monad m => FreshM m where diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index d6a8f8344..03a2dfcdf 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -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 diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 14dd01209..77645bb94 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -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 } diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index 342eade88..fefc91d6e 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -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 () diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index e6bcdf52f..5d1f79db5 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -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)] diff --git a/src/Cryptol/TypeCheck/Interface.hs b/src/Cryptol/TypeCheck/Interface.hs index 57588c4f7..6e8422496 100644 --- a/src/Cryptol/TypeCheck/Interface.hs +++ b/src/Cryptol/TypeCheck/Interface.hs @@ -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 } diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index f7524b4cf..3b2dfac51 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index a30f060c9..84dd52b79 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -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) }