		Search-engine friendly clone of the ACL2 documentation.

Primitive-function-macros

Def-primitive-unary

Macro to formalize a unary ACL2 function over Java primitive values.

This macro takes as required arguments the name of the function to define, the primitive type of the operand, the primitive type of the result, and an untranslated term that defines the operation on the core value. This term must have x as the only free variable, which the boilerplate code generated by the macro binds to the core value of the operand.

This macro also takes optional arguments for XDOC documentation: parents, short string, and long string. The latter may be forms, e.g. involving XDOC constructors.

Macro: def-primitive-unary

(defmacro def-primitive-unary (name &key in-type out-type operation
                                    (parents 'nil parents-suppliedp)
                                    (short 'nil short-suppliedp)
                                    (long 'nil long-suppliedp))
 (cons
  'make-event
  (cons
   (cons
    'def-primitive-unary-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      in-type
      (cons
       out-type
       (cons
        (cons 'quote (cons operation 'nil))
        (cons
         (cons 'quote (cons parents 'nil))
         (cons
              parents-suppliedp
              (cons short
                    (cons short-suppliedp
                          (cons long
                                (cons long-suppliedp 'nil)))))))))))
   'nil)))

Definitions and Theorems

Function: def-primitive-unary-fn

(defun def-primitive-unary-fn
       (name in-type out-type operation
             parents parents-suppliedp short
             short-suppliedp long long-suppliedp)
 (declare (xargs :guard (and (symbolp name)
                             (primitive-typep in-type)
                             (primitive-typep out-type)
                             (symbol-listp parents)
                             (booleanp parents-suppliedp)
                             (booleanp short-suppliedp)
                             (booleanp long-suppliedp))))
 (let ((__function__ 'def-primitive-unary-fn))
  (declare (ignorable __function__))
  (b* ((in-predicate (primitive-type-predicate in-type))
       (in-destructor (primitive-type-destructor in-type))
       (out-predicate (primitive-type-predicate out-type))
       (out-constructor (primitive-type-constructor out-type)))
   (cons
    'define
    (cons
     name
     (cons
      (cons (cons 'operand (cons in-predicate 'nil))
            'nil)
      (cons
       ':returns
       (cons
        (cons 'result (cons out-predicate 'nil))
        (append
         (and parents-suppliedp
              (list :parents parents))
         (append
          (and short-suppliedp (list :short short))
          (append
           (and long-suppliedp (list :long long))
           (cons
            (cons
             'b*
             (cons
                  (cons (cons 'x
                              (cons (cons in-destructor '(operand))
                                    'nil))
                        'nil)
                  (cons (cons out-constructor (cons operation 'nil))
                        'nil)))
            '(:hooks (:fix)
                     :no-function t)))))))))))))