mlw_dexpr.mli 5.02 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
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2013   --   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 Mlw_ty
open Mlw_ty.T
open Mlw_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) *)

30 31 32 33
val dity_is_bool : dity -> bool

val dvty_is_chainable : dvty -> bool

34 35 36 37 38
(** Patterns *)

type dpattern = private {
  dp_pat  : pre_ppattern;
  dp_dity : dity;
39
  dp_vars : dity Mstr.t;
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
  dp_loc  : Loc.position option;
}

type dpattern_node =
  | DPwild
  | DPvar  of preid
  | DPlapp of lsymbol * dpattern list
  | DPpapp of plsymbol * dpattern list
  | DPor   of dpattern * dpattern
  | DPas   of dpattern * preid

(** Specifications *)

type ghost = bool

55 56
type opaque = Stv.t

57
type dbinder = preid option * ghost * opaque * dity
58 59 60 61 62 63

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. *)

64 65 66 67 68
type dpre = Loc.position option * term
type dpost = Loc.position option * (pattern * term) list
type dxpost = Loc.position option * (xsymbol * pattern * term) list
type dinvariant = (Loc.position option * term) list

69
type dspec = {
70 71 72
  ds_pre     : dpre list;
  ds_post    : dpost list;
  ds_xpost   : dxpost list;
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
  ds_reads   : vsymbol list;
  ds_writes  : term list;
  ds_variant : variant list;
}

type dtype_v =
  | DSpecV of dity
  | DSpecA of dbinder list * dtype_c

and dtype_c = dtype_v * dspec later

(** Expressions *)

type dlazy_op = DEand | DEor

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
  | DEplapp of plsymbol * dexpr list
  | DElsapp of lsymbol * dexpr list
  | DEapply of dexpr * dexpr list
101
  | DEconst of Number.constant
102 103 104 105 106 107 108 109 110 111 112 113 114
  | DEval of dval_decl * dexpr
  | DElet of dlet_defn * dexpr
  | DEfun of dfun_defn * dexpr
  | DErec of dfun_defn list * dexpr
  | DEif of dexpr * dexpr * dexpr
  | DEmatch of dexpr * (dpattern * dexpr) list
  | DEassign of plsymbol * dexpr * dexpr
  | DElazy of dlazy_op * dexpr * dexpr
  | DEnot of dexpr
  | DEtrue
  | DEfalse
  | DEraise of xsymbol * dexpr
  | DEtry of dexpr * (xsymbol * dpattern * dexpr) list
115 116
  | DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
  | DEloop of (variant list * dinvariant) later * dexpr
117 118 119 120 121 122 123 124 125 126 127 128 129 130
  | DEabsurd
  | DEassert of assertion_kind * term later
  | DEabstract of dexpr * dspec later
  | DEmark of preid * dexpr
  | DEghost of dexpr
  | DEany of dtype_c
  | DEcast of dexpr * ity
  | DEuloc of dexpr * Loc.position
  | DElabel of dexpr * Slab.t

and dval_decl = preid * ghost * dtype_v

and dlet_defn = preid * ghost * dexpr

131
and dfun_defn = preid * ghost * dbinder list * dexpr * dspec later
132 133 134 135 136 137 138 139 140 141 142 143 144

(** Environment *)

type denv

val denv_empty : denv

val denv_add_val : denv -> dval_decl -> denv

val denv_add_let : denv -> dlet_defn -> denv

val denv_add_fun : denv -> dfun_defn -> denv

145 146 147
val denv_prepare_rec : denv -> (preid * dbinder list * dity) list -> denv
  (* [denv_prepare_rec] adds to the environment the user-supplied
     types of every function in a (mutually) recursive definition.
148 149 150
     Functions with fully specified prototypes are generalized in
     the recursive block (polymorphic recursion), except for the
     type variables that appear in the upper context. *)
151 152 153 154 155 156 157

val denv_verify_rec : denv -> preid -> unit
  (* after a (mutually) recursive definition has been typechecked,
     [denv_verify_rec] should be called for every function on the
     [denv] before [denv_prepare_rec]. This function verifies that
     the resulting functions are not less polymorphic than expected
     according the user-supplied type annotations. *)
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174

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

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

(** Final stage *)

175 176 177 178 179
val expr     : keep_loc:bool -> dexpr -> expr
val val_decl : keep_loc:bool -> dval_decl -> let_sym
val let_defn : keep_loc:bool -> dlet_defn -> let_defn
val fun_defn : keep_loc:bool -> dfun_defn -> fun_defn
val rec_defn : keep_loc:bool -> dfun_defn list -> fun_defn list