Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

pgm_types.mli 3.66 KB
Newer Older
1 2 3 4 5 6 7 8 9

open Why
open Util
open Ident
open Ty
open Theory
open Term
open Decl

10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
(* mutable type symbols *)

type mtsymbol = private {
  mt_name  : ident;
  mt_args  : tvsymbol list;
  mt_model : ty option;
  mt_abstr : tysymbol;
}

val create_mtsymbol : preid -> tvsymbol list -> ty option -> mtsymbol

val mt_equal : mtsymbol -> mtsymbol -> bool

exception NotMutable

val get_mtsymbol : tysymbol -> mtsymbol
  (** raises [NotMutable] if [ts] is not a mutable type *)

28 29
val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty       -> bool
30

31
val ts_arrow : tysymbol
32
val make_arrow_type : ty list -> ty -> ty
33

34 35 36
val ts_exn : tysymbol
val ty_exn : ty

37 38
(* val ts_label : tysymbol *)

39
(* program types *)
40
module rec T : sig
41

42
  type pre = Term.fmla
43

44 45 46 47
  type post_fmla = Term.vsymbol (* result *) * Term.fmla
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
      
  type esymbol = lsymbol
48

49 50 51 52 53
  type post = post_fmla * (esymbol * exn_post_fmla) list
      
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
54

55 56 57 58 59 60
  and type_c = { 
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
    c_post        : post; 
  }
61

62 63 64 65 66 67
  and pvsymbol = private {
    pv_name : ident;
    pv_tv   : type_v;
    pv_ty   : ty;      (* as a logic type, for typing purposes only *)
    pv_vs   : vsymbol; (* for use in the logic *)
  }
68

69 70
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
71

72
  val create_pvsymbol : preid -> ?vs:vsymbol -> type_v -> pvsymbol
73

74
  (* program symbols *)
75

76 77 78 79 80 81 82 83
  type psymbol = private {
    p_name : ident;
    p_tv   : type_v;
    p_ty   : ty;      (* as a logic type, for typing purposes only *)
    p_ls   : lsymbol; (* for use in the logic *) 
  }
      
  val create_psymbol : preid -> type_v -> psymbol
84

85
  val p_equal : psymbol -> psymbol -> bool
86

87
  (* program types -> logic types *)
88

89 90 91 92 93 94 95 96
  val purify : ty -> ty
  val purify_type_v : ?logic:bool -> type_v -> ty
    (** when [logic] is [true], mutable types are turned into their models *)
    
  (* operations on program types *)
    
  val apply_type_v_var : type_v -> pvsymbol -> type_c
  val apply_type_v_sym : type_v -> psymbol  -> type_c
97
  val apply_type_v_ref : type_v -> R.t      -> type_c
98 99 100 101 102 103 104 105 106 107 108
    
  val occur_type_v : R.t -> type_v -> bool
    
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
    
  val post_map : (fmla -> fmla) -> post -> post
    
  val subst1 : vsymbol -> term -> term Mvs.t
    
  val eq_type_v : type_v -> type_v -> bool
109

110
  (* pretty-printers *)
111

112 113
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
114
  val print_pre    : Format.formatter -> pre    -> unit
115
  val print_post   : Format.formatter -> post   -> unit
116

117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
end 

and Mpv :  sig include Map.S with type key = T.pvsymbol end

(* references *)
and R : sig

  type t = 
    | Rlocal  of T.pvsymbol
    | Rglobal of T.psymbol

  val type_of : t -> ty

  val name_of : t -> ident

end 
and Sref : sig include Set.S with type elt = R.t end
and Mref : sig include Map.S with type key = R.t end
and Sexn : sig include Set.S with type elt = T.esymbol end

(* effects *)
and E : sig
139

140 141 142 143 144
  type t = private {
    reads  : Sref.t;
    writes : Sref.t;
    raises : Sexn.t;
  }
145

146
  val empty : t
147

148 149 150
  val add_read  : R.t -> t -> t
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
151

152 153
  val remove_reference : R.t -> t -> t    
  val filter : (R.t -> bool) -> t -> t
154

155
  val remove_raise : T.esymbol -> t -> t
156

157
  val union : t -> t -> t
158

159 160 161 162 163
  val equal : t -> t -> bool
    
  val no_side_effect : t -> bool
    
  val subst : R.t Mpv.t -> t -> t
164

165
  val occur : R.t -> t -> bool
166

167 168
  val print : Format.formatter -> t -> unit

169
end 
170 171