Implement :focus

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

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''

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."

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

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 -----------------------------------------------------------------------
 

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

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)
+        ]

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)

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

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