		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-fnnative-method-name

Name of the AIJ method that natively implements an ACL2 function.

Signature
(atj-fnnative-method-name fn guards$) → method-name
Arguments: fn — Guard (symbolp fn).; guards$ — Guard (booleanp guards$).
Returns: method-name — Type (stringp method-name).

The choice depends, in some cases, by the :guards input. If :guards is t, ACL2 booleans are mapped to Java booleans and ACL2 characters are mapped to Java characters, and thus we pick the method names that end with Boolean and Char, i.e. the ones that return Java booleans and Java characters. If :guards is nil, we pick the method names that do not end with Boolean and Char.

The correctness of the choice between the method names should be based not only on whether :guards is t or nil, but also whether the corresponding functions (characterp etc.) are recorded to have return types :aboolean and :acharacter (via atj-main-function-type or not. By including, in this file, the file "types-for-natives.lisp", we ensure that the second condition is always true. Thus, the choice can be simplified by just looking at :guards. If :guards is nil, any recorded ATJ types are ignored.

Definitions and Theorems

Function: atj-fnnative-method-name

(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: stringp-of-atj-fnnative-method-name

(defthm stringp-of-atj-fnnative-method-name
  (b* ((method-name (atj-fnnative-method-name fn guards$)))
    (stringp method-name))
  :rule-classes :rewrite)