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 gArchetypeDir : string
val gArchetypeLib : string
val gArchetypeColl : string
val gArchetypeSum : string
val gArchetypeSort : string
val gListLib : string
val gArchetypeTrace : 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 map_lident : M.lident -> Mlwtree.loc_ident
val map_btype : M.btyp -> 'a Mlwtree.abstract_type
val map_mtype : M.type_ -> Mlwtree.loc_typ
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
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 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 -> Ident.ident Location.loced Archetype__Model.mterm_gen -> ('b, 'c, Ident.ident) Mlwtree.abstract_decl
val mk_keys_eq_axiom : Mlwtree.ident -> Mlwtree.ident -> Mlwtree.typ -> Mlwtree.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 : (string * M.sort_kind) list -> (((('a, 'b Mlwtree.abstract_type, string) Mlwtree.abstract_term, 'c Mlwtree.abstract_type, string) Mlwtree.abstract_term as 'a, 'b Mlwtree.abstract_type, string) Mlwtree.abstract_term, 'c Mlwtree.abstract_type, string) Mlwtree.abstract_term
val mk_sort_clone_id : string -> (string * M.sort_kind) list -> string
val mk_sort_clone : 'a -> string -> (string * M.sort_kind) list -> ('b, 'c, string) Mlwtree.abstract_decl
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 : bool -> Mlwtree.ident -> (('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 Mlwtree.abstract_type) list
val mk_select_name : string -> Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Ident.ident Location.loced Archetype__Model.mterm_gen -> string
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
val cap : string Mlwtree.with_loc -> string Mlwtree.with_loc
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 map_record_field_type : M.type_ -> Mlwtree.loc_typ
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 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_cmp_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_eq_extensionality : 'a -> M.asset -> Mlwtree.loc_decl
val record_to_clone : Ident.ident Location.loced Archetype__Model.model_gen -> M.asset -> ('a, 'b, Ident.ident 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. | 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 map_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
val map_record_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_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
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_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 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 Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_get_asset : string -> string -> string Mlwtree.abstract_type -> ((((((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, string) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, string) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_cnth_asset : string -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val mk_vnth_asset : string -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, string 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 Mlwtree.abstract_type, 'g) 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 Mlwtree.abstract_type, 'g) Mlwtree.abstract_term, 'h, 'i) Mlwtree.abstract_term, string 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 Mlwtree.abstract_type, 'g) 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 Mlwtree.abstract_type -> (((('b, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e Mlwtree.abstract_type, string) Mlwtree.abstract_term, 'a 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 mk_listtocoll : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> (Mlwtree.term, Ident.ident Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val gen_field_getter : 'a -> 'b -> (('c, 'd, 'e) Mlwtree.abstract_term, 'f Mlwtree.abstract_type, 'a) Mlwtree.abstract_decl
val gen_field_getters : ('a, 'b, 'c) Mlwtree.abstract_decl -> (('d, 'e, 'f) Mlwtree.abstract_term, 'g 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 Mlwtree.abstract_type, string) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, 'h) 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 Mlwtree.abstract_type, string) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, 'h) Mlwtree.abstract_term -> 'i) -> Ident.ident -> 'j -> ('i, 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 Mlwtree.abstract_type, 'e) 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 Mlwtree.abstract_type, 'e) 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 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_coll : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.decl
val mk_clear_view : 'a -> Mlwtree.ident -> Mlwtree.decl
val mk_add_field : Ident.ident Location.loced Archetype__Model.model_gen -> bool -> Mlwtree.ident -> 'a -> Ident.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
val mk_rm_field : Ident.ident Location.loced Archetype__Model.model_gen -> bool -> Mlwtree.ident -> 'a -> Ident.ident -> Mlwtree.ident -> 'b -> Mlwtree.decl
val mk_removeall : 'a -> bool -> string -> string -> string -> ((((((('b, 'c, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term, 'e, string) Mlwtree.abstract_term, 'f, string) Mlwtree.abstract_term, 'g, string) Mlwtree.abstract_term, 'h, string) Mlwtree.abstract_term, 'i Mlwtree.abstract_type, string) Mlwtree.abstract_decl
val gnthgen : bool Stdlib.ref
val gselectgen : bool Stdlib.ref
val gremoveifgen : bool Stdlib.ref
val gcleargen : bool Stdlib.ref
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