dexpr.mli 5.02 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10 11 12 13 14 15 16
(********************************************************************)

open Stdlib
open Ident
open Term
open Ity
open Expr
17
open Pmodule
18 19 20 21 22 23 24 25 26

(** Program types *)

type dity

val dity_fresh : unit -> dity

val dity_of_ity : ity -> dity

27
val dity_int  : dity
28
val dity_real : dity
29 30
val dity_bool : dity
val dity_unit : dity
31

32 33 34 35 36
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)

(** Patterns *)

type dpattern = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
37
  dp_pat  : pre_pattern;
38 39 40 41 42 43 44
  dp_dity : dity;
  dp_vars : dity Mstr.t;
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
45
  | DPvar  of preid * bool
46
  | DPapp  of rsymbol * dpattern list
47
  | DPas   of dpattern * preid * bool
48 49 50 51 52 53 54
  | DPor   of dpattern * dpattern
  | DPcast of dpattern * ity

(** Binders *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
55
type dbinder = preid option * ghost * dity
56 57 58

(** Specifications *)

59 60 61 62
exception UnboundLabel of string

type register_old = pvsymbol -> string -> pvsymbol
  (** Program variables occurring under [old] or [at] are passed to
63
      a registrar function. The label string must be ["0"] for [old]. *)
64

65
type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a
66 67 68
  (** Specification terms are parsed and typechecked after the program
      expressions, when the types of locally bound program variables are
      already established. *)
69 70 71

type dspec_final = {
  ds_pre     : term list;
72
  ds_post    : (pvsymbol * term) list;
73
  ds_xpost   : (pvsymbol * term) list Mxs.t;
74
  ds_reads   : pvsymbol list;
75 76
  ds_writes  : term list;
  ds_diverge : bool;
77
  ds_checkrw : bool;
78 79
}

80
type dspec = ity -> dspec_final
81 82 83 84 85 86 87 88 89
  (* Computation specification is also parametrized by the result type.
     All vsymbols in the postcondition clauses in the [ds_post] field
     must have this type. All vsymbols in the exceptional postcondition
     clauses must have the type of the corresponding exception. *)

(** Expressions *)

type dinvariant = term list

90 91 92 93
type dxsymbol =
  | DElexn of string * dity
  | DEgexn of xsymbol

94 95 96 97 98 99 100 101
type dexpr = private {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
102
  | DEsym of prog_symbol
103
  | DEls of lsymbol
104
  | DEconst of Number.constant * dity
105
  | DEapp of dexpr * dexpr
106 107
  | DEfun of dbinder list * mask * dspec later * dexpr
  | DEany of dbinder list * mask * dspec later * dity
108 109
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
110
  | DEnot of dexpr
111 112
  | DEand of dexpr * dexpr
  | DEor of dexpr * dexpr
113 114
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) list
115
  | DEassign of (dexpr * rsymbol * dexpr) list
116
  | DEwhile of dexpr * dinvariant later * variant list later * dexpr
117
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
118 119
  | DEtry of dexpr * (dxsymbol * dpattern * dexpr) list
  | DEraise of dxsymbol * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
120
  | DEghost of dexpr
121
  | DEexn of preid * dity * mask * dexpr
122
  | DEassert of assertion_kind * term later
123
  | DEpure of term later * dity
Andrei Paskevich's avatar
Andrei Paskevich committed
124 125 126
  | DEabsurd
  | DEtrue
  | DEfalse
127 128 129 130 131
  | DEmark of preid * dexpr
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

132
and dlet_defn = preid * ghost * rs_kind * dexpr
133 134 135

and drec_defn = private { fds : dfun_defn list }

136
and dfun_defn = preid * ghost * rs_kind *
137
  dbinder list * mask * dspec later * variant list later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
138

139 140 141 142 143 144 145 146 147 148 149 150 151 152
(** Environment *)

type denv

val denv_empty : denv

val denv_add_var : denv -> preid -> dity -> denv

val denv_add_let : denv -> dlet_defn -> denv

val denv_add_args : denv -> dbinder list -> denv

val denv_add_pat : denv -> dpattern -> denv

153 154
val denv_add_exn : denv -> preid -> dity -> denv

155 156 157 158
val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *)

val denv_get_opt : denv -> string -> dexpr_node option

159 160 161 162
val denv_get_exn : denv -> string -> dxsymbol (** raises Not_found *)

val denv_get_exn_opt : denv -> string -> dxsymbol option

163 164
val denv_contents : denv -> (Ty.Stv.t option * dvty) Mstr.t

165 166
val denv_pure : denv -> (Dterm.denv -> Dterm.dty) -> dity

167 168 169 170 171 172
(** Constructors *)

val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern

val dexpr : ?loc:Loc.position -> dexpr_node -> dexpr

173
type pre_fun_defn = preid * ghost * rs_kind * dbinder list *
174
  dity * mask * (denv -> dspec later * variant list later * dexpr)
175 176 177 178 179

val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn

(** Final stage *)

180
val expr : ?keep_loc:bool -> dexpr -> expr
181

182
val let_defn : ?keep_loc:bool -> dlet_defn -> let_defn
183
val rec_defn : ?keep_loc:bool -> drec_defn -> let_defn