pgm_types.mli 1.68 KB
Newer Older
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

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

(* types *)

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
  | Tpure of Ty.ty
  | Tarrow of binder list * type_c

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

(* symbols *)

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

44
val create_psymbol : preid -> type_v -> psymbol
45 46 47

type esymbol = lsymbol

48 49 50 51 52 53 54 55 56 57
type mtsymbol = private {
  mt_name  : ident;
  mt_args  : tvsymbol list;
  mt_model : ty option;
}

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

val mt_equal : mtsymbol -> mtsymbol -> bool

58 59 60 61
(* program types -> logic types *)

val ts_arrow : tysymbol

62
val purify : type_v -> ty
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

(* 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