pgm_effect.mli 2.27 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
19
20

open Why
21
open Term
22
23
24
25

type reference = 
  | Rlocal  of Term.vsymbol
  | Rglobal of Term.lsymbol
26

27
28
29
val name_of_reference : reference -> Ident.ident
val type_of_reference : reference -> Ty.ty
val ref_equal : reference -> reference -> bool
30
val reference_of_term : Term.term -> reference
31

32
33
module Sref : Set.S with type elt = reference
module Mref : Map.S with type key = reference
34
35

type t = private {
36
37
  reads  : Sref.t;
  writes : Sref.t;
38
39
40
41
42
  raises : Sls.t;
}

val empty : t

Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
43
44
45
val add_read  : reference -> t -> t
val add_write : reference -> t -> t
val add_raise : lsymbol -> t -> t
46

47
48
val remove_reference : reference -> t -> t

49
50
val remove_raise : lsymbol -> t -> t

51
val union : t -> t -> t
52

53
54
val equal : t -> t -> bool

55
56
val no_side_effect : t -> bool

57
58
val subst : vsymbol -> reference -> t -> t

59
60
val occur : reference -> t -> bool

61
62
val print_reference : Format.formatter -> reference -> unit
val print           : Format.formatter -> t         -> unit