diff --git a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
index 9dbdbdea87..d0d0fcf588 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs
@@ -26,6 +26,8 @@ between these two modules is mostly a function of historical accident.
 
 module CryptolSAWCore.Cryptol
   ( module CryptolSAWCore.GlobalCryptolEnv
+  , ImportVisibility(..)
+  , ImportInfo(..)
 
   , isErasedProp
   , proveProp
@@ -118,6 +120,7 @@ import CryptolSAWCore.Panic
 import qualified CryptolSAWCore.Pretty as CryPP
 import CryptolSAWCore.GlobalCryptolEnv
 
+
 -- | bindTParam' - create a binding for a type parameter, returning 3-tuple:
 --                 - environment
 --                 - the SAWCore kind of the parameter
diff --git a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
index eb515c2d5e..1d15576739 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/CryptolEnv.hs
@@ -103,10 +103,11 @@ import           Cryptol.Utils.Ident
                            , mkIdent, interactiveName, identText
                            , textToModName
                            , prelPrim)
+import           Cryptol.Utils.PP (pretty) -- pp, Doc
 
 -- local:
 import qualified CryptolSAWCore.Cryptol as C
-import           CryptolSAWCore.FileReader 
+import           CryptolSAWCore.FileReader
 import           CryptolSAWCore.GlobalCryptolEnv
 import           CryptolSAWCore.Panic
 import qualified CryptolSAWCore.Pretty as CryPP
@@ -117,6 +118,9 @@ import           SAWCore.SharedTerm (NameInfo, SharedContext, Term, ppTerm)
 import           SAWSupport.Console
 import qualified SAWSupport.Pretty as PPS
 
+-- FIXME: temporary:
+-- import qualified Debug.Trace as TR
+
 ---- Key Types -----------------------------------------------------------------
 
 -- | Input to send to Cryptol's parser, including the starting source position.
@@ -204,9 +208,9 @@ initCryptolEnv sc = do
 
   -- initialize the module environment stored in the context
   (_,refTop) <- liftModuleM sc $ do
-    MM.modifyModuleEnv $ \env -> 
+    MM.modifyModuleEnv $ \env ->
       env { ME.meSearchPath = cryptolPaths ++
-              (instDir </> "lib") : ME.meSearchPath env 
+              (instDir </> "lib") : ME.meSearchPath env
            }
     -- Load Cryptol prelude and magic Array module
     _ <- MB.loadModuleFrom False (MM.FromModule preludeName)
