Convert STV input/output names into similar C++ names.
(stv2c-c-symbol-name x) → str
Function:
(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:
(defthm stringp-of-stv2c-c-symbol-name (b* ((str (stv2c-c-symbol-name x))) (stringp str)) :rule-classes :type-prescription)