pgm_ttree.ml 4.84 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20 21
open Why

22 23 24 25 26 27
type loc = Loc.position

type constant = Term.constant

type assertion_kind = Pgm_ptree.assertion_kind

28
type lazy_op = Pgm_ptree.lazy_op
29

30
(* phase 1: destructive typing *)
31

32 33 34 35 36 37 38 39 40
type dreference = 
  | DRlocal  of string
  | DRglobal of Term.lsymbol

type deffect = {
  de_reads  : dreference list;
  de_writes : dreference list;
  de_raises : Term.lsymbol list;
}
41

42 43
type dlexpr = Typing.denv * Ptree.lexpr

44 45 46 47
type dpre = dlexpr

type dpost = dlexpr * (Term.lsymbol * dlexpr) list

48 49
type dtype_v = 
  | DTpure of Denv.dty
50
  | DTarrow of dbinder list * dtype_c
51 52

and dtype_c = 
53
  { dc_result_name : string;
54 55
    dc_result_type : dtype_v;
    dc_effect      : deffect;
56 57
    dc_pre         : dpre;
    dc_post        : dpost; }
58

59
and dbinder = string * dtype_v
60

61 62 63 64 65 66
type dloop_annotation = {
  dloop_invariant : Ptree.lexpr option;
  dloop_variant   : Ptree.lexpr option;
}

type dvariant = Ptree.lexpr 
67

68 69
type dexpr = {
  dexpr_desc : dexpr_desc;
70
  dexpr_denv : Typing.denv;
71 72 73 74 75 76 77 78 79
  dexpr_type : Denv.dty;
  dexpr_loc  : loc;
}

and dexpr_desc =
  | DEconstant of constant
  | DElocal of string
  | DEglobal of Term.lsymbol
  | DEapply of dexpr * dexpr
80
  | DEfun of dbinder list * dtriple
81
  | DElet of string * dexpr * dexpr
82 83 84
  | DEletrec of 
      ((string * Denv.dty) * dbinder list * dvariant option * dtriple) list * 
      dexpr
85 86 87

  | DEsequence of dexpr * dexpr
  | DEif of dexpr * dexpr * dexpr
88
  | DEwhile of dexpr *  dloop_annotation * dexpr
89
  | DElazy of lazy_op * dexpr * dexpr
90
  | DEmatch of dexpr list * (Typing.dpattern list * dexpr) list
91 92
  | DEskip
  | DEabsurd 
93
  | DEraise of Term.lsymbol * dexpr option
94
  | DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
95 96 97 98

  | DEassert of assertion_kind * Ptree.lexpr
  | DEghost of dexpr
  | DElabel of string * dexpr
99
  | DEany of dtype_c
100

101
and dtriple = dpre * dexpr * dpost
102

103 104
(* phase 2: typing annotations *)

105 106
type variant = Term.term

107 108 109 110 111 112 113 114 115
type reference = 
  | Rlocal  of Term.vsymbol
  | Rglobal of Term.lsymbol

type effect = {
  e_reads  : reference list;
  e_writes : reference list;
  e_raises : Term.lsymbol list;
}
116

117 118 119 120
type pre = Term.fmla

type post = Term.fmla * (Term.lsymbol * Term.fmla) list

121 122
type type_v = 
  | Tpure of Ty.ty
123
  | Tarrow of binder list * type_c
124 125

and type_c = 
126 127 128
  { c_result_name : Term.vsymbol;
    c_result_type : type_v;
    c_effect      : effect;
129 130
    c_pre         : pre;
    c_post        : post; }
131

132
and binder = Term.vsymbol * type_v
133

134 135
type loop_annotation = {
  loop_invariant : Term.fmla option;
136
  loop_variant   : variant option;
137
}
138

139 140
type expr = {
  expr_desc : expr_desc;
141
  expr_type : Ty.ty;
142 143 144 145 146
  expr_loc  : loc;
}

and expr_desc =
  | Econstant of constant
147
  | Elocal of Term.vsymbol
148 149
  | Eglobal of Term.lsymbol
  | Eapply of expr * expr
150
  | Efun of binder list * triple
151
  | Elet of Term.vsymbol * expr * expr
152
  | Eletrec of recfun list * expr
153

154 155
  | Esequence of expr * expr
  | Eif of expr * expr * expr
156
  | Ewhile of expr * loop_annotation * expr
157
  | Elazy of lazy_op * expr * expr
158
  | Ematch of expr list * (Term.pattern list * expr) list
159
  | Eskip 
160
  | Eabsurd
161
  | Eraise of Term.lsymbol * expr option
162
  | Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
163 164

  | Eassert of assertion_kind * Term.fmla
165
  | Eghost of expr
166
  | Elabel of string * expr
167
  | Eany of type_c
168

169 170
and recfun = Term.vsymbol * binder list * variant option * triple

171
and triple = pre * expr * post
172 173

type decl =
174
  | Dlet    of Term.lsymbol * expr
175
  | Dletrec of (Term.lsymbol * recfun) list
176
  | Dparam  of Term.lsymbol * type_v
177

178 179 180 181 182
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)