Name of the AIJ method that natively implements an ACL2 function.
The choice depends, in some cases, by the
The correctness of the choice between the method names
should be based not only on whether
Function:
(defun atj-fnnative-method-name (fn guards$) (declare (xargs :guard (and (symbolp fn) (booleanp guards$)))) (declare (xargs :guard (aij-nativep fn))) (let ((__function__ 'atj-fnnative-method-name)) (declare (ignorable __function__)) (case fn (characterp (if guards$ "execCharacterpBoolean" "execCharacterp")) (stringp (if guards$ "execStringpBoolean" "execStringp")) (symbolp (if guards$ "execSymbolpBoolean" "execSymbolp")) (integerp (if guards$ "execIntegerpBoolean" "execIntegerp")) (rationalp (if guards$ "execRationalpBoolean" "execRationalp")) (complex-rationalp (if guards$ "execComplexRationalpBoolean" "execComplexRationalp")) (acl2-numberp (if guards$ "execAcl2NumberpBoolean" "execAcl2Numberp")) (consp (if guards$ "execConspBoolean" "execConsp")) (char-code "execCharCode") (code-char (if guards$ "execCodeCharChar" "execCodeChar")) (coerce "execCoerce") (intern-in-package-of-symbol "execInternInPackageOfSymbol") (symbol-package-name (if guards$ "execSymbolPackageNameString" "execSymbolPackageName")) (symbol-name (if guards$ "execSymbolNameString" "execSymbolName")) (pkg-imports "execPkgImports") (pkg-witness "execPkgWitness") (unary-- "execUnaryMinus") (unary-/ "execUnarySlash") (binary-+ "execBinaryPlus") (binary-* "execBinaryStar") (< (if guards$ "execLessThanBoolean" "execLessThan")) (complex "execComplex") (realpart "execRealPart") (imagpart "execImagPart") (numerator "execNumerator") (denominator "execDenominator") (cons "execCons") (car "execCar") (cdr "execCdr") (equal (if guards$ "execEqualBoolean" "execEqual")) (bad-atom<= "execBadAtomLessThanOrEqualTo") (if "execIf") (nonnegative-integer-quotient "execNonnegativeIntegerQuotient") (string-append "execStringAppend") (len "execLen") (char (if guards$ "execCharChar" "execChar")) (hard-error "execHardError") (t (prog2$ (impossible) "irrelevant-method-name")))))
Theorem:
(defthm stringp-of-atj-fnnative-method-name (b* ((method-name (atj-fnnative-method-name fn guards$))) (stringp method-name)) :rule-classes :rewrite)