		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-operations

Defun-integer

Function definition macro specialized for C integer operations.

The ACL2 functions that model the C integer operations (and their guards) have a fairly uniform structure. This macro generates functions with that structure.

The arguments of this macro are:

name — The name of the function.
arg-type — The argument type, for a unary function. The name is always x.
arg1-type — The first argument type, for a binary function. The name is always x.
arg2-type — The second argument type, for a binary function. The name is always y.
guard — The guard, in addition to the argument type(s).
res-type — The result type.
short — The XDOC short string.
body — The body of the function.
guard-hints — Hints to verify guards.
no-fix — Do not generate fixing theorem when non-nil.

The presence (i.e. being non-nil) of arg-type determines whether the function is unary or binary.

Besides shortening the formulation of the function definitions, this macro results in both faster certification and faster inclusion compared to just using define, which is not much more verbose. Give the large number of functions generated in this file, the savings are significant.

Macro: defun-integer

(defmacro defun-integer
          (name &key arg-type
                arg1-type arg2-type guard res-type
                short body guard-hints no-fix prepwork)
 (cons
  'defsection
  (cons
   name
   (cons
    ':short
    (cons
     short
     (append
      prepwork
      (cons
       (cons
        'defun
        (cons
         name
         (cons
          (if arg-type '(x) '(x y))
          (cons
           (cons
            'declare
            (cons
             (cons
              'xargs
              (cons
               ':guard
               (cons
                (cons
                 'and
                 (append
                  (and arg-type
                       (cons (cons arg-type '(x)) 'nil))
                  (append
                     (and arg1-type
                          (cons (cons arg1-type '(x)) 'nil))
                     (append (and arg2-type
                                  (cons (cons arg2-type '(y)) 'nil))
                             (and guard (list guard))))))
                (and guard-hints
                     (cons ':guard-hints
                           (cons guard-hints 'nil))))))
             'nil))
           (cons body 'nil)))))
       (cons
        (cons
         'defthm
         (cons
             (pack res-type '-of- name)
             (cons (cons res-type
                         (cons (cons name (if arg-type '(x) '(x y)))
                               'nil))
                   'nil)))
        (append
         (and
          (not no-fix)
          (cons
           (cons
            'fty::deffixequiv
            (cons
             name
             (cons
              ':args
              (cons
                   (if arg-type (cons (cons 'x (cons arg-type 'nil))
                                      'nil)
                     (cons (cons 'x (cons arg1-type 'nil))
                           (cons (cons 'y (cons arg2-type 'nil))
                                 'nil)))
                   'nil))))
           'nil))
         (cons (cons 'in-theory
                     (cons (cons 'disable (cons name 'nil))
                           'nil))
               'nil))))))))))