diff options
Diffstat (limited to 'contrib/correctness/prename.ml')
| -rw-r--r-- | contrib/correctness/prename.ml | 139 |
1 files changed, 0 insertions, 139 deletions
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml deleted file mode 100644 index 4ef1982d..00000000 --- a/contrib/correctness/prename.ml +++ /dev/null @@ -1,139 +0,0 @@ -(************************************************************************) -(* 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 5920 2004-07-16 20:01:26Z herbelin $ *) - -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) - |