|
|
|---|
|
|
|
|---|
Initial variable index alist.
When we rename ACL2 variables to Java variables, we must avoid the names in *atj-disallowed-jvar-names*. We do that by initializing the alist from variables to indices to associate index 1 to all the disallowed names. That is, we pretend that variables with the disallowed names have already been used, so that an index 1 (or greater) will be appended to any variable that would otherwise happen to be a disallowed name. Appending an index to a disallowed name always yields an allowed name.
Note that *atj-disallowed-jvar-names* is a list of strings,
but the keys of the index map must be symbols.
We use str::intern-list to convert them.
It is critical to use the same package (currently
Definition:
(defconst *atj-init-indices* (pairlis$ (str::intern-list *atj-disallowed-jvar-names* (pkg-witness "JAVA")) (repeat (len *atj-disallowed-jvar-names*) 1)))