dterm.mli 2.65 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
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
(*                                                                  *)
(*  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

(** Types *)

type dty

val dty_fresh : unit -> dty

val dty_of_ty : ty -> dty

(** Patterns, terms, and formulas *)

type dpattern = private {
  dp_node : dpattern_node;
  dp_dty  : dty;
30
  dp_vars : dty Mstr.t;
31 32 33 34 35 36 37 38 39 40
  dp_loc  : Loc.position option;
}

and dpattern_node =
  | DPwild
  | DPvar of preid
  | DPapp of lsymbol * dpattern list
  | DPor of dpattern * dpattern
  | DPas of dpattern * preid

41 42 43
type dbinop =
  | DTand | DTand_asym | DTor | DTor_asym | DTimplies | DTiff

44 45 46 47 48 49 50
type dterm = private {
  dt_node  : dterm_node;
  dt_dty   : dty option;
  dt_loc   : Loc.position option;
}

and dterm_node =
51 52
  | DTvar of string * dty
  | DTgvar of vsymbol
53 54
  | DTconst of Number.constant
  | DTapp of lsymbol * dterm list
55
  | DTfapp of dterm * dterm
56 57 58 59 60
  | DTif of dterm * dterm * dterm
  | DTlet of dterm * preid * dterm
  | DTcase of dterm * (dpattern * dterm) list
  | DTeps of preid * dty * dterm
  | DTquant of quant * (preid * dty) list * dterm list list * dterm
61
  | DTbinop of dbinop * dterm * dterm
62 63 64
  | DTnot of dterm
  | DTtrue
  | DTfalse
65 66 67
  | DTcast of dterm * ty
  | DTuloc of dterm * Loc.position
  | DTlabel of dterm * Slab.t
68 69 70 71 72 73 74 75

(** Environment *)

exception TermExpected
exception FmlaExpected
exception DuplicateVar of string
exception UnboundVar of string

76 77 78
type denv = dterm_node Mstr.t (** bound variables *)

val denv_empty : denv (** Mstr.empty *)
79 80 81 82 83 84 85 86 87

val denv_add_var : denv -> preid -> dty -> denv

val denv_add_let : denv -> dterm -> preid -> denv

val denv_add_quant : denv -> (preid * dty) list -> denv

val denv_add_pat : denv -> dpattern -> denv

88 89 90
val denv_get : denv -> string -> dterm_node (** raises UnboundVar *)

val denv_get_opt : denv -> string -> dterm_node option
91 92 93 94 95 96 97 98 99

(** Constructors *)

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

val dterm : ?loc:Loc.position -> dterm_node -> dterm

(** Final stage *)

100
val term : strict:bool -> keep_loc:bool -> dterm -> term
101

102
val fmla : strict:bool -> keep_loc:bool -> dterm -> term