mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Renamings and comments
This commit is contained in:
parent
6a1f12e42c
commit
2c8cfd2499
@ -59,14 +59,13 @@ type Iface = IfaceG ModName
|
||||
|
||||
-- | The resulting interface generated by a module that has been typechecked.
|
||||
data IfaceG name = Iface
|
||||
{ ifNames :: IfaceNames name
|
||||
, ifPublic :: IfaceDecls -- ^ Exported definitions
|
||||
{ ifNames :: IfaceNames name -- ^ Info about names in this module
|
||||
, ifParams :: IfaceFunctorParams -- ^ Module parameters, if any
|
||||
, ifPublic :: IfaceDecls -- ^ Exported definitions
|
||||
, ifPrivate :: IfaceDecls
|
||||
, ifParams :: IfaceFunctorParams
|
||||
-- ^ Private definitions. We keep those so that we can browse them.
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
-- XXX: signature
|
||||
|
||||
ifaceForgetName :: IfaceG name -> IfaceG ()
|
||||
ifaceForgetName i = i { ifNames = newNames }
|
||||
where newNames = (ifNames i) { ifsName = () }
|
||||
@ -74,6 +73,7 @@ ifaceForgetName i = i { ifNames = newNames }
|
||||
ifModName :: Iface -> ModName
|
||||
ifModName = ifsName . ifNames
|
||||
|
||||
-- | Information about the names in a module.
|
||||
data IfaceNames name = IfaceNames
|
||||
{ ifsName :: name -- ^ Name of this submodule
|
||||
, ifsNested :: Set Name -- ^ Things nested in this module
|
||||
@ -81,7 +81,9 @@ 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
|
||||
|
||||
@ -97,8 +99,9 @@ emptyIface nm = Iface
|
||||
, ifParams = mempty
|
||||
}
|
||||
|
||||
type IfaceFunctorParams = Map Ident IfaceModParam
|
||||
|
||||
-- | 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
|
||||
@ -108,7 +111,8 @@ data IfaceModParam = IfaceModParam
|
||||
the `ifmpParameters` would all be different. -}
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
-- | A bunch of module parameters.
|
||||
-- | 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
|
||||
|
@ -141,7 +141,7 @@ import Paths_cryptol
|
||||
|
||||
DOC { $$@(Located _ (Token (White DocStr) _)) }
|
||||
|
||||
%name vmodule vmodule
|
||||
%name top_module top_module
|
||||
%name program program
|
||||
%name programLayout program_layout
|
||||
%name expr expr
|
||||
@ -165,7 +165,7 @@ import Paths_cryptol
|
||||
%%
|
||||
|
||||
|
||||
vmodule :: { [Module PName] }
|
||||
top_module :: { [Module PName] }
|
||||
: 'module' module_def { mkTopMods $2 }
|
||||
| 'v{' vmod_body 'v}' { [mkAnonymousModule $2] }
|
||||
|
||||
@ -911,7 +911,7 @@ parseProgramWith cfg s = case res s of
|
||||
NoLayout -> program
|
||||
|
||||
parseModule :: Config -> Text -> Either ParseError [Module PName]
|
||||
parseModule cfg = parse cfg { cfgModuleScope = True } vmodule
|
||||
parseModule cfg = parse cfg { cfgModuleScope = True } top_module
|
||||
|
||||
parseProgram :: Layout -> Text -> Either ParseError (Program PName)
|
||||
parseProgram l = parseProgramWith defaultConfig { cfgLayout = l }
|
||||
|
@ -238,13 +238,12 @@ data TopDecl name =
|
||||
Decl (TopLevel (Decl name))
|
||||
| DPrimType (TopLevel (PrimType name))
|
||||
| TDNewtype (TopLevel (Newtype name)) -- ^ @newtype T as = t
|
||||
| Include (Located FilePath) -- ^ @include File@
|
||||
| Include (Located FilePath) -- ^ @include File@ (until NoPat)
|
||||
|
||||
-- Anonymous module parameters.
|
||||
-- DParameterType and DParameterFun should only exist during parsing
|
||||
-- and are converted to
|
||||
| DParameterType (ParameterType name) -- ^ @parameter type T : #@
|
||||
-- Sugar for anonymous module parameters
|
||||
| DParameterType (ParameterType name) -- ^ @parameter type T : #@ (parser only)
|
||||
| DParameterFun (ParameterFun name) -- ^ @parameter someVal : [256]@
|
||||
-- (parser only)
|
||||
|
||||
| DParameterConstraint [Located (Prop name)]
|
||||
-- ^ @parameter type constraint (fin T)@
|
||||
@ -259,8 +258,8 @@ data ModuleInstanceArgs name =
|
||||
-- ^ Single parameter instantitaion
|
||||
|
||||
| DefaultInstAnonArg [TopDecl name]
|
||||
-- ^ Single parameter instantitaion using this anonymous module
|
||||
-- Only appears while parsing, shouldn't be in the results of the parser.
|
||||
-- ^ Single parameter instantitaion using this anonymous module.
|
||||
-- (parser only)
|
||||
|
||||
| NamedInstArgs [ModuleInstanceArg name]
|
||||
deriving (Show, Generic, NFData)
|
||||
|
@ -44,7 +44,7 @@ import Cryptol.TypeCheck.Monad
|
||||
, lookupVar
|
||||
, newLocalScope, endLocalScope
|
||||
)
|
||||
import Cryptol.TypeCheck.Infer (inferModule, inferBinds, checkTopDecls)
|
||||
import Cryptol.TypeCheck.Infer (inferTopModule, inferBinds, checkTopDecls)
|
||||
import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..), defaultSolverConfig)
|
||||
import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
|
||||
-- import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
|
||||
@ -56,7 +56,7 @@ import Cryptol.Utils.Panic(panic)
|
||||
|
||||
|
||||
tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
|
||||
tcModule m inp = runInferM inp (inferModule m)
|
||||
tcModule m inp = runInferM inp (inferTopModule m)
|
||||
|
||||
tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))
|
||||
tcExpr e0 inp = runInferM inp
|
||||
|
@ -18,7 +18,7 @@
|
||||
module Cryptol.TypeCheck.Infer
|
||||
( checkE
|
||||
, checkSigB
|
||||
, inferModule
|
||||
, inferTopModule
|
||||
, inferBinds
|
||||
, checkTopDecls
|
||||
)
|
||||
@ -65,8 +65,8 @@ import Control.Monad(zipWithM,unless,foldM,forM_,mplus)
|
||||
|
||||
|
||||
|
||||
inferModule :: P.Module Name -> InferM Module
|
||||
inferModule m =
|
||||
inferTopModule :: P.Module Name -> InferM Module
|
||||
inferTopModule m =
|
||||
case P.mDef m of
|
||||
P.NormalModule ds ->
|
||||
do newModuleScope (thing (P.mName m)) (map thing (P.mImports m))
|
||||
@ -81,6 +81,8 @@ inferModule m =
|
||||
Just mo -> pure mo
|
||||
Nothing -> panic "inferModule" ["Didnt' get a module"]
|
||||
|
||||
|
||||
|
||||
-- | Construct a Prelude primitive in the parsed AST.
|
||||
mkPrim :: String -> InferM (P.Expr Name)
|
||||
mkPrim str =
|
||||
@ -1092,16 +1094,7 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
do let doc = P.thing <$> P.tlDoc tl
|
||||
inRange (srcRange (P.mName m))
|
||||
do newSignatureScope (thing (P.mName m)) doc
|
||||
|
||||
forM_ (P.sigTypeParams sig) \pt ->
|
||||
addParamType =<< checkParameterType pt
|
||||
|
||||
addParameterConstraints =<<
|
||||
checkParameterConstraints (P.sigConstraints sig)
|
||||
|
||||
forM_ (P.sigFunParams sig) \f ->
|
||||
addParamFun =<< checkParameterFun f
|
||||
|
||||
checkSignature sig
|
||||
endSignature
|
||||
|
||||
|
||||
@ -1139,13 +1132,12 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
mapM_ addParamType actualTys
|
||||
addParameterConstraints actualCtrs
|
||||
mapM_ addParamFun actualVals
|
||||
addModParam param
|
||||
|
||||
P.DImport {} -> pure ()
|
||||
P.DImport {} -> pure ()
|
||||
P.Include {} -> bad "Include"
|
||||
P.DParameterType{} -> bad "DParameterType"
|
||||
P.DParameterFun{} -> bad "DParameterFun"
|
||||
@ -1154,6 +1146,17 @@ checkTopDecls = mapM_ checkTopDecl
|
||||
bad x = panic "checkTopDecl" [ x ]
|
||||
|
||||
|
||||
checkSignature :: P.Signature Name -> InferM ()
|
||||
checkSignature sig =
|
||||
do forM_ (P.sigTypeParams sig) \pt ->
|
||||
addParamType =<< checkParameterType pt
|
||||
|
||||
addParameterConstraints =<<
|
||||
checkParameterConstraints (P.sigConstraints sig)
|
||||
|
||||
forM_ (P.sigFunParams sig) \f ->
|
||||
addParamFun =<< checkParameterFun f
|
||||
|
||||
|
||||
|
||||
checkDecl :: Bool -> P.Decl Name -> Maybe Text -> InferM ()
|
||||
|
Loading…
Reference in New Issue
Block a user