From 1020f76fbe1691a8e059a58d9ebd1a02b7d19ed1 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 7 Jun 2022 10:43:09 -0700 Subject: [PATCH] Move module parameters datatype from Interface to the typechecker --- bench/Main.hs | 3 +- src/Cryptol/ModuleSystem.hs | 3 +- src/Cryptol/ModuleSystem/Base.hs | 15 +++--- src/Cryptol/ModuleSystem/Binds.hs | 3 +- src/Cryptol/ModuleSystem/Env.hs | 4 +- src/Cryptol/ModuleSystem/Interface.hs | 66 +++---------------------- src/Cryptol/ModuleSystem/NamingEnv.hs | 8 +-- src/Cryptol/REPL/Browse.hs | 12 ++--- src/Cryptol/REPL/Help.hs | 8 ++- src/Cryptol/TypeCheck/AST.hs | 4 +- src/Cryptol/TypeCheck/Infer.hs | 31 ++++++------ src/Cryptol/TypeCheck/Module.hs | 13 +++-- src/Cryptol/TypeCheck/ModuleInstance.hs | 25 +++++----- src/Cryptol/TypeCheck/Monad.hs | 24 ++++----- src/Cryptol/TypeCheck/Type.hs | 34 ++++++++++++- 15 files changed, 111 insertions(+), 142 deletions(-) diff --git a/bench/Main.hs b/bench/Main.hs index aa1886f4..761c3c5c 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -26,7 +26,6 @@ import qualified Cryptol.ModuleSystem.Base as M import qualified Cryptol.ModuleSystem.Env as M import qualified Cryptol.ModuleSystem.Monad as M import qualified Cryptol.ModuleSystem.NamingEnv as M -import Cryptol.ModuleSystem.Interface (noIfaceParams) import qualified Cryptol.Parser as P import qualified Cryptol.Parser.AST as P @@ -130,7 +129,7 @@ tc cd name path = , M.tcLinter = M.moduleLinter (P.thing (P.mName scm)) , M.tcPrims = prims } - M.typecheck act scm noIfaceParams tcEnv + M.typecheck act scm mempty tcEnv ceval :: String -> String -> FilePath -> T.Text -> Benchmark ceval cd name path expr = diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index cf8986b1..7b3a359b 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -29,8 +29,7 @@ module Cryptol.ModuleSystem ( , renameType -- * Interfaces - , Iface, IfaceG(..), IfaceParams(..), IfaceDecls(..), T.genIface - , IfaceTySyn, IfaceDecl(..) + , Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..) ) where import Data.Map (Map) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index caf32609..5c7967e3 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -534,7 +534,7 @@ data TCAction i o = TCAction typecheck :: (Show i, Show o, HasLoc i) => - TCAction i o -> i -> IfaceFunctorParams -> IfaceDecls -> ModuleM o + TCAction i o -> i -> T.FunctorParams -> IfaceDecls -> ModuleM o typecheck act i params env = do let range = fromMaybe emptyRange (getLoc i) @@ -562,9 +562,8 @@ typecheck act i params env = do typeCheckingFailed nameMap errs -- | Generate input for the typechecker. -genInferInput :: - Range -> PrimMap -> IfaceFunctorParams -> IfaceDecls -> - ModuleM T.InferInput +genInferInput :: Range -> PrimMap -> T.FunctorParams -> IfaceDecls -> + ModuleM T.InferInput genInferInput r prims params env = do seeds <- getNameSeeds monoBinds <- getMonoBinds @@ -574,10 +573,10 @@ genInferInput r prims params env = do callStacks <- getCallStacks let (paramTys,paramCtrs,paramVs) = - let ps = map ifmpParameters (Map.elems params) - in ( mconcat (map ifParamTypes ps) - , mconcat (map ifParamConstraints ps) - , mconcat (map ifParamFuns ps) + let ps = map T.mpParameters (Map.elems params) + in ( mconcat (map T.mpnTypes ps) + , mconcat (map T.mpnConstraints ps) + , mconcat (map T.mpnFuns ps) ) topMods <- getAllLoaded diff --git a/src/Cryptol/ModuleSystem/Binds.hs b/src/Cryptol/ModuleSystem/Binds.hs index 7f6c163f..ab982d96 100644 --- a/src/Cryptol/ModuleSystem/Binds.hs +++ b/src/Cryptol/ModuleSystem/Binds.hs @@ -38,6 +38,7 @@ import Cryptol.ModuleSystem.Name import Cryptol.ModuleSystem.Names import Cryptol.ModuleSystem.NamingEnv import Cryptol.ModuleSystem.Interface +import Cryptol.TypeCheck.Type(ModParamNames(..)) @@ -113,7 +114,7 @@ ifaceNamesToMod iface params names = decls = filterIfaceDecls isLocal (ifPublic iface <> ifPrivate iface) -ifaceSigToMod :: IfaceParams -> Mod () +ifaceSigToMod :: ModParamNames -> Mod () ifaceSigToMod ps = Mod { modImports = [] , modKind = ASignature diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index 0c72419d..4f56433d 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -171,7 +171,7 @@ loadedModules = map lmModule . getLoadedModules . meLoadedModules loadedNonParamModules :: ModuleEnv -> [T.Module] loadedNonParamModules = map lmModule . lmLoadedModules . meLoadedModules -loadedNewtypes :: ModuleEnv -> Map Name IfaceNewtype +loadedNewtypes :: ModuleEnv -> Map Name T.Newtype loadedNewtypes menv = Map.unions [ ifNewtypes (ifPublic i) <> ifNewtypes (ifPrivate i) | i <- map lmInterface (getLoadedModules (meLoadedModules menv)) @@ -187,7 +187,7 @@ allDeclGroups = concatMap T.mDecls . loadedNonParamModules -- | Contains enough information to browse what's in scope, -- or type check new expressions. data ModContext = ModContext - { mctxParams :: IfaceFunctorParams + { mctxParams :: T.FunctorParams , mctxExported :: Set Name , mctxDecls :: IfaceDecls -- ^ Should contain at least names in NamingEnv, but may have more diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index 4fab83b8..01c9ba01 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -15,19 +15,12 @@ module Cryptol.ModuleSystem.Interface ( Iface , IfaceG(..) , IfaceDecls(..) - , IfaceTySyn, ifTySynName - , IfaceNewtype , IfaceDecl(..) - , IfaceFunctorParams - , IfaceParams(..) - , IfaceModParam(..) , IfaceNames(..) , ifModName , emptyIface , ifacePrimMap - , noIfaceParams - , isEmptyIfaceParams , ifaceForgetName , ifaceIsFunctor , filterIfaceDecls @@ -36,7 +29,6 @@ module Cryptol.ModuleSystem.Interface ( import Data.Set(Set) import qualified Data.Set as Set -import Data.Map(Map) import qualified Data.Map as Map import Data.Semigroup import Data.Text (Text) @@ -48,11 +40,10 @@ import Prelude () import Prelude.Compat import Cryptol.ModuleSystem.Name -import Cryptol.Utils.Ident (ModName,Ident) +import Cryptol.Utils.Ident (ModName) import Cryptol.Utils.Panic(panic) import Cryptol.Utils.Fixity(Fixity) -import Cryptol.Parser.AST(Pragma,ImpName(..)) -import Cryptol.Parser.Position(Located) +import Cryptol.Parser.AST(Pragma) import Cryptol.TypeCheck.Type type Iface = IfaceG ModName @@ -60,7 +51,7 @@ type Iface = IfaceG ModName -- | The resulting interface generated by a module that has been typechecked. data IfaceG name = Iface { ifNames :: IfaceNames name -- ^ Info about names in this module - , ifParams :: IfaceFunctorParams -- ^ Module parameters, if any + , ifParams :: FunctorParams -- ^ Module parameters, if any , ifPublic :: IfaceDecls -- ^ Exported definitions , ifPrivate :: IfaceDecls -- ^ Private definitions. We keep those so that we can browse them. @@ -81,8 +72,6 @@ data IfaceNames name = IfaceNames , ifsPublic :: Set Name -- ^ Subset of `ifsDefines` that is public } deriving (Show, Generic, NFData) -type IfaceFunctorParams = Map Ident IfaceModParam - -- | Is this interface for a functor. ifaceIsFunctor :: IfaceG name -> Bool ifaceIsFunctor = not . Map.null . ifParams @@ -99,48 +88,15 @@ emptyIface nm = Iface , ifParams = mempty } - --- | A module parameter. Corresponds to a "signature import". --- A single module parameter can bring multiple things in scope. -data IfaceModParam = IfaceModParam - { ifmpName :: Ident - , ifmpSignature :: ImpName Name - , ifmpParameters :: IfaceParams - {- ^ These are the actual parameters, not the ones in the signature - For example if the same signature is used for multiple parameters - the `ifmpParameters` would all be different. -} - } deriving (Show, Generic, NFData) - --- | Information about the names brought in through a "signature import". --- This is also used to keep information about signatures. -data IfaceParams = IfaceParams - { ifParamTypes :: Map.Map Name ModTParam - , ifParamConstraints :: [Located Prop] -- ^ Constraints on param. types - , ifParamFuns :: Map.Map Name ModVParam - , ifParamDoc :: !(Maybe Text) - } deriving (Show, Generic, NFData) - -noIfaceParams :: IfaceParams -noIfaceParams = IfaceParams - { ifParamTypes = Map.empty - , ifParamConstraints = [] - , ifParamFuns = Map.empty - , ifParamDoc = Nothing - } - -isEmptyIfaceParams :: IfaceParams -> Bool -isEmptyIfaceParams IfaceParams { .. } = - Map.null ifParamTypes && null ifParamConstraints && Map.null ifParamFuns - -- | Declarations in a module. Note that this includes things from nested -- modules, but not things from nested functors, which are in `ifFunctors`. data IfaceDecls = IfaceDecls - { ifTySyns :: Map.Map Name IfaceTySyn - , ifNewtypes :: Map.Map Name IfaceNewtype - , ifAbstractTypes :: Map.Map Name IfaceAbstractType + { ifTySyns :: Map.Map Name TySyn + , ifNewtypes :: Map.Map Name Newtype + , ifAbstractTypes :: Map.Map Name AbstractType , ifDecls :: Map.Map Name IfaceDecl , ifModules :: !(Map.Map Name (IfaceNames Name)) - , ifSignatures :: !(Map.Map Name IfaceParams) + , ifSignatures :: !(Map.Map Name ModParamNames) , ifFunctors :: !(Map.Map Name (IfaceG Name)) {- ^ XXX: Maybe arg info? Also, with the current implementation we aim to complete remove functors @@ -210,14 +166,6 @@ instance Monoid IfaceDecls where , ifSignatures = Map.unions (map ifSignatures ds) } -type IfaceTySyn = TySyn - -ifTySynName :: TySyn -> Name -ifTySynName = tsName - -type IfaceNewtype = Newtype -type IfaceAbstractType = AbstractType - data IfaceDecl = IfaceDecl { ifDeclName :: !Name -- ^ Name of thing , ifDeclSig :: Schema -- ^ Type diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index eed1cbf3..c12fcbf5 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -230,11 +230,11 @@ isEmptyNamingEnv (NamingEnv mp) = Map.null mp -- | Compute an unqualified naming environment, containing the various module -- parameters. -modParamsNamingEnv :: IfaceParams -> NamingEnv -modParamsNamingEnv IfaceParams { .. } = +modParamsNamingEnv :: T.ModParamNames -> NamingEnv +modParamsNamingEnv T.ModParamNames { .. } = NamingEnv $ Map.fromList - [ (NSValue, Map.fromList $ map fromFu $ Map.keys ifParamFuns) - , (NSType, Map.fromList $ map fromTy $ Map.elems ifParamTypes) + [ (NSValue, Map.fromList $ map fromFu $ Map.keys mpnFuns) + , (NSType, Map.fromList $ map fromTy $ Map.elems mpnTypes) ] where toPName n = mkUnqual (nameIdent n) diff --git a/src/Cryptol/REPL/Browse.hs b/src/Cryptol/REPL/Browse.hs index f4abc726..7d9c51ee 100644 --- a/src/Cryptol/REPL/Browse.hs +++ b/src/Cryptol/REPL/Browse.hs @@ -47,19 +47,19 @@ data DispInfo = DispInfo { dispHow :: BrowseHow, env :: NameDisp } -------------------------------------------------------------------------------- -browseMParams :: NameDisp -> IfaceFunctorParams -> [Doc] +browseMParams :: NameDisp -> T.FunctorParams -> [Doc] browseMParams disp params | Map.null params = [] | otherwise = ppSectionHeading "Module Parameters" - $ [ "parameter" <+> pp (ifmpName p) <+> ":" <+> - "signature" <+> pp (ifmpSignature p) $$ + $ [ "parameter" <+> pp (T.mpName p) <+> ":" <+> + "signature" <+> pp (T.mpSignature p) $$ indent 2 (vcat $ - map ppParamTy (sortByName disp (Map.toList (ifParamTypes names))) ++ - map ppParamFu (sortByName disp (Map.toList (ifParamFuns names))) + map ppParamTy (sortByName disp (Map.toList (T.mpnTypes names))) ++ + map ppParamFu (sortByName disp (Map.toList (T.mpnFuns names))) ) | p <- Map.elems params - , let names = ifmpParameters p + , let names = T.mpParameters p ] ++ [" "] where diff --git a/src/Cryptol/REPL/Help.hs b/src/Cryptol/REPL/Help.hs index 1747a4e0..f4297e8f 100644 --- a/src/Cryptol/REPL/Help.hs +++ b/src/Cryptol/REPL/Help.hs @@ -68,13 +68,12 @@ showSigHelp env nameEnv name = do rPrint $ runDoc nameEnv $ vcat [ "`" <> pp name <> "` is a signature." ] fromMaybe (noInfo nameEnv name) do s <- Map.lookup name (M.ifSignatures env) - d <- M.ifParamDoc s + d <- T.mpnDoc s pure (rPrint (pp d)) -- XXX: show doc. if any, and maybe other stuff -showTypeHelp :: - M.IfaceFunctorParams -> M.IfaceDecls -> NameDisp -> T.Name -> REPL () +showTypeHelp :: T.FunctorParams -> M.IfaceDecls -> NameDisp -> T.Name -> REPL () showTypeHelp mbParams env nameEnv name = fromMaybe (noInfo nameEnv name) $ msum [ fromTySyn, fromPrimType, fromNewtype, fromTyParam ] @@ -154,8 +153,7 @@ doShowFix fx = showValHelp :: - M.IfaceFunctorParams -> - M.IfaceDecls -> NameDisp -> P.PName -> T.Name -> REPL () + T.FunctorParams -> M.IfaceDecls -> NameDisp -> P.PName -> T.Name -> REPL () showValHelp mbParams env nameEnv qname name = fromMaybe (noInfo nameEnv name) diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 4f9cdd79..99fd3b54 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -64,7 +64,7 @@ data ModuleG mname = , mParamFuns :: Map Name ModVParam , mParamConstraints :: [Located Prop] - , mParams :: Map Ident IfaceModParam + , mParams :: Map Ident ModParam -- ^ Parameters grouped by "import". , mFunctors :: Map Name (ModuleG Name) @@ -83,7 +83,7 @@ data ModuleG mname = , mPrimTypes :: Map Name AbstractType , mDecls :: [DeclGroup] , mSubmodules :: Map Name (IfaceNames Name) - , mSignatures :: !(Map Name IfaceParams) + , mSignatures :: !(Map Name ModParamNames) } deriving (Show, Generic, NFData) emptyModule :: mname -> ModuleG mname diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 200e58ac..7fada063 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -32,7 +32,6 @@ import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc) import Cryptol.Parser.Position import qualified Cryptol.Parser.AST as P import qualified Cryptol.ModuleSystem.Exports as P -import Cryptol.ModuleSystem.Interface import Cryptol.TypeCheck.AST hiding (tSub,tMul,tExp) import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Error @@ -1108,27 +1107,25 @@ checkTopDecls = mapM_ checkTopDecl ips <- lookupSignature (thing (P.mpSignature p)) let actualTys = [ mapNames actualName mp - | mp <- Map.elems (ifParamTypes ips) ] + | mp <- Map.elems (mpnTypes ips) ] actualCtrs = [ mapNames actualName prop - | prop <- ifParamConstraints ips ] + | prop <- mpnConstraints ips ] actualVals = [ mapNames actualName vp - | vp <- Map.elems (ifParamFuns ips) ] + | vp <- Map.elems (mpnFuns ips) ] param = - IfaceModParam - { ifmpName = P.mpName p - , ifmpSignature = thing (P.mpSignature p) - , ifmpParameters = - IfaceParams - { ifParamTypes = - Map.fromList [ (mtpName tp, tp) - | tp <- actualTys ] + ModParam + { mpName = P.mpName p + , mpSignature = thing (P.mpSignature p) + , mpParameters = + ModParamNames + { mpnTypes = Map.fromList [ (mtpName tp, tp) + | tp <- actualTys ] - , ifParamConstraints = actualCtrs - , ifParamFuns = - Map.fromList [ (mvpName vp, vp) - | vp <- actualVals ] - , ifParamDoc = thing <$> P.mpDoc p + , mpnConstraints = actualCtrs + , mpnFuns = Map.fromList [ (mvpName vp, vp) + | vp <- actualVals ] + , mpnDoc = thing <$> P.mpDoc p } } diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index e7d05087..667db161 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -13,8 +13,7 @@ import Cryptol.Parser.Position (Range,Located(..), thing) import qualified Cryptol.Parser.AST as P import Cryptol.ModuleSystem.Name(nameIdent) import Cryptol.ModuleSystem.Interface - ( IfaceG(..), IfaceModParam(..), IfaceDecls(..), IfaceNames(..) - , IfaceParams(..), IfaceDecl(..) + ( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..) , filterIfaceDecls ) import Cryptol.TypeCheck.AST @@ -79,7 +78,7 @@ checkArity :: Range {- ^ Location for reporting errors -} -> ModuleG () {- ^ The functor being instantiated -} -> P.ModuleInstanceArgs Name {- ^ The arguments -} -> - InferM [ (Range, IfaceModParam, IfaceG ()) ] + InferM [ (Range, ModParam, IfaceG ()) ] {- ^ Associates functor parameters with the interfaces of the instantiating modules -} checkArity r mf args = @@ -117,9 +116,9 @@ checkArity r mf args = checkArgs done ps more -checkArg :: (Range, IfaceModParam, IfaceG ()) -> InferM (Subst, [Decl]) +checkArg :: (Range, ModParam, IfaceG ()) -> InferM (Subst, [Decl]) checkArg (r,expect,actual) = - do tRens <- mapM (checkParamType r tyMap) (Map.toList (ifParamTypes params)) + do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params)) let renSu = listParamSubst (concat tRens) {- Note: the constraints from the signature are already added to the @@ -133,7 +132,7 @@ checkArg (r,expect,actual) = vDecls <- concat <$> mapM (checkParamValue r vMap) [ s { mvpType = apSubst renSu (mvpType s) } - | s <- Map.elems (ifParamFuns params) ] + | s <- Map.elems (mpnFuns params) ] pure (renSu, vDecls) @@ -141,7 +140,7 @@ checkArg (r,expect,actual) = where - params = ifmpParameters expect + params = mpParameters expect localNames = ifsDefines (ifNames actual) isLocal x = x `Set.member` localNames diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 2c252cf0..23da23ba 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -7,8 +7,7 @@ import Data.Set(Set) import qualified Data.Set as Set import Cryptol.Parser.Position(Located) -import Cryptol.ModuleSystem.Interface - (IfaceParams(..), IfaceNames(..), IfaceModParam(..)) +import Cryptol.ModuleSystem.Interface(IfaceNames(..)) import Cryptol.IR.TraverseNames(TraverseNames,mapNames) import Cryptol.Parser.AST(ImpName(..)) import Cryptol.TypeCheck.AST @@ -130,13 +129,13 @@ instance ModuleInstance name => ModuleInstance (IfaceNames name) where , ifsPublic = doSet (ifsPublic ns) } -instance ModuleInstance IfaceParams where +instance ModuleInstance ModParamNames where moduleInstance si = - IfaceParams { ifParamTypes = doMap (ifParamTypes si) - , ifParamConstraints = moduleInstance (ifParamConstraints si) - , ifParamFuns = doMap (ifParamFuns si) - , ifParamDoc = ifParamDoc si - } + ModParamNames { mpnTypes = doMap (mpnTypes si) + , mpnConstraints = moduleInstance (mpnConstraints si) + , mpnFuns = doMap (mpnFuns si) + , mpnDoc = mpnDoc si + } instance ModuleInstance ModTParam where moduleInstance mp = @@ -154,12 +153,12 @@ instance ModuleInstance ModVParam where , mvpFixity = mvpFixity mp } -instance ModuleInstance IfaceModParam where +instance ModuleInstance ModParam where moduleInstance p = - IfaceModParam { ifmpName = ifmpName p - , ifmpSignature = moduleInstance (ifmpSignature p) - , ifmpParameters = moduleInstance (ifmpParameters p) - } + ModParam { mpName = mpName p + , mpSignature = moduleInstance (mpSignature p) + , mpParameters = moduleInstance (mpParameters p) + } diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index ff405ea5..1efbe1ac 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -65,8 +65,8 @@ data InferInput = InferInput , inpVars :: Map Name Schema -- ^ Variables that are in scope , inpTSyns :: Map Name TySyn -- ^ Type synonyms that are in scope , inpNewtypes :: Map Name Newtype -- ^ Newtypes in scope - , inpAbstractTypes :: Map Name AbstractType -- ^ Abstract types in scope - , inpSignatures :: !(Map Name If.IfaceParams) -- ^ Signatures in scope + , inpAbstractTypes :: Map Name AbstractType -- ^ Abstract types in scope + , inpSignatures :: !(Map Name ModParamNames) -- ^ Signatures in scope , inpTopModules :: ModName -> Maybe (ModuleG (), If.IfaceG ()) @@ -699,7 +699,7 @@ lookupAbstractType x = Map.lookup x <$> getAbstractTypes lookupParamType :: Name -> InferM (Maybe ModTParam) lookupParamType x = Map.lookup x <$> getParamTypes -lookupSignature :: P.ImpName Name -> InferM If.IfaceParams +lookupSignature :: P.ImpName Name -> InferM ModParamNames lookupSignature nx = case nx of -- XXX: top @@ -831,7 +831,7 @@ getMonoBinds = IM (asks iMonoBinds) getCallStacks :: InferM Bool getCallStacks = IM (asks iCallStacks) -getSignatures :: InferM (Map Name If.IfaceParams) +getSignatures :: InferM (Map Name ModParamNames) getSignatures = getScope mSignatures @@ -985,11 +985,11 @@ endSignature = rw { iScope = z : more } where z = y { mSignatures = Map.insert m sig (mSignatures y) } - sig = If.IfaceParams - { If.ifParamTypes = mParamTypes x - , If.ifParamConstraints = mParamConstraints x - , If.ifParamFuns = mParamFuns x - , If.ifParamDoc = doc + sig = ModParamNames + { mpnTypes = mParamTypes x + , mpnConstraints = mParamConstraints x + , mpnFuns = mParamFuns x + , mpnDoc = doc } _ -> panic "endSignature" [ "Not a signature scope" ] @@ -1042,7 +1042,7 @@ addParamType :: ModTParam -> InferM () addParamType a = updScope \r -> r { mParamTypes = Map.insert (mtpName a) a (mParamTypes r) } -addSignatures :: Map Name If.IfaceParams -> InferM () +addSignatures :: Map Name ModParamNames -> InferM () addSignatures mp = updScope \r -> r { mSignatures = Map.union mp (mSignatures r) } @@ -1068,9 +1068,9 @@ addParameterConstraints :: [Located Prop] -> InferM () addParameterConstraints ps = updScope \r -> r { mParamConstraints = ps ++ mParamConstraints r } -addModParam :: If.IfaceModParam -> InferM () +addModParam :: ModParam -> InferM () addModParam p = - updScope \r -> r { mParams = Map.insert (If.ifmpName p) p (mParams r) } + updScope \r -> r { mParams = Map.insert (mpName p) p (mParams r) } diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 929d1648..58eed0cc 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -16,6 +16,8 @@ module Cryptol.TypeCheck.Type import GHC.Generics (Generic) import Control.DeepSeq +import Data.Map(Map) +import qualified Data.Map as Map import qualified Data.IntMap as IntMap import Data.Maybe (fromMaybe) import Data.Set (Set) @@ -23,7 +25,8 @@ import qualified Data.Set as Set import Data.Text (Text) import Cryptol.Parser.Selector -import Cryptol.Parser.Position(Range,emptyRange) +import Cryptol.Parser.Position(Located,Range,emptyRange) +import Cryptol.Parser.AST(ImpName(..)) import Cryptol.ModuleSystem.Name import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName, ogModule) import Cryptol.TypeCheck.TCon @@ -37,6 +40,33 @@ import Prelude infix 4 =#=, >== infixr 5 `tFun` + +-------------------------------------------------------------------------------- +-- Module parameters + +type FunctorParams = Map Ident ModParam + + +-- | A module parameter. Corresponds to a "signature import". +-- A single module parameter can bring multiple things in scope. +data ModParam = ModParam + { mpName :: Ident + , mpSignature :: ImpName Name + , mpParameters :: ModParamNames + {- ^ These are the actual parameters, not the ones in the signature + For example if the same signature is used for multiple parameters + the `ifmpParameters` would all be different. -} + } deriving (Show, Generic, NFData) + +-- | Information about the names brought in through a "signature import". +-- This is also used to keep information about signatures. +data ModParamNames = ModParamNames + { mpnTypes :: Map Name ModTParam + , mpnConstraints :: [Located Prop] -- ^ Constraints on param. types + , mpnFuns :: Map.Map Name ModVParam + , mpnDoc :: !(Maybe Text) + } deriving (Show, Generic, NFData) + -- | A type parameter of a module. data ModTParam = ModTParam { mtpName :: Name @@ -67,7 +97,7 @@ data ModVParam = ModVParam , mvpDoc :: Maybe Text , mvpFixity :: Maybe Fixity -- XXX: This should be in the name? } deriving (Show,Generic,NFData) - +--------------------------------------------------------------------------------