Module `Archetype.Gen_why3`Source

Sourcemodule M = Model

Sourcetype error_desc =

| NotSupported of string
| TODONotTranslated of string

Sourceval pp_error_desc : Format.formatter -> error_desc -> unit

Sourcetype error = Location.t * error_desc

Sourceval emit_error : (Location.t * error_desc) -> unit

Sourceval dl : 'a -> 'a Mlwtree.with_loc

Sourceval gArchetypeDir : string

Sourceval gArchetypeLib : string

Sourceval gArchetypeField : string

Sourceval gArchetypeView : string

Sourceval gArchetypeColl : string

Sourceval gArchetypeAgg : string

Sourceval gArchetypeSum : string

Sourceval gArchetypeSort : string

Sourceval gArchetypeTrace : string

Sourceval gArchetypeSet : string

Sourceval gArchetypeList : string

Sourceval gOperations : string

Sourceval gListAs : string

Sourceval gFieldAs : string

Sourceval gViewAs : string

Sourceval mk_module_name : string -> string

Sourceval mk_id : string -> string

Sourceval mk_param_value : string -> string

Sourceval mk_ac_id : string -> string

Sourceval mk_ac_added_id : string -> string

Sourceval mk_ac_rmed_id : string -> string

Sourceval mk_ac_unmvd_id : string -> string

Sourceval mk_aggregate_id : string -> string

Sourceval gs : string

Sourceval gsinit : string

Sourceval gsarg : string

