|
|
|---|
|
|
|
|---|
Rename all the ACL2 variables in an ACL2 term to their Java names.
(atj-rename-term term renaming-new renaming-old
indices curr-pkg vars-by-name)
→
(mv new-term new-renaming-old new-indices)The alist from variables to indices is threaded through this function and its mutually recursive companion, in the same way as the renaming alist for the `old' variables; thus different variables in different Java scopes may have the same index. This alist contains variables without annotations or markings; see atj-rename-formals for motivation.
The renaming alist for variables marked as `new' is not threaded through: it is just passed down, according to ACL2's scoping. This alist contains variables with type annotations but without markings for `old' or `new'; see atj-rename-formals for motivation.
The renaming alist for variables marked as `old' is threaded through instead, in the same way as the set of variables in scope in atj-mark-term (see that function for details). This is because variables are marked for reuse based (also) on that threading of the variables in scope: when we encounter a variable to rename that is marked for reuse, we must have its name available in the renaming alist. This alist contains variables with type annotations but without markings for `old' or `new'; see atj-rename-formals for motivation.
If the term is a variable, it is unmarked, looked up in the appropriate renaming alist based on the marking, and replaced with the renamed variable, which is re-marked. Recall that variable names are generated via atj-rename-formals when variables are introduced, i.e. from formal parameters of defined functions and lambda expressions.
If the term is a quoted constant, it is obviously left unchanged.
If the term is a function call, its actual arguments are recursively processed, renaming all their variables. If the function is a named one, it is of course left unchanged. If instead it is a lambda expression, we process the renaming of its formal parameters, which in general augments the two renaming alists, and then recursively process the body of the lambda expression.
Theorem:
(defthm return-type-of-atj-rename-term.new-term (b* (((mv ?new-term ?new-renaming-old ?new-indices) (atj-rename-term term renaming-new renaming-old indices curr-pkg vars-by-name))) (pseudo-termp new-term)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-rename-term.new-renaming-old (b* (((mv ?new-term ?new-renaming-old ?new-indices) (atj-rename-term term renaming-new renaming-old indices curr-pkg vars-by-name))) (symbol-symbol-alistp new-renaming-old)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-rename-term.new-indices (b* (((mv ?new-term ?new-renaming-old ?new-indices) (atj-rename-term term renaming-new renaming-old indices curr-pkg vars-by-name))) (symbol-pos-alistp new-indices)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-rename-terms.new-terms (b* (((mv ?new-terms ?new-renaming-old ?new-indices) (atj-rename-terms terms renaming-new renaming-old indices curr-pkg vars-by-name))) (and (pseudo-term-listp new-terms) (equal (len new-terms) (len terms)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-rename-terms.new-renaming-old (b* (((mv ?new-terms ?new-renaming-old ?new-indices) (atj-rename-terms terms renaming-new renaming-old indices curr-pkg vars-by-name))) (symbol-symbol-alistp new-renaming-old)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-rename-terms.new-indices (b* (((mv ?new-terms ?new-renaming-old ?new-indices) (atj-rename-terms terms renaming-new renaming-old indices curr-pkg vars-by-name))) (symbol-pos-alistp new-indices)) :rule-classes :rewrite)