Atj-gen-shallow-symbol-field-name
Generate the name of the Java field for an ACL2 quoted symbol.
- Signature
(atj-gen-shallow-symbol-field-name symbol) → name
- Arguments
- symbol — Guard (symbolp symbol).
- Returns
- name — Type (stringp name).
We prepend $Q_ (for `quote')
to a representation of the symbol itself.
We only use the name of the symbol, not the package name,
because unlike other fields for quoted constants
(which go into the main class)
the ones for symbols go into the classes for the packages.
We do not flip uppercase and lowercase,
but we map dashes (which are very common in ACL2 symbols)
to underscores (which are more readable in Java).
However, for t and nil, we just generate T and NIL.
These two symbols are very common, and this special treatment in Java
somewhat mirrors the fact that they do not need to be quoted
in untranslated ACL2 terms.
Definitions and Theorems
Function: atj-gen-shallow-symbol-field-name
(defun atj-gen-shallow-symbol-field-name (symbol)
(declare (xargs :guard (symbolp symbol)))
(let ((__function__ 'atj-gen-shallow-symbol-field-name))
(declare (ignorable __function__))
(cond
((eq symbol t) "T")
((eq symbol nil) "NIL")
(t
(str::cat
"$Q_"
(implode (atj-chars-to-jchars-id (explode (symbol-name symbol))
nil
:dash nil)))))))
Theorem: stringp-of-atj-gen-shallow-symbol-field-name
(defthm stringp-of-atj-gen-shallow-symbol-field-name
(b* ((name (atj-gen-shallow-symbol-field-name symbol)))
(stringp name))
:rule-classes :rewrite)