package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
module M = Model
type error_desc =
  1. | NotSupported of string
  2. | 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 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_id : string -> string
val mk_ac_id : string -> string
val mk_ac_added_id : string -> string
val mk_ac_rmed_id : string -> string
val gs : string
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 : 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 : 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_ac_sv : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
val mk_field_id : string -> string
val mk_view_id : string -> string
val mk_use_euclidean_div : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val mk_use_min_max : Ident.ident Location.loced Archetype__Model.model_gen -> (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 get_type_idx : M.type_ -> M.type_ list -> int
val mk_map_name : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> string
val mk_set_name : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> string
val mk_list_name : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> string
val map_mtype : Ident.ident Location.loced Archetype__Model.model_gen -> M.type_ -> Mlwtree.loc_typ
val mk_list_name_from_mlwtype : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.typ -> string
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 =
  1. | CAdd of Mlwtree.ident
  2. | CRm of Mlwtree.ident
  3. | CUpdate of Mlwtree.ident
  4. | CTransfer of Mlwtree.ident
  5. | CGet of Mlwtree.ident
  6. | CIterate of Mlwtree.ident
  7. | CCall of Mlwtree.ident
type trace_id_type =
  1. | Asset
  2. | Entry
  3. | 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_entry : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl Mlwtree.with_loc
val mk_const_fields : Ident.ident Location.loced Archetype__Model.model_gen -> (('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 : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> 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 : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> 'a -> M.type_ -> Ident.ident Location.loced Archetype__Model.mterm_gen -> ('b, (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 : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> (Ident.ident * M.sort_kind) list -> (((('a, ('b, 'c) Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term as 'a, ('b, 'c) Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term, Mlwtree.typ, Ident.ident) Mlwtree.abstract_term
val mk_cmp_function : Ident.ident Location.loced Archetype__Model.model_gen -> 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 match_get : 'a -> 'b -> 'c -> 'c -> ('c, 'd, 'a) Mlwtree.abstract_term -> ('c, 'd, 'a) Mlwtree.abstract_term -> (('c, 'd, 'a) Mlwtree.abstract_term, 'e, 'b) Mlwtree.abstract_term
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 mk_select_body : Mlwtree.ident -> Mlwtree.ident -> Mlwtree.typ -> (('a, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term as 'a -> Mlwtree.term
val extract_args : M.lident M.mterm_gen -> (M.mterm * string * ('a, 'b) Mlwtree.abstract_type) list
val mk_select_name : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> string
val mk_select_formula : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> (('a, 'b, string) Mlwtree.abstract_term, 'b, string) Mlwtree.abstract_term as 'a -> (string * M.type_) list -> ((('a, 'b, string) Mlwtree.abstract_term, 'b, string) Mlwtree.abstract_term, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_removeif_body : Ident.ident Location.loced Archetype__Model.model_gen -> bool -> Ident.ident -> (('a, Mlwtree.typ, Ident.ident) Mlwtree.abstract_term, Mlwtree.typ, Ident.ident) Mlwtree.abstract_term as 'a -> Mlwtree.term
val mk_removeif_name : string -> Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> string
val wdl : 'a list -> 'a 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_map_clone : string -> 'a -> 'a -> ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_set_clone : string -> 'a -> ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_list_clone : string -> 'a -> ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl
val map_record_fields : Ident.ident Location.loced Archetype__Model.model_gen -> M.record_field list -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field list
val map_lidents : M.lident list -> Mlwtree.loc_ident list
val type_to_init : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.loc_typ -> Mlwtree.loc_term
val is_local_invariant : 'a -> Ident.ident -> M.lident M.mterm_gen -> bool
val adds_asset : Ident.ident Location.loced Archetype__Model.model_gen -> 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_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_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> 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_pre_list : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_pre_coll : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_pre_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_loop_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_axiom_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_axiom2_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
val mk_eq_enums : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> (Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl list
val mk_field : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> ('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl
val mk_view : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> ('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl
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
type logical_mod =
  1. | Nomod
  2. | Added
  3. | Removed
type lctx =
  1. | Inv
  2. | Logic
  3. | Other
type logical_context = {
  1. lctx : lctx;
  2. old : bool;
  3. lmod : logical_mod;
  4. localold : Mlwtree.ident list;
  5. loop_id : Mlwtree.ident option;
}
val init_ctx : logical_context
val is_old : logical_context -> M.mterm -> bool
val mk_ac_ctx : string -> logical_context -> Mlwtree.loc_term
val is_coll_field : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> bool
val is_exec_divergent : ('a, 'b) M.mterm_node -> bool
val get_tuple_size : M.type_ -> int
val map_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
val map_asset_values : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset_item list -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field list
val map_init_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
val mk_asset_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_contract_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
val mk_variable_invariants : Ident.ident Location.loced Archetype__Model.model_gen -> 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_api_precond : Ident.ident Location.loced Archetype__Model.model_gen -> 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_get_asset : string -> string -> (string, 'a) Mlwtree.abstract_type -> ((((((('b, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, string) Mlwtree.abstract_term, ('g, 'h) Mlwtree.abstract_type, string) Mlwtree.abstract_term, ('i, 'j) Mlwtree.abstract_type, string) Mlwtree.abstract_term, (string, 'a) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_nth_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, (Mlwtree.ident, Mlwtree.typ) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val gen_exists_asset : [< `Curr | `Old ] -> string -> string -> string -> ((((('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 -> ((((((('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, 'i, 'j) Mlwtree.abstract_term, (string, 'k) Mlwtree.abstract_type, string) Mlwtree.abstract_term
val mk_set_count_ensures : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> ((((((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, Ident.ident) Mlwtree.abstract_term, 'f, string) Mlwtree.abstract_term, ('g, 'h) Mlwtree.abstract_type, 'i) Mlwtree.abstract_term, string) Mlwtree.abstract_formula list
val mk_set_asset_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
val mk_contains : string -> ('a, 'b) Mlwtree.abstract_type -> (((('c, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, ('f, 'g) Mlwtree.abstract_type, string) Mlwtree.abstract_term, ('a, 'b) Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_add_asset_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
val mk_listtocoll_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
val gen_field_getter : 'a -> 'b -> (('c, 'd, 'e) Mlwtree.abstract_term, ('f, 'g) Mlwtree.abstract_type, 'a) Mlwtree.abstract_decl
val gen_field_getters : ('a, 'b, 'c) Mlwtree.abstract_decl -> (('d, 'e, 'f) Mlwtree.abstract_term, ('g, 'h) Mlwtree.abstract_type, 'c) Mlwtree.abstract_decl list
val mk_add_sum_ensures : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> string -> ((((((('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, string) Mlwtree.abstract_term, ('h, 'i) Mlwtree.abstract_type, 'j) Mlwtree.abstract_term, string) Mlwtree.abstract_formula list
val mk_add_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
val mk_rm_sum_ensures : Ident.ident Location.loced Archetype__Model.model_gen -> ((((((('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, string) Mlwtree.abstract_term, ('h, 'i) Mlwtree.abstract_type, 'j) Mlwtree.abstract_term -> 'k) -> Ident.ident -> 'l -> ('k, string) Mlwtree.abstract_formula list
val mk_clear_sum_ensures : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, ('d, 'e) Mlwtree.abstract_type, 'f) Mlwtree.abstract_term, string) Mlwtree.abstract_formula list
val mk_clear_count_ensures : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> ((((('a, 'b, string) Mlwtree.abstract_term, 'c, Ident.ident) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, ('e, 'f) Mlwtree.abstract_type, 'g) Mlwtree.abstract_term, string) Mlwtree.abstract_formula list
val mk_clear_ensures : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> ((((('a, 'b, string) Mlwtree.abstract_term, 'c, Ident.ident) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, ('e, 'f) Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term, string) Mlwtree.abstract_formula list
val mk_rm_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.decl
val mk_clear_view : 'a -> string -> Mlwtree.decl
val mk_add_field : Ident.ident Location.loced Archetype__Model.model_gen -> bool -> Ident.ident -> 'a -> Ident.ident -> Ident.ident -> Mlwtree.ident -> Mlwtree.decl
val mk_rm_field : Ident.ident Location.loced Archetype__Model.model_gen -> bool -> Ident.ident -> 'a -> Ident.ident -> Ident.ident -> 'b -> Mlwtree.decl
val mk_storage_api_before_storage : M.model -> 'a -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
val is_partition : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident -> bool
val fold_exns : Ident.ident Location.loced Archetype__Model.model_gen -> M.lident M.mterm_gen -> Mlwtree.term list
val is_fail : M.mterm -> bool
val flatten_if_fail : Ident.ident Location.loced Archetype__Model.model_gen -> M.mterm -> Mlwtree.loc_term
val mk_require : string -> int -> 'a -> ('a, string Mlwtree.with_loc) Mlwtree.abstract_formula
val mk_requires : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident Location.loced Archetype__Model.specification_gen option -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_entry_require : Ident.ident Location.loced Archetype__Model.model_gen -> string list -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
val mk_functions : Ident.ident Location.loced Archetype__Model.model_gen -> (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 to_whyml : M.model -> Mlwtree.mlw_tree
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct