1 files changed, 159 insertions, 0 deletions
diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
new file mode 100644
index 00000000..08d6b002
--- /dev/null
+++ b/contrib/correctness/peffect.ml
@@ -0,0 +1,159 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certification of Imperative Programs / Jean-Christophe Filliātre *)
+
+(* $Id: peffect.ml,v 1.3.14.1 2004/07/16 19:30:01 herbelin Exp $ *)
+
+open Names
+open Nameops
+open Pmisc
+
+(* The type of effects.
+ *
+ * An effect is composed of two lists (r,w) of variables.
+ * The first one is the list of read-only variables
+ * and the second one is the list of read-write variables.
+ *
+ * INVARIANT: 1. each list is sorted in decreasing order for Pervasives.compare
+ *            2. there are no duplicate elements in each list
+ *            3. the two lists are disjoint
+ *)
+
+type t = identifier list * identifier list
+
+
+(* the empty effect *)
+
+let bottom = ([], [])
+
+(* basic operations *)
+
+let push x l =
+  let rec push_rec = function
+      [] -> [x]
+    | (y::rem) as l ->
+	if x = y then l else if x > y then x::l else y :: push_rec rem
+  in
+    push_rec l
+
+let basic_remove x l =
+  let rec rem_rec = function
+      [] -> []
+    | y::l -> if x = y then l else y :: rem_rec l
+  in
+    rem_rec l
+
+let mem x (r,w) = (List.mem x r) or (List.mem x w)
+
+let rec basic_union = function
+    [], s2 -> s2
+  | s1, [] -> s1
+  | ((v1::l1) as s1), ((v2::l2) as s2) ->
+      if v1 > v2 then
+	v1 :: basic_union (l1,s2)
+      else if v1 < v2 then
+	v2 :: basic_union (s1,l2)
+      else
+	v1 :: basic_union (l1,l2)
+
+(* adds reads and writes variables *)
+
+let add_read id ((r,w) as e) =
+  (* if the variable is already a RW it is ok, otherwise adds it as a RO. *)
+  if List.mem id w then
+    e
+  else
+    push id r, w
+
+let add_write id (r,w) =
+  (* if the variable is a RO then removes it from RO. Adds it to RW. *)
+  if List.mem id r then
+    basic_remove id r, push id w
+  else
+    r, push id w
+
+(* access *)
+
+let get_reads = basic_union
+let get_writes = snd
+let get_repr e = (get_reads e, get_writes e)
+
+(* tests *)
+
+let is_read  (r,_) id = List.mem id r
+let is_write (_,w) id = List.mem id w
+
+(* union and disjunction *)
+
+let union (r1,w1) (r2,w2) = basic_union (r1,r2), basic_union (w1,w2)
+
+let rec diff = function
+    [], s2 -> []
+  | s1, [] -> s1
+  | ((v1::l1) as s1), ((v2::l2) as s2) ->
+      if v1 > v2 then
+	v1 :: diff (l1,s2)
+      else if v1 < v2 then
+	diff (s1,l2)
+      else
+	diff (l1,l2)
+
+let disj (r1,w1) (r2,w2) =
+  let w1_w2 = diff (w1,w2) and w2_w1 = diff (w2,w1) in
+  let r = basic_union (basic_union (r1,r2), basic_union (w1_w2,w2_w1))
+  and w = basic_union (w1,w2) in
+  r,w
+
+(* comparison relation *)
+
+let le e1 e2 = failwith "effects: le: not yet implemented"
+
+let inf e1 e2 = failwith "effects: inf: not yet implemented"
+
+(* composition *)
+
+let compose (r1,w1) (r2,w2) =
+  let r = basic_union (r1, diff (r2,w1)) in
+  let w = basic_union (w1,w2) in
+    r,w
+
+(* remove *)
+
+let remove (r,w) name = basic_remove name r, basic_remove name w
+
+(* substitution *)
+
+let subst_list (x,x') l =
+  if List.mem x l then push x' (basic_remove x l) else l
+
+let subst_one (r,w) s = subst_list s r, subst_list s w
+
+let subst s e = List.fold_left subst_one e s
+
+(* pretty-print *)
+
+open Pp
+open Util
+open Himsg
+
+let pp (r,w) =
+  hov 0 (if r<>[] then
+	     (str"reads " ++
+		prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r)
+	   else (mt ()) ++
+	   spc () ++
+	   if w<>[] then
+	     (str"writes " ++
+		prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w)
+	   else (mt ())
+)
+
+let ppr e =
+  Pp.pp (pp e)
+