package archetype

  1. Overview
  2. Docs
val function_name_from_storage_const : storage_const -> string
val function_name_from_container_const : container_const -> string
val function_name_from_function_const : function_const -> string
val function_name_from_builtin_const : builtin_const -> string
val get_assets : model -> info_asset list
val get_records : model -> record list
val get_variables : model -> storage_item list
val get_storage : model -> storage
val get_info_asset : model -> lident -> info_asset
val get_asset_field : model -> (lident * Ident.ident) -> Ident.ident * type_ * mterm option
val get_asset_key : model -> lident -> Ident.ident * btyp
val get_field_container : model -> Ident.ident -> Ident.ident -> Ident.ident * container
val is_storage_attribute : model -> lident -> bool
val get_named_field_list : model -> lident -> 'a list -> (Ident.ident * 'a) list
val get_partitions : model -> (Ident.ident * Ident.ident * type_) list
val dest_partition : type_ -> lident
val get_partition_asset_key : model -> lident -> lident -> Ident.ident * Ident.ident * btyp
val get_partition_assets : model -> Ident.ident -> Ident.ident list
val get_entries : model -> (specification option * function_struct) list
val get_functions : model -> (specification option * function_struct * type_) list
val has_partition : model -> Ident.ident -> bool
val get_asset_partitions : model -> Ident.ident -> (Ident.ident * type_ * mterm option) list
val get_field_list : model -> lident -> Ident.ident list
val get_field_pos : model -> lident -> lident -> int
val get_nth_record_val : int -> mterm -> mterm
val dest_array : mterm -> mterm list
val get_asset_type : mterm -> lident
val is_local_assigned : lident -> mterm -> bool
val get_function_args : function__ -> argument list
val set_function_args : function__ -> argument list -> function__
val map_function_terms : (mterm -> mterm) -> function__ -> function__
val is_record : mterm -> bool
val is_varlocal : mterm -> bool
val dest_varlocal : mterm -> lident
val is_container : type_ -> bool
val get_key_pos : model -> lident -> int
val get_loop_invariants : model -> (lident * mterm) list -> Ident.ident -> (lident * mterm) list
val get_formula : model -> mterm option -> Ident.ident -> mterm option
val is_post : postcondition -> bool
val get_sum_fields : model -> Ident.ident -> Ident.ident list
val get_added_removed_sets : model -> specification option -> (lident, lident mterm_gen) mterm_node list
val get_storage_invariants : model -> Ident.ident option -> (Ident.ident * Ident.ident * mterm) list
val is_field_storage : model -> Ident.ident -> bool
val with_trace : model -> bool
val get_callers : model -> Ident.ident -> Ident.ident list
val no_fail : model -> Ident.ident -> lident option
val type_to_asset : type_ -> lident