		Search-engine friendly clone of the ACL2 documentation.

Stv2c

Stv2c-c-symbol-name

Convert STV input/output names into similar C++ names.

Signature
(stv2c-c-symbol-name x) → str
Arguments: x — A user-level STV input/output name.
Returns: str — Type (stringp str).

Definitions and Theorems

Function: stv2c-c-symbol-name

(defun
 stv2c-c-symbol-name (x)
 (declare (xargs :guard t))
 (let
   ((__function__ 'stv2c-c-symbol-name))
   (declare (ignorable __function__))
   (b* (((unless (symbolp x))
         (raise "Expected STV names to be symbols, found ~x0."
                x)
         "")
        (name (symbol-name x))
        (c-name (str::downcase-string (str::strsubst "-" "_" name)))
        (chars (explode c-name))
        ((unless (consp chars))
         (raise "Empty symbol-name used in the STV?")
         "")
        ((cons head tail) chars)
        ((unless (and (or (str::down-alpha-p head)
                          (str::up-alpha-p head)
                          (eql head #\_))
                      (stv2c-tailchars-p tail)))
         (raise "Can't translate name ~x0 into a nice C name."
                x)
         ""))
       c-name)))

Theorem: stringp-of-stv2c-c-symbol-name

(defthm stringp-of-stv2c-c-symbol-name
        (b* ((str (stv2c-c-symbol-name x)))
            (stringp str))
        :rule-classes :type-prescription)

Subtopics

Stv2c-tailchars-p: (stv2c-tailchars-p x) recognizes lists where every element satisfies stv2c-tailchar-p.
Stv2c-tailchar-p