		Search-engine friendly clone of the ACL2 documentation.
Definterface-hash-implementation
Definterface-hash-fn

Events generated by definterface-hash.
Signature
(definterface-hash-fn name input-size-limit output-size name-bits name-bytes topic parents short long) → event?
Returns: event? — A ACL2::maybe-pseudo-event-formp.
Definitions and Theorems

Function: definterface-hash-fn
(defun definterface-hash-fn
       (name input-size-limit output-size name-bits
             name-bytes topic parents short long)
 (declare (xargs :guard t))
 (let ((__function__ 'definterface-hash-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                but it is ~x0 instead."
      name))
    ((unless (or (null input-size-limit)
                 (and (posp input-size-limit)
                      (integerp (/ input-size-limit 8)))))
     (raise
      "The :INPUT-SIZE-LIMIT must be NIL or ~
                a positive integer multiple of 8, ~
                but it is ~x0 instead."
      input-size-limit))
    (input-size-limit-/-8
         (if input-size-limit (/ input-size-limit 8)
           nil))
    ((unless (and (posp output-size)
                  (integerp (/ output-size 8))))
     (raise
      "The :OUTPUT-SIZE must be ~
                a positive integer multiple of 8, ~
                but it is ~x0 instead."
      output-size))
    (output-size-/-8 (/ output-size 8))
    ((unless (symbolp name-bits))
     (raise
      "The :NAME-BITS input must be a symbol, ~
                but it is ~x0 instead."
      name-bits))
    ((unless (symbolp name-bytes))
     (raise
      "The :NAME-BITS input must be a symbol, ~
                but it is ~x0 instead."
      name-bits))
    ((unless (symbolp topic))
     (raise
      "The :TOPIC input must be a symbol, ~
                but it is ~x0 instead."
      topic))
    (pkg (symbol-package-name name))
    (pkg (if (equal pkg *main-lisp-package-name*)
             "ACL2"
           pkg))
    (pkg-witness (pkg-witness pkg))
    (topic (or topic
               (add-suffix-to-fn name "-INTERFACE")))
    (name-bits (or name-bits
                   (add-suffix-to-fn name "-BITS")))
    (name-bytes (or name-bytes
                    (add-suffix-to-fn name "-BYTES")))
    (bit-listp-bits (acl2::packn-pos (list 'bit-list-of- name-bits)
                                     pkg-witness))
    (byte-listp-bytes
         (acl2::packn-pos (list 'byte-list-of- name-bytes)
                          pkg-witness))
    (len-bits (acl2::packn-pos (list 'len-of- name-bits)
                               pkg-witness))
    (len-bytes (acl2::packn-pos (list 'len-of- name-bytes)
                                pkg-witness))
    (true-listp-bits
         (acl2::packn-pos (list 'true-listp-of- name-bits)
                          pkg-witness))
    (true-listp-bytes
         (acl2::packn-pos (list 'true-listp-of- name-bytes)
                          pkg-witness))
    (consp-bits (acl2::packn-pos (list 'consp-of- name-bits)
                                 pkg-witness))
    (consp-bytes (acl2::packn-pos (list 'consp-of- name-bytes)
                                  pkg-witness))
    (guard-bits
      (if input-size-limit
        (cons 'and
              (cons '(bit-listp bits)
                    (cons (cons '<
                                (cons '(len bits)
                                      (cons input-size-limit 'nil)))
                          'nil)))
        '(bit-listp bits)))
    (guard-bytes
     (if input-size-limit
      (cons
          'and
          (cons '(byte-listp bytes)
                (cons (cons '<
                            (cons '(len bytes)
                                  (cons input-size-limit-/-8 'nil)))
                      'nil)))
      '(byte-listp bytes)))
    (sig-bits
     (cons
         (cons name-bits '(*))
         (cons '=>
               (cons '*
                     (cons ':formals
                           (cons '(bits)
                                 (cons ':guard
                                       (cons guard-bits 'nil))))))))
    (sig-bytes
     (cons
        (cons name-bytes '(*))
        (cons '=>
              (cons '*
                    (cons ':formals
                          (cons '(bytes)
                                (cons ':guard
                                      (cons guard-bytes 'nil))))))))
    (wit-bits
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         name-bits
         (cons
          '(bits)
          (cons
               '(declare (ignore bits))
               (cons (cons 'make-list
                           (cons output-size '(:initial-element 0)))
                     'nil)))))
       'nil)))
    (wit-bytes
     (cons
      'local
      (cons
       (cons
        'defun
        (cons
         name-bytes
         (cons
          '(bytes)
          (cons
           '(declare (ignore bytes))
           (cons (cons 'make-list
                       (cons output-size-/-8 '(:initial-element 0)))
                 'nil)))))
       'nil)))
    (bit-listp-thm
       (cons 'defrule
             (cons bit-listp-bits
                   (cons (cons 'bit-listp
                               (cons (cons name-bits '(bits)) 'nil))
                         'nil))))
    (byte-listp-thm
     (cons 'defrule
           (cons byte-listp-bytes
                 (cons (cons 'byte-listp
                             (cons (cons name-bytes '(bytes)) 'nil))
                       'nil))))
    (len-bits-thm
     (cons
      'defrule
      (cons
       len-bits
       (cons (cons 'equal
                   (cons (cons 'len
                               (cons (cons name-bits '(bits)) 'nil))
                         (cons output-size 'nil)))
             'nil))))
    (len-bytes-thm
     (cons
      'defrule
      (cons
       len-bytes
       (cons
           (cons 'equal
                 (cons (cons 'len
                             (cons (cons name-bytes '(bytes)) 'nil))
                       (cons output-size-/-8 'nil)))
           'nil))))
    (fix-bits-thms
         (cons 'fty::deffixequiv
               (cons name-bits '(:args ((bits bit-listp))))))
    (fix-bytes-thms (cons 'fty::deffixequiv
                          (cons name-bytes
                                '(:args ((bytes byte-listp))))))
    (true-listp-bits-thm
     (cons
      'defrule
      (cons
       true-listp-bits
       (cons
        (cons 'true-listp
              (cons (cons name-bits '(bits)) 'nil))
        '(:rule-classes
            :type-prescription
            :enable
            acl2::true-listp-when-bit-listp-compound-recognizer)))))
    (true-listp-bytes-thm
     (cons
      'defrule
      (cons
       true-listp-bytes
       (cons
        (cons 'true-listp
              (cons (cons name-bytes '(bytes)) 'nil))
        '(:rule-classes
           :type-prescription
           :enable
           acl2::true-listp-when-byte-listp-compound-recognizer)))))
    (consp-bits-thm
     (cons
      'defrule
      (cons
       consp-bits
       (cons
         (cons 'consp
               (cons (cons name-bits '(bits)) 'nil))
         (cons ':rule-classes
               (cons ':type-prescription
                     (cons ':use
                           (cons len-bits
                                 (cons ':disable
                                       (cons len-bits 'nil))))))))))
    (consp-bytes-thm
     (cons
      'defrule
      (cons
       consp-bytes
       (cons
        (cons 'consp
              (cons (cons name-bytes '(bytes)) 'nil))
        (cons ':rule-classes
              (cons ':type-prescription
                    (cons ':use
                          (cons len-bytes
                                (cons ':disable
                                      (cons len-bytes 'nil))))))))))
    (table-event
     (cons
      'table
      (cons
       *definterface-hash-table-name*
       (cons
           (cons 'quote (cons name 'nil))
           (cons (cons 'quote
                       (cons (make-definterface-hash-info
                                  :input-size-limit input-size-limit
                                  :output-size output-size)
                             'nil))
                 'nil))))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(logic)
      (cons
       (cons
        'defsection
        (cons
         topic
         (append
          (and parents (list :parents parents))
          (append
           (and short (list :short short))
           (append
            (and long (list :long long))
            (cons
             (cons
              'encapsulate
              (cons
               (cons sig-bits (cons sig-bytes 'nil))
               (cons
                wit-bits
                (cons
                 wit-bytes
                 (cons
                  bit-listp-thm
                  (cons
                   byte-listp-thm
                   (cons
                     len-bits-thm
                     (cons len-bytes-thm
                           (cons fix-bits-thms
                                 (cons fix-bytes-thms 'nil))))))))))
             (cons true-listp-bits-thm
                   (cons true-listp-bytes-thm
                         (cons consp-bits-thm
                               (cons consp-bytes-thm 'nil))))))))))
       (cons table-event 'nil))))))))