Static Environment used for type-checking (cf Typing.
type global = {declared_types : (AST.ty * SideEffect.TimeFrame.t) ASTUtils.IMap.t;Maps a type name t to its declaration and its time-frame.
As expressions on which a type depends need to be statically evaluable, the only effects allowed in a type are statically evaluable, so need to be reading immutable (global) storage elements. This makes it possible only to store the time-frame of the type, and not the whole side-effect set.
*)constant_values : AST.literal Storage.t;Maps a global constant name to its value.
*)storage_types : (AST.ty * AST.global_decl_keyword) ASTUtils.IMap.t;Maps global declared storage elements to their types.
*)subtypes : AST.identifier ASTUtils.IMap.t;Maps an identifier s to its parent in the subtype relation.
*)subprograms : (AST.func * SideEffect.SES.t) ASTUtils.IMap.t;Maps each subprogram runtime name to its signature and the side-effects inferred for it.
*)overloaded_subprograms : ASTUtils.ISet.t ASTUtils.IMap.t;Maps the name of each declared subprogram to the equivalence class of all the subprogram runtime names that were declared with this name.
*)expr_equiv : AST.expr ASTUtils.IMap.t;Maps every expression to a reduced immutable form.
*)}Store all the global environment information at compile-time.
type local = {constant_values : AST.literal Storage.t;Maps a local constant to its value.
*)storage_types : (AST.ty * AST.local_decl_keyword) ASTUtils.IMap.t;Maps an locally declared names to their type.
*)expr_equiv : AST.expr ASTUtils.IMap.t;Maps immutable storage to their oldest equivalent expression.
*)return_type : AST.ty option;Local return type, None for procedures, global constants, or setters.
}Store all the local environment information at compile-time.
val pp_env : Format.formatter -> env -> unitval pp_global : Format.formatter -> global -> unitval pp_local : Format.formatter -> local -> unitval empty_global : globalval empty_local : localval empty : envval lookup_constants : env -> AST.identifier -> AST.literallookup x env is the value of x as defined in environment.
val lookup_constants_opt : env -> AST.identifier -> AST.literal optionval type_of : env -> AST.identifier -> AST.tytype_of env "x" is the type of "x" in the environment env.
val type_of_opt : env -> AST.identifier -> AST.ty optionval lookup_immutable_expr : env -> AST.identifier -> AST.exprval lookup_immutable_expr_opt : env -> AST.identifier -> AST.expr optionval mem_constants : env -> AST.identifier -> boolval add_subprogram :
AST.identifier ->
AST.func ->
SideEffect.SES.t ->
env ->
envval set_renamings : AST.identifier -> ASTUtils.ISet.t -> env -> envval add_global_storage :
AST.identifier ->
AST.ty ->
AST.global_decl_keyword ->
global ->
globalval add_type : AST.identifier -> AST.ty -> SideEffect.TimeFrame.t -> env -> envval add_global_constant : AST.identifier -> AST.literal -> global -> globalval add_local_constant : AST.identifier -> AST.literal -> env -> envval add_local_immutable_expr : AST.identifier -> AST.expr -> env -> envadd_local_immutable_expr x e env binds x to e in env. x is assumed to name an immutable local storage element. e is supposed to be the oldest expression corresponding to x.
val add_global_immutable_expr : AST.identifier -> AST.expr -> env -> envadd_global_immutable_expr x e env binds x to e in env. x is assumed to name an immutable global storage element. e is supposed to be the oldest expression corresponding to x.
val add_local :
AST.identifier ->
AST.ty ->
AST.local_decl_keyword ->
env ->
envval add_subtype : AST.identifier -> AST.identifier -> env -> envval is_local_undefined : AST.identifier -> local -> boolval is_global_undefined : AST.identifier -> global -> boolval is_undefined : AST.identifier -> env -> boolval is_subprogram : AST.identifier -> env -> bool