1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
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)
|