@@ -230,9 +234,9 @@ initCryptolEnv sc = do
       arrayName'            = locatedUnknown arrayName
 
   let env0 = C.mapImports (\_ ->
-            [ mkImport OnlyPublic preludeName'          Nothing Nothing
-            , mkImport OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing
-            , mkImport OnlyPublic arrayName'            Nothing Nothing
+            [ mkImport C.ImportTop OnlyPublic preludeName'          Nothing Nothing
+            , mkImport C.ImportTop OnlyPublic preludeReferenceName' (Just preludeReferenceName) Nothing
+            , mkImport C.ImportTop OnlyPublic arrayName'            Nothing Nothing
             ]) $ C.initEnv
   C.addRefPrims sc refPrims
   -- Generate SAWCore translations for all values in scope
@@ -301,7 +305,6 @@ ioParseResult res = case res of
 --   on with `MR.shadowing` so they hide any imported occurrences.
 --   The environment for each scoping level then shadows everything
 --   above it.
-
 --
 --   Note that while each `sImports` is (mostly) maintained with more
 --   recent imports at the front of the list, this should be
@@ -313,31 +316,83 @@ getNamingEnv sc env = do
   modEnv <- eModuleEnv sc
   return $ eExtraNaming env
     `MR.shadowing`
-    (mconcat $ map (getNamingEnvForImport modEnv)
-                  (eImports env)
-    )
+    (foldr (getNamingEnvForImport modEnv)
+           mempty
+           (eImports env))
 
--- | Get the `MR.NamingEnv` for one `T.Import`.
+-- | Extend the `MR.NamingEnv` for a single import (`ImportData)
 getNamingEnvForImport :: ME.ModuleEnv
-                      -> (ImportVisibility, T.Import)
+                      -> ImportData
                       -> MR.NamingEnv
-getNamingEnvForImport modEnv (vis, imprt) =
-    MN.interpImportEnv'
-      MN.nameToPNameWithQualifiers (T.iAs imprt) (T.iSpec imprt)
-         -- adjusting for qualified imports
-  $ MN.namingEnvNames
-  $ computeNamingEnv lm vis
+                      -> MR.NamingEnv
+getNamingEnvForImport modEnv (importInfo, vis, imprt) nmEnv0 =
+  nmEnv1 <> nmEnv0
 
   where
-  modName :: C.ModName
-  modName = P.thing $ T.iModule imprt
-
-  lm = case ME.lookupModule modName modEnv of
-         Just lm' -> lm'
-         Nothing  -> panic "getNamingEnvForImport"
-                       ["cannot lookupModule: " <> CryPP.pp modName]
+  nmEnv1 =
+      MN.interpImportEnv'
+        nameToPName (T.iAs imprt) (T.iSpec imprt)
+           -- adjusting for qualified imports
+    $ MN.namingEnvNames
+    $ baseNamingEnvToAdd
+
+  -- For submodules, strip the submodule nesting to get unqualified names.
+  -- For top-level modules, use nameToPNameWithQualifiers to preserve paths.
+  nameToPName =
+    case importInfo of
+      C.ImportNested nm -> stripSubmodulePrefix nm
+      C.ImportTop       -> MN.nameToPNameWithQualifiers
+
+  baseNamingEnvToAdd =
+    case importInfo of
+      C.ImportNested nm ->
+          -- find the submodule in the current environment and compute namingEnv
+          -- respecting the visibility parameter (PublicAndPrivate vs OnlyPublic)
+          case ME.modContextOf (P.ImpNested nm) modEnv of
+              Just mc ->
+                case vis of
+                  PublicAndPrivate ->
+                    -- Include all names (public and private) from the submodule
+                    ME.mctxNames mc
+                  OnlyPublic ->
+                    -- Include only exported names
+                    MN.filterUNames (`Set.member` ME.mctxExported mc)
+                                    (ME.mctxNames mc)
+              Nothing -> panic "getNamingEnvForImport"
+                               ["name: " <> Text.pack (show nm)]
+
+      C.ImportTop ->
+          -- find the top-level loaded module and compute NamingEnv:
+          --   NOTE: does not depend on `nmEnv0`
+          let
+            modName :: C.ModName
+            modName = P.thing $ T.iModule imprt
+
+            lm = case ME.lookupModule modName modEnv of
+                   Just lm' -> lm'
+                   Nothing  -> panic "getNamingEnvForImport"
+                                 ["cannot lookupModule: " <> CryPP.pp modName]
+          in
+            computeNamingEnv lm vis
+
+
+-- | Strip the submodule path prefix from a Name.
+-- E.g., intuitively:
+--    stripSubmodulePrefix "X.Y" "X.Y.Z.name" == "Z.name"
+--
+stripSubmodulePrefix :: MN.Name -> MN.Name -> P.PName
+stripSubmodulePrefix submodName name =
+  case C.modPathCommon submodPath (MN.nameModPath name) of
+    Just (_, [], path) | not (null path) ->
+        P.Qual (C.packModName (map C.identText path)) nmIdent
+    _ ->
+        P.UnQual' nmIdent (MN.nameSrc name)
+  where
+  nmIdent = MN.nameIdent name
+  submodPath = C.Nested (MN.nameModPath submodName)
+                        (MN.nameIdent submodName)
 
--- | Compute a `MR.NamingEnv` for a module based on the
+-- | Compute a `MR.NamingEnv` for a loaded module based on the
 --   `ImportVisibility`.
 computeNamingEnv :: ME.LoadedModule -> ImportVisibility -> MR.NamingEnv
 computeNamingEnv lm vis =
@@ -352,7 +407,6 @@ computeNamingEnv lm vis =
     --    - Does not include privates in submodules (which makes for
     --      much of the complications of this function).
     --    - Includes everything in scope at the toplevel of 'lm' module
-
     envTopLevels :: MR.NamingEnv
     envTopLevels = ME.lmNamingEnv lm
 
@@ -629,9 +683,9 @@ bindExtCryptolModule sc (modName, ecm) =
 -- add the module into the import list.
 bindLoadedModule ::
   SharedContext -> (P.ModName, P.Located C.ModName) -> CryptolEnv -> IO CryptolEnv
-bindLoadedModule _ (asName, origName) env = 
-  return $ C.mapImports 
-    ((:) (mkImport PublicAndPrivate origName (Just asName) Nothing)) env
+bindLoadedModule _ (asName, origName) env =
+  return $ C.mapImports
+    ((:) (mkImport C.ImportTop PublicAndPrivate origName (Just asName) Nothing)) env
 
 -- | bindCryptolModule - when we have the @cryptol_prims ()@ created
 --   object, add the `CryptolModule` to the relevant maps in the
@@ -721,7 +775,7 @@ extractDefFromExtCryptolModule sc env_0 ecm name =
 
 -- | Load a Cryptol module and translate its contents to SAWCore.
 --
--- There are three paths here:
+-- There are three paths that lead here:
 --    - `importCryptolModule`, which is the back end for SAWScript @import@
 --    - `loadExtCryptolModule`, which is the back end for SAWScript @cryptol_load@
 --    - `loadCryptolModule`, which is used for Rocq export and from crux-mir-comp
@@ -830,33 +884,117 @@ importCryptolModule ::
   CryptolEnv                {- ^ Extend this environment -} ->
   Either FilePath P.ModName {- ^ Where to find the module -} ->
   Maybe P.ModName           {- ^ Name qualifier -} ->
-  Bool                      {- ^ isSubmodule: True if 'import submodule ...' -} ->
+  C.IsSubmodule             {- ^ isSubmodule: True if 'import submodule ...' -} ->
   ImportVisibility          {- ^ What visibility to give symbols from this module -} ->
   Maybe P.ImportSpec        {- ^ What to import -} ->
   IO CryptolEnv
-importCryptolModule sc env src as False vis imps =
-  -- importing full module:
+importCryptolModule sc env src as isSubmodule vis imps =
+  if isSubmodule then
+    -- importing submodule (which is in current scope):
+    case src of
+      Left _ ->
+          fail $ "`import submodule PATHNAME` is not allowed."
+          -- NOTE: this is allowed by parser (thus we can reach this code).
+          -- FIXME: Would we want to implement this check in the typechecker?
+
+      Right modName ->
+          -- importing submodule by name:
+          do
+          let modNameTxt = C.modNameToText modName
+          mName <- resolveIdentifier' sc env C.NSModule modNameTxt
+          name <- case mName of
+              Nothing -> fail $ "submodule `"
+                                <> Text.unpack modNameTxt
+                                <> "` is not in scope or ambiguous"
+                         -- FIXME: distinguish dups from not in scope!
+              Just nm -> return nm
+
+          let import' = mkImport
+                          (C.ImportNested name)
+                          vis (locatedUnknown modName) as imps
+                        -- FIXME[MT]: verify the above works.
+                        -- FIXME: modname unused?
+                        --   Refactor to make unnecessary?
+
+          -- DEBUG:
+          when debug $
+            do
+            putStrLn $ "modName = " ++ show modName
+            putStrLn $ "name = " ++ show (name :: T.Name)
+            putStrLn $ "submodule: "
+                        ++ (Text.unpack $ C.identText $ MN.nameIdent name)
+            debugImportMT sc import'
+
+          return $ C.mapImports (\imports -> import':imports) env
+            -- FIXME[MT]: Verify you understand what's happening.
+
+  else -- importing full module (by path or name):
+    do
+    mod' <- loadAndTranslateModule sc src
+    let modName = locatedUnknown (T.mName mod')
+    let import' = mkImport C.ImportTop vis modName as imps
+
+    -- DEBUG:
+    when debug $ putStrLn $ "modName= " ++ show modName
+    when debug $ debugImportMT sc import'
+
+    return $ C.mapImports (\imports -> import':imports) env
+
+debug :: Bool
+debug = False
+
+-- Function to print a NamingEnv to stdout
+printNamingEnv :: MN.NamingEnv -> IO ()
+printNamingEnv = putStrLn . pretty
+
+{-
+DEBUG: print what users of the import will get (someawhat duplicating
+       getNamingEnvForImport)
+-}
+debugImportMT :: SharedContext
+              -> ImportData
+              -> IO ()
+debugImportMT sc (info,vis,imprt) =
   do
-  mod' <- loadAndTranslateModule sc src
-  let import' = mkImport vis (locatedUnknown (T.mName mod')) as imps
-  return $ C.mapImports (\imports -> import':imports) env
-importCryptolModule _sc _env (Right __nm) _as True _vis _imps =
-  -- importing submodule by name:
-  -- FIXME: this will be implemented in #2618 (soon).
-  fail $ "`import submodule` is unsupported."
-importCryptolModule _sc _env (Left _)  _as True _vis _imps =
-  -- importing submodule by FilePath: disallowed:
-  fail $ "`import submodule PATHNAME` is not allowed."
-     -- NOTE: this is allowed by parser (thus we can get here).
-     -- FIXME: Would we want to implement this check in the typechecker?
+  modEnv <- eModuleEnv sc
+
+  putStrLn $ "vis: " ++ show vis
+  case vis of
+    OnlyPublic -> return ()
+    _          ->
+        do
+        let ne1_OP =
+                getNamingEnvForImport modEnv (info,OnlyPublic,imprt) mempty
+        putStrLn "ne1_OP (ne1 but only public):"
+        printNamingEnv ne1_OP -- OnlyPublic
+
+  let ne1    = getNamingEnvForImport modEnv (info,vis,imprt) mempty
+  putStrLn "\nimprt:"
+  print imprt
+  putStrLn "\nne1:"
+  printNamingEnv ne1
+
+  where
+
+  {-
+  modName :: C.ModName
+  modName = P.thing $ T.iModule imprt
+
+   -- FIXME[MT]: what was this: ?
+  _lm = case ME.lookupModule modName modEnv of
+         Just lm' -> lm'
+         Nothing  -> panic "debugImportMT: getNamingEnvForImport"
+                       ["cannot lookupModule: " <> CryPP.pp modName]
+  -}
 
 -- | Create an entry for the `eImports` list in `CryptolEnv`.
-mkImport :: ImportVisibility
+mkImport :: C.ImportInfo
+         -> ImportVisibility
          -> P.Located C.ModName
          -> Maybe C.ModName
          -> Maybe T.ImportSpec
-         -> (ImportVisibility, T.Import)
-mkImport vis nm as imps =
+         -> ImportData
+mkImport importInfo vis nm as imps =
     let im = T.Import { T.iModule = nm
                       , T.iAs     = as
                       , T.iSpec   = imps
@@ -864,7 +1002,7 @@ mkImport vis nm as imps =
                       , T.iDoc    = Nothing
                       }
     in
-    (vis, im)
+    (importInfo, vis, im)
 
 
 ---- Binding -------------------------------------------------------------------
@@ -893,7 +1031,7 @@ bindExtraVar :: SharedContext -> (Ident, TypedTerm) -> CryptolEnv -> IO CryptolE
 bindExtraVar sc (ident, TypedTerm (TypedTermSchema schema) trm) env0 = do
   name <- bindIdent sc ident
   let pname = P.mkUnqual ident
-  addExtraVars sc (Map.singleton name schema) 
+  addExtraVars sc (Map.singleton name schema)
   addToAllTerms sc (Map.singleton name trm)
   return $ C.mapNaming (MR.shadowing $ MN.singletonNS C.NSValue pname name) env0
 
@@ -934,7 +1072,7 @@ bindTySyn sc (ident, T.Forall [] [] ty) env = do
   addExtraTySyns sc (Map.singleton name tysyn)
   let pname = P.mkUnqual ident
   return $ C.mapNaming (MR.shadowing (MN.singletonNS C.NSType pname name)) env
-  
+
 bindTySyn _ _ env = pure env -- only monomorphic types may be bound
 
 -- | Add a new Cryptol integer type as an "extra" declration.
@@ -957,30 +1095,33 @@ bindIntegerType sc (ident, n) env = do
 meSolverConfig :: ME.ModuleEnv -> TM.SolverConfig
 meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)
 
-
 -- | Look up an identifier in the Cryptol environment and return its
 --   full name.
 resolveIdentifier ::
   (HasCallStack) =>
   SharedContext -> CryptolEnv -> Text -> IO (Maybe T.Name)
-resolveIdentifier sc env nm = do
+resolveIdentifier sc env = resolveIdentifier' sc env C.NSValue
+
+
+resolveIdentifier' ::
+  (HasCallStack) =>
+  SharedContext -> CryptolEnv -> C.Namespace -> Text -> IO (Maybe T.Name)
+resolveIdentifier' sc env nameSpace nm =
   case splitOn (pack "::") nm of
-    []  -> pure Nothing
-           -- FIXME: shouldn't this be error?
+    []  -> panic "resolveIdentifier'" ["splitOn returning []!"]
     [i] -> doResolve (P.mkUnqual (C.mkIdent i))
     xs  -> let (qs,i) = (init xs, last xs)
            in  doResolve (P.Qual (C.packModName qs) (C.mkIdent i))
     -- FIXME: Is there no function that parses Text into PName?
 
   where
-
   doResolve pnm = do
     nameEnv <- getNamingEnv sc env
     (res, _ws) <- runModuleM sc $
       MM.interactive (MB.rename interactiveName nameEnv
-                            (MR.resolveNameUse C.NSValue pnm))
+                            (MR.resolveNameUse nameSpace pnm))
     case res of
-      Left _ -> return Nothing
+      Left _  -> pure Nothing
       Right x -> pure (Just x)
 
 -- | Read a Cryptol expression from `InputText` and return it as a
@@ -1012,7 +1153,7 @@ pExprToTypedTerm sc env pexpr = do
     -- Eliminate patterns:
     npe <- MM.interactive (MB.noPat pexpr)
 
-    
+
     let npe' = MR.rename npe
     re <- MM.interactive (MB.rename interactiveName nameEnv npe')
       -- NOTE: if a name is not in scope, it is reported here.
diff --git a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
index 51a3d7660e..6dcc629ab8 100644
--- a/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
+++ b/cryptol-saw-core/src/CryptolSAWCore/GlobalCryptolEnv.hs
@@ -12,8 +12,11 @@ Portability : non-portable (language extensions)
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ViewPatterns #-}
 
-module CryptolSAWCore.GlobalCryptolEnv 
+module CryptolSAWCore.GlobalCryptolEnv
   ( ImportVisibility(..)
+  , IsSubmodule
+  , ImportInfo(..)
+  , ImportData
   , isToplevel
   , sameHeight
   , pushScope
@@ -109,6 +112,15 @@ data ImportVisibility
                      --   and (arbitrarily nested) submodules.
   deriving (Eq, Show)
 
+-- | type synonym indicating module is nested (is submodule)
+type IsSubmodule = Bool
+
+-- | capture extra information needed for "import submodule"
+data ImportInfo = ImportNested C.Name  -- ^ "import submodule ..."
+                | ImportTop            -- ^ "import ...
+
+type ImportData = (ImportInfo, ImportVisibility, C.Import)
+  -- FIXME: change to datatype.
 
 -- | The global environment for capturing the Cryptol state, both
 --   Cryptol's own state and the state associated with
@@ -137,7 +149,7 @@ data GlobalCryptolEnv = GlobalCryptolEnv
 initGlobalEnv :: ME.ModuleEnv -> GlobalCryptolEnv
 initGlobalEnv modEnv = refreshCryptolEnv $
     GlobalCryptolEnv modEnv
-      mempty mempty mempty mempty mempty mempty mempty mempty mempty 
+      mempty mempty mempty mempty mempty mempty mempty mempty mempty
       mempty
 
 instance IsMetadata GlobalCryptolEnv where
@@ -167,9 +179,9 @@ instance IsMetadata GlobalCryptolEnv where
   restoreMetadata chk now = return $
     let newMEnv = geModuleEnv now
         chkMEnv = geModuleEnv chk
-    in chk { geModuleEnv = chkMEnv 
+    in chk { geModuleEnv = chkMEnv
                { ME.meNameSeeds = ME.meNameSeeds newMEnv
-               , ME.meSupply = ME.meSupply newMEnv 
+               , ME.meSupply = ME.meSupply newMEnv
                }
            }
 
@@ -182,7 +194,7 @@ instance IsMetadata GlobalCryptolEnv where
 
 data CryptolFrame =
   CryptolFrame { fNamingEnv :: MR.NamingEnv
-               , fImports :: [(ImportVisibility, C.Import)] 
+               , fImports :: [ImportData]
                }
 
 initFrame :: CryptolFrame
@@ -203,12 +215,12 @@ isToplevel (CryptolEnv (_ :| frames)) = null frames
 
 -- | Test if the scopes have the same number of frames pushed.
 sameHeight :: CryptolEnv -> CryptolEnv -> Bool
-sameHeight (CryptolEnv scope1) (CryptolEnv scope2) = 
+sameHeight (CryptolEnv scope1) (CryptolEnv scope2) =
   NE.length scope1 == NE.length scope2
 
-mapCurFrame :: 
-  (CryptolFrame -> CryptolFrame) -> 
-  CryptolEnv -> 
+mapCurFrame ::
+  (CryptolFrame -> CryptolFrame) ->
+  CryptolEnv ->
   CryptolEnv
 mapCurFrame f (CryptolEnv (frame :| frames)) =
   CryptolEnv (f frame :| frames)
@@ -225,30 +237,30 @@ popScope (CryptolEnv frames) = case snd (NE.uncons frames) of
   Just frames' -> CryptolEnv frames'
 
 -- | Map the naming environment of the frame currently in scope.
-mapNaming :: 
-  (MR.NamingEnv -> MR.NamingEnv) -> 
-  CryptolEnv -> 
+mapNaming ::
+  (MR.NamingEnv -> MR.NamingEnv) ->
+  CryptolEnv ->
   CryptolEnv
-mapNaming f = mapCurFrame $ 
+mapNaming f = mapCurFrame $
       \fr -> fr {fNamingEnv = f (fNamingEnv fr) }
 
 -- | Map the module imports of the frame currently in scope.
-mapImports :: 
-  ([(ImportVisibility, C.Import)] -> [(ImportVisibility, C.Import)] ) -> 
-  CryptolEnv -> 
+mapImports ::
+  ([ImportData] -> [ImportData]) ->
+  CryptolEnv ->
   CryptolEnv
-mapImports f = mapCurFrame $ 
+mapImports f = mapCurFrame $
       \fr -> fr {fImports = f (fImports fr) }
 
 -- | Run the inner action bracketed new frame pushed/popped on
 --   the 'CryptolScope' stack.
 --   Fails if the inner action changes the scope height
 --   (i.e. it does not properly bracket its pushes and pops).
-withFreshScope :: 
+withFreshScope ::
   MonadFail m =>
-  CryptolEnv -> 
-  (CryptolEnv -> 
-  m (a, CryptolEnv)) -> 
+  CryptolEnv ->
+  (CryptolEnv ->
+  m (a, CryptolEnv)) ->
   m (a, CryptolEnv)
 withFreshScope env0 f = do
   let env1 = pushScope env0
@@ -319,7 +331,7 @@ eRefPrims = getGlobal geRefPrims
 
 -- | Add entries to 'eRefPrims'
 addRefPrims :: SharedContext -> Map C.PrimIdent C.Expr -> IO ()
-addRefPrims sc m = mapGlobal sc $ \genv -> 
+addRefPrims sc m = mapGlobal sc $ \genv ->
   genv { geRefPrims = Map.union m (geRefPrims genv) }
 
 -- | Map from names of Cryptol primitives to their implementations
@@ -329,7 +341,7 @@ ePrims = getGlobal gePrims
 
 -- | Add entries to 'ePrims'
 addPrims :: SharedContext -> Map C.PrimIdent Term -> IO ()
-addPrims sc m = mapGlobal sc $ \genv -> 
+addPrims sc m = mapGlobal sc $ \genv ->
   genv { gePrims = Map.union m (gePrims genv) }
 
 -- | Map from names of Cryptol primitive types to their
@@ -339,7 +351,7 @@ ePrimTypes = getGlobal gePrimTypes
 
 -- | Add entries to 'ePrimTypes'
 addPrimTypes :: SharedContext -> Map C.PrimIdent Term -> IO ()
-addPrimTypes sc m = mapGlobal sc $ \genv -> 
+addPrimTypes sc m = mapGlobal sc $ \genv ->
   genv { gePrimTypes = Map.union m (gePrimTypes genv) }
 
 
@@ -362,8 +374,8 @@ meSolverConfig env = TM.defaultSolverConfig (ME.meSearchPath env)
 -- | Add an entry to the 'ME.meSearchPath' of the 'eModuleEnv'.
 addSearchPath :: SharedContext -> FilePath -> IO ()
 addSearchPath sc fp = mapGlobal sc $ \genv ->
-  genv { geModuleEnv = (geModuleEnv genv) 
-    { ME.meSearchPath = fp : ME.meSearchPath (geModuleEnv genv) } } 
+  genv { geModuleEnv = (geModuleEnv genv)
+    { ME.meSearchPath = fp : ME.meSearchPath (geModuleEnv genv) } }
 
 -- | Run an 'MM.ModuleM' action using the module environment from
 -- 'eModuleEnv'. If the action is successful, updates the module
@@ -401,7 +413,7 @@ eExtraTySyns = getGlobal geExtraTySyns
 
 -- | Add entries to 'eExtraTySyns'
 addExtraTySyns :: SharedContext -> Map C.Name C.TySyn -> IO ()
-addExtraTySyns sc m = mapGlobal sc $ \genv -> 
+addExtraTySyns sc m = mapGlobal sc $ \genv ->
   genv { geExtraTySyns = Map.union m (geExtraTySyns genv) }
 
 -- | Formerly @eExtraTypes@, holds the Cryptol-level
@@ -412,9 +424,9 @@ eExtraVars = getGlobal geExtraVars
 
 -- | Add entries to both 'eExtraVars' and 'eAllVars'
 addExtraVars :: SharedContext -> Map C.Name C.Schema -> IO ()
-addExtraVars sc m = mapGlobal sc $ \genv -> 
+addExtraVars sc m = mapGlobal sc $ \genv ->
   genv { geExtraVars = Map.union m (geExtraVars genv)
-       , geAllVars = Map.union m (geAllVars genv) 
+       , geAllVars = Map.union m (geAllVars genv)
        }
 
 -- | Map from Cryptol names to Cryptol types. This is
@@ -457,7 +469,7 @@ eTyVars = getGlobal geTyVars
 
 -- | Add entries to 'eTyVars'
 addTyVars :: SharedContext -> Map Int Term -> IO ()
-addTyVars sc m = mapGlobal sc $ \genv -> 
+addTyVars sc m = mapGlobal sc $ \genv ->
   genv { geTyVars = Map.union m (geTyVars genv) }
 
 -- | Map from Cryptol `C.Prop`, which are type constraints, to
@@ -483,7 +495,7 @@ eTyProps = getGlobal geTyProps
 --   This is not expensive, but would become problematic
 --   if we wanted to enforce a write-once policy.
 addTyProps :: SharedContext -> Map C.Prop (Term, [FieldName]) -> IO ()
-addTyProps sc m = mapGlobal sc $ \genv -> 
+addTyProps sc m = mapGlobal sc $ \genv ->
   genv { geTyProps = Map.union m (geTyProps genv)  }
 
 -- | The translations for all Cryptol names in scope. It maps names to
@@ -508,7 +520,7 @@ eFFITypes = getGlobal geFFITypes
 
 -- | Add entries to 'eFFITypes'
 addFFITypes :: SharedContext -> Map NameInfo C.FFI -> IO ()
-addFFITypes sc m = mapGlobal sc $ \genv -> 
+addFFITypes sc m = mapGlobal sc $ \genv ->
   genv { geFFITypes = Map.union m (geFFITypes genv) }
 
 --
@@ -530,7 +542,7 @@ addFFITypes sc m = mapGlobal sc $ \genv ->
 -- irregularities that can creep in when we reimplement Cryptol name
 -- resolution.
 eExtraNaming :: CryptolEnv -> MR.NamingEnv
-eExtraNaming (CryptolEnv (frame :| frames)) = 
+eExtraNaming (CryptolEnv (frame :| frames)) =
   foldr (\fr ne -> ne `MR.shadowing` (fNamingEnv fr)) (fNamingEnv frame) frames
 
 -- | The list of Cryptol modules which have been brought into the
@@ -540,8 +552,8 @@ eExtraNaming (CryptolEnv (frame :| frames)) =
 --   according to the associated 'ImportVisibility'. The modules here
 --   should only correspond to modules that are present in the module
 --   environment *and* have been translated into SAWCore.
-eImports :: CryptolEnv -> [(ImportVisibility, C.Import)]
-eImports (CryptolEnv frames) = 
+eImports :: CryptolEnv -> [ImportData]
+eImports (CryptolEnv frames) =
   concat $ map fImports $ NE.toList frames
 
 
diff --git a/intTests/test_cryptolquotes/.gitignore b/intTests/test_cryptolquotes/.gitignore
new file mode 100644
index 0000000000..4619758def
--- /dev/null
+++ b/intTests/test_cryptolquotes/.gitignore
@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff
diff --git a/intTests/test_cryptolquotes/Makefile b/intTests/test_cryptolquotes/Makefile
new file mode 100644
index 0000000000..c9e12c62ae
--- /dev/null
+++ b/intTests/test_cryptolquotes/Makefile
@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean
diff --git a/intTests/test_cryptolquotes/P.cry b/intTests/test_cryptolquotes/P.cry
new file mode 100644
index 0000000000..e221a32fd5
--- /dev/null
+++ b/intTests/test_cryptolquotes/P.cry
@@ -0,0 +1,9 @@
+module P where
+
+p1 = "p1"
+
+submodule P2 where
+  p2 = "p2"
+
+  submodule P3 where
+    p3 = "p3"
\ No newline at end of file
diff --git a/intTests/test_cryptolquotes/test.sh b/intTests/test_cryptolquotes/test.sh
new file mode 100755
index 0000000000..5fcd79d0a6
--- /dev/null
+++ b/intTests/test_cryptolquotes/test.sh
@@ -0,0 +1 @@
+exec ${TEST_SHELL:-bash} ../support/test-and-diff.sh "$@"
diff --git a/intTests/test_cryptolquotes/testQuotes1a.log.good b/intTests/test_cryptolquotes/testQuotes1a.log.good
new file mode 100644
index 0000000000..498b12066e
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1a.log.good
@@ -0,0 +1,8 @@
+Loading file "testQuotes1a.saw"
+ss: p1a
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+testQuotes1a.saw:9:5-9:7: Warning: Redeclaration of p1
+testQuotes1a.saw:1:5-1:7: Warning: Previous declaration was here
+ss: p1b
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes1a.saw b/intTests/test_cryptolquotes/testQuotes1a.saw
new file mode 100644
index 0000000000..be594195c4
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1a.saw
@@ -0,0 +1,11 @@
+let p1 = "ss: p1a";
+print p1;
+print {{ p1 }};
+
+import "P.cry";
+
+print {{ p1 }};
+
+let p1 = "ss: p1b";
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_cryptolquotes/testQuotes1b.log.good b/intTests/test_cryptolquotes/testQuotes1b.log.good
new file mode 100644
index 0000000000..c43d2ba49a
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1b.log.good
@@ -0,0 +1,4 @@
+Loading file "testQuotes1b.saw"
+[112, 49]
+ss: p1b
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes1b.saw b/intTests/test_cryptolquotes/testQuotes1b.saw
new file mode 100644
index 0000000000..a65802454e
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes1b.saw
@@ -0,0 +1,7 @@
+import "P.cry";
+
+print {{ p1 }};
+
+let p1 = "ss: p1b";
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_cryptolquotes/testQuotes2a.log.good b/intTests/test_cryptolquotes/testQuotes2a.log.good
new file mode 100644
index 0000000000..48415fb59c
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2a.log.good
@@ -0,0 +1,9 @@
+Loading file "testQuotes2a.saw"
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+[115, 115, 58, 32, 112, 49, 97]
+testQuotes2a.saw:10:5-10:7: Warning: Redeclaration of p1
+testQuotes2a.saw:1:5-1:7: Warning: Previous declaration was here
+[115, 115, 58, 32, 112, 49, 98]
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes2a.saw b/intTests/test_cryptolquotes/testQuotes2a.saw
new file mode 100644
index 0000000000..5bce2aaac7
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2a.saw
@@ -0,0 +1,12 @@
+let p1 = {{ "ss: p1a" }};
+print p1;
+print {{ p1 }};
+
+import "P.cry";
+
+print p1;
+print {{ p1 }};
+
+let p1 = {{ "ss: p1b" }};
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_cryptolquotes/testQuotes2b.log.good b/intTests/test_cryptolquotes/testQuotes2b.log.good
new file mode 100644
index 0000000000..6c5e6eaa1c
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2b.log.good
@@ -0,0 +1,4 @@
+Loading file "testQuotes2b.saw"
+[112, 49]
+[115, 115, 58, 32, 112, 49, 98]
+[115, 115, 58, 32, 112, 49, 98]
diff --git a/intTests/test_cryptolquotes/testQuotes2b.saw b/intTests/test_cryptolquotes/testQuotes2b.saw
new file mode 100644
index 0000000000..868ea30d41
--- /dev/null
+++ b/intTests/test_cryptolquotes/testQuotes2b.saw
@@ -0,0 +1,7 @@
+import "P.cry";
+
+print {{ p1 }};
+
+let p1 = {{ "ss: p1b" }};
+print p1;
+print {{ p1 }};
diff --git a/intTests/test_saw_import/M.cry b/intTests/test_saw_import/M.cry
new file mode 100644
index 0000000000..a6af940ee4
--- /dev/null
+++ b/intTests/test_saw_import/M.cry
@@ -0,0 +1,7 @@
+module M where
+
+newtype T = { x : Bit }
+
+t1 = T{x= 1}
+
+type U = T
diff --git a/intTests/test_saw_import/testNewTypes.log.good b/intTests/test_saw_import/testNewTypes.log.good
new file mode 100644
index 0000000000..167f53bded
--- /dev/null
+++ b/intTests/test_saw_import/testNewTypes.log.good
@@ -0,0 +1,22 @@
+Loading file "testNewTypes.saw"
+{x = True}
+{x = True}
+
+errors follow:
+
+Error: Cryptol: [error] at testNewTypes.saw:9:25--9:26
+    Type not in scope: T
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:9:1-9:31 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testNewTypes.saw:12:20--12:21
+    Value not in scope: T
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:12:1-12:31 (at top level)
+
+(Failure was expected, continuing)
diff --git a/intTests/test_saw_import/testNewTypes.saw b/intTests/test_saw_import/testNewTypes.saw
new file mode 100644
index 0000000000..a6aef1a09d
--- /dev/null
+++ b/intTests/test_saw_import/testNewTypes.saw
@@ -0,0 +1,12 @@
+import "M.cry" hiding (T);
+
+print {{ t1 }};
+print {{ t1:U }};
+
+print "\nerrors follow:\n";
+
+// the Type T (of the newtype) is hidden, will fail:
+fails (do{print {{ t1 : T }};}) ;
+
+// the constructor T of the newtype is hidden, will fail:
+fails (do{print {{ T{x=1} }};}) ;
diff --git a/intTests/test_saw_submodule_access1/D.cry b/intTests/test_saw_submodule_access1/D.cry
index c806e3e091..1d0414090c 100644
--- a/intTests/test_saw_submodule_access1/D.cry
+++ b/intTests/test_saw_submodule_access1/D.cry
@@ -14,6 +14,7 @@ submodule D2 where
 
   submodule D3 where
     d3 = d00 + d2 + 1  // 14229
+    d4 = d5
 
     type D3TySy = [32]
 
@@ -21,5 +22,6 @@ submodule D2 where
 //  - type synonyms and values
 d01 : D2::D3::D3TySy
 d01 = 5 + D2::d2   // D2 is not referencable till now!
-    + D2::D3::d3   
+    + D2::D3::d3
 
+d5 = 1  // we can reference this from above submodule!
diff --git a/intTests/test_saw_submodule_import/F.cry b/intTests/test_saw_submodule_import/F.cry
new file mode 100644
index 0000000000..bc327efc59
--- /dev/null
+++ b/intTests/test_saw_submodule_import/F.cry
@@ -0,0 +1,27 @@
+module F where
+
+import D as D_A (d00, notinscope)
+import D as D_B hiding (d00, notinscope)
+
+x = D_A::d00
+
+// NOTE: one cannot import qualified names in 'D', e.g., D2::d2, D2::D3
+import D(d00)             //
+import D                  // D2 now in scope
+import D(D2)              // D2 in scope
+import D hiding (D2,d01)  // cryptol allows us to hide submodule D2
+
+import submodule D2 (d2,D3)
+
+x2 = d2
+
+import submodule D3 (d3)
+
+x3 = d3
+
+submodule D2a = submodule D2
+
+x4 = D2a::d2
+
+submodule FSubMod where
+  d3' = 1 + x4
diff --git a/intTests/test_saw_submodule_import/M.cry b/intTests/test_saw_submodule_import/M.cry
new file mode 100644
index 0000000000..29ddc72199
--- /dev/null
+++ b/intTests/test_saw_submodule_import/M.cry
@@ -0,0 +1,12 @@
+module M where
+
+submodule S1 where
+
+  newtype T1 = { x : [8] }
+
+  t11 = T1{x= 1}
+
+type T2 = S1::T1
+
+T2 = (S1::T1)
+t2 = T2{x=2}
diff --git a/intTests/test_saw_submodule_import/cryptol-bug/D.cry b/intTests/test_saw_submodule_import/cryptol-bug/D.cry
new file mode 100644
index 0000000000..c2ac844c56
--- /dev/null
+++ b/intTests/test_saw_submodule_import/cryptol-bug/D.cry
@@ -0,0 +1,4 @@
+module D where
+
+submodule D2 where
+  d2 = 2
diff --git a/intTests/test_saw_submodule_import/cryptol-bug/F.cry b/intTests/test_saw_submodule_import/cryptol-bug/F.cry
new file mode 100644
index 0000000000..612494c2fe
--- /dev/null
+++ b/intTests/test_saw_submodule_import/cryptol-bug/F.cry
@@ -0,0 +1,16 @@
+module F where
+
+import D                   // D2 now in scope
+
+submodule D2a = submodule D2  // PREVIEW: problematic when F imported.
+
+x1 = D2a::d2                  // sanity check.
+
+submodule D3 where            // PREVIEW: works as expected.
+  d3 = 3
+
+private submodule D4 where    // PREVIEW: works as expected.
+  d4 = 4
+
+submodule D4a = submodule D4  // PREVEW: works as expected
+                              //   D4a is public alias to private submodule
diff --git a/intTests/test_saw_submodule_import/cryptol-bug/G.cry b/intTests/test_saw_submodule_import/cryptol-bug/G.cry
new file mode 100644
index 0000000000..6bf3ab72ce
--- /dev/null
+++ b/intTests/test_saw_submodule_import/cryptol-bug/G.cry
@@ -0,0 +1,40 @@
+module G where
+
+import F
+
+// things work when D3 is submodule defined in F:
+import submodule D3
+x1 = d3
+
+
+// things work when D4a is an alias to private sub-module of F:
+import submodule D4a
+x2 = d4
+
+
+/*
+// when we try to import private submodule, we get reasonable error:
+import submodule D4  // gives error HERE.
+                     //   Module not in scope: D4
+x3 = d4              // doesn't get here.
+*/
+
+
+/*
+// Gives slightly suspicious errors/non-errors
+// when we try to import a submodule "two imports away" that should not be
+// visible.
+import submodule D2
+  // INTERESTING and SUSPICIOUS:
+  //   The submodule D2 is not in scope, but we do not get this message
+  //     "Module not in scope: D2"
+  //   -
+x4 = d2
+  // This gives error:
+  //   Value not in scope: d2
+*/
+
+// The problematic case:
+import submodule D2a
+x5 = d2
+     // d2 reference crashes cryptol.
diff --git a/intTests/test_saw_submodule_import/testGoodImport1.log.good b/intTests/test_saw_submodule_import/testGoodImport1.log.good
index 4d67535fe7..2016318ff8 100644
--- a/intTests/test_saw_submodule_import/testGoodImport1.log.good
+++ b/intTests/test_saw_submodule_import/testGoodImport1.log.good
@@ -1,2 +1,8 @@
 Loading file "testGoodImport1.saw"
+12114
+14229
+14229
+12114
+14229
+14229
 done
diff --git a/intTests/test_saw_submodule_import/testGoodImport1.saw b/intTests/test_saw_submodule_import/testGoodImport1.saw
index 71edc9f5ad..0632fc7575 100644
--- a/intTests/test_saw_submodule_import/testGoodImport1.saw
+++ b/intTests/test_saw_submodule_import/testGoodImport1.saw
@@ -1,3 +1,29 @@
 import "D.cry";
 
+// access vars fully qualified:
+print {{D2::d2}};
+print {{D2::D3::d3}};
+
+// direct import of doubly nested submodule:
+import submodule D2::D3 as D2_D3;
+print {{D2_D3::d3}};
+
+
+// submodule D2 is in scope, let's import it:
+import submodule D2;
+
+// can now access `D2::d2` w/o "D2" prefix:
+print {{d2}};
+
+// and D3 is in scope:
+print {{D3::d3}};
+
+///////////////////////////////////////
+// Now test we can import what's brought in scope by import.
+
+// let's import submodule D3.
+import submodule D3;
+
+print {{d3}};  // can now access w/o "D3::" prefix.
+
 print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport10.log.good b/intTests/test_saw_submodule_import/testGoodImport10.log.good
new file mode 100644
index 0000000000..dd5ab92aa2
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport10.log.good
@@ -0,0 +1,6 @@
+Loading file "testGoodImport10.saw"
+12114
+14229
+0
+0
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport10.saw b/intTests/test_saw_submodule_import/testGoodImport10.saw
new file mode 100644
index 0000000000..7f724458ce
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport10.saw
@@ -0,0 +1,13 @@
+// Test: Import with empty hiding list (should import everything)
+
+import "D.cry";
+
+import submodule D2 hiding ();
+
+// Everything should be accessible
+print {{d2}};
+print {{D3::d3}};
+print {{0 : D2TySy}};
+print {{0 : D3::D3TySy}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport11.log.good b/intTests/test_saw_submodule_import/testGoodImport11.log.good
new file mode 100644
index 0000000000..2138969663
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport11.log.good
@@ -0,0 +1,9 @@
+Loading file "testGoodImport11.saw"
+12114
+("MYSTRING", 5)
+12114
+testGoodImport11.saw:23:5-23:7: Warning: Redeclaration of d2
+testGoodImport11.saw:13:5-13:7: Warning: Previous declaration was here
+12115
+12115
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport11.saw b/intTests/test_saw_submodule_import/testGoodImport11.saw
new file mode 100644
index 0000000000..6e1ff7b2d9
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport11.saw
@@ -0,0 +1,27 @@
+// Test: Shadowing - import submodule that shadows top-level names
+
+import "D.cry";
+
+// Import D2 unqualified (brings d2 into scope)
+import submodule D2;
+
+// print D2::d2:
+print {{d2}};         // we get the value in D::D2::d2
+
+
+// Define sawscript local variable that does not shadow (no Cryptol type for)
+let d2 = ("MYSTRING",5);
+print d2;
+
+// Original d2 is shadowed inside {{-}}'s as ...
+print {{d2}};
+  // still, we get the value in D::D2::d2
+  // because the type of d2 is not one of the
+  // 'special' "use inside {{-}}" types.
+
+// Define sawscript local variable that does shadow:
+let d2 = {{d2 + 1}};
+print d2;        //
+print {{d2}};   // this and ^, both show 12115 == D::D2::D1 + 1
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport12.log.good b/intTests/test_saw_submodule_import/testGoodImport12.log.good
new file mode 100644
index 0000000000..665c2c4583
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport12.log.good
@@ -0,0 +1,8 @@
+Loading file "testGoodImport12.saw"
+12114
+12114
+12114
+14229
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport12.saw b/intTests/test_saw_submodule_import/testGoodImport12.saw
new file mode 100644
index 0000000000..aeb964b4cb
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport12.saw
@@ -0,0 +1,21 @@
+// Test: Import same submodule with multiple different qualifications
+
+import "D.cry";
+
+// Import D2 unqualified
+import submodule D2;
+
+// Also import D2 with qualification
+import submodule D2 as D2_Alias;
+
+// Both should work:
+print {{d2}};           // from unqualified import
+print {{D2::d2}};       // original qualified path
+print {{D2_Alias::d2}}; // from aliased import
+
+// Nested submodule should work through all paths:
+print {{D3::d3}};
+print {{D2::D3::d3}};
+print {{D2_Alias::D3::d3}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport13.log.good b/intTests/test_saw_submodule_import/testGoodImport13.log.good
new file mode 100644
index 0000000000..003939bb5f
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport13.log.good
@@ -0,0 +1,18 @@
+Loading file "testGoodImport13.saw"
+Error: Cryptol: [error] at testGoodImport13.saw:9:22--9:24
+    Value not in scope: d2
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport13.saw:9:1-9:29 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport13.saw:10:22--10:28
+    Value not in scope: D3::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport13.saw:10:1-10:33 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport13.saw b/intTests/test_saw_submodule_import/testGoodImport13.saw
new file mode 100644
index 0000000000..26e5bf2c5e
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport13.saw
@@ -0,0 +1,12 @@
+// Test: Import with parenthesized empty list (different from no parens)
+
+import "D.cry";
+
+// Empty list means import nothing
+import submodule D2 ();
+
+// Should fail - nothing was imported
+fails ( do { print {{d2}}; } );
+fails ( do { print {{D3::d3}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport14.log.good b/intTests/test_saw_submodule_import/testGoodImport14.log.good
new file mode 100644
index 0000000000..22a1477006
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14.log.good
@@ -0,0 +1,6 @@
+Loading file "testGoodImport14.saw"
+14229
+12114
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport14.saw b/intTests/test_saw_submodule_import/testGoodImport14.saw
new file mode 100644
index 0000000000..7298d2b2dd
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14.saw
@@ -0,0 +1,17 @@
+// Test: Import nested submodule, then separately import its parent
+
+import "D.cry";
+
+// First import the nested D3
+import submodule D2::D3 as MyD3;
+print {{MyD3::d3}};
+
+// Now import its parent D2
+import submodule D2;
+print {{d2}};
+
+// Both paths to D3 should work:
+print {{MyD3::d3}};
+print {{D3::d3}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport14b.log.good b/intTests/test_saw_submodule_import/testGoodImport14b.log.good
new file mode 100644
index 0000000000..115a174b78
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14b.log.good
@@ -0,0 +1,7 @@
+Loading file "testGoodImport14b.saw"
+14229
+12114
+14229
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport14b.saw b/intTests/test_saw_submodule_import/testGoodImport14b.saw
new file mode 100644
index 0000000000..a90b5e5527
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport14b.saw
@@ -0,0 +1,19 @@
+// Test: Import nested submodule, then separately import its parent
+//    - Differs from testGoodImport14.saw: 1st `import submodule` has no `as`
+
+import "D.cry";
+
+// First import the nested D3
+import submodule D2::D3;
+print {{d3}};
+
+// Now import its parent D2
+import submodule D2;
+print {{d2}};
+
+// All paths to D::D2::D3::d should work:
+print {{d3}};
+print {{D3::d3}};
+print {{D2::D3::d3}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport15.log.good b/intTests/test_saw_submodule_import/testGoodImport15.log.good
new file mode 100644
index 0000000000..9488810994
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport15.log.good
@@ -0,0 +1,11 @@
+Loading file "testGoodImport15.saw"
+0
+Error: Cryptol: [error] at testGoodImport15.saw:12:22--12:24
+    Value not in scope: d2
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport15.saw:12:1-12:29 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport15.saw b/intTests/test_saw_submodule_import/testGoodImport15.saw
new file mode 100644
index 0000000000..1eb95d6399
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport15.saw
@@ -0,0 +1,14 @@
+// Test: Selective import of type synonym but not values
+
+import "D.cry";
+
+// Import only the type synonym, not the value
+import submodule D2 (D2TySy);
+
+// Should work: type is imported
+print {{0 : D2TySy}};
+
+// Should fail: value was not imported
+fails ( do { print {{d2}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport2.log.good b/intTests/test_saw_submodule_import/testGoodImport2.log.good
new file mode 100644
index 0000000000..7c2f2d8336
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport2.log.good
@@ -0,0 +1,7 @@
+Loading file "testGoodImport2.saw"
+12114
+14229
+12114
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport2.saw b/intTests/test_saw_submodule_import/testGoodImport2.saw
new file mode 100644
index 0000000000..d45f02745d
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport2.saw
@@ -0,0 +1,27 @@
+// This test mirrors testGoodImport1 but with "import submodule ... as ..."
+//                                                                  --
+
+import "D.cry";
+
+// access vars fully qualified:
+print {{D2::d2}};
+print {{D2::D3::d3}};
+
+// submodule D2 is in scope, let's import it qualified:
+import submodule D2 as MYD2;
+
+// can now access elements w/ "MYD2" prefix:
+print {{MYD2::d2}};
+
+// and we can accesss submodule D3 via MYD2::D3
+print {{MYD2::D3::d3}};
+
+///////////////////////////////////////
+// Now test we can import what's brought in scope by import.
+
+// let's import submodule D3:
+import submodule MYD2::D3 as MYD3;
+
+print {{MYD3::d3}}; // can now access w/ "MYD3::" prefix.
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport3.log.good b/intTests/test_saw_submodule_import/testGoodImport3.log.good
new file mode 100644
index 0000000000..e5009a6445
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport3.log.good
@@ -0,0 +1,19 @@
+Loading file "testGoodImport3.saw"
+12114
+Error: Cryptol: [error] at testGoodImport3.saw:13:22--13:28
+    Value not in scope: D3::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport3.saw:13:1-13:33 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport3.saw:19:27--19:33
+    Type not in scope: D2TySy
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport3.saw:19:1-19:39 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport3.saw b/intTests/test_saw_submodule_import/testGoodImport3.saw
new file mode 100644
index 0000000000..bb270debef
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport3.saw
@@ -0,0 +1,22 @@
+// Exercise more of the `import submodule` variances.
+
+import "D.cry";
+
+import submodule D2 (d2);
+
+print {{d2}};
+
+// expected failures:
+
+// test 1: ensure submodules of D2 are not in scope: /////
+
+fails ( do { print {{D3::d3}}; } );
+  // should fail b/c D3 & D3::d3 are not in scope
+
+
+// test 2: ensure types in D2 are not in scope: //////////
+
+fails ( do { print {{ 0 : D2TySy }}; } );
+  // should fail b/c D2TySy is not in scope
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport4.log.good b/intTests/test_saw_submodule_import/testGoodImport4.log.good
new file mode 100644
index 0000000000..6409e5e0d4
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport4.log.good
@@ -0,0 +1,20 @@
+Loading file "testGoodImport4.saw"
+14229
+0
+Error: Cryptol: [error] at testGoodImport4.saw:16:22--16:24
+    Value not in scope: d2
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport4.saw:16:1-16:29 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport4.saw:17:26--17:32
+    Type not in scope: D2TySy
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport4.saw:17:1-17:37 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport4.saw b/intTests/test_saw_submodule_import/testGoodImport4.saw
new file mode 100644
index 0000000000..a9a93d284e
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport4.saw
@@ -0,0 +1,19 @@
+// Exercise more of the `import submodule` variances.
+
+import "D.cry";
+
+import submodule D2 hiding (d2, D2TySy);
+
+
+// test 1: check we can access names not hid:
+
+print {{D3::d3 }};
+print {{0 : D3::D3TySy }};
+
+
+// test 2: ensure hidden symbols are hiddden:
+
+fails ( do { print {{d2}}; } );
+fails ( do { print {{0 : D2TySy}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport5.log.good b/intTests/test_saw_submodule_import/testGoodImport5.log.good
new file mode 100644
index 0000000000..720ca07f6f
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport5.log.good
@@ -0,0 +1,29 @@
+Loading file "testGoodImport5.saw"
+14229
+0
+14229
+Error: Cryptol: [error] at testGoodImport5.saw:17:23--17:25
+    Value not in scope: d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport5.saw:17:1-17:31 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport5.saw:18:23--18:31
+    Value not in scope: Y::Z::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport5.saw:18:1-18:37 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testGoodImport5.saw:19:23--19:31
+    Value not in scope: X::Y::d3
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport5.saw:19:1-19:37 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport5.saw b/intTests/test_saw_submodule_import/testGoodImport5.saw
new file mode 100644
index 0000000000..4e736eeb82
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport5.saw
@@ -0,0 +1,22 @@
+// Exercise more of the `import submodule` variances.
+
+import "D.cry";
+
+import submodule D2::D3 as X::Y::Z;
+
+// test 1: check we can access names:
+
+print {{ X::Y::Z::d3 }};
+print {{ 0 : X::Y::Z::D3TySy }};
+
+// test 2: still access the 'default' names brought into scope by 1st import?
+print {{ D2::D3::d3 }};
+
+// test 3:
+// Various fails
+fails ( do { print {{ d3 }}; } );
+fails ( do { print {{ Y::Z::d3 }}; } );
+fails ( do { print {{ X::Y::d3 }}; } );
+
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport6.log.good b/intTests/test_saw_submodule_import/testGoodImport6.log.good
new file mode 100644
index 0000000000..288c8c3383
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport6.log.good
@@ -0,0 +1,11 @@
+Loading file "testGoodImport6.saw"
+14229
+Error: Cryptol: [error] at testGoodImport6.saw:12:26--12:38
+    Type not in scope: MyD3::D3TySy
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testGoodImport6.saw:12:1-12:43 (at top level)
+
+(Failure was expected, continuing)
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport6.saw b/intTests/test_saw_submodule_import/testGoodImport6.saw
new file mode 100644
index 0000000000..d7b648026e
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport6.saw
@@ -0,0 +1,14 @@
+// Test: Import nested submodule with 'as' and 'hiding' together
+
+import "D.cry";
+
+// Test importing deeply nested submodule with both 'as' and 'hiding'
+import submodule D2::D3 as MyD3 hiding (D3TySy);
+
+// Should work: d3 is imported
+print {{MyD3::d3}};
+
+// Should fail: D3TySy is hidden
+fails ( do { print {{0 : MyD3::D3TySy}}; } );
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testGoodImport8.log.good b/intTests/test_saw_submodule_import/testGoodImport8.log.good
new file mode 100644
index 0000000000..32c9f55d75
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport8.log.good
@@ -0,0 +1,5 @@
+Loading file "testGoodImport8.saw"
+12114
+14229
+14229
+done
diff --git a/intTests/test_saw_submodule_import/testGoodImport8.saw b/intTests/test_saw_submodule_import/testGoodImport8.saw
new file mode 100644
index 0000000000..417fb67436
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testGoodImport8.saw
@@ -0,0 +1,19 @@
+// Test: Import submodule qualified, then import nested submodule
+//       from the qualified name
+
+import "D.cry";
+
+// Import D2 qualified as MyD2
+import submodule D2 as MyD2;
+
+// Now import the nested D3 via the qualified path
+import submodule MyD2::D3 as MyD3;
+
+// Both should work:
+print {{MyD2::d2}};
+print {{MyD3::d3}};
+
+// Test accessing via full path through MyD2
+print {{MyD2::D3::d3}};
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors1.saw b/intTests/test_saw_submodule_import/testImportErrors1.saw
index f62a753078..ad4ff5d3a2 100644
--- a/intTests/test_saw_submodule_import/testImportErrors1.saw
+++ b/intTests/test_saw_submodule_import/testImportErrors1.saw
@@ -1,3 +1,4 @@
 import submodule "D.cry";
+  // An error to "import submodule" a top-level module.
 
 print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors2.log.good b/intTests/test_saw_submodule_import/testImportErrors2.log.good
index 6449490fbb..d12bf560e1 100644
--- a/intTests/test_saw_submodule_import/testImportErrors2.log.good
+++ b/intTests/test_saw_submodule_import/testImportErrors2.log.good
@@ -1,6 +1,6 @@
 Loading file "testImportErrors2.saw"
 Stack trace:
    (builtin) (at top level)
-`import submodule` is unsupported.
+submodule `D` is not in scope or ambiguous
 
 FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors2.saw b/intTests/test_saw_submodule_import/testImportErrors2.saw
index 2e4c424cc1..7377c1c027 100644
--- a/intTests/test_saw_submodule_import/testImportErrors2.saw
+++ b/intTests/test_saw_submodule_import/testImportErrors2.saw
@@ -1,3 +1,5 @@
 import submodule D;
+  // D is not in scope, thus an error.
+  // NOTE: we do not search for top-level modules named 'D'.
 
 print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors3.log.good b/intTests/test_saw_submodule_import/testImportErrors3.log.good
new file mode 100644
index 0000000000..db55677faf
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors3.log.good
@@ -0,0 +1,6 @@
+Loading file "testImportErrors3.saw"
+Stack trace:
+   (builtin) (at top level)
+submodule `D3` is not in scope or ambiguous
+
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors3.saw b/intTests/test_saw_submodule_import/testImportErrors3.saw
new file mode 100644
index 0000000000..8a03492d9b
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors3.saw
@@ -0,0 +1,4 @@
+import "D.cry";
+
+// import submodule D2::D3;   // this would work
+import submodule D3;          // this should *not* work
diff --git a/intTests/test_saw_submodule_import/testImportErrors4.log.good b/intTests/test_saw_submodule_import/testImportErrors4.log.good
new file mode 100644
index 0000000000..06eb5ca2f2
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors4.log.good
@@ -0,0 +1,3 @@
+Loading file "testImportErrors4.saw"
+testImportErrors4.saw:6:24-6:26: Error: Syntax error: missing ')'
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors4.saw b/intTests/test_saw_submodule_import/testImportErrors4.saw
new file mode 100644
index 0000000000..2b4323134d
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors4.saw
@@ -0,0 +1,8 @@
+// Test: Error case - trying to import submodule with wrong qualification
+
+import "D.cry";
+
+// This should error: trying to use full qualified path in import spec list
+import submodule D2 (D2::d2);
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors5.log.good b/intTests/test_saw_submodule_import/testImportErrors5.log.good
new file mode 100644
index 0000000000..d917f0e154
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors5.log.good
@@ -0,0 +1,6 @@
+Loading file "testImportErrors5.saw"
+Stack trace:
+   (builtin) (at top level)
+submodule `D2::D4` is not in scope or ambiguous
+
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors5.saw b/intTests/test_saw_submodule_import/testImportErrors5.saw
new file mode 100644
index 0000000000..c564752113
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors5.saw
@@ -0,0 +1,8 @@
+// Test: Error case - importing nonexistent submodule
+
+import "D.cry";
+
+// D2 exists, but D2::D4 does not
+import submodule D2::D4;
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors6.log.good b/intTests/test_saw_submodule_import/testImportErrors6.log.good
new file mode 100644
index 0000000000..f22e8da740
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors6.log.good
@@ -0,0 +1,3 @@
+Loading file "testImportErrors6.saw"
+testImportErrors6.saw:6:27-6:29: Error: Syntax error: missing name
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors6.saw b/intTests/test_saw_submodule_import/testImportErrors6.saw
new file mode 100644
index 0000000000..9eee5691f4
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors6.saw
@@ -0,0 +1,8 @@
+// Test: Error case - trying to import with 'as' using invalid path syntax
+
+import "D.cry";
+
+// Invalid: empty component in path
+import submodule D2 as A::::B;
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testImportErrors7.log.good b/intTests/test_saw_submodule_import/testImportErrors7.log.good
new file mode 100644
index 0000000000..bccd61f948
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors7.log.good
@@ -0,0 +1,3 @@
+Loading file "testImportErrors7.saw"
+testImportErrors7.saw:6:26-6:32: Error: Syntax error: missing ';'
+FAILED
diff --git a/intTests/test_saw_submodule_import/testImportErrors7.saw b/intTests/test_saw_submodule_import/testImportErrors7.saw
new file mode 100644
index 0000000000..f01aa5e777
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testImportErrors7.saw
@@ -0,0 +1,8 @@
+// Test: Error case - hiding and importing list together (should conflict)
+
+import "D.cry";
+
+// This should be an error: can't have both hiding and import list
+import submodule D2 (d2) hiding (D2TySy);
+
+print "done";
diff --git a/intTests/test_saw_submodule_import/testNewTypes.log.good b/intTests/test_saw_submodule_import/testNewTypes.log.good
new file mode 100644
index 0000000000..5246c38aea
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testNewTypes.log.good
@@ -0,0 +1,44 @@
+Loading file "testNewTypes.saw"
+{x = 2}
+{x = 2}
+{x = 3}
+
+
+errors follow:
+
+
+Error: Cryptol: [error] at testNewTypes.saw:16:20--16:23
+    Value not in scope: t11
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:16:1-16:28 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testNewTypes.saw:19:25--19:27
+    Type not in scope: T1
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:19:1-19:32 (at top level)
+
+(Failure was expected, continuing)
+Error: Cryptol: [error] at testNewTypes.saw:22:20--22:22
+    Value not in scope: T1
+Stack trace:
+   (builtin) in (callback)
+   (builtin) in fails
+   testNewTypes.saw:22:1-22:32 (at top level)
+
+(Failure was expected, continuing)
+
+
+M::S1::T1
+{x = 1}
+{x = 2}
+{x = 2}
+{x = 2}
+{x = 2}
+{x = 3}
+{x = 3}
+{x = 3}
diff --git a/intTests/test_saw_submodule_import/testNewTypes.saw b/intTests/test_saw_submodule_import/testNewTypes.saw
new file mode 100644
index 0000000000..6ca658c101
--- /dev/null
+++ b/intTests/test_saw_submodule_import/testNewTypes.saw
@@ -0,0 +1,40 @@
+import "M.cry";
+
+print {{ t2 }};
+print {{ t2 : T2 }};
+print {{ T2{x=3} : T2 }};
+
+/* *******************************
+  errors:
+ */
+
+print "\n";
+print "errors follow:";
+print "\n";
+
+// cannot access t11 (in submodule)
+fails (do{print {{ t11 }};}) ;
+
+// cannot access T1 type (in submodule)
+fails (do{print {{ t2 : T1 }};}) ;
+
+// cannot access T1 constructor (in submodule)
+fails (do{print {{ T1{x=3} }};}) ;
+
+print "\n";
+
+/* *******************************
+   import the submodule and test:
+ */
+
+import submodule S1;
+
+print (type {{t11}}) ;
+print {{t11}}  ;
+print {{t2}}   ;
+print {{t2 : T2}} ;
+print {{t2 : T1}} ;
+print {{t2 : S1::T1}} ;
+print {{ T2{x=3} }} ;
+print {{ T1{x=3} }} ;
+print {{ T1{x=3} : T1 }} ;