To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
module M = Model
val pp_error_desc : 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 mk_ac_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_ac_old_st :
'a ->
string ->
((('b, 'c, 'd) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term,
'f,
'g)
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, 'd) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term,
'f,
'g)
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, 'd) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term,
'f,
'g)
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_use_list :
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use :
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_field :
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_view :
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_module :
Mlwtree.ident Mlwtree.with_loc ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val mk_use_euclidean_div :
Archetype__Model.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
list
val mk_use_min_max :
Archetype__Model.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.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 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.ident, Mlwtree.typ) Mlwtree.abstract_type ->
((((('a, ('b, 'c) Mlwtree.abstract_type, Mlwtree.ident) Mlwtree.abstract_term as 'a,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term
val mk_le_type :
Archetype__Model.model ->
Mlwtree.ident ->
Mlwtree.ident ->
Mlwtree.typ ->
((((('a, ('b, 'c) Mlwtree.abstract_type, Mlwtree.ident) Mlwtree.abstract_term as 'a,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Mlwtree.ident)
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
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_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
Mlwtree.with_loc
list
val mk_trace_entry :
Archetype__Model.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
Mlwtree.with_loc
val mk_trace_field :
Archetype__Model.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
Mlwtree.with_loc
val mk_trace_clone :
unit ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
Mlwtree.with_loc
val mk_trace_utils :
Archetype__Model.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
Mlwtree.with_loc
list
val mk_default_init :
(Mlwtree.term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_decl ->
((Mlwtree.term, 'a, Mlwtree.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_term, Mlwtree.loc_typ, Mlwtree.ident Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
'b 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_gen ->
string
val mk_sum :
string ->
int ->
'a ->
'b ->
('c, 'd, string) Mlwtree.abstract_term
val mk_sum_from_col :
string ->
int ->
'a ->
('b, 'c, string) Mlwtree.abstract_term
val mk_sum_clone :
Archetype__Model.model ->
Ident.ident ->
string ->
M.type_ ->
Archetype__Model.mterm_gen ->
('a, (Ident.ident, Mlwtree.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, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, Ident.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Ident.ident)
Mlwtree.abstract_term as 'a,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
Ident.ident)
Mlwtree.abstract_term,
('b, 'c) Mlwtree.abstract_type,
Ident.ident)
Mlwtree.abstract_term,
Mlwtree.typ,
Ident.ident)
Mlwtree.abstract_term
val mk_cmp_function :
Archetype__Model.model ->
Mlwtree.ident ->
(Ident.ident * M.sort_kind) list ->
(Mlwtree.term, Mlwtree.typ, Mlwtree.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
val mk_afun_test :
((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term as 'a,
'b,
string)
Mlwtree.abstract_term ->
((('a, 'b, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
'e,
string)
Mlwtree.abstract_term
val extract_args :
M.mterm ->
(M.mterm * string * ('a, 'b) Mlwtree.abstract_type) list
val mk_filter_name :
Archetype__Model.model ->
Ident.ident ->
Archetype__Model.mterm_gen ->
filter ->
string
val mk_select_name :
Archetype__Model.model ->
Ident.ident ->
Archetype__Model.mterm_gen ->
string
val mk_removeif_name :
Archetype__Model.model ->
Ident.ident ->
Archetype__Model.mterm_gen ->
string
val mk_filter_predicate :
filter ->
Archetype__Model.model ->
Ident.ident ->
Archetype__Model.mterm_gen ->
((('a, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'b,
('c, 'd) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term as 'a,
('c, 'd) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term ->
(string * M.type_) list ->
(((('b, ('c, 'd) Mlwtree.abstract_type, string) Mlwtree.abstract_term,
('c, 'd) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term,
('c, 'd) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term,
Mlwtree.typ,
string)
Mlwtree.abstract_decl
val mk_select_predicate :
Archetype__Model.model ->
Ident.ident ->
Archetype__Model.mterm_gen ->
(('a, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, string)
Mlwtree.abstract_term,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term as 'a ->
(string * M.type_) list ->
(((('a, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, string)
Mlwtree.abstract_term,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term,
Mlwtree.typ,
string)
Mlwtree.abstract_decl
val mk_removeif_predicate :
Archetype__Model.model ->
Ident.ident ->
Archetype__Model.mterm_gen ->
(('a, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, string)
Mlwtree.abstract_term,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term as 'a ->
(string * M.type_) list ->
(((('a, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, string)
Mlwtree.abstract_term,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term,
(Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type,
string)
Mlwtree.abstract_term,
Mlwtree.typ,
string)
Mlwtree.abstract_decl
val get_definition_body :
Archetype__Model.model ->
Ident.ident ->
M.mterm option
val get_predicate_body :
Archetype__Model.model ->
Ident.ident ->
M.mterm option
val is_predicate : Archetype__Model.model -> Ident.ident -> bool
val extract_def_args :
Archetype__Model.model ->
M.mterm ->
(('a, 'b, Ident.ident) Mlwtree.abstract_term * Ident.ident * Mlwtree.loc_typ)
list
val get_def_params :
Archetype__Model.model ->
Ident.ident ->
('a, 'b, Ident.ident) Mlwtree.abstract_term list
val get_pred_params :
Archetype__Model.model ->
Ident.ident ->
('a, 'b, Ident.ident) Mlwtree.abstract_term list
val wdl : 'a list -> 'a0 Mlwtree.with_loc list
val unloc_decl :
Mlwtree.loc_decl list ->
(Mlwtree.term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_decl list
val loc_decl :
Mlwtree.decl list ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
Mlwtree.with_loc
list
val loc_field :
Mlwtree.field list ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field
Mlwtree.with_loc
list
val deloc : 'a Mlwtree.with_loc list -> 'b list
val cap : string Mlwtree.with_loc -> string Mlwtree.with_loc
val mk_eq_type_fun :
Archetype__Model.model ->
string ->
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc ->
(Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_le_type_fun :
Archetype__Model.model ->
string ->
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc ->
(Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_map_clone :
string ->
'a ->
'b ->
('c, 'd, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_map_type :
Archetype__Model.model ->
M.type_ ->
(Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
list
val mk_set_clone :
string ->
'a ->
('b, 'c, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_type :
Archetype__Model.model ->
M.type_ ->
(Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
list
val mk_list_clone :
string ->
'a ->
('b, 'c, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_list_type :
Archetype__Model.model ->
M.type_ ->
(Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
list
val map_record_fields :
Archetype__Model.model ->
M.record_field list ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field
list
val mk_record :
Archetype__Model.model ->
M.record ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.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.mterm -> bool
val adds_asset : Archetype__Model.model -> Ident.ident -> M.mterm -> 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_type, Ident.ident) Mlwtree.abstract_term as 'a,
('b, 'c) Mlwtree.abstract_type,
Ident.ident)
Mlwtree.abstract_term,
'd,
'e)
Mlwtree.abstract_term
val mk_spec_invariant :
[< `Loop | `Storage ] ->
M.security_item ->
(Mlwtree.loc_term, Mlwtree.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_term, Mlwtree.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_loc,
Mlwtree.loc_ident)
Mlwtree.abstract_formula
val mk_eq_enums :
Archetype__Model.model ->
M.asset ->
(Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_decl
list
val mk_eq_key :
Archetype__Model.model ->
M.asset ->
(Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_le_key :
Archetype__Model.model ->
M.asset ->
(Mlwtree.loc_term, Mlwtree.loc_typ, string 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_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_enum :
'a ->
M.enum ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.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_term, Mlwtree.loc_typ, Mlwtree.ident Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_field :
Archetype__Model.model ->
M.asset ->
('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_view :
Archetype__Model.model ->
M.asset ->
('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_coll :
Archetype__Model.model ->
M.asset ->
('a, Mlwtree.loc_typ, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_field :
'a ->
Mlwtree.ident ->
string ->
string ->
((Mlwtree.loc_term, 'b, string Mlwtree.with_loc) Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_aggregates :
Archetype__Model.model ->
M.asset ->
((Mlwtree.loc_term, 'a, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
Ident.ident Mlwtree.with_loc)
Mlwtree.abstract_decl
list
val mk_partition_axioms :
M.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
list
val get_record :
'a ->
('b, 'c, 'd) Mlwtree.abstract_decl list ->
('e, 'f, 'g) Mlwtree.abstract_decl
val get_record_name : ('a, 'b, 'c) Mlwtree.abstract_decl -> 'd
val mk_storage_loop_inv :
string option ->
Mlwtree.ident ->
Mlwtree.ident ->
(Mlwtree.loc_term, string 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_gen ->
(Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
type logical_context = {
lctx : mode;
entry_id : Mlwtree.ident option;
locals : Mlwtree.ident list;
loop_id : Mlwtree.ident option;
fun_ : bool;
fails : bool;
}
val init_ctx : logical_context
val mk_sid : logical_context -> string
val add_local : Mlwtree.ident -> logical_context -> logical_context
val mk_trace_seq :
Archetype__Model.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_term ->
change list ->
((Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
Mlwtree.loc_ident)
Mlwtree.abstract_term
val map_mpattern : M.pattern_node -> Mlwtree.loc_ident Mlwtree.pattern_node
val is_coll_field : Archetype__Model.model -> Ident.ident -> bool
val is_exec_divergent : 'a 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_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
Mlwtree.loc_ident)
Mlwtree.abstract_term
Mlwtree.with_loc ->
((Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type
Mlwtree.with_loc,
Mlwtree.loc_ident)
Mlwtree.abstract_term
Mlwtree.with_loc,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
Mlwtree.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 :
logical_context ->
Mlwtree.loc_ident ->
Mlwtree.loc_term ->
Mlwtree.loc_term ->
((Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_term
Mlwtree.with_loc,
'a,
string Mlwtree.with_loc)
Mlwtree.abstract_term
val mk_match_get_some :
logical_context ->
string ->
Mlwtree.loc_term ->
(Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc ->
Mlwtree.term Mlwtree.exn ->
((Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
'a,
'b)
Mlwtree.abstract_term
val mk_match_get_some_id :
logical_context ->
'a ->
string ->
Mlwtree.loc_term ->
(Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc ->
Mlwtree.term Mlwtree.exn ->
((Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
'b,
'c)
Mlwtree.abstract_term
val mk_match_get_some_id_nil :
'a ->
string ->
Mlwtree.loc_term ->
(Mlwtree.loc_term, 'b, string Mlwtree.with_loc) Mlwtree.abstract_term
Mlwtree.with_loc ->
((Mlwtree.loc_term, 'b, string Mlwtree.with_loc) Mlwtree.abstract_term
Mlwtree.with_loc,
'c,
'd)
Mlwtree.abstract_term
val mk_match_get_none :
logical_context ->
string ->
Mlwtree.loc_term ->
(Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc ->
Mlwtree.term Mlwtree.exn ->
((Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
'a,
'b)
Mlwtree.abstract_term
val mk_match :
logical_context ->
Mlwtree.loc_term ->
'a ->
Mlwtree.loc_term ->
Mlwtree.term Mlwtree.exn ->
(Mlwtree.loc_term, 'b, 'c 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,
'd,
Ident.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 : M.model -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_invariants :
M.model ->
logical_context ->
Ident.ident Location.loced option ->
Ident.ident option ->
M.mterm_gen ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_filter_args :
M.model ->
logical_context ->
(Mlwtree.ident * M.type_) list ->
M.mterm_gen ->
Mlwtree.loc_term list
val mk_asset_key_value :
M.model ->
logical_context ->
Ident.ident ->
M.mterm_gen ->
Mlwtree.loc_term
val mk_container_term :
M.model ->
Ident.ident ->
logical_context ->
M.mterm_gen M.container_kind_gen ->
Mlwtree.loc_term
val map_asset_values :
M.model ->
M.asset_item list ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field
list
val mk_asset :
M.model ->
M.asset ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val map_init_mterm : M.model -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_storage_items :
M.model ->
M.storage_item list ->
((Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.ident Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
Ident.ident Mlwtree.with_loc)
Mlwtree.abstract_field
list
val mk_asset_invariants :
M.model ->
logical_context ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_contract_invariants :
M.model ->
logical_context ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_variable_invariants :
M.model ->
logical_context ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_security_invariants :
M.model ->
'a ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_state_invariants :
M.model ->
logical_context ->
((Mlwtree.loc_term, 'a, 'b) Mlwtree.abstract_term Mlwtree.with_loc,
Mlwtree.loc_ident)
Mlwtree.abstract_formula
list
val mk_cp_storage :
M.model ->
M.storage ->
(Mlwtree.loc_term,
('a, 'b) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
val mk_axioms :
M.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
list
val mk_api_precond :
M.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, 'c, string) Mlwtree.abstract_term as 'b, 'c, string)
Mlwtree.abstract_term as 'a,
'c,
string)
Mlwtree.abstract_term ->
((((('b, 'c, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term,
'c,
string)
Mlwtree.abstract_term,
'c,
string)
Mlwtree.abstract_term,
(string, 'd) Mlwtree.abstract_type,
string)
Mlwtree.abstract_decl
val mk_get_sum_value :
string ->
int ->
((('a, 'c, string) Mlwtree.abstract_term as 'b, 'c, string)
Mlwtree.abstract_term as 'a,
'c,
string)
Mlwtree.abstract_term ->
((('b, 'c, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term,
(string, 'd) Mlwtree.abstract_type,
string)
Mlwtree.abstract_decl
val parameter_to_val :
Archetype__Model.model ->
M.parameter ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val mk_storage_api_before_storage :
M.model ->
'a ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
list
val mk_storage_api :
M.model ->
'a ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
list
val fold_fails :
M.model ->
logical_context ->
M.mterm ->
Mlwtree.struct_fail list
val fold_exns : Archetype__Model.model -> M.mterm -> Mlwtree.term list
val mk_theory :
M.model ->
((((Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident)
Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
Ident.ident Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
Mlwtree.loc_typ,
Ident.ident Mlwtree.with_loc)
Mlwtree.abstract_term
Mlwtree.with_loc,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
Mlwtree.loc_ident)
Mlwtree.abstract_decl
list
val is_fail : M.mterm -> bool
val flatten_if_fail : M.model -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_ensures :
M.model ->
logical_context ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list ->
M.specification ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_delta_requires :
Archetype__Model.model ->
(Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_preconds :
M.model ->
M.argument list ->
M.mterm ->
(Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_entry_require :
Archetype__Model.model ->
string list ->
(Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_functions :
M.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
list
val mk_entries :
M.model ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.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_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl ->
(Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
val show_desc_container : desc_container -> Ppx_deriving_runtime.string
val pp_desc_container : Format.formatter -> desc_container -> unit
val cmp_desc_container : desc_container -> desc_container -> bool
val mk_decls :
M.model ->
(Mlwtree.loc_term,
(Mlwtree.loc_ident, Mlwtree.loc_typ) Mlwtree.abstract_type Mlwtree.with_loc,
string Mlwtree.with_loc)
Mlwtree.abstract_decl
list
val to_whyml : M.model -> Mlwtree.mlw_tree
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>