Merge pull request #1559 from GaloisInc/T1455

Make names in scope in functors accessible when their instantiations are loaded at the REPL

CHANGES.md

@@ -1,3 +1,11 @@
+# UNRELEASED
+
+* Fixed #1556, #1237, and #1561.
+* Fixed #1455, making anything in scope of the functor in scope at the REPL as
+  well when an instantiation of the functor is loaded and focused,
+  design choice (3) on the ticket.  In particular, the prelude will be in scope.
+
+
 # 3.0.0 -- 2023-06-26
 
 ## Language changes

cryptol.cabal

@@ -141,6 +141,7 @@ library
                        Cryptol.ModuleSystem.Name,
                        Cryptol.ModuleSystem.Names,
                        Cryptol.ModuleSystem.NamingEnv,
+                       Cryptol.ModuleSystem.NamingEnv.Types,
                        Cryptol.ModuleSystem.Binds
                        Cryptol.ModuleSystem.Exports,
                        Cryptol.ModuleSystem.Renamer,

src/Cryptol/ModuleSystem/Base.hs

@@ -631,7 +631,11 @@ checkModule isrc m = do
   rewMod <- case tcm of
               T.TCTopModule mo -> T.TCTopModule <$> liftSupply (`rewModule` mo)
               T.TCTopSignature {} -> pure tcm
-  pure (R.rmInScope renMod,rewMod)
+  let nameEnv = case tcm of
+                  T.TCTopModule mo -> T.mInScope mo
+                  -- Name env for signatures does not change after typechecking
+                  T.TCTopSignature {} -> mInScope (R.rmModule renMod)
+  pure (nameEnv,rewMod)
 
 data TCLinter o = TCLinter
   { lintCheck ::

src/Cryptol/ModuleSystem/Binds.hs

@@ -13,6 +13,7 @@ module Cryptol.ModuleSystem.Binds
   , topModuleDefs
   , topDeclsDefs
   , newModParam
+  , newFunctorInst
   , InModule(..)
   , ifaceToMod
   , ifaceSigToMod
@@ -125,7 +126,7 @@ ifaceSigToMod ps = Mod
   , modState     = ()
   }
   where
-  env = modParamsNamingEnv ps
+  env = modParamNamesNamingEnv ps
 
 
 
@@ -420,6 +421,13 @@ newLocal ns thing rng = liftSupply (mkLocal ns (getIdent thing) rng)
 newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name
 newModParam m i rng n = liftSupply (mkModParam m i rng n)
 
