		Search-engine friendly clone of the ACL2 documentation.

Std/system

Fresh-logical-name-with-$s-suffix

Suffix a name with as many $ signs as needed to make it a valid new logical name that is also not among a given list of names to avoid.

Signature
(fresh-logical-name-with-$s-suffix name type names-to-avoid wrld) → (mv fresh-name updated-names-to-avoid)
Arguments: name — Guard (symbolp name).; type — Guard (member-eq type '(function macro const stobj constrained-function nil)) .; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: fresh-name — Type (symbolp fresh-name), given (symbolp name).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (and (symbolp name) (symbol-listp names-to-avoid)).

The returned name can be used for a new function, macro, constant, etc., based on the type argument passed to this utility; for theorems, use nil as the type. (These are all logical names.) When names for multiple new functions, macros, etc. must be generated, the list of names to avoid can be threaded through multiple calls of this utility, starting with the empty list nil and extending it with each name returned by this utility.

The resulting name may be the same as the argument, with no $ signs added, if the argument is already a valid fresh logical name of the given type.

We use fresh-namep-msg-weak to check the freshness of names, which may miss names of functions in raw Lisp. But the more accurate check fresh-namep-msg, which takes into account names of functions in raw Lisp, is state-changing, which would therefore force this utility to be state-changing too. Thus, for now we use the weaker check, and avoid passing and returning state. If we encounter problems in the future, we will revise this utility, or introduce a new one.

Note that if the logical name is for a constant, the $ signs are added just before the final *, so that the resulting name is still a valid constant name; see add-suffix-to-fn-or-const. If the name is for a function (constrained or not), macro, or stobj, and is in the "COMMON-LISP" package, the call of add-suffix-to-fn-or-const, which reduces to add-suffix-to-fn in this case, will ``move'' the name to the "ACL2" package. If the name is for a theorem, in which case type is nil, then we just use add-suffix, because theorem names may be in the "COMMON-LISP" package. This holds for other types of logical names too for which type is nil: fresh-namep-msg-weak succeeds when called on a symbol in the "COMMON-LISP" package and with nil as type.

Since the ACL2 world is finite, eventually we must find a fresh name, with enough $s. Turning this into a termination proof requires a bit of work, so for now we use a counter that gets decremented at every recursive call, making for an easy termination proof. We initialize the counter to 1000, which is very large for the expected use cases; think of a generated logical name with 1000 $s in it. Nonetheless, this is a bit inelegant, and we should eventually formalize the termination argument above, avoiding the counter altogether.

Definitions and Theorems

Function: fresh-logical-name-with-$s-suffix-aux

(defun fresh-logical-name-with-$s-suffix-aux
       (name type names-to-avoid wrld counter)
 (declare
  (xargs
   :guard
   (and (symbolp name)
        (member-eq type
                   '(function macro
                              const stobj constrained-function nil))
        (symbol-listp names-to-avoid)
        (plist-worldp wrld)
        (natp counter))))
 (let ((__function__ 'fresh-logical-name-with-$s-suffix-aux))
   (declare (ignorable __function__))
   (b* (((when (zp counter))
         (raise "Internal error: exhausted counter at ~x0."
                name)
         (mv name names-to-avoid))
        (msg/nil (fresh-namep-msg-weak name type wrld))
        ((when (or msg/nil
                   (member-eq name names-to-avoid)))
         (fresh-logical-name-with-$s-suffix-aux
              (if type (add-suffix-to-fn-or-const name "$")
                (add-suffix name "$"))
              type names-to-avoid wrld (1- counter))))
     (mv name (cons name names-to-avoid)))))

Theorem: symbolp-of-fresh-logical-name-with-$s-suffix-aux.fresh-name

(defthm symbolp-of-fresh-logical-name-with-$s-suffix-aux.fresh-name
  (implies (symbolp name)
           (b* (((mv ?fresh-name ?updated-names-to-avoid)
                 (fresh-logical-name-with-$s-suffix-aux
                      name type names-to-avoid wrld counter)))
             (symbolp fresh-name)))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-fresh-logical-name-with-$s-suffix-aux.updated-names-to-avoid

(defthm
 symbol-listp-of-fresh-logical-name-with-$s-suffix-aux.updated-names-to-avoid
 (implies (and (symbolp name)
               (symbol-listp names-to-avoid))
          (b* (((mv ?fresh-name ?updated-names-to-avoid)
                (fresh-logical-name-with-$s-suffix-aux
                     name type names-to-avoid wrld counter)))
            (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)

Function: fresh-logical-name-with-$s-suffix

(defun fresh-logical-name-with-$s-suffix
       (name type names-to-avoid wrld)
 (declare
  (xargs
   :guard
   (and (symbolp name)
        (member-eq type
                   '(function macro
                              const stobj constrained-function nil))
        (symbol-listp names-to-avoid)
        (plist-worldp wrld))))
 (let ((__function__ 'fresh-logical-name-with-$s-suffix))
   (declare (ignorable __function__))
   (fresh-logical-name-with-$s-suffix-aux
        name type names-to-avoid wrld 1000)))

Theorem: symbolp-of-fresh-logical-name-with-$s-suffix.fresh-name

(defthm symbolp-of-fresh-logical-name-with-$s-suffix.fresh-name
  (implies (symbolp name)
           (b* (((mv ?fresh-name ?updated-names-to-avoid)
                 (fresh-logical-name-with-$s-suffix
                      name type names-to-avoid wrld)))
             (symbolp fresh-name)))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-fresh-logical-name-with-$s-suffix.updated-names-to-avoid

(defthm
 symbol-listp-of-fresh-logical-name-with-$s-suffix.updated-names-to-avoid
 (implies (and (symbolp name)
               (symbol-listp names-to-avoid))
          (b* (((mv ?fresh-name ?updated-names-to-avoid)
                (fresh-logical-name-with-$s-suffix
                     name type names-to-avoid wrld)))
            (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)