diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-03-29 09:47:11 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-03-29 09:47:11 +0000 |
commit | a5f03d96eee482cd84861fc8cefff9eb451c0cad (patch) | |
tree | cbc66cbc183a7c5ef2c044ed9ed04b8011df9cd4 /cil/ocamlutil/alpha.mli | |
parent | a9621943087a5578c995d88b06f87c5158eb5d00 (diff) | |
download | compcert-a5f03d96eee482cd84861fc8cefff9eb451c0cad.tar.gz compcert-a5f03d96eee482cd84861fc8cefff9eb451c0cad.zip |
Cleaned up configure script.
Distribution of CIL as an expanded source tree with changes applied
(instead of original .tar.gz + patches to be applied at config time).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cil/ocamlutil/alpha.mli')
-rwxr-xr-x | cil/ocamlutil/alpha.mli | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/cil/ocamlutil/alpha.mli b/cil/ocamlutil/alpha.mli new file mode 100755 index 00000000..e1e430dc --- /dev/null +++ b/cil/ocamlutil/alpha.mli @@ -0,0 +1,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 |