pdecl.mli 2.31 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

open Ident
open Ty
open Term
open Ity
open Expr

(** {2 Type declarations} *)

type its_defn = private {
  itd_its          : itysymbol;
  itd_fields       : rsymbol list;
  itd_constructors : rsymbol list;
  itd_invariant    : term list;
}

val create_abstract_type_decl : preid -> tvsymbol list -> bool -> its_defn

val create_alias_decl : preid -> tvsymbol list -> ity -> its_defn

val create_flat_record_decl : preid -> tvsymbol list ->
  bool -> bool -> (bool * pvsymbol) list -> term list -> its_defn

val create_rec_record_decl : itysymbol -> pvsymbol list -> its_defn

val create_flat_variant_decl : preid -> tvsymbol list ->
  (preid * (bool * pvsymbol) list) list -> its_defn

val create_rec_variant_decl : itysymbol ->
  (preid * (bool * pvsymbol) list) list -> its_defn

(** {2 Module declarations} *)

44 45 46 47 48 49
type pdecl = private {
  pd_node : pdecl_node;
  pd_pure : Decl.decl list;
  pd_syms : Sid.t;
  pd_news : Sid.t;
  pd_tag  : int;
Andrei Paskevich's avatar
Andrei Paskevich committed
50 51
}

52 53 54 55 56
and pdecl_node = private
  | PDtype of its_defn list
  | PDlet  of let_defn
  | PDexn  of xsymbol
  | PDpure
57

58
val create_type_decl : its_defn list -> pdecl
59

60
val create_let_decl : let_defn -> pdecl
61

62
val create_exn_decl : xsymbol -> pdecl
63

64
val create_pure_decl : Decl.decl -> pdecl
65 66 67

(** {2 Built-in decls} *)

68 69 70 71 72 73 74 75 76
val pd_int : pdecl
val pd_real : pdecl
val pd_equ : pdecl
val pd_bool : pdecl
val pd_unit : pdecl
val pd_tuple : int -> pdecl
val pd_func : pdecl
val pd_pred : pdecl
val pd_func_app : pdecl
77 78 79

(** {2 Known identifiers} *)

80
type known_map = pdecl Mid.t
81 82

val known_id : known_map -> ident -> unit
83
val known_add_decl : known_map -> pdecl -> known_map
84
val merge_known : known_map -> known_map -> known_map