1 files changed, 139 insertions, 0 deletions
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
new file mode 100644
index 00000000..864f6abd
--- /dev/null
+++ b/contrib/correctness/prename.ml
@@ -0,0 +1,139 @@
+(************************************************************************)
+(*  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: prename.ml,v 1.3.14.1 2004/07/16 19:30:05 herbelin Exp $ *)
+
+open Names
+open Nameops
+open Util
+open Pp
+open Himsg
+open Pmisc
+
+(* Variables names management *)
+
+type date = string
+
+(* The following data structure keeps the successive names of the variables
+ * as we traverse the program. A each step a ``date'' and a
+ * collection of new names is (possibly) given, and updates the
+ * previous renaming.
+ * 
+ * Then, we can ask for the name of a variable, at current date or
+ * at a given date.
+ *
+ * It is easily represented by a list of date x assoc list, most recent coming 
+ * first i.e. as follows:
+ *
+ *   [ date (= current), [ (x,xi); ... ];
+ *     date            , [ (z,zk); ... ];
+ *     ...
+ *     date (= initial), [ (x,xj); (y,yi); ... ]
+ *
+ * We also keep a list of all names already introduced, in order to
+ * quickly get fresh names.
+ *)
+
+type t =
+    { levels : (date * (identifier * identifier) list) list;
+      avoid  : identifier list;
+      cpt    : int }
+    
+
+let empty_ren = { levels = []; avoid = []; cpt = 0 }
+
+let update r d ids =
+  let al,av = renaming_of_ids r.avoid ids in
+  { levels = (d,al) :: r.levels; avoid = av; cpt = r.cpt }
+
+let push_date r d = update r d []
+
+let next r ids =
+  let al,av = renaming_of_ids r.avoid ids in
+  let n = succ r.cpt in
+  let d = string_of_int n in
+  { levels = (d,al) :: r.levels; avoid = av; cpt = n }
+
+
+let find r x =
+  let rec find_in_one = function
+      []         -> raise Not_found
+    | (y,v)::rem -> if y = x then v else find_in_one rem
+  in
+  let rec find_in_all = function
+      []         -> raise Not_found
+    | (_,l)::rem -> try find_in_one l with Not_found -> find_in_all rem
+  in
+    find_in_all r.levels
+
+
+let current_var = find
+
+let current_vars r ids = List.map (fun id -> id,current_var r id) ids
+
+
+let avoid r ids = { levels = r.levels; avoid = r.avoid @ ids; cpt = r.cpt }
+
+let fresh r ids = fst (renaming_of_ids r.avoid ids)
+
+
+let current_date r =
+  match r.levels with
+      [] -> invalid_arg "Renamings.current_date"
+    | (d,_)::_ -> d
+
+let all_dates r = List.map fst r.levels
+
+let rec valid_date da r = 
+  let rec valid = function
+      [] -> false
+    | (d,_)::rem -> (d=da) or (valid rem)
+  in
+    valid r.levels
+
+(* [until d r] selects the part of the renaming [r] starting from date [d] *)
+let rec until da r =
+  let rec cut = function
+      [] -> invalid_arg "Renamings.until"
+    | (d,_)::rem as r -> if d=da then r else cut rem
+  in
+    { avoid = r.avoid; levels = cut r.levels; cpt = r.cpt }
+
+let var_at_date r d id =
+  try
+    find (until d r) id
+  with Not_found ->
+    raise (UserError ("Renamings.var_at_date",
+	      hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++
+		       str"at date " ++ str d)))
+
+let vars_at_date r d ids =
+  let r' = until d r in List.map (fun id -> id,find r' id) ids
+
+
+(* pretty-printers *)
+
+open Pp
+open Util
+open Himsg
+
+let pp r = 
+  hov 2 (prlist_with_sep (fun () -> (fnl ()))
+	   (fun (d,l) -> 
+	      (str d ++ str": " ++ 
+		 prlist_with_sep (fun () -> (spc ()))
+		   (fun (id,id') -> 
+		      (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")"))
+		   l))
+	   r.levels)
+
+let ppr e =
+  Pp.pp (pp e)
+