		Search-engine friendly clone of the ACL2 documentation.

Primitive-function-macros

Def-primitive-binary

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

This is similar to def-primitive-unary, but it takes two input type arguments instead of one (the one for the left operand, followed by the one for the right operand). The untranslated term that defines the operation on the core values must have x and y as its only free variables: they are for the (core) left and right operand, respectively.

This macro also takes an optional argument saying whether the right operand should be non-zero; in this case, the right operand type must be int or long. If this argument is t, the guard of the generated function requires the right operand to be different from the zero value of the respective type. This is used to define the integer division and reminder operations; it is nil by default.

This macro also takes an optional argument saying whether a theorem should be generated that asserts the commutativity of the operation. There is also an optional argument to supply hints for this.

Macro: def-primitive-binary

(defmacro def-primitive-binary
          (name &key in-type-left
                in-type-right out-type operation
                nonzero commutative commutative-hints
                (parents 'nil parents-suppliedp)
                (short 'nil short-suppliedp)
                (long 'nil long-suppliedp))
 (cons
  'make-event
  (cons
   (cons
    'def-primitive-binary-fn
    (cons
     (cons 'quote (cons name 'nil))
     (cons
      in-type-left
      (cons
       in-type-right
       (cons
        out-type
        (cons
         (cons 'quote (cons operation 'nil))
         (cons
          nonzero
          (cons
           commutative
           (cons
            (cons 'quote
                  (cons commutative-hints '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-binary-fn

(defun def-primitive-binary-fn
       (name in-type-left
             in-type-right out-type operation
             nonzero commutative commutative-hints
             parents parents-suppliedp short
             short-suppliedp long long-suppliedp)
 (declare (xargs :guard (and (symbolp name)
                             (primitive-typep in-type-left)
                             (primitive-typep in-type-right)
                             (primitive-typep out-type)
                             (booleanp nonzero)
                             (booleanp commutative)
                             (true-listp commutative-hints)
                             (symbol-listp parents)
                             (booleanp parents-suppliedp)
                             (booleanp short-suppliedp)
                             (booleanp long-suppliedp))))
 (let ((__function__ 'def-primitive-binary-fn))
  (declare (ignorable __function__))
  (b*
   ((in-predicate-left (primitive-type-predicate in-type-left))
    (in-predicate-right (primitive-type-predicate in-type-right))
    (in-destructor-left (primitive-type-destructor in-type-left))
    (in-destructor-right (primitive-type-destructor in-type-right))
    (out-predicate (primitive-type-predicate out-type))
    (out-constructor (primitive-type-constructor out-type))
    ((when (and nonzero
                (not (primitive-type-case in-type-right :int))
                (not (primitive-type-case in-type-right :long))))
     (raise
      "The :NONZERO argument may be T ~
                  only if the right operand type is int or long, ~
                  but it is ~x0 instead."
      (primitive-type-kind in-type-right)))
    (guard?
     (and
      nonzero
      (cons
       'not
       (cons (cons 'equal
                   (cons (cons in-destructor-right '(operand-right))
                         '(0)))
             'nil))))
    (commutative-thm?
     (and
        commutative
        (cons 'defthm-commutative
              (cons (add-suffix name "-COMMUTATIVE")
                    (cons name
                          (cons ':hints
                                (cons commutative-hints 'nil))))))))
   (cons
    'define
    (cons
     name
     (cons
      (cons (cons 'operand-left
                  (cons in-predicate-left 'nil))
            (cons (cons 'operand-right
                        (cons in-predicate-right 'nil))
                  'nil))
      (append
       (and guard? (list :guard guard?))
       (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-left '(operand-left))
                           'nil))
                (cons
                 (cons
                   'y
                   (cons (cons in-destructor-right '(operand-right))
                         'nil))
                 'nil))
               (cons (cons out-constructor (cons operation 'nil))
                     'nil)))
             (cons
              ':hooks
              (cons
               '(:fix)
               (cons
                ':no-function
                (cons
                 't
                 (cons
                     '///
                     (and commutative
                          (list commutative-thm?))))))))))))))))))))