diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/correctness/peffect.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/correctness/peffect.ml')
-rw-r--r-- | contrib/correctness/peffect.ml | 159 |
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) + |