		Search-engine friendly clone of the ACL2 documentation.

Semantics-shallowly-embedded

Name-to-symbol

Turn a PFCS relation or variable name into an ACL2 symbol.

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

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

Assuming that PFCS relation and 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 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: name-to-symbol-aux

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

Theorem: character-listp-of-name-to-symbol-aux

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

Function: name-to-symbol

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

Theorem: symbolp-of-name-to-symbol

(defthm symbolp-of-name-to-symbol
  (b* ((sym (name-to-symbol name state)))
    (symbolp sym))
  :rule-classes :rewrite)