Module Archetype.Gen_why3

module M = Model
type error_desc =
| NotSupported of string
| TODONotTranslated of string
val pp_error_desc : Stdlib.Format.formatter -> error_desc -> unit
type error = Location.t * error_desc
val emit_error : (Location.t * error_desc) -> unit
val dl : 'a -> 'a Mlwtree.with_loc
val gArchetypeDir : string
val gArchetypeLib : string
val gArchetypeField : string
val gArchetypeView : string
val gArchetypeColl : string
val gArchetypeAgg : string
val gArchetypeSum : string
val gArchetypeSort : string
val gArchetypeTrace : string
val gArchetypeSet : string
val gArchetypeList : string
val gOperations : string
val gListAs : string
val gFieldAs : string
val gViewAs : string
val mk_module_name : string -> string
val mk_id : string -> string
val mk_ac_id : string -> string
val mk_ac_added_id : string -> string
val mk_ac_rmed_id : string -> string
val mk_ac_unmvd_id : string -> string
val mk_aggregate_id : string -> string
val gs : string
val gsinit : string
val gsarg : string
val mk_ac_st : string -> string -> ('a'b, string) Mlwtree.abstract_term
val mk_ac_old_st : 'a -> string -> ((('b'c'a) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term'e'f) Mlwtree.abstract_term
val mk_ac : string -> ('a'b, string) Mlwtree.abstract_term
val mk_ac_old : string -> ((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd'e) Mlwtree.abstract_term
val mk_ac_added_st : string -> string -> ('a'b, string) Mlwtree.abstract_term
val mk_ac_old_added_st : 'a -> string -> ((('b'c'a) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term'e'f) Mlwtree.abstract_term
val mk_ac_added : string -> ('a'b, string) Mlwtree.abstract_term
val mk_ac_old_added : string -> ((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd'e) Mlwtree.abstract_term
val mk_ac_rmed_st : string -> string -> ('a'b, string) Mlwtree.abstract_term
val mk_ac_old_rmed_st : 'a -> string -> ((('b'c'a) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term'e'f) Mlwtree.abstract_term
val mk_ac_rmed : string -> ('a'b, string) Mlwtree.abstract_term
val mk_ac_old_rmed : string -> ((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd'e) Mlwtree.abstract_term
val mk_field_id : string -> string
val mk_view_id : string -> string
val mk_use_list : (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use : (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_field : (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_view : (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_module : Mlwtree.ident Mlwtree.with_loc -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_euclidean_div : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_use_min_max : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val map_lident : M.lident -> Mlwtree.loc_ident
val map_btype : M.btyp -> ('a'b) Mlwtree.abstract_type
val get_type_idx : M.type_ -> M.type_ list -> int
val mk_map_name : Archetype__Model.model -> M.type_ -> string
val mk_set_name : Archetype__Model.model -> M.type_ -> string
val mk_list_name : Archetype__Model.model -> M.type_ -> string
val map_mtype : Archetype__Model.model -> M.type_ -> Mlwtree.loc_typ
val mk_list_name_from_mlwtype : Archetype__Model.model -> Mlwtree.typ -> string
val mk_eq_type : Archetype__Model.model -> Mlwtree.ident -> Mlwtree.ident -> (Mlwtree.identMlwtree.typ) Mlwtree.abstract_type -> (((('a('b'c) Mlwtree.abstract_typeMlwtree.ident) Mlwtree.abstract_term as 'a, ('b'c) Mlwtree.abstract_typeMlwtree.ident) Mlwtree.abstract_term('b'c) Mlwtree.abstract_typeMlwtree.ident) Mlwtree.abstract_term('b'c) Mlwtree.abstract_typeMlwtree.ident) Mlwtree.abstract_term
val mk_le_type : string -> string -> ('b'a) Mlwtree.abstract_type as 'a -> (((('c('d'e) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'c, ('d'e) Mlwtree.abstract_type, string) Mlwtree.abstract_term('d'e) Mlwtree.abstract_type, string) Mlwtree.abstract_term('d'e) Mlwtree.abstract_type, string) Mlwtree.abstract_term
type change =
| CAdd of Mlwtree.ident
| CRm of Mlwtree.ident
| CUpdate of Mlwtree.ident
| CTransfer of Mlwtree.ident
| CGet of Mlwtree.ident
| CIterate of Mlwtree.ident
| CCall of Mlwtree.ident
type trace_id_type =
| Asset
| Entry
| Field
val trace_value_type_to_string : trace_id_type -> string
val mk_trace_id : trace_id_type -> string -> string
val mk_change_term : change -> (('a'b, string) Mlwtree.abstract_term'c'd) Mlwtree.abstract_term
val mk_trace : change -> Mlwtree.loc_term
val mk_trace_asset : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc list
val mk_trace_entry : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc
val mk_trace_field : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc
val mk_trace_clone : unit -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc
val mk_trace_utils : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc list
val mk_default_init : (Mlwtree.termMlwtree.typMlwtree.ident) Mlwtree.abstract_decl -> ((Mlwtree.term'aMlwtree.ident) Mlwtree.abstract_term(Mlwtree.ident'b) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_collection_field : Mlwtree.ident -> (Mlwtree.ident -> 'a) -> Mlwtree.loc_term list option -> ((Mlwtree.loc_termMlwtree.loc_typMlwtree.ident Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typ'a Mlwtree.with_loc) Mlwtree.abstract_field
val mk_const_fields : Archetype__Model.model -> (('a'b, string) Mlwtree.abstract_term(string, (string, 'c) Mlwtree.abstract_type) Mlwtree.abstract_type, string) Mlwtree.abstract_field list
val mk_sum_clone_id : Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> string
val mk_sum_clone_from_id : string -> int -> string
val mk_get_sum_value_id : string -> int -> string
val mk_get_sum_value_from_pos_id : string -> int -> string
val mk_sum : string -> int -> 'a -> 'a -> ('a'b, string) Mlwtree.abstract_term
val mk_sum_from_col : string -> int -> 'a -> ('a'b, string) Mlwtree.abstract_term
val mk_sum_clone : Archetype__Model.model -> Ident.ident -> string -> M.type_ -> Archetype__Model.mterm -> ('a(Ident.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_partition_axiom : Mlwtree.ident -> Mlwtree.ident -> 'a -> Mlwtree.ident -> Mlwtree.typ -> Mlwtree.decl
val sort_kind_to_string : M.sort_kind -> string
val mk_cmp_function_id : string -> (string * M.sort_kind) list -> string
val mk_cmp_function_body : Archetype__Model.model -> Ident.ident -> (Ident.ident * M.sort_kind) list -> (((('a('b'c) Mlwtree.abstract_typeIdent.ident) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_typeIdent.ident) Mlwtree.abstract_term as 'a, ('b'c) Mlwtree.abstract_typeIdent.ident) Mlwtree.abstract_termMlwtree.typIdent.ident) Mlwtree.abstract_term
val mk_cmp_function : Archetype__Model.model -> Mlwtree.ident -> (Ident.ident * M.sort_kind) list -> (Mlwtree.termMlwtree.typMlwtree.ident) Mlwtree.abstract_decl
val mk_sort_clone_id : string -> (string * M.sort_kind) list -> string
val mk_sort_clone : 'a -> string -> (string * M.sort_kind) list -> ('b(string, 'c) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
type filter =
| Select
| Removeif
val mk_afun_test : (('a'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term as 'a -> (('a'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term
val acc_has_id : 'a -> ('b * 'a * 'c) list -> bool
val extract_args : M.lident M.mterm_gen -> (M.mterm * string * ('a'b) Mlwtree.abstract_type) list
val mk_filter_name : Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> filter -> string
val mk_select_name : Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> string
val mk_removeif_name : Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> string
val mk_filter_predicate : filter -> Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> (('a('b'c) Mlwtree.abstract_type, string) Mlwtree.abstract_term('b'c) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'a -> (string * M.type_) list -> (((('a('b'c) Mlwtree.abstract_type, string) Mlwtree.abstract_term('b'c) Mlwtree.abstract_type, string) Mlwtree.abstract_term('b'c) Mlwtree.abstract_type, string) Mlwtree.abstract_termMlwtree.typ, string) Mlwtree.abstract_decl
val mk_select_predicate : Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> (('a(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'a -> (string * M.type_) list -> (((('a(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_termMlwtree.typ, string) Mlwtree.abstract_decl
val mk_removeif_predicate : Archetype__Model.model -> Ident.ident -> Archetype__Model.mterm -> (('a(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'a -> (string * M.type_) list -> (((('a(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_term(Mlwtree.identMlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_termMlwtree.typ, string) Mlwtree.abstract_decl
val get_definition_body : Archetype__Model.model -> Ident.ident -> M.lident M.mterm_gen option
val get_predicate_body : Archetype__Model.model -> Ident.ident -> M.lident M.mterm_gen option
val is_predicate : Archetype__Model.model -> Ident.ident -> bool
val extract_def_args : Archetype__Model.model -> M.lident M.mterm_gen -> (('a'bIdent.ident) Mlwtree.abstract_term * Ident.ident * Mlwtree.loc_typ) list
val get_def_params : Archetype__Model.model -> Ident.ident -> ('a'bIdent.ident) Mlwtree.abstract_term list
val get_pred_params : Archetype__Model.model -> Ident.ident -> ('a'bIdent.ident) Mlwtree.abstract_term list
val wdl : 'a list -> 'a Mlwtree.with_loc list
val unloc_decl : Mlwtree.loc_decl list -> (Mlwtree.termMlwtree.typMlwtree.ident) Mlwtree.abstract_decl list
val loc_decl : Mlwtree.decl list -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc list
val loc_field : Mlwtree.field list -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_field Mlwtree.with_loc list
val deloc : 'a Mlwtree.with_loc list -> 'a list
val zip : 'a list -> 'a list -> 'a list -> 'a list -> 'a list -> 'a list -> 'a list -> 'a list -> 'a list
val cap : string Mlwtree.with_loc -> string Mlwtree.with_loc
val mk_eq_type_fun : Archetype__Model.model -> string -> (Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc -> (Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_le_type_fun : 'a -> string -> (Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc -> (Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_map_clone : string -> 'a -> 'a -> ('b'astring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_map_type : Archetype__Model.model -> M.type_ -> (Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl list
val mk_set_clone : string -> 'a -> ('b'astring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_type : Archetype__Model.model -> M.type_ -> (Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl list
val mk_list_clone : string -> 'a -> ('b'astring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_list_type : Archetype__Model.model -> M.type_ -> (Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl list
val map_record_fields : Archetype__Model.model -> M.record_field list -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_field list
val mk_record : Archetype__Model.model -> M.record -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val map_lidents : M.lident list -> Mlwtree.loc_ident list
val type_to_init : Archetype__Model.model -> Mlwtree.loc_typ -> Mlwtree.loc_term
val is_local_invariant : 'a -> Ident.ident -> M.lident M.mterm_gen -> bool
val adds_asset : Archetype__Model.model -> Ident.ident -> M.lident M.mterm_gen -> bool
val is_only_security : M.security_predicate -> bool
val map_action_to_change : M.entry_description -> change
val map_security_pred : [< `Loop | `Storage ] -> M.security_predicate -> ((('a('b'c) Mlwtree.abstract_typeIdent.ident) Mlwtree.abstract_term as 'a, ('b'c) Mlwtree.abstract_typeIdent.ident) Mlwtree.abstract_term'd'e) Mlwtree.abstract_term
val mk_spec_invariant : [< `Loop | `Storage ] -> M.security_item -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_app_field : Mlwtree.ident -> Mlwtree.loc_ident -> Mlwtree.loc_term * Mlwtree.loc_term
val mk_invariant : Archetype__Model.model -> Ident.ident Location.loced -> [> `Axiom | `Axiom2 | `Loop | `Preasset of Mlwtree.ident | `Precoll of Mlwtree.ident | `Prelist of Mlwtree.ident | `Storage ] -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_storage_invariant : Archetype__Model.model -> Ident.ident Location.loced -> M.lident -> Mlwtree.loc_term -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula
val mk_pre_coll : Archetype__Model.model -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_pre_asset : Archetype__Model.model -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_loop_invariant : Archetype__Model.model -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_axiom_invariant : Archetype__Model.model -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_axiom2_invariant : Archetype__Model.model -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_state_invariant : 'a -> Mlwtree.ident Location.loced -> M.lident -> Mlwtree.loc_term -> ((Mlwtree.loc_term'b'c) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_ident) Mlwtree.abstract_formula
val mk_eq_enums : Archetype__Model.model -> M.asset -> (Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_decl list
val mk_eq_key : Archetype__Model.model -> M.asset -> (Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_le_key : Archetype__Model.model -> M.asset -> (Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_eq_asset : Archetype__Model.model -> M.asset -> (Mlwtree.loc_term(Mlwtree.loc_ident'a) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_enum : 'a -> M.enum -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val get_fail_idx : Archetype__Model.model -> M.type_ -> int
val mk_exn : Archetype__Model.model -> int -> M.type_ -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.ident Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_field : Archetype__Model.model -> M.asset -> ('aMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_view : Archetype__Model.model -> M.asset -> ('aMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_coll : Archetype__Model.model -> M.asset -> ('aMlwtree.loc_typIdent.ident Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_field_id : string -> string
val mk_set_field : 'a -> Mlwtree.ident -> string -> string -> ((Mlwtree.loc_term'bstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_aggregates : Archetype__Model.model -> M.asset -> ((Mlwtree.loc_term'aIdent.ident Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typIdent.ident Mlwtree.with_loc) Mlwtree.abstract_decl list
val mk_partition_axioms : M.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val get_record : 'a -> ('b'c'a) Mlwtree.abstract_decl list -> ('b'c'a) Mlwtree.abstract_decl
val get_record_name : ('a'b'c) Mlwtree.abstract_decl -> 'c
val mk_lbl_before : string option -> string
val mk_inv_lbl : string option -> string -> string
val mk_storage_loop_inv : string option -> Mlwtree.ident -> Mlwtree.ident -> (Mlwtree.loc_termstring Mlwtree.with_loc) Mlwtree.abstract_formula
val is_identical : Tools.String.t -> M.effect list -> bool
val mk_vars_loop_invariants : Archetype__Model.model -> Ident.ident option -> string option -> Mlwtree.ident -> Archetype__Model.mterm -> (Mlwtree.loc_termstring Mlwtree.with_loc) Mlwtree.abstract_formula list
type mode =
| Inv
| Logic
| Exec
| Def
type logical_context = {
lctx : mode;
entry_id : Mlwtree.ident option;
locals : Mlwtree.ident list;
loop_id : Mlwtree.ident option;
}
val init_ctx : logical_context
val add_local : Mlwtree.ident -> logical_context -> logical_context
val mk_trace_seq : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_term -> change list -> ((Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_term
val map_mpattern : M.lident M.pattern_node -> Mlwtree.loc_ident Mlwtree.pattern_node
val is_coll_field : Archetype__Model.model -> Ident.ident -> bool
val is_exec_divergent : ('a'b) M.mterm_node -> bool
val get_tuple_size : M.ntype -> int
val cp_storage : string -> (('a'b, string) Mlwtree.abstract_term'c'd) Mlwtree.abstract_term
val fail_if_neg_nat_value : M.type_ -> Mlwtree.loc_term -> Mlwtree.loc_term -> (Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locMlwtree.loc_ident) Mlwtree.abstract_term Mlwtree.with_loc -> ((Mlwtree.loc_term(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locMlwtree.loc_ident) Mlwtree.abstract_term Mlwtree.with_loc(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locMlwtree.loc_ident) Mlwtree.abstract_term Mlwtree.with_loc
val get_assign_value : M.type_ -> Mlwtree.loc_term -> Mlwtree.loc_term -> M.assignment_operator -> Mlwtree.loc_term
val is_partition : Archetype__Model.model -> Ident.ident -> Ident.ident -> bool
val mk_get_force : Mlwtree.loc_ident -> Mlwtree.loc_term -> Mlwtree.loc_term -> ((Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_term Mlwtree.with_loc'astring Mlwtree.with_loc) Mlwtree.abstract_term
val mk_match_get_some : string -> Mlwtree.loc_term -> (Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc -> Mlwtree.term Mlwtree.exn -> ((Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc'a'b) Mlwtree.abstract_term
val mk_match_get_some_id : 'a -> string -> Mlwtree.loc_term -> (Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc -> Mlwtree.term Mlwtree.exn -> ((Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc'b'a) Mlwtree.abstract_term
val mk_match_get_some_id_nil : 'a -> string -> Mlwtree.loc_term -> (Mlwtree.loc_term'bstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc -> ((Mlwtree.loc_term'bstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc'c'a) Mlwtree.abstract_term
val mk_match_get_none : string -> Mlwtree.loc_term -> (Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc -> Mlwtree.term Mlwtree.exn -> ((Mlwtree.loc_termMlwtree.loc_typstring Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc'a'b) Mlwtree.abstract_term
val mk_match : Mlwtree.loc_term -> 'a -> Mlwtree.loc_term -> Mlwtree.term Mlwtree.exn -> (Mlwtree.loc_term'b'a Mlwtree.with_loc) Mlwtree.abstract_term
val mk_storage_id : logical_context -> string
val mk_coll_term : string -> logical_context -> (M.temp * M.delta) -> ((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'dIdent.ident) Mlwtree.abstract_term
val mk_loc_coll_term : string -> logical_context -> (M.temp * M.delta) -> Mlwtree.loc_term
val mk_lc_term : string -> logical_context -> Mlwtree.loc_term
val mk_temp_delta : 'a M.container_kind_gen -> M.temp * M.delta
val assign_operation : Mlwtree.loc_term -> Mlwtree.loc_term -> Mlwtree.loc_term -> (Mlwtree.loc_term'a'b) Mlwtree.abstract_term
val map_mterm : Archetype__Model.model -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_invariants : Archetype__Model.model -> logical_context -> Ident.ident Location.loced option -> Ident.ident option -> M.lident M.mterm_gen -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_filter_args : Archetype__Model.model -> logical_context -> (Mlwtree.ident * M.type_) list -> M.lident M.mterm_gen -> Mlwtree.loc_term list
val mk_asset_key_value : Archetype__Model.model -> logical_context -> Ident.ident -> M.lident M.mterm_gen -> Mlwtree.loc_term
val mk_container_term : Archetype__Model.model -> Ident.ident -> logical_context -> M.lident M.mterm_gen M.container_kind_gen -> Mlwtree.loc_term
val map_asset_values : Archetype__Model.model -> M.asset_item list -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_field list
val mk_asset : Archetype__Model.model -> M.asset -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val map_init_mterm : Archetype__Model.model -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_storage_items : Archetype__Model.model -> M.storage_item list -> ((Mlwtree.loc_termMlwtree.loc_typMlwtree.ident Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typIdent.ident Mlwtree.with_loc) Mlwtree.abstract_field list
val mk_asset_invariants : Archetype__Model.model -> logical_context -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_contract_invariants : Archetype__Model.model -> logical_context -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_variable_invariants : Archetype__Model.model -> logical_context -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_security_invariants : M.model -> 'a -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_state_invariants : Archetype__Model.model -> logical_context -> ((Mlwtree.loc_term'a'b) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_storage : Archetype__Model.model -> M.storage -> ((Mlwtree.loc_termMlwtree.loc_typMlwtree.ident Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typIdent.ident Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_cp_storage : Archetype__Model.model -> M.storage -> (Mlwtree.loc_term('a'b) Mlwtree.abstract_type Mlwtree.with_locstring Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_axioms : M.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_api_precond : Archetype__Model.model -> string -> Ident.ident -> [> `Axiom | `Axiom2 | `Loop | `Preasset of Mlwtree.ident | `Precoll of Mlwtree.ident | `Prelist of Mlwtree.ident | `Storage ] -> (Mlwtree.term, string) Mlwtree.abstract_formula list
val mk_key_found_cond : [< `Curr | `Old ] -> string -> ((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term -> ((((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term'e, string) Mlwtree.abstract_term('f'g) Mlwtree.abstract_type'h) Mlwtree.abstract_term
val mk_not_found_cond : [< `Curr | `Old ] -> string -> ((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term -> ((((('a'b, string) Mlwtree.abstract_term'c, string) Mlwtree.abstract_term'd, string) Mlwtree.abstract_term'e, string) Mlwtree.abstract_term('f'g) Mlwtree.abstract_type'h) Mlwtree.abstract_term
val mk_get_sum_value_from_pos : string -> int -> (('a'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term as 'a -> ((((('a'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term(string, 'c) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_get_sum_value : string -> int -> (('a'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term as 'a -> ((('a'b, string) Mlwtree.abstract_term'b, string) Mlwtree.abstract_term(string, 'c) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_storage_api_before_storage : M.model -> 'a -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_storage_api : M.model -> 'a -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val fold_fails : Archetype__Model.model -> logical_context -> M.lident M.mterm_gen -> (Mlwtree.loc_ident option * Mlwtree.loc_term) list
val fold_exns : Archetype__Model.model -> M.lident M.mterm_gen -> Mlwtree.term list
val mk_theory : Archetype__Model.model -> ((((Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typIdent.ident Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_locMlwtree.loc_typIdent.ident Mlwtree.with_loc) Mlwtree.abstract_term Mlwtree.with_loc(Mlwtree.loc_identMlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_locMlwtree.loc_ident) Mlwtree.abstract_decl list
val is_fail : M.mterm -> bool
val flatten_if_fail : Archetype__Model.model -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_ensures : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list -> M.specification -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_delta_requires : Archetype__Model.model -> (Mlwtree.loc_termstring Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_preconds : Archetype__Model.model -> M.argument list -> M.lident M.mterm_gen -> (Mlwtree.loc_termMlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_entry_require : Archetype__Model.model -> string list -> (Mlwtree.loc_termstring Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_functions : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_entries : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl list
val rm_fail_exn : Mlwtree.loc_term list -> Mlwtree.loc_term list
val process_no_fail : Archetype__Model.model -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl -> (Mlwtree.loc_termMlwtree.loc_typMlwtree.loc_ident) Mlwtree.abstract_decl
val to_whyml : M.model -> Mlwtree.mlw_tree