		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-var-name

Lift a PFCS variable name to an ACL2 symbol.

Signature
(lift-var-name name state) → sym
Arguments: name — Guard (stringp name).
Returns: sym — Type (symbolp sym).

The PFCS abstract syntax uses strings for variable names. These are turned into symbols in the shallowly embedded semantics. Here we define the mapping.

Assuming that PFCS variable names would normally consist of lowercase letters, digits, and underscores, we map lowercase letters to uppercase letters, digits to themselves, and underscores to dashes; we use the resulting string as name of the symbol, which we put in the current package. This way, idiomatic PFCS names are mapped to idiomatic ACL2 symbols.

This mapping is not bulletproof. The current package may import symbols from the Lisp package, for example, and a PFCS variable name may end up being mapped to a symbol in the Lisp package, which cannot be used as an ACL2 name. In the future, we may make this mapping more robust.

Definitions and Theorems

Function: lift-var-name-aux

(defun lift-var-name-aux (chars)
  (declare (xargs :guard (character-listp chars)))
  (let ((__function__ 'lift-var-name-aux))
    (declare (ignorable __function__))
    (b* (((when (endp chars)) nil)
         (char (car chars))
         (new-char (if (equal char #\_)
                       #\-
                     (str::upcase-char char)))
         (new-chars (lift-var-name-aux (cdr chars))))
      (cons new-char new-chars))))

Theorem: character-listp-of-lift-var-name-aux

(defthm character-listp-of-lift-var-name-aux
  (b* ((new-chars (lift-var-name-aux chars)))
    (character-listp new-chars))
  :rule-classes :rewrite)

Function: lift-var-name

(defun lift-var-name (name state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'lift-var-name))
    (declare (ignorable __function__))
    (b* ((chars (acl2::explode name))
         (new-chars (lift-var-name-aux chars))
         (new-string (acl2::implode new-chars)))
      (intern$ new-string (current-package+ state)))))

Theorem: symbolp-of-lift-var-name

(defthm symbolp-of-lift-var-name
  (b* ((sym (lift-var-name name state)))
    (symbolp sym))
  :rule-classes :rewrite)