GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-14 11:16:33 +03:00
Code Issues Projects Releases Wiki Activity

Don't discrad documentation during type checking

Browse Source
This commit is contained in:
Iavor Diatchki 2022-07-25 14:05:32 +03:00
parent 24b1ba6dc6
commit 9c9d0db38f
7 changed files with 22 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Cryptol/ModuleSystem/Interface.hs
View File

@ -69,6 +69,7 @@ data IfaceNames name = IfaceNames
, ifsNested :: Set Name -- ^ Things nested in this module
, 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)
-- | Is this interface for a functor.
@ -81,6 +82,7 @@ emptyIface nm = Iface
, ifsDefines = mempty
, ifsPublic = mempty
, ifsNested = mempty
, ifsDoc = Nothing
}
, ifParams = mempty
, ifDefines = mempty

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

@ -76,6 +76,7 @@ tcTopEntityToModule ent =
-- | A Cryptol module.
data ModuleG mname =
Module { mName :: !mname
, mDoc :: !(Maybe Text)
, mExports :: ExportSpec Name
, mImports :: [Import]
@ -110,6 +111,7 @@ emptyModule :: mname -> ModuleG mname
emptyModule nm =
Module
{ mName = nm
, mDoc = Nothing
, mExports = mempty
, mImports = []

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

@ -78,7 +78,7 @@ inferTopModule m =
endModule
P.FunctorInstance f as inst ->
do mb <- doFunctorInst (P.ImpTop <$> P.mName m) f as inst
do mb <- doFunctorInst (P.ImpTop <$> P.mName m) f as inst Nothing
case mb of
Just mo -> pure mo
Nothing -> panic "inferModule" ["Didnt' get a module"]
@ -1088,6 +1088,7 @@ 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
@ -1095,7 +1096,8 @@ checkTopDecls = mapM_ checkTopDecl
endSubmodule
P.FunctorInstance f as inst ->
do _ <- doFunctorInst (P.ImpNested <$> P.mName m) f as inst
do let doc = thing <$> P.tlDoc tl
_ <- doFunctorInst (P.ImpNested <$> P.mName m) f as inst doc
pure ()
P.InterfaceModule sig ->

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

@ -27,6 +27,7 @@ genIfaceNames m = IfaceNames
, ifsNested = mNested m
, ifsDefines = genModDefines m
, ifsPublic = allExported (mExports m)
, ifsDoc = mDoc m
}
-- | Things defines by a module

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

@ -1,6 +1,7 @@
{-# Language BlockArguments, ImplicitParams #-}
module Cryptol.TypeCheck.Module (doFunctorInst) where
import Data.Text(Text)
import Data.Map(Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
@ -32,8 +33,9 @@ doFunctorInst ::
{- ^ Instantitation. These is the renaming for the functor that arises from
generativity (i.e., it is something that will make the names "fresh").
-} ->
Maybe Text {- ^ Documentation -} ->
InferM (Maybe TCTopEntity)
doFunctorInst m f as inst =
doFunctorInst m f as inst doc =
inRange (srcRange m)
do mf <- lookupFunctor (thing f)
argIs <- checkArity (srcRange f) mf as
@ -44,6 +46,7 @@ doFunctorInst m f as inst =
?vSu = inst
let m1 = moduleInstance mf
m2 = m1 { mName = m
, mDoc = Nothing
, mParamTypes = mempty
, mParamFuns = mempty
, mParamConstraints = mempty
@ -57,7 +60,7 @@ doFunctorInst m f as inst =
case thing m of
P.ImpTop mn -> newModuleScope mn (mImports m2) (mExports m2)
P.ImpNested mn -> newSubmoduleScope mn (mImports m2) (mExports m2)
P.ImpNested mn -> newSubmoduleScope mn doc (mImports m2) (mExports m2)
mapM_ addTySyn (Map.elems (mTySyns m2))
mapM_ addNewtype (Map.elems (mNewtypes m2))

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

@ -61,6 +61,7 @@ instance ModuleInstance name => ModuleInstance (ImpName name) where
instance ModuleInstance (ModuleG name) where
moduleInstance m =
Module { mName = mName m
, mDoc = Nothing
, mExports = doVInst (mExports m)
, mImports = mImports m
, mParamTypes = doMap (mParamTypes m)
@ -127,6 +128,7 @@ instance ModuleInstance name => ModuleInstance (IfaceNames name) where
, ifsNested = doSet (ifsNested ns)
, ifsDefines = doSet (ifsDefines ns)
, ifsPublic = doSet (ifsPublic ns)
, ifsDoc = ifsDoc ns
}
instance ModuleInstance ModParamNames where

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

@ -916,16 +916,17 @@ newTopSignatureScope x = newScope (TopSignatureScope x)
{- | Start a new submodule scope. The imports and exports are just used
to initialize an empty module. As we type check declarations they are
added to this module's scope. -}
newSubmoduleScope :: Name -> [Import] -> ExportSpec Name -> InferM ()
newSubmoduleScope x is e =
newSubmoduleScope ::
Name -> Maybe Text -> [Import] -> ExportSpec Name -> InferM ()
newSubmoduleScope x docs is e =
do updScope \o -> o { mNested = Set.insert x (mNested o) }
newScope (SubModule x)
updScope \m -> m { mImports = is, mExports = e }
updScope \m -> m { mDoc = docs, mImports = is, mExports = e }
newModuleScope :: P.ModName -> [Import] -> ExportSpec Name -> InferM ()
newModuleScope x is e =
do newScope (MTopModule x)
updScope \m -> m { mImports = is, mExports = e }
updScope \m -> m { mDoc = Nothing, mImports = is, mExports = e }
-- | Update the current scope (first in the list). Assumes there is one.
updScope :: (ModuleG ScopeName -> ModuleG ScopeName) -> InferM ()
@ -960,6 +961,7 @@ endSubmodule =
z = Module
{ mName = mName y
, mDoc = mDoc y
, mExports = mExports y
, mParamTypes = mParamTypes y
, mParamFuns = mParamFuns y