pgm_types.mli 1.99 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 28
(* 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 *)

(* program types *)
29 30 31 32 33 34 35 36 37 38 39 40

type effect = Pgm_effect.t
type reference = Pgm_effect.reference

type pre = Term.fmla

type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla

type post = post_fmla * (Term.lsymbol * exn_post_fmla) list

type type_v = private
41 42
  | Tpure    of Ty.ty
  | Tarrow   of binder list * type_c
43 44 45 46 47 48 49 50 51 52 53 54

and type_c =
  { c_result_type : type_v;
    c_effect      : effect;
    c_pre         : pre;
    c_post        : post; }

and binder = Term.vsymbol * type_v

val tpure : Ty.ty -> type_v
val tarrow : binder list -> type_c -> type_v

55
(* program symbols *)
56 57 58 59 60 61

type psymbol = private {
  p_ls : lsymbol;
  p_tv : type_v;
}

62
val create_psymbol : preid -> type_v -> psymbol
63

64
(* exception symbols *)
65

66
type esymbol = lsymbol
67

68 69 70 71
(* program types -> logic types *)

val ts_arrow : tysymbol

72 73
val purify : ?logic:bool -> type_v -> ty
  (** when [logic] is [true], mutable types are turned into their models *)
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96

(* operations on program types *)

val apply_type_v     : type_v -> vsymbol   -> type_c
val apply_type_v_ref : type_v -> reference -> type_c

val occur_type_v : reference -> 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

(* pretty-printers *)

val print_type_v : Format.formatter -> type_v -> unit
val print_type_c : Format.formatter -> type_c -> unit
val print_post   : Format.formatter -> post   -> unit