+-- | Given a name in a functor, make a fresh name for the corresponding thing in
+-- the instantiation.
+--
+-- The 'ModPath' should be the instantiation not the functor.
+newFunctorInst :: FreshM m => ModPath -> Name -> m Name
+newFunctorInst m n = liftSupply (freshNameFor m n)
+
 
 {- | Do something in the context of a module.
 If `Nothing` than we are working with a local declaration.

src/Cryptol/ModuleSystem/Name.hs

@@ -29,6 +29,7 @@ module Cryptol.ModuleSystem.Name (
   , nameLoc
   , nameFixity
   , nameNamespace
+  , nameToDefPName
   , asPrim
   , asOrigName
   , nameModPath
@@ -70,7 +71,8 @@ import qualified Data.Text as Text
 import           Data.Char(isAlpha,toUpper)
 
 
-
+import           Cryptol.Parser.Name (PName)
+import qualified Cryptol.Parser.Name as PName
 import           Cryptol.Parser.Position (Range,Located(..))
 import           Cryptol.Utils.Fixity
 import           Cryptol.Utils.Ident
@@ -146,9 +148,9 @@ cmpNameDisplay disp l r =
                  NotInScope  ->
                     let m = Text.pack (show (pp (ogModule og)))
                     in
-                    case ogSource og of
-                      FromModParam q  -> m <> "::" <> Text.pack (show (pp q))
-                      _ -> m
+                    case ogFromParam og of
+                      Just q  -> m <> "::" <> Text.pack (show (pp q))
+                      Nothing -> m
 
   -- Note that this assumes that `xs` is `l` and `ys` is `r`
   cmpText xs ys =
@@ -227,12 +229,21 @@ nameLoc  = nLoc
 nameFixity :: Name -> Maybe Fixity
 nameFixity = nFixity
 
+-- | Compute a `PName` for the definition site corresponding to the given
+-- `Name`.   Usually this is an unqualified name, but names that come
+-- from module parameters are qualified with the corresponding parameter name.
+nameToDefPName :: Name -> PName
+nameToDefPName n =
+  case nInfo n of
+    GlobalName _ og -> PName.origNameToDefPName og
+    LocalName _ txt -> PName.mkUnqual txt
+
 -- | Primtiives must be in a top level module, at least for now.
 asPrim :: Name -> Maybe PrimIdent
 asPrim n =
   case nInfo n of
     GlobalName _ og
-      | TopModule m <- ogModule og, not (ogFromModParam og) ->
+      | TopModule m <- ogModule og, not (ogIsModParam og) ->
         Just $ PrimIdent m $ identText $ ogName og
 
     _ -> Nothing
@@ -371,6 +382,7 @@ mkDeclared ns m sys ident fixity loc s = (name, s')
                                 , ogModule    = m
                                 , ogName      = ident
                                 , ogSource    = FromDefinition
+                                , ogFromParam = Nothing
                                 }
               }
 
@@ -410,7 +422,8 @@ mkModParam own pname rng n s = (name, s')
                               { ogModule    = own
                               , ogName      = nameIdent n
                               , ogNamespace = nameNamespace n
-                              , ogSource    = FromModParam pname
+                              , ogSource    = FromModParam
+                              , ogFromParam = Just pname
                               }
               , nFixity = nFixity n
               , nLoc    = rng

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -6,14 +6,14 @@
 -- Stability   :  provisional
 -- Portability :  portable
 
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
 -- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
-module Cryptol.ModuleSystem.NamingEnv where
+module Cryptol.ModuleSystem.NamingEnv
+  ( module Cryptol.ModuleSystem.NamingEnv.Types
+  , module Cryptol.ModuleSystem.NamingEnv
+  ) where
 
 import Data.Maybe (mapMaybe,maybeToList)
 import           Data.Map.Strict (Map)
@@ -22,9 +22,6 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Foldable(foldl')
 
-import GHC.Generics (Generic)
-import Control.DeepSeq(NFData)
-
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Ident(allNamespaces)
@@ -34,24 +31,7 @@ import Cryptol.ModuleSystem.Name
 import Cryptol.ModuleSystem.Names
 import Cryptol.ModuleSystem.Interface
 
-
--- | The 'NamingEnv' is used by the renamer to determine what
--- identifiers refer to.
-newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names))
-  deriving (Show,Generic,NFData)
-
-instance Monoid NamingEnv where
-  mempty = NamingEnv Map.empty
-  {-# INLINE mempty #-}
-
-instance Semigroup NamingEnv where
-  NamingEnv l <> NamingEnv r =
-    NamingEnv (Map.unionWith (Map.unionWith (<>)) l r)
-
-instance PP NamingEnv where
-  ppPrec _ (NamingEnv mps)   = vcat $ map ppNS $ Map.toList mps
-    where ppNS (ns,xs) = nest 2 (vcat (pp ns : map ppNm (Map.toList xs)))
-          ppNm (x,as)  = pp x <+> "->" <+> commaSep (map pp (namesToList as))
+import Cryptol.ModuleSystem.NamingEnv.Types
 
 
 {- | This "joins" two naming environments by matching the text name.
@@ -91,14 +71,16 @@ namingEnvNames (NamingEnv xs) =
     Just (One x) -> Set.singleton x
     Just (Ambig as) -> as
 
--- | Get a unqualified naming environment for the given names
+-- | Get a naming environment for the given names.  The `PName`s correspond
+-- to the definition sites of the corresponding `Name`s, so typically they
+-- will be unqualified.  The exception is for names that comre from parameters,
+-- which are qualified with the relevant parameter.
 namingEnvFromNames :: Set Name -> NamingEnv
 namingEnvFromNames xs = NamingEnv (foldl' add mempty xs)
   where
   add mp x = let ns = nameNamespace x
-                 txt = nameIdent x
              in Map.insertWith (Map.unionWith (<>))
-                               ns (Map.singleton (mkUnqual txt) (One x))
+                               ns (Map.singleton (nameToDefPName x) (One x))
                                mp
 
 
@@ -231,8 +213,8 @@ isEmptyNamingEnv (NamingEnv mp) = Map.null mp
 
 -- | Compute an unqualified naming environment, containing the various module
 -- parameters.
-modParamsNamingEnv :: T.ModParamNames -> NamingEnv
-modParamsNamingEnv T.ModParamNames { .. } =
+modParamNamesNamingEnv :: T.ModParamNames -> NamingEnv
+modParamNamesNamingEnv T.ModParamNames { .. } =
   NamingEnv $ Map.fromList
     [ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns)
     , (NSType,  Map.fromList $ map fromTS (Map.elems mpnTySyn) ++
@@ -248,6 +230,11 @@ modParamsNamingEnv T.ModParamNames { .. } =
 
   fromTS ts = (toPName (T.tsName ts), One (T.tsName ts))
 
+-- | Compute a naming environment from a module parameter, qualifying it
+-- according to 'mpQual'.
+modParamNamingEnv :: T.ModParam -> NamingEnv
+modParamNamingEnv mp = maybe id qualify (T.mpQual mp) $
+  modParamNamesNamingEnv (T.mpParameters mp)
 
 -- | Generate a naming environment from a declaration interface, where none of
 -- the names are qualified.

src/Cryptol/ModuleSystem/NamingEnv/Types.hs

@@ -0,0 +1,34 @@
+{-# LANGUAGE DeriveAnyClass    #-}
+{-# LANGUAGE DeriveGeneric     #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Cryptol.ModuleSystem.NamingEnv.Types where
+
+import           Data.Map.Strict            (Map)
+import qualified Data.Map.Strict            as Map
+
+import           Control.DeepSeq            (NFData)
+import           GHC.Generics               (Generic)
+
+import           Cryptol.ModuleSystem.Names
+import           Cryptol.Parser.Name
+import           Cryptol.Utils.Ident
+import           Cryptol.Utils.PP
+
+-- | The 'NamingEnv' is used by the renamer to determine what
+-- identifiers refer to.
+newtype NamingEnv = NamingEnv (Map Namespace (Map PName Names))
+  deriving (Show,Generic,NFData)
+
+instance Monoid NamingEnv where
+  mempty = NamingEnv Map.empty
+  {-# INLINE mempty #-}
+
+instance Semigroup NamingEnv where
+  NamingEnv l <> NamingEnv r =
+    NamingEnv (Map.unionWith (Map.unionWith (<>)) l r)
+
+instance PP NamingEnv where
+  ppPrec _ (NamingEnv mps)   = vcat $ map ppNS $ Map.toList mps
+    where ppNS (ns,xs) = nest 2 (vcat (pp ns : map ppNm (Map.toList xs)))
+          ppNm (x,as)  = pp x <+> "->" <+> commaSep (map pp (namesToList as))

src/Cryptol/ModuleSystem/Renamer.hs

@@ -118,7 +118,6 @@ The Renamer Algorithm
 data RenamedModule = RenamedModule
   { rmModule   :: Module Name     -- ^ The renamed module
   , rmDefines  :: NamingEnv       -- ^ What this module defines
-  , rmInScope  :: NamingEnv       -- ^ What's in scope in this module
   , rmImported :: IfaceDecls
     -- ^ Imported declarations.  This provides the types for external
     -- names (used by the type-checker).
@@ -152,12 +151,11 @@ renameModule m0 =
 
      setResolvedLocals resolvedMods $
        setNestedModule pathToName
-       do (ifs,(inScope,m1)) <- collectIfaceDeps (renameModule' mname m)
+       do (ifs,m1) <- collectIfaceDeps (renameModule' mname m)
           env <- rmodDefines <$> lookupResolved mname
           pure RenamedModule
                  { rmModule = m1
                  , rmDefines = env
-                 , rmInScope = inScope
                  , rmImported = ifs
                   -- XXX: maybe we should keep the nested defines too?
                  }
@@ -220,12 +218,9 @@ class Rename f where
 renameModule' ::
   ImpName Name {- ^ Resolved name for this module -} ->
   ModuleG mname PName ->
-  RenameM (NamingEnv, ModuleG mname Name)
+  RenameM (ModuleG mname Name)
 renameModule' mname m =
-  setCurMod
-    case mname of
-      ImpTop r    -> TopModule r
-      ImpNested r -> Nested (nameModPath r) (nameIdent r)
+  setCurMod (impNameModPath mname)
 
   do resolved <- lookupResolved mname
      shadowNames' CheckNone (rmodImports resolved)
@@ -247,7 +242,7 @@ renameModule' mname m =
                      let exports = exportedDecls ds1
                      mapM_ recordUse (exported NSType exports)
                      inScope <- getNamingEnv
-                     pure (inScope, m { mDef = NormalModule ds1 })
+                     pure m { mDef = NormalModule ds1, mInScope = inScope }
 
          -- The things defined by this module are the *results*
          -- of the instantiation, so we should *not* add them
@@ -260,30 +255,20 @@ renameModule' mname m =
               let l = Just (srcRange f')
               imap <- mkInstMap l mempty (thing f') mname
 
-              {- Now we need to compute what's "in scope" of the instantiated
-              module.  This is used when the module is loaded at the command
-              line and users want to evalute things in the context of the
-              module -}
-              fuEnv <- if isFakeName (thing f')
-                          then pure mempty
-                          else lookupDefines (thing f')
-              let ren x = Map.findWithDefault x x imap
-
-              -- XXX: This is not quite right as it only considers the things
-              -- defined in the module to be in scope.  It misses things
-              -- that are *imported* by the functor, in particular the Cryptol
-              -- library
-              -- is missing.  See #1455.
-              inScope <- shadowNames' CheckNone (mapNamingEnv ren fuEnv)
-                         getNamingEnv
-
-              pure (inScope, m { mDef = FunctorInstance f' as' imap })
+              -- This inScope is incomplete; it only contains names from the
+              -- enclosing scope, but we also want the names in scope from the
+              -- functor, for ease of testing at the command line. We will fix
+              -- this up in doFunctorInst in the typechecker, because right now
+              -- we don't have access yet to the inScope of the functor.
+              inScope <- getNamingEnv
+
+              pure m { mDef = FunctorInstance f' as' imap, mInScope = inScope }
 
          InterfaceModule s ->
            shadowNames' CheckNone (rmodDefines resolved)
              do d <- InterfaceModule <$> renameIfaceModule mname s
                 inScope <- getNamingEnv
-                pure (inScope, m { mDef = d })
+                pure m { mDef = d, mInScope = inScope }
 
 
 checkFunctorArgs :: ModuleInstanceArgs Name -> RenameM ()
@@ -820,10 +805,8 @@ instance Rename NestedModule where
            nm             = thing lnm
        n   <- resolveName NameBind NSModule nm
        depsOf (NamedThing n)
-         do -- XXX: we should store in scope somewhere if we want to browse
-            -- nested modules properly
-            let m' = m { mName = ImpNested <$> mName m }
-            (_inScope,m1) <- renameModule' (ImpNested n) m'
+         do let m' = m { mName = ImpNested <$> mName m }
+            m1 <- renameModule' (ImpNested n) m'
             pure (NestedModule m1 { mName = lnm { thing = n } })
 
 
@@ -1416,8 +1399,6 @@ instance PP RenamedModule where
     doc =
       vcat [ "// --- Defines -----------------------------"
            , pp (rmDefines rn)
-           , "// --- In scope ----------------------------"
-           , pp (rmInScope rn)
            , "// -- Module -------------------------------"
            , pp (rmModule rn)
            , "// -----------------------------------------"