GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-28 18:32:07 +03:00
Code Issues Projects Releases Wiki Activity

Remove mImports from typechecked modules.

Browse Source 
This wasn't well specified or used for anything.
This commit is contained in:
Iavor Diatchki 2022-11-22 11:48:27 -08:00
parent b6f744f983
commit fe00904e38
5 changed files with 9 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -82,7 +82,6 @@ data ModuleG mname =
Module { mName :: !mname
, mDoc :: !(Maybe Text)
, mExports :: ExportSpec Name
, mImports :: [Import]
-- Functors:
, mParamTypes :: Map Name ModTParam
@ -117,7 +116,6 @@ emptyModule nm =
{ mName = nm
, mDoc = Nothing
, mExports = mempty
, mImports = []
, mParams = mempty
, mParamTypes = mempty
@ -455,7 +453,6 @@ instance PP n => PP (WithNames (ModuleG n)) where
ppPrec _ (WithNames Module { .. } nm) =
vcat [ text "module" <+> pp mName
-- XXX: Print exports?
, vcat (map pp mImports)
, vcat (map pp' (Map.elems mTySyns))
-- XXX: Print abstarct types/functions
, vcat (map pp' mDecls)

4
src/Cryptol/TypeCheck/Infer.hs
View File

@ -81,8 +81,7 @@ inferTopModule :: P.Module Name -> InferM TCTopEntity
inferTopModule m =
case P.mDef m of
P.NormalModule ds ->
do newModuleScope (thing (P.mName m)) (map thing (P.mImports m))
(P.exportedDecls ds)
do newModuleScope (thing (P.mName m)) (P.exportedDecls ds)
checkTopDecls ds
proveModuleTopLevel
endModule
@ -1324,7 +1323,6 @@ checkTopDecls = mapM_ checkTopDecl
P.NormalModule ds ->
do newSubmoduleScope (thing (P.mName m))
(thing <$> P.tlDoc tl)
(map thing (P.mImports m))
(P.exportedDecls ds)
checkTopDecls ds
proveModuleTopLevel

4
src/Cryptol/TypeCheck/Module.hs
View File

@ -59,8 +59,8 @@ doFunctorInst m f as inst doc =
newGoals CtModuleInstance (map thing (mParamConstraints m1))
case thing m of
P.ImpTop mn -> newModuleScope mn (mImports m2) (mExports m2)
P.ImpNested mn -> newSubmoduleScope mn doc (mImports m2) (mExports m2)
P.ImpTop mn -> newModuleScope mn (mExports m2)
P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2)
mapM_ addTySyn (Map.elems (mTySyns m2))
mapM_ addNewtype (Map.elems (mNewtypes m2))

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

@ -63,7 +63,6 @@ instance ModuleInstance (ModuleG name) where
Module { mName = mName m
, mDoc = Nothing
, mExports = doVInst (mExports m)
, mImports = mImports m
, mParamTypes = doMap (mParamTypes m)
, mParamFuns = doMap (mParamFuns m)
, mParamConstraints = moduleInstance (mParamConstraints m)

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

@ -991,16 +991,16 @@ newTopSignatureScope x = newScope (TopSignatureScope x)
to initialize an empty module. As we type check declarations they are
added to this module's scope. -}
newSubmoduleScope ::
Name -> Maybe Text -> [Import] -> ExportSpec Name -> InferM ()
newSubmoduleScope x docs is e =
Name -> Maybe Text -> ExportSpec Name -> InferM ()
newSubmoduleScope x docs e =
do updScope \o -> o { mNested = Set.insert x (mNested o) }
newScope (SubModule x)
updScope \m -> m { mDoc = docs, mImports = is, mExports = e }
updScope \m -> m { mDoc = docs, mExports = e }
newModuleScope :: P.ModName -> [Import] -> ExportSpec Name -> InferM ()
newModuleScope x is e =
newModuleScope :: P.ModName -> ExportSpec Name -> InferM ()
newModuleScope x e =
do newScope (MTopModule x)
updScope \m -> m { mDoc = Nothing, mImports = is, mExports = e }
updScope \m -> m { mDoc = Nothing, mExports = e }
-- | Update the current scope (first in the list). Assumes there is one.
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
@ -1043,7 +1043,6 @@ endSubmodule =
, mParams = mParams y
, mNested = mNested y
, mImports = add mImports -- just for deps
, mTySyns = add mTySyns
, mNewtypes = add mNewtypes
, mPrimTypes = add mPrimTypes