archetype 0.1.3 · OCaml Package

module M = Model

val gArchetypeDir : string

val gArchetypeLib : string

val gArchetypeColl : string

val gArchetypeSum : string

val gArchetypeList : 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 mk_use : 
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl

val mk_use_list : 
  (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

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

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

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 Mlwtree.abstract_type,
    string)
    Mlwtree.abstract_decl

val mk_collection_field : 
  Mlwtree.ident ->
  (Mlwtree.ident -> 'a) ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, 'b 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 Mlwtree.abstract_type,
    string)
    Mlwtree.abstract_field
    list

val mk_sum_clone_id : string -> string -> string

val mk_sum_clone : 
  'a ->
  string ->
  string ->
  string ->
  ('b, 'c, string) 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 mk_select_test : 
  ((('a, 'b, string) Mlwtree.abstract_term, 'c, string) Mlwtree.abstract_term as 'a,
    'b,
    string)
    Mlwtree.abstract_term ->
  ((('a, 'b, string) Mlwtree.abstract_term, 'd, string) Mlwtree.abstract_term,
    'e,
    string)
    Mlwtree.abstract_term

val mk_select_body : 
  Mlwtree.ident ->
  ((('a, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_term,
     Mlwtree.typ,
     Mlwtree.ident)
     Mlwtree.abstract_term as 'a,
    Mlwtree.typ,
    Mlwtree.ident)
    Mlwtree.abstract_term ->
  Mlwtree.term

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

val get_select_id : M.model -> Ident.ident -> M.mterm -> int

val mk_select_name : M.model -> Ident.ident -> M.mterm -> string

val mk_select : 
  M.model ->
  Ident.ident ->
  M.mterm ->
  ((('a, Mlwtree.typ, Ident.ident) Mlwtree.abstract_term,
     Mlwtree.typ,
     Ident.ident)
     Mlwtree.abstract_term as 'a,
    Mlwtree.typ,
    Ident.ident)
    Mlwtree.abstract_term ->
  bool ->
  (((((('a, Mlwtree.typ, Ident.ident) Mlwtree.abstract_term,
        Mlwtree.typ,
        Ident.ident)
        Mlwtree.abstract_term,
       Mlwtree.typ,
       Ident.ident)
       Mlwtree.abstract_term,
      Mlwtree.typ,
      Ident.ident)
      Mlwtree.abstract_term,
     Ident.ident Mlwtree.abstract_type,
     Ident.ident)
     Mlwtree.abstract_term,
    Ident.ident Mlwtree.abstract_type,
    string)
    Mlwtree.abstract_decl

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

val zip : 'a list -> 'b list -> 'c list -> 'd list -> 'e list

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

val map_lident : M.lident -> Mlwtree.loc_ident

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

val type_to_init : Mlwtree.loc_typ -> Mlwtree.loc_term

val map_btype : M.btyp -> 'a Mlwtree.abstract_type

val map_mtype : M.type_ -> Mlwtree.loc_typ

val map_term : M.mterm -> Mlwtree.loc_term

val map_record_term : 'a -> M.mterm -> Mlwtree.loc_term

val map_record_values : 
  M.record_item list ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_field
    list

val map_storage_items : 
  M.storage_item list ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Ident.ident Mlwtree.with_loc)
    Mlwtree.abstract_field
    list

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.action_description -> change

val map_security_pred : 
  [< `Loop | `Storage ] ->
  M.security_predicate ->
  ((('a, 'b Mlwtree.abstract_type, Ident.ident) Mlwtree.abstract_term as 'a,
     'b Mlwtree.abstract_type,
     Ident.ident)
     Mlwtree.abstract_term,
    'c,
    'd)
    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 ->
  [> `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.label_term ->
  (Mlwtree.loc_term, Mlwtree.loc_ident) Mlwtree.abstract_formula

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_eq_asset : 
  'a ->
  M.record ->
  (Mlwtree.loc_term,
    Mlwtree.loc_ident Mlwtree.abstract_type Mlwtree.with_loc,
    string Mlwtree.with_loc)
    Mlwtree.abstract_decl

val mk_eq_extensionality : 'a -> M.record -> Mlwtree.loc_decl

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

val record_to_clone : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.info_asset ->
  ('a, 'b, Ident.ident Mlwtree.with_loc) Mlwtree.abstract_decl

val map_storage : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  M.storage ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Ident.ident 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_partition_axioms : 
  M.model ->
  (Mlwtree.loc_term, Mlwtree.loc_typ, Mlwtree.loc_ident) Mlwtree.abstract_decl
    list

val get_record : 
  'a ->
  ('b, 'c, 'd) Mlwtree.abstract_decl list ->
  ('e, 'f, 'g) Mlwtree.abstract_decl

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

val mk_var : Mlwtree.ident -> ('a, 'b, Mlwtree.ident) Mlwtree.abstract_term

val get_for_fun : 
  M.type_ ->
  ((Mlwtree.term * Mlwtree.term) ->
  Mlwtree.loc_term)
  * (Mlwtree.term ->
  Mlwtree.loc_term)

type logical_mod =

| Nomod
| Added
| Removed

type logical_context = {

old : bool;
lmod : logical_mod;

}

val init_ctx : 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_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 option ->
  M.lident M.mterm_gen ->
  (Mlwtree.loc_term, Ident.ident Mlwtree.with_loc) 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_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

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_set_sum_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,
       string)
       Mlwtree.abstract_term,
      'e Mlwtree.abstract_type,
      'f)
      Mlwtree.abstract_term,
     'g Mlwtree.abstract_type,
     'h)
     Mlwtree.abstract_term,
    string)
    Mlwtree.abstract_formula
    list

val mk_set_ensures : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.field list ->
  (((((('a, 'b, string) Mlwtree.abstract_term, 'c, Mlwtree.ident)
        Mlwtree.abstract_term,
       'd Mlwtree.abstract_type,
       Mlwtree.ident)
       Mlwtree.abstract_term,
      'e Mlwtree.abstract_type,
      'f)
      Mlwtree.abstract_term,
     'g Mlwtree.abstract_type,
     'h)
     Mlwtree.abstract_term,
    string)
    Mlwtree.abstract_formula
    list

val mk_set_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.ident ->
  (Mlwtree.term, Mlwtree.typ, Mlwtree.ident) Mlwtree.abstract_decl ->
  ((((((('a, 'b, string) Mlwtree.abstract_term, 'c, string)
         Mlwtree.abstract_term,
        'd,
        Mlwtree.ident)
        Mlwtree.abstract_term,
       'e Mlwtree.abstract_type,
       Mlwtree.ident)
       Mlwtree.abstract_term,
      'f Mlwtree.abstract_type,
      'g)
      Mlwtree.abstract_term,
     'h Mlwtree.abstract_type,
     'i)
     Mlwtree.abstract_term,
    Mlwtree.ident Mlwtree.abstract_type,
    string)
    Mlwtree.abstract_decl

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

val mk_api_precond : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  [> `Loop
  | `Preasset of Mlwtree.ident
  | `Precoll of Mlwtree.ident
  | `Prelist of Mlwtree.ident
  | `Storage ] ->
  (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list

val mk_add_asset_precond : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.ident ->
  (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list

val mk_listtocoll_precond : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  Mlwtree.ident ->
  (Mlwtree.term, Ident.ident) Mlwtree.abstract_formula list

val mk_listtocoll : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  (Mlwtree.term, Ident.ident Mlwtree.abstract_type, Ident.ident)
    Mlwtree.abstract_decl

val gen_field_getter : 
  'a ->
  'b ->
  (('c, 'd, 'e) Mlwtree.abstract_term, 'f Mlwtree.abstract_type, 'g)
    Mlwtree.abstract_decl

val gen_field_getters : 
  ('a, 'b, 'c) Mlwtree.abstract_decl ->
  (('d, 'e, 'f) Mlwtree.abstract_term, 'g Mlwtree.abstract_type, 'h)
    Mlwtree.abstract_decl
    list

val mk_add_sum_ensures : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Ident.ident ->
  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,
     'h Mlwtree.abstract_type,
     'i)
     Mlwtree.abstract_term,
    string)
    Mlwtree.abstract_formula
    list

val mk_add_ensures : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  string ->
  Ident.ident ->
  Ident.ident ->
  ((((((('a, 'b, string) Mlwtree.abstract_term, 'c, string)
         Mlwtree.abstract_term,
        'd,
        Ident.ident)
        Mlwtree.abstract_term,
       'e,
       Ident.ident)
       Mlwtree.abstract_term,
      'f Mlwtree.abstract_type,
      Ident.ident)
      Mlwtree.abstract_term,
     Ident.ident Mlwtree.abstract_type,
     Ident.ident)
     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 ->
  Ident.ident ->
  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,
     'h Mlwtree.abstract_type,
     'i)
     Mlwtree.abstract_term,
    string)
    Mlwtree.abstract_formula
    list

val mk_rm_ensures : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  string ->
  Ident.ident ->
  Ident.ident ->
  ((((((('a, 'b, string) Mlwtree.abstract_term, 'c, string)
         Mlwtree.abstract_term,
        'd,
        Ident.ident)
        Mlwtree.abstract_term,
       'e,
       Ident.ident)
       Mlwtree.abstract_term,
      'f Mlwtree.abstract_type,
      Ident.ident)
      Mlwtree.abstract_term,
     Ident.ident Mlwtree.abstract_type,
     'g)
     Mlwtree.abstract_term,
    string)
    Mlwtree.abstract_formula
    list

val mk_rm_asset : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.decl

val mk_add_partition_field : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.decl

val mk_rm_partition_field : 
  Ident.ident Location.loced Archetype__Model.model_gen ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.ident ->
  Mlwtree.decl

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

val fold_exns : 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_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_require : 
  string ->
  int ->
  'a ->
  ('b, 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_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 is_src : M.source -> ('a * 'b M.function_struct_gen * 'c) -> bool

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 add_raise_ctx : 
  (Ident.ident Mlwtree.with_loc
   * Ident.ident Mlwtree.with_loc Mlwtree.abstract_type Mlwtree.with_loc)
    list ->
  M.source ->
  Ident.ident Location.loced Archetype__Model.model_gen ->
  (((((((('a, Ident.ident Mlwtree.abstract_type, Ident.ident)
           Mlwtree.abstract_term as 'a,
          Ident.ident Mlwtree.abstract_type,
          Ident.ident)
          Mlwtree.abstract_term,
         Ident.ident Mlwtree.abstract_type,
         Ident.ident)
         Mlwtree.abstract_term,
        Ident.ident Mlwtree.abstract_type,
        Ident.ident)
        Mlwtree.abstract_term,
       Ident.ident Mlwtree.abstract_type,
       Ident.ident)
       Mlwtree.abstract_term,
      Ident.ident Mlwtree.abstract_type,
      Ident.ident)
      Mlwtree.abstract_term,
     Ident.ident Mlwtree.abstract_type,
     Ident.ident)
     Mlwtree.abstract_term,
    Ident.ident Mlwtree.abstract_type,
    Ident.ident)
    Mlwtree.abstract_term ->
  (((((((('a, Ident.ident Mlwtree.abstract_type, Ident.ident)
           Mlwtree.abstract_term,
          Ident.ident Mlwtree.abstract_type,
          Ident.ident)
          Mlwtree.abstract_term,
         Ident.ident Mlwtree.abstract_type,
         Ident.ident)
         Mlwtree.abstract_term,
        Ident.ident Mlwtree.abstract_type,
        Ident.ident)
        Mlwtree.abstract_term,
       Ident.ident Mlwtree.abstract_type,
       Ident.ident)
       Mlwtree.abstract_term,
      Ident.ident Mlwtree.abstract_type,
      Ident.ident)
      Mlwtree.abstract_term,
     Ident.ident Mlwtree.abstract_type,
     Ident.ident)
     Mlwtree.abstract_term,
    Ident.ident Mlwtree.abstract_type,
    Ident.ident)
    Mlwtree.abstract_term

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

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

val mk_exo_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