Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

mlw_dtree.ml 3.18 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
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2012                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Guillaume Melquiond                                                 *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

open Why3
open Ident
open Denv
open Ty
open Mlw_ty
26 27
open Mlw_ty.T
open Mlw_expr
28
open Mlw_module
29
open Mlw_dty
30 31 32 33

type loc = Loc.position
type ident = Ptree.ident

34
type ghost = bool
35
type dpre = Ptree.pre
36 37
type dpost = Ptree.pre
type dxpost = (xsymbol * dpost) list
Andrei Paskevich's avatar
Andrei Paskevich committed
38
type dbinder = ident * ghost * dity
39

40 41 42 43 44
type deffect = {
  deff_reads  : (ghost * Ptree.lexpr) list;
  deff_writes : (ghost * Ptree.lexpr) list;
  deff_raises : (ghost * xsymbol) list;
}
45

46 47 48 49 50 51 52 53 54 55 56
type dtype_v =
  | DSpecV of dity
  | DSpecA of dbinder list * dtype_c

and dtype_c = {
  dc_result : dtype_v;
  dc_effect : deffect;
  dc_pre    : dpre;
  dc_post   : dpost;
  dc_xpost  : dxpost;
}
57 58 59

type dvariant = Ptree.lexpr * Term.lsymbol option

Andrei Paskevich's avatar
Andrei Paskevich committed
60
type dinvariant = Ptree.lexpr option
61 62

type dexpr = {
63 64 65 66
  de_desc : dexpr_desc;
  de_type : dity;
  de_lab  : Ident.label list;
  de_loc  : loc;
67 68 69
}

and dexpr_desc =
Andrei Paskevich's avatar
Andrei Paskevich committed
70
  | DEconstant of Term.constant
71
  | DElocal of string
72 73
  | DEglobal_pv of pvsymbol
  | DEglobal_ps of psymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74 75 76
  | DEglobal_pl of plsymbol
  | DEglobal_ls of Term.lsymbol
  | DEapply of dexpr * dexpr list
77
  | DEfun of dlambda
78 79
  | DElet of ident * dexpr * dexpr
  | DEletrec of drecfun list * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
80
  | DEassign of dexpr * dexpr
81
  | DEif of dexpr * dexpr * dexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
82 83
  | DEloop of dvariant list * dinvariant * dexpr
  | DElazy of Ptree.lazy_op * dexpr * dexpr
84
  | DEnot of dexpr
85
  | DEmatch of dexpr * (pre_ppattern * dexpr) list
86
  | DEabsurd
Andrei Paskevich's avatar
Andrei Paskevich committed
87 88
  | DEraise of xsymbol * dexpr
  | DEtry of dexpr * (xsymbol * ident * dexpr) list
Andrei Paskevich's avatar
Andrei Paskevich committed
89 90
  | DEfor of ident * dexpr * Ptree.for_direction * dexpr * dinvariant * dexpr
  | DEassert of Ptree.assertion_kind * Ptree.lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
91
  | DEmark of ident * dexpr
92
  | DEghost of dexpr
93
  | DEany of dtype_c
94

95
and drecfun = ident * dity * dlambda
96

97
and dlambda = dbinder list * dvariant list * dpre * dexpr * dpost * dxpost