blob: e1e430dcaf1507a9b7b03f25e91fe7417ce8feeb (
plain)
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
|
(** {b ALPHA conversion} *)
(** This is the type of the elements that are recorded by the alpha
* conversion functions in order to be able to undo changes to the tables
* they modify. Useful for implementing
* scoping *)
type 'a undoAlphaElement
(** This is the type of the elements of the alpha renaming table. These
* elements can carry some data associated with each occurrence of the name. *)
type 'a alphaTableData
(** Create a new name based on a given name. The new name is formed from a
* prefix (obtained from the given name by stripping a suffix consisting of _
* followed by only digits), followed by a special separator and then by a
* positive integer suffix. The first argument is a table mapping name
* prefixes to some data that specifies what suffixes have been used and how
* to create the new one. This function updates the table with the new
* largest suffix generated. The "undolist" argument, when present, will be
* used by the function to record information that can be used by
* {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo
* information will be in reverse order in which the action occurred. Returns
* the new name and, if different from the lookupname, the location of the
* previous occurrence. This function knows about the location implicitly
* from the {!Cil.currentLoc}. *)
val newAlphaName: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t ->
undolist: 'a undoAlphaElement list ref option ->
lookupname:string -> data:'a -> string * 'a
(** Register a name with an alpha conversion table to ensure that when later
* we call newAlphaName we do not end up generating this one *)
val registerAlphaName: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t ->
undolist: 'a undoAlphaElement list ref option ->
lookupname:string -> data:'a -> unit
(** Split the name in preparation for newAlphaName. The prefix returned is
used to index into the hashtable. The next result value is a separator
(either empty or the separator chosen to separate the original name from
the index) *)
val docAlphaTable: unit ->
(string, 'a alphaTableData ref) Hashtbl.t -> Pretty.doc
val getAlphaPrefix: lookupname:string -> string
(** Undo the changes to a table *)
val undoAlphaChanges: alphaTable:(string, 'a alphaTableData ref) Hashtbl.t ->
undolist:'a undoAlphaElement list -> unit
|
