archetype 1.2.1 · OCaml Package

module M = Model

type error_desc =

| NotSupported of string
| 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 gArchetypeAgg : 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_module_name : string -> 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 mk_ac_unmvd_id : string -> string

val mk_aggregate_id : string -> string

val gs : string

val gsinit : string

val gsarg : string

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

val mk_ac_old_st : 
  'a ->
  string ->
  ((('b, 'c, 'a) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    'f)
    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, 'a) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    'f)
    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, 'a) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    'f)
    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_field_id : string -> string

val mk_view_id : string -> string

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 : 
  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_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

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 =

| 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

type trace_id_type =

| Asset
| Entry
| 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_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

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_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

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

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

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

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 ->
  string ->
  M.type_ ->
  Ident.ident Location.loced 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 : 
  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

type filter =

| Select
| Removeif

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 acc_has_id : 'a -> ('b * 'a * 'c) list -> bool

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

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

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_removeif_name : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Ident.ident Location.loced Archetype__Model.mterm_gen ->
  string

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

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

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

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

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

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

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

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

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

val wdl : 'a list -> 'a 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 -> '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_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

val mk_le_type_fun : 
  'a ->
  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 ->
  'a ->
  ('b, 'a, string Mlwtree.with_loc) Mlwtree.abstract_decl

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

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

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

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

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

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 mk_record : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  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 : 
  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_app_field : 
  Mlwtree.ident ->
  Mlwtree.loc_ident ->
  Mlwtree.loc_term * Mlwtree.loc_term

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_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

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_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 : 
  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_key : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, string Mlwtree.with_loc)
    Mlwtree.abstract_decl

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

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

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

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

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

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 mk_coll : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  ('a, Mlwtree.loc_typ, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_decl

val mk_set_field_id : string -> string

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

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, 'a) Mlwtree.abstract_decl list ->
  ('b, 'c, 'a) Mlwtree.abstract_decl

val get_record_name : ('a, 'b, 'c) Mlwtree.abstract_decl -> 'c

val mk_lbl_before : string option -> string

val mk_inv_lbl : string option -> string -> string

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

type mode =

| Inv
| Logic
| Exec
| Def

type logical_context = {

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

}

val init_ctx : logical_context

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

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

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

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 cp_storage : 
  string ->
  (('a, 'b, string) Mlwtree.abstract_term, 'c, 'd) Mlwtree.abstract_term

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

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

val mk_get_force : 
  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 : 
  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 : 
  '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

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

val mk_match_get_none : 
  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 : 
  Mlwtree.loc_term ->
  'a ->
  Mlwtree.loc_term ->
  Mlwtree.term Mlwtree.exn ->
  (Mlwtree.loc_term, 'b, 'a 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 : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.mterm ->
  Mlwtree.loc_term

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

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

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

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

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 mk_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.asset ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

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

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

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_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

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

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

val mk_axioms : 
  M.model ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    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_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 : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.lident M.mterm_gen ->
  (Mlwtree.loc_ident option * Mlwtree.loc_term) list

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

val mk_theory : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  ((((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 : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  logical_context ->
  M.mterm ->
  Mlwtree.loc_term

val mk_ensures : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (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 : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.loc_term, string Mlwtree.with_loc) Mlwtree.abstract_formula list

val mk_preconds : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (Mlwtree.ident Location.loced * M.type_ * 'a) list ->
  M.lident M.mterm_gen ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) 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 mk_entries : 
  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 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

val to_whyml : M.model -> Mlwtree.mlw_tree

package archetype