diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:25:25 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:25:25 +0000 |
commit | 93d89c2b5e8497365be152fb53cb6cd4c5764d34 (patch) | |
tree | 0de8d05bbd0eeaeb5e4b85395f8dd576984b6a9e /cil/ocamlutil/alpha.mli | |
parent | 891377ce1962cdb31357d6580d6546ec22df2b4f (diff) | |
download | compcert-93d89c2b5e8497365be152fb53cb6cd4c5764d34.tar.gz compcert-93d89c2b5e8497365be152fb53cb6cd4c5764d34.zip |
Getting rid of CIL
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cil/ocamlutil/alpha.mli')
-rwxr-xr-x | cil/ocamlutil/alpha.mli | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/cil/ocamlutil/alpha.mli b/cil/ocamlutil/alpha.mli deleted file mode 100755 index e1e430dc..00000000 --- a/cil/ocamlutil/alpha.mli +++ /dev/null @@ -1,50 +0,0 @@ -(** {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 |