package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Archetype.Gen_why3Source

Sourcemodule M = Model
Sourceval gArchetypeDir : string
Sourceval gArchetypeLib : string
Sourceval gArchetypeColl : string
Sourceval gArchetypeSum : string
Sourceval gArchetypeList : string
Sourceval gArchetypeTrace : string
Sourceval mk_id : string -> string
Sourceval mk_ac_id : string -> string
Sourceval mk_ac_added_id : string -> string
Sourceval mk_ac_rmed_id : string -> string
Sourceval gs : string
Sourceval mk_ac : string -> ('a, 'b, string) Mlwtree.abstract_term
Sourceval mk_ac_old : string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
Sourceval mk_ac_added : string -> ('a, 'b, string) Mlwtree.abstract_term
Sourceval mk_ac_old_added : string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
Sourceval mk_ac_rmed : string -> ('a, 'b, string) Mlwtree.abstract_term
Sourceval mk_ac_old_rmed : string -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term
Sourceval mk_ac_sv : string -> string -> ('a, 'b, string) Mlwtree.abstract_term
Sourcetype 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
Sourceval mk_change_term : change -> (('a, 'b, string) Mlwtree.abstract_term, 'c, 'd) Mlwtree.abstract_term
Sourceval mk_trace : change -> Mlwtree.loc_term
Sourceval 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
Sourceval 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
Sourceval mk_sum_clone_id : string -> string -> string
Sourceval mk_sum_clone : 'a -> string -> string -> string -> ('b, 'c, string) Mlwtree.abstract_decl
Sourceval mk_partition_axiom : Mlwtree.ident -> Mlwtree.ident -> 'a -> Mlwtree.ident -> Mlwtree.typ -> Mlwtree.decl
Sourceval mk_select_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
Sourceval mk_select_body : Mlwtree.ident -> ((('a, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term as 'a) -> Mlwtree.term
Sourceval extract_args : M.lident M.mterm_gen -> (M.mterm * string * 'a Mlwtree.abstract_type) list
Sourceval get_select_id : M.model -> Ident.ident -> M.mterm -> int
Sourceval mk_select_name : M.model -> Ident.ident -> M.mterm -> string
Sourceval wdl : 'a list -> 'a Mlwtree.with_loc list
Sourceval deloc : 'a Mlwtree.with_loc list -> 'a list
Sourceval zip : 'a list -> 'a list -> 'a list -> 'a list -> 'a list
Sourceval cap : string Mlwtree.with_loc -> string Mlwtree.with_loc
Sourceval map_lident : M.lident -> Mlwtree.loc_ident
Sourceval map_lidents : M.lident list -> Mlwtree.loc_ident list
Sourceval map_btype : M.btyp -> 'a Mlwtree.abstract_type
Sourceval map_mtype : M.type_ -> Mlwtree.loc_typ
Sourceval map_record_term : 'a -> M.mterm -> Mlwtree.loc_term
Sourceval is_local_invariant : 'a -> Ident.ident -> M.lident M.mterm_gen -> bool
Sourceval adds_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> M.lident M.mterm_gen -> bool
Sourceval is_only_security : M.security_predicate -> bool
Sourceval map_action_to_change : M.action_description -> change
Sourceval mk_spec_invariant : [< `Loop | `Storage ] -> M.security_item -> (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list
Sourceval 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
Sourceval mk_pre_list : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
Sourceval mk_pre_coll : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
Sourceval mk_pre_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
Sourceval mk_loop_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
Sourceval mk_axiom_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
Sourceval mk_axiom2_invariant : Ident.ident Location.loced Archetype__Model.model_gen -> Ident.ident -> Mlwtree.loc_term -> Mlwtree.loc_term
Sourceval mk_eq_extensionality : 'a -> M.record -> Mlwtree.loc_decl
Sourceval record_to_clone : Ident.ident Location.loced Archetype__Model.model_gen -> M.info_asset -> ('a, 'b, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_decl
Sourceval get_record : 'a -> ('b, 'c, 'a) Mlwtree.abstract_decl list -> ('b, 'c, 'a) Mlwtree.abstract_decl
Sourceval get_record_name : ('a, 'b, 'c) Mlwtree.abstract_decl -> 'c
Sourcetype logical_mod =
  1. | Nomod
  2. | Added
  3. | Removed
Sourcetype logical_context = {
  1. old : bool;
  2. lmod : logical_mod;
}
Sourceval init_ctx : logical_context
Sourceval map_mterm : Ident.ident Location.loced Archetype__Model.model_gen -> logical_context -> M.mterm -> Mlwtree.loc_term
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval mk_get_field_from_pos : string -> string -> (((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, 'd, 'e) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
Sourceval 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
Sourceval mk_set_asset_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
Sourceval mk_unshallow : string -> string Mlwtree.abstract_type -> ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term, string Mlwtree.abstract_type, string) Mlwtree.abstract_decl
Sourceval mk_add_asset_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
Sourceval mk_listtocoll_precond : Ident.ident Location.loced Archetype__Model.model_gen -> string -> Ident.ident -> Mlwtree.ident -> (Mlwtree.term, string) Mlwtree.abstract_formula list
Sourceval gen_field_getter : 'a -> 'b -> (('c, 'd, 'e) Mlwtree.abstract_term, 'f Mlwtree.abstract_type, 'a) Mlwtree.abstract_decl
Sourceval gen_field_getters : ('a, 'b, 'c) Mlwtree.abstract_decl -> (('d, 'e, 'f) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, 'c) Mlwtree.abstract_decl list
Sourceval mk_add_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
Sourceval mk_rm_asset : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
Sourceval mk_add_partition_field : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
Sourceval mk_rm_partition_field : Ident.ident Location.loced Archetype__Model.model_gen -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.ident -> Mlwtree.decl
Sourceval fold_exns : M.lident M.mterm_gen -> Mlwtree.term list
Sourceval is_fail : M.mterm -> bool
Sourceval flatten_if_fail : Ident.ident Location.loced Archetype__Model.model_gen -> M.mterm -> Mlwtree.loc_term
Sourceval mk_require : string -> int -> 'a -> ('a, string Mlwtree.with_loc) Mlwtree.abstract_formula
Sourceval 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
Sourceval is_src : M.source -> ('a * 'b M.function_struct_gen * 'c) -> bool
Sourceval mk_entry_require : Ident.ident Location.loced Archetype__Model.model_gen -> string list -> (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list
Sourceval mk_endo_functions : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
Sourceval mk_exo_functions : Ident.ident Location.loced Archetype__Model.model_gen -> (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl list
Sourceval rm_fail_exn : Mlwtree.loc_term list -> Mlwtree.loc_term list
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