Sourceval mk_ac_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_ac_old_st : 
  'a ->
  string ->
  ((('b, 'c, 'a) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    'f)
    Mlwtree.abstract_term

Sourceval mk_ac : string -> ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_ac_old : 
  string ->
  ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term,
    'd,
    'e)
    Mlwtree.abstract_term

Sourceval mk_ac_added_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_ac_old_added_st : 
  'a ->
  string ->
  ((('b, 'c, 'a) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    'f)
    Mlwtree.abstract_term

Sourceval mk_ac_added : string -> ('a, 'b, string) Mlwtree.abstract_term

Source

val 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_st : string -> string -> ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_ac_old_rmed_st : 
  'a ->
  string ->
  ((('b, 'c, 'a) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    'f)
    Mlwtree.abstract_term

Sourceval mk_ac_rmed : string -> ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_ac_old_rmed : 
  string ->
  ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term,
    'd,
    'e)
    Mlwtree.abstract_term

Sourceval mk_field_id : string -> string

Sourceval mk_view_id : string -> string

Source

val mk_use_list : 
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val mk_use : 
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val mk_use_field : 
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val mk_use_view : 
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val mk_use_module : 
  Mlwtree.ident Mlwtree.with_loc ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

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

Source

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

Sourceval map_lident : M.lident -> Mlwtree.loc_ident

Sourceval map_btype : M.btyp -> ('a, 'b) Mlwtree.abstract_type

Sourceval get_type_idx : M.type_ -> M.type_ list -> int

Source

val mk_map_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.type_ ->
  string

Source

val mk_set_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.type_ ->
  string

Source

val mk_list_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.type_ ->
  string

Source

val map_mtype : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.type_ ->
  Mlwtree.loc_typ

Source

val mk_list_name_from_mlwtype : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.typ ->
  string

Source

val mk_eq_type : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_le_type : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Sourcetype 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

Sourcetype trace_id_type =

| Asset
| Entry
| Field

Sourceval trace_value_type_to_string : trace_id_type -> string

Sourceval mk_trace_id : trace_id_type -> string -> string

Source

val mk_change_term : 
  change ->
  (('a, 'b, string) Mlwtree.abstract_term, 'c, 'd) Mlwtree.abstract_term

Sourceval mk_trace : change -> Mlwtree.loc_term

Source

val mk_trace_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    Mlwtree.with_loc
    list

Source

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

Source

val mk_trace_field : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    Mlwtree.with_loc

Source

val mk_trace_clone : 
  unit ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    Mlwtree.with_loc

Source

val mk_trace_utils : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    Mlwtree.with_loc
    list

Source

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

Source

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,
    'a Mlwtree.with_loc)
    Mlwtree.abstract_field

Source

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

Source

val mk_sum_clone_id : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  string

Sourceval mk_sum_clone_from_id : string -> int -> string

Sourceval mk_get_sum_value_id : string -> int -> string

Sourceval mk_get_sum_value_from_pos_id : string -> int -> string

Source

val mk_sum : 
  string ->
  int ->
  'a ->
  'a ->
  ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_sum_from_col : 
  string ->
  int ->
  'a ->
  ('a, 'b, string) Mlwtree.abstract_term

Source

val mk_sum_clone : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  string ->
  M.type_ ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  ('a, (Ident.ident, Mlwtree.typ) Mlwtree.abstract_type, string)
    Mlwtree.abstract_decl

Source

val mk_partition_axiom : 
  Mlwtree.ident ->
  Mlwtree.ident ->
  'a ->
  Mlwtree.ident ->
  Mlwtree.typ ->
  Mlwtree.decl

Sourceval sort_kind_to_string : M.sort_kind -> string

Sourceval mk_cmp_function_id : string -> (string * M.sort_kind) list -> string

Source

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

Source

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

Sourceval mk_sort_clone_id : string -> (string * M.sort_kind) list -> string

Source

val mk_sort_clone : 
  'a ->
  string ->
  (string * M.sort_kind) list ->
  ('b, (string, 'c) Mlwtree.abstract_type, string) Mlwtree.abstract_decl

Sourcetype filter =

| Select
| Removeif

Source

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

Sourceval acc_has_id : 'a -> ('b * 'a * 'c) list -> bool

Source

val extract_args : 
  M.lident M.mterm_gen ->
  (M.mterm * string * ('a, 'b) Mlwtree.abstract_type) list

Source

val mk_filter_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  filter ->
  string

Source

val mk_select_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  string

Source

val mk_removeif_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  string

Source

val mk_filter_predicate : 
  filter ->
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  ((('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_term,
    Mlwtree.typ,
    string)
    Mlwtree.abstract_decl

Source

val mk_select_predicate : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced 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

Source

val mk_removeif_predicate : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced 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

Source

val get_definition_body : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  M.lident M.mterm_gen option

Source

val get_predicate_body : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  M.lident M.mterm_gen option

Source

val is_predicate : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  bool

Source

val extract_def_args : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.lident M.mterm_gen ->
  (('a, 'b, Ident.ident) Mlwtree.abstract_term * Ident.ident * Mlwtree.loc_typ)
    list

Source

val get_def_params : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  ('a, 'b, Ident.ident) Mlwtree.abstract_term list

Source

val get_pred_params : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  ('a, 'b, Ident.ident) Mlwtree.abstract_term list

Sourceval wdl : 'a list -> 'a Mlwtree.with_loc list

Source

val unloc_decl : 
  Mlwtree.loc_decl list ->
  (Mlwtree.term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_decl list

Source

val loc_decl : 
  Mlwtree.decl list ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    Mlwtree.with_loc
    list

Source

val loc_field : 
  Mlwtree.field list ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field
    Mlwtree.with_loc
    list

Sourceval deloc : 'a Mlwtree.with_loc list -> 'a list

Source

val zip : 
  'a list ->
  'a list ->
  'a list ->
  'a list ->
  'a list ->
  'a list ->
  'a list ->
  'a list ->
  'a list

Sourceval cap : string Mlwtree.with_loc -> string Mlwtree.with_loc

Source

val mk_eq_type_fun : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_le_type_fun : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_map_clone : 
  string ->
  'a ->
  'a ->
  ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl

Source

val mk_map_type : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_set_clone : 
  string ->
  'a ->
  ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl

Source

val mk_set_type : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_list_clone : 
  string ->
  'a ->
  ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl

Source

val mk_list_type : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

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

Source

val mk_record : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.record ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Sourceval map_lidents : M.lident list -> Mlwtree.loc_ident list

Source

val type_to_init : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.loc_typ ->
  Mlwtree.loc_term

Sourceval is_local_invariant : 'a -> Ident.ident -> M.lident M.mterm_gen -> bool

Source

val 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.entry_description -> change

Source

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

Source

val mk_spec_invariant : 
  [< `Loop | `Storage ] ->
  M.security_item ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_app_field : 
  Mlwtree.ident ->
  Mlwtree.loc_ident ->
  Mlwtree.loc_term * Mlwtree.loc_term

Source

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

Source

val mk_storage_invariant : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident Location.loced ->
  M.lident ->
  Mlwtree.loc_term ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula

Source

val mk_pre_coll : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.ident ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term

Source

val mk_pre_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.ident ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term

Source

val mk_loop_invariant : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term

Source

val mk_axiom_invariant : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term

Source

val mk_axiom2_invariant : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term

Source

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

Source

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

Source

val mk_eq_key : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
    Mlwtree.abstract_decl

Source

val mk_le_key : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
    Mlwtree.abstract_decl

Source

val mk_eq_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  (Mlwtree.loc_term,
    (Mlwtree.loc_ident, 'a) Mlwtree.abstract_type Mlwtree.with_loc,
    string Mlwtree.with_loc)
    Mlwtree.abstract_decl

Source

val mk_enum : 
  'a ->
  M.enum ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val get_fail_idx : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.type_ ->
  int

Source

val mk_exn : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  int ->
  M.type_ ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.ident Mlwtree.with_loc)
    Mlwtree.abstract_decl

Source

val mk_field : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  ('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl

Source

val mk_view : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  ('a, Mlwtree.loc_typ, string Mlwtree.with_loc) Mlwtree.abstract_decl

Source

val mk_coll : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  ('a, Mlwtree.loc_typ, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_decl

Sourceval mk_set_field_id : string -> string

Source

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

Source

val mk_aggregates : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_partition_axioms : 
  M.model ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    list

Source

val 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

Sourceval mk_lbl_before : string option -> string

Sourceval mk_inv_lbl : string option -> string -> string

Source

val mk_storage_loop_inv : 
  string option ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula

Sourceval is_identical : Tools.String.t -> M.effect list -> bool

Source

val mk_vars_loop_invariants : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident option ->
  string option ->
  Mlwtree.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list

Sourcetype mode =

| Inv
| Logic
| Exec
| Def

Sourcetype logical_context = {

lctx : mode;
entry_id : Mlwtree.ident option;
locals : Mlwtree.ident list;
loop_id : Mlwtree.ident option;
fun_ : bool;
fails : bool;

}

Sourceval init_ctx : logical_context

Sourceval mk_sid : logical_context -> string

Sourceval add_local : Mlwtree.ident -> logical_context -> logical_context

Source

val mk_trace_seq : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (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

Source

val map_mpattern : 
  M.lident M.pattern_node ->
  Mlwtree.loc_ident Mlwtree.pattern_node

Source

val is_coll_field : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  bool

Sourceval is_exec_divergent : ('a, 'b) M.mterm_node -> bool

Sourceval get_tuple_size : M.ntype -> int

Source

val cp_storage : 
  string ->
  (('a, 'b, string) Mlwtree.abstract_term, 'c, 'd) Mlwtree.abstract_term

Source

val get_assign_value : 
  M.type_ ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term ->
  M.assignment_operator ->
  Mlwtree.loc_term

Source

val is_partition : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident ->
  bool

Source

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

Source

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

Source

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,
    'a)
    Mlwtree.abstract_term

Source

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,
    'a)
    Mlwtree.abstract_term

Source

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

Source

val mk_match : 
  logical_context ->
  Mlwtree.loc_term ->
  'a ->
  Mlwtree.loc_term ->
  Mlwtree.term Mlwtree.exn ->
  (Mlwtree.loc_term, 'b, 'a Mlwtree.with_loc) Mlwtree.abstract_term

Sourceval mk_storage_id : logical_context -> string

Source

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

Source

val mk_loc_coll_term : 
  string ->
  logical_context ->
  (M.temp * M.delta) ->
  Mlwtree.loc_term

Sourceval mk_lc_term : string -> logical_context -> Mlwtree.loc_term

Sourceval mk_temp_delta : 'a M.container_kind_gen -> M.temp * M.delta

Source

val assign_operation : 
  Mlwtree.loc_term ->
  Mlwtree.loc_term ->
  Mlwtree.loc_term ->
  (Mlwtree.loc_term, 'a, 'b) Mlwtree.abstract_term

Source

val map_mterm : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.mterm ->
  Mlwtree.loc_term

Source

val mk_invariants : 
  M.model ->
  logical_context ->
  Ident.ident Location.loced option ->
  Mlwtree.ident option ->
  M.lident M.mterm_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_filter_args : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  (Mlwtree.ident * M.type_) list ->
  M.lident M.mterm_gen ->
  Mlwtree.loc_term list

Source

val mk_asset_key_value : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  Ident.ident ->
  M.lident M.mterm_gen ->
  Mlwtree.loc_term

Source

val mk_container_term : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  logical_context ->
  M.lident M.mterm_gen M.container_kind_gen ->
  Mlwtree.loc_term

Source

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

Source

val mk_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val map_init_mterm : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.mterm ->
  Mlwtree.loc_term

Source

val mk_storage_items : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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

Source

val mk_asset_invariants : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_contract_invariants : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_variable_invariants : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_security_invariants : 
  M.model ->
  'a ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_state_invariants : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  ((Mlwtree.loc_term, 'a, 'b) Mlwtree.abstract_term Mlwtree.with_loc,
    Mlwtree.loc_ident)
    Mlwtree.abstract_formula
    list

Source

val mk_storage : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.storage ->
  ((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_decl

Source

val mk_cp_storage : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.storage ->
  (Mlwtree.loc_term,
    ('a, 'b) Mlwtree.abstract_type Mlwtree.with_loc,
    string Mlwtree.with_loc)
    Mlwtree.abstract_decl

Source

val mk_axioms : 
  M.model ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    list

Source

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

Source

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

Source

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

Source

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

Source

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

Source

val parameter_to_val : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.parameter ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Source

val mk_storage_api_before_storage : 
  M.model ->
  'a ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    list

Source

val mk_storage_api : 
  M.model ->
  'a ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    list

Source

val fold_fails : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.lident M.mterm_gen ->
  Mlwtree.struct_fail list

Source

val fold_exns : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.lident M.mterm_gen ->
  Mlwtree.term list

Sourceval is_fail : M.mterm -> bool

Source

val flatten_if_fail : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.mterm ->
  Mlwtree.loc_term

Source

val mk_ensures : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list ->
  M.specification ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

val mk_delta_requires : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list

Source

val mk_preconds : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.argument list ->
  M.lident M.mterm_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula list

Source

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

Source

val mk_functions : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    list

Source

val mk_entries : 
  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

Source

val process_no_fail : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

Sourcetype desc_container =

| Dset of M.type_
| Dlist of M.type_
| Dmap of M.type_
| Dasset of M.asset
| Denum of M.enum
| Drecord of M.record

Sourceval show_desc_container : desc_container -> Ppx_deriving_runtime.string

Sourceval pp_desc_container : Format.formatter -> desc_container -> unit

Sourceval cmp_desc_container : desc_container -> desc_container -> bool

Source

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

Sourceval to_whyml : M.model -> Mlwtree.mlw_tree

package archetype

Module Archetype.Gen_why3Source

Module `Archetype.Gen_why3`Source