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