dexpr.mli 4.73 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
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
open Ident
open Ty
open Term
open Ity
open Expr

(** Program types *)

type dity

val dity_fresh : unit -> dity

val dity_of_ity : ity -> dity

type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)

val dity_is_bool : dity -> bool

val dvty_is_chainable : dvty -> bool

(** Patterns *)

type dpattern = private {
Andrei Paskevich's avatar
Andrei Paskevich committed
36
  dp_pat  : pre_pattern;
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
  dp_dity : dity;
  dp_vars : dity Mstr.t;
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
  | DPvar  of preid
  | DPapp  of psymbol * dpattern list
  | DPor   of dpattern * dpattern
  | DPas   of dpattern * preid
  | DPcast of dpattern * ity

(** Binders *)

type ghost = bool

Andrei Paskevich's avatar
Andrei Paskevich committed
54
type dbinder = preid option * ghost * dity
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78

(** Specifications *)

type 'a later = vsymbol Mstr.t -> 'a
  (* Specification terms are parsed and typechecked after the program
     expressions, when the types of locally bound program variables are
     already established. *)

type dspec_final = {
  ds_pre     : term list;
  ds_post    : (vsymbol option * term) list;
  ds_xpost   : (vsymbol option * term) list Mexn.t;
  ds_reads   : vsymbol list;
  ds_writes  : term list;
  ds_checkrw : bool;
  ds_diverge : bool;
}

type dspec = ty -> dspec_final
  (* 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. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
79
type dtype_c = dbinder list * dspec later * dity
80

Andrei Paskevich's avatar
Andrei Paskevich committed
81 82 83
type dtype_v =
  | DSpecI of dity
  | DSpecC of dtype_c
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99

(** Expressions *)

type dinvariant = term list

type dexpr = private {
  de_node : dexpr_node;
  de_dvty : dvty;
  de_loc  : Loc.position option;
}

and dexpr_node =
  | DEvar of string * dvty
  | DEgpvar of pvsymbol
  | DEgpsym of psymbol
  | DEconst of Number.constant
Andrei Paskevich's avatar
Andrei Paskevich committed
100 101
  | DEapp of dexpr * dexpr list
  | DEfun of dbinder list * dspec later * dexpr
102 103
  | DElet of dlet_defn * dexpr
  | DErec of drec_defn * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
104 105
  | DEnot of dexpr
  | DElazy of lazy_op * dexpr * dexpr
106 107
  | DEif of dexpr * dexpr * dexpr
  | DEcase of dexpr * (dpattern * dexpr) list
Andrei Paskevich's avatar
Andrei Paskevich committed
108 109
  | DEassign of (dexpr * pvsymbol * dexpr) list
  | DEwhile of dexpr * (dinvariant * variant list) later * dexpr
110
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
111 112 113
  | DEtry of dexpr * (xsymbol * dpattern * dexpr) list
  | DEraise of xsymbol * dexpr
  | DEghost of dexpr
114
  | DEassert of assertion_kind * term later
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116 117 118 119
  | DEpure of term later
  | DEabsurd
  | DEtrue
  | DEfalse
  | DEany of dtype_v
120 121 122 123 124
  | DEmark of preid * dexpr
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

Andrei Paskevich's avatar
Andrei Paskevich committed
125
and dlet_defn = preid * ghost * ps_kind * dexpr
126 127 128

and drec_defn = private { fds : dfun_defn list }

Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131 132
and dfun_defn = preid * ghost * ps_kind *
  dbinder list * (dspec * variant list) later * dexpr

type dval_decl = preid * ghost * ps_kind * dtype_v
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155

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

val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *)

val denv_get_opt : denv -> string -> dexpr_node option

(** Constructors *)

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

Andrei Paskevich's avatar
Andrei Paskevich committed
156
(*
157
val dexpr : ?loc:Loc.position -> dexpr_node -> dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
158
*)
159

Andrei Paskevich's avatar
Andrei Paskevich committed
160 161
type pre_fun_defn = preid * ghost * ps_kind *
  dbinder list * dity * (denv -> (dspec * variant list) later * dexpr)
162 163 164

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

Andrei Paskevich's avatar
Andrei Paskevich committed
165
(*
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
(** Final stage *)

val expr : keep_loc:bool ->
  Decl.known_map -> Mlw_decl.known_map -> dexpr -> expr

val let_defn : keep_loc:bool ->
  Decl.known_map -> Mlw_decl.known_map -> dlet_defn -> let_defn

val fun_defn : keep_loc:bool ->
  Decl.known_map -> Mlw_decl.known_map -> dfun_defn -> fun_defn

val rec_defn : keep_loc:bool ->
  Decl.known_map -> Mlw_decl.known_map -> drec_defn -> fun_defn list

val val_decl : keep_loc:bool ->
  Decl.known_map -> Mlw_decl.known_map -> dval_decl -> let_sym
*)