Module Asllib.StaticEnvSource

Static Environment used for type-checking (cf Typing.

Sourcetype global = {
  1. 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.

    *)
  2. constant_values : AST.literal Storage.t;
    (*

    Maps a global constant name to its value.

    *)
  3. storage_types : (AST.ty * AST.global_decl_keyword) ASTUtils.IMap.t;
    (*

    Maps global declared storage elements to their types.

    *)
  4. subtypes : AST.identifier ASTUtils.IMap.t;
    (*

    Maps an identifier s to its parent in the subtype relation.

    *)
  5. subprograms : (AST.func * SideEffect.SES.t) ASTUtils.IMap.t;
    (*

    Maps each subprogram runtime name to its signature and the side-effects inferred for it.

    *)
  6. 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.

    *)
  7. expr_equiv : AST.expr ASTUtils.IMap.t;
    (*

    Maps every expression to a reduced immutable form.

    *)
}

Store all the global environment information at compile-time.

Sourcetype local = {
  1. constant_values : AST.literal Storage.t;
    (*

    Maps a local constant to its value.

    *)
  2. storage_types : (AST.ty * AST.local_decl_keyword) ASTUtils.IMap.t;
    (*

    Maps an locally declared names to their type.

    *)
  3. expr_equiv : AST.expr ASTUtils.IMap.t;
    (*

    Maps immutable storage to their oldest equivalent expression.

    *)
  4. return_type : AST.ty option;
    (*

    Local return type, None for procedures, global constants, or setters.

    *)
}

Store all the local environment information at compile-time.

Sourcetype env = {
  1. global : global;
  2. local : local;
}

The static environment type.

Sourceval pp_env : Format.formatter -> env -> unit
Sourceval pp_global : Format.formatter -> global -> unit
Sourceval pp_local : Format.formatter -> local -> unit
Sourceval empty_global : global
Sourceval empty_local : local
Sourceval empty_local_return_type : AST.ty option -> local
Sourceval empty : env
Sourceval with_empty_local : global -> env
Sourceval lookup_constants : env -> AST.identifier -> AST.literal

lookup x env is the value of x as defined in environment.

  • raises Not_found

    if it is not defined inside.

Sourceval lookup_constants_opt : env -> AST.identifier -> AST.literal option
Sourceval type_of : env -> AST.identifier -> AST.ty

type_of env "x" is the type of "x" in the environment env.

Sourceval type_of_opt : env -> AST.identifier -> AST.ty option
Sourceval lookup_immutable_expr : env -> AST.identifier -> AST.expr
Sourceval lookup_immutable_expr_opt : env -> AST.identifier -> AST.expr option
Sourceval mem_constants : env -> AST.identifier -> bool
Sourceval add_subprogram : AST.identifier -> AST.func -> SideEffect.SES.t -> env -> env
Sourceval set_renamings : AST.identifier -> ASTUtils.ISet.t -> env -> env
Sourceval add_global_storage : AST.identifier -> AST.ty -> AST.global_decl_keyword -> global -> global
Sourceval add_global_constant : AST.identifier -> AST.literal -> global -> global
Sourceval add_local_constant : AST.identifier -> AST.literal -> env -> env
Sourceval add_local_immutable_expr : AST.identifier -> AST.expr -> env -> env

add_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.

Sourceval add_global_immutable_expr : AST.identifier -> AST.expr -> env -> env

add_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.

Sourceval add_subtype : AST.identifier -> AST.identifier -> env -> env
Sourceval is_local_undefined : AST.identifier -> local -> bool
Sourceval is_global_undefined : AST.identifier -> global -> bool
Sourceval is_undefined : AST.identifier -> env -> bool
Sourceval is_subprogram : AST.identifier -> env -> bool