herdtools7 7.57 (latest) · OCaml Package

Static Environment used for type-checking (cf Typing.

type global = {

declared_types : AST.ty ASTUtils.IMap.t;
(*
Maps a type name t to its declaration.
*)
constant_values : AST.literal ASTUtils.IMap.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 ASTUtils.IMap.t;
(*
Maps each subprogram runtime name to its signature.
*)
subprogram_renamings : ASTUtils.ISet.t ASTUtils.IMap.t;
(*
Maps each subprogram declared name to the equivalence class of all the subprogram runtime names that were declared with this name.
*)

}

Store all the global environment information at compile-time.

type local = {

constant_values : AST.literal ASTUtils.IMap.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.
*)
return_type : AST.ty option;
(*
Local return type, None for procedures, global constants, or setters.
*)

}

Store all the local environment information at compile-time.

type env = {

}

The static environment type.

val pp_env : Format.formatter -> env -> unit

val pp_global : Format.formatter -> global -> unit

val empty_global : global

val empty_local : local

val empty_local_return_type : AST.ty option -> local

val empty : env

val lookup_constants : env -> AST.identifier -> AST.literal

val type_of : env -> AST.identifier -> AST.ty

val type_of_opt : env -> AST.identifier -> AST.ty option

val mem_constants : env -> AST.identifier -> bool

val add_subprogram : AST.identifier -> AST.func -> env -> env

val set_renamings : AST.identifier -> ASTUtils.ISet.t -> env -> env

val add_global_storage : 
  AST.identifier ->
  AST.ty ->
  AST.global_decl_keyword ->
  env ->
  env

val add_type : AST.identifier -> AST.ty -> env -> env

val add_global_constant : AST.identifier -> AST.literal -> env -> env

val add_local_constant : AST.identifier -> AST.literal -> env -> env

val add_local : 
  AST.identifier ->
  AST.ty ->
  AST.local_decl_keyword ->
  env ->
  env

val add_subtype : AST.identifier -> AST.identifier -> env -> env

val is_undefined : AST.identifier -> env -> bool

package herdtools7