		Search-engine friendly clone of the ACL2 documentation.
Defdigit-grouping-implementation
Defdigit-grouping-fn

Event generated by defdigit-grouping.
Signature
(defdigit-grouping-fn name smaller larger group-bendian group-lendian ungroup-bendian ungroup-lendian parents short long wrld) → event
Arguments: wrld — Guard (plist-worldp wrld).
Returns: event — A pseudo-event-formp.
Definitions and Theorems

Function: defdigit-grouping-fn
(defun defdigit-grouping-fn
       (name smaller larger group-bendian
             group-lendian ungroup-bendian
             ungroup-lendian parents short long wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'defdigit-grouping-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (raise
      "The NAME input must be a symbol, ~
                 but it is ~x0 instead."
      name))
    ((unless (symbolp smaller))
     (raise
      "The :SMALLER input must be a symbol, ~
                 but it is ~x0 instead."
      smaller))
    (pair (assoc-eq smaller
                    (table-alist *defdigits-table-name* wrld)))
    ((unless pair)
     (raise
      "The :SMALLER input ~x0 must be the name of ~
                an existing DEFDIGITS, but it is not."
      smaller))
    ((defdigits-info smaller) (cdr pair))
    ((unless (symbolp larger))
     (raise
      "The :LARGER input must be a symbol, ~
                 but it is ~x0 instead."
      larger))
    (pair (assoc-eq larger
                    (table-alist *defdigits-table-name* wrld)))
    ((unless pair)
     (raise
      "The :LARGER input ~x0 must be the name of ~
                an existing DEFDIGITS, but it is not."
      larger))
    ((defdigits-info larger) (cdr pair))
    (exp? (defdigit-grouping-find-exp smaller.base larger.base))
    ((unless exp?)
     (raise
      "The :LARGER input ~x0 must be a positive power of ~
                the :SMALLER input ~x1, but it is not."
      larger smaller))
    (exp exp?)
    ((when (= exp 1))
     (raise
      "The :LARGER input ~x0 must be a positive power of ~
                the :SMALLER input ~x1 and must be larger, ~
                but this is not the case."
      larger smaller))
    ((unless (symbolp group-bendian))
     (raise
      "The :GROUP-BENDIAN input must be a symbol, ~
                 but it is ~x0 instead."
      group-bendian))
    ((unless (symbolp group-lendian))
     (raise
      "The :GROUP-LENDIAN input must be a symbol, ~
                 but it is ~x0 instead."
      group-lendian))
    ((unless (symbolp ungroup-bendian))
     (raise
      "The :UNGROUP-BENDIAN input must be a symbol, ~
                 but it is ~x0 instead."
      ungroup-bendian))
    ((unless (symbolp ungroup-lendian))
     (raise
      "The :UNGROUP-LENDIAN input must be a symbol, ~
                 but it is ~x0 instead."
      ungroup-lendian))
    (len-of-group-bendian (packn-pos (list 'len-of- group-bendian)
                                     name))
    (len-of-group-lendian (packn-pos (list 'len-of- group-lendian)
                                     name))
    (len-of-ungroup-bendian
         (packn-pos (list 'len-of- ungroup-bendian)
                    name))
    (len-of-ungroup-lendian
         (packn-pos (list 'len-of- ungroup-lendian)
                    name))
    (digits (packn-pos (list "DIGITS") name))
    (new-digits (packn-pos (list "NEW-DIGITS") name))
    (group-bendian-event
     (cons
      'define
      (cons
       group-bendian
       (cons
        (cons (cons digits (cons smaller.digits-pred 'nil))
              'nil)
        (cons
         ':guard
         (cons
          (cons 'integerp
                (cons (cons '/
                            (cons (cons 'len (cons digits 'nil))
                                  (cons exp 'nil)))
                      'nil))
          (cons
           ':returns
           (cons
            (cons
             new-digits
             (cons
              larger.digits-pred
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    (cons
                        'quote
                        (cons (cons group-bendian
                                    (cons larger.digits-pred-correct
                                          '(return-type-of-group-bendian
                                                (:e dab-base-fix)
                                                (:e pos-fix)
                                                (:e expt))))
                              'nil))
                    'nil)))
                 'nil)
                'nil))))
            (cons
             ':parents
             (cons
              (cons name 'nil)
              (cons
               ':short
               (cons
                (cons
                   'xdoc::topstring
                   (cons '"Group "
                         (cons smaller.digits-description
                               (cons '" into "
                                     (cons larger.digits-description
                                           '(", big-endian."))))))
                (cons
                 (cons 'group-bendian
                       (cons smaller.base
                             (cons exp (cons digits 'nil))))
                 (cons
                  ':guard-hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                         (cons
                           smaller.digits-pred-correct
                           '((:e dab-basep) (:e posp) (:e pos-fix)))
                         'nil))
                       'nil)))
                    'nil)
                   (cons
                    '///
                    (cons
                     (cons
                      'fty::deffixequiv
                      (cons
                       group-bendian
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons (cons smaller.digits-fix-correct
                                          (cons group-bendian
                                                '(group-bendian-of-dab-digit-list-fix-digits)))
                                    'nil))
                             'nil)))
                          'nil)
                         'nil))))
                     'nil)))))))))))))))))
    (group-lendian-event
     (cons
      'define
      (cons
       group-lendian
       (cons
        (cons (cons digits (cons smaller.digits-pred 'nil))
              'nil)
        (cons
         ':guard
         (cons
          (cons 'integerp
                (cons (cons '/
                            (cons (cons 'len (cons digits 'nil))
                                  (cons exp 'nil)))
                      'nil))
          (cons
           ':returns
           (cons
            (cons
             new-digits
             (cons
              larger.digits-pred
              (cons
               ':hints
               (cons
                (cons
                 (cons
                  '"Goal"
                  (cons
                   ':in-theory
                   (cons
                    (cons
                        'quote
                        (cons (cons group-lendian
                                    (cons larger.digits-pred-correct
                                          '(return-type-of-group-lendian
                                                (:e dab-base-fix)
                                                (:e pos-fix)
                                                (:e expt))))
                              'nil))
                    'nil)))
                 'nil)
                'nil))))
            (cons
             ':parents
             (cons
              (cons name 'nil)
              (cons
               ':short
               (cons
                (cons
                  'xdoc::topstring
                  (cons '"Group "
                        (cons smaller.digits-description
                              (cons '" into "
                                    (cons larger.digits-description
                                          '(", little-endian."))))))
                (cons
                 (cons 'group-lendian
                       (cons smaller.base
                             (cons exp (cons digits 'nil))))
                 (cons
                  ':guard-hints
                  (cons
                   (cons
                    (cons
                     '"Goal"
                     (cons
                      ':in-theory
                      (cons
                       (cons
                        'quote
                        (cons
                         (cons
                           smaller.digits-pred-correct
                           '((:e dab-basep) (:e posp) (:e pos-fix)))
                         'nil))
                       'nil)))
                    'nil)
                   (cons
                    '///
                    (cons
                     (cons
                      'fty::deffixequiv
                      (cons
                       group-lendian
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"Goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'quote
                              (cons (cons smaller.digits-fix-correct
                                          (cons group-lendian
                                                '(group-lendian-of-dab-digit-list-fix-digits)))
                                    'nil))
                             'nil)))
                          'nil)
                         'nil))))
                     'nil)))))))))))))))))
    (ungroup-bendian-event
     (cons
      'define
      (cons
       ungroup-bendian
       (cons
        (cons (cons digits (cons larger.digits-pred 'nil))
              'nil)
        (cons
         ':returns
         (cons
          (cons
           new-digits
           (cons
            smaller.digits-pred
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                     (cons ungroup-bendian
                           (cons smaller.digits-pred-correct
                                 '(return-type-of-ungroup-bendian)))
                     'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
                  'xdoc::topstring
                  (cons '"Ungroup "
                        (cons larger.digits-description
                              (cons '" into "
                                    (cons smaller.digits-description
                                          '(", big-endian."))))))
              (cons
               (cons 'ungroup-bendian
                     (cons smaller.base
                           (cons exp (cons digits 'nil))))
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                        (cons 'quote
                              (cons (cons larger.digits-pred-correct
                                          '((:e dab-basep)
                                            (:e dab-base-fix)
                                            (:e posp)
                                            (:e pos-fix)
                                            (:e expt)))
                                    'nil))
                        'nil)))
                  'nil)
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     ungroup-bendian
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons
                                 (cons larger.digits-fix-correct
                                       (cons ungroup-bendian
                                             '(ungroup-bendian-of-dab-digit-list-fix-digits
                                                   (:e dab-base-fix)
                                                   (:e pos-fix)
                                                   (:e expt))))
                                 'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (ungroup-lendian-event
     (cons
      'define
      (cons
       ungroup-lendian
       (cons
        (cons (cons digits (cons larger.digits-pred 'nil))
              'nil)
        (cons
         ':returns
         (cons
          (cons
           new-digits
           (cons
            smaller.digits-pred
            (cons
             ':hints
             (cons
              (cons
               (cons
                '"Goal"
                (cons
                 ':in-theory
                 (cons
                  (cons
                   'quote
                   (cons
                     (cons ungroup-lendian
                           (cons smaller.digits-pred-correct
                                 '(return-type-of-ungroup-lendian)))
                     'nil))
                  'nil)))
               'nil)
              'nil))))
          (cons
           ':parents
           (cons
            (cons name 'nil)
            (cons
             ':short
             (cons
              (cons
                  'xdoc::topstring
                  (cons '"Ungroup "
                        (cons larger.digits-description
                              (cons '" into "
                                    (cons smaller.digits-description
                                          '(", little-endian."))))))
              (cons
               (cons 'ungroup-lendian
                     (cons smaller.base
                           (cons exp (cons digits 'nil))))
               (cons
                ':guard-hints
                (cons
                 (cons
                  (cons
                   '"Goal"
                   (cons
                    ':in-theory
                    (cons
                        (cons 'quote
                              (cons (cons larger.digits-pred-correct
                                          '((:e dab-basep)
                                            (:e dab-base-fix)
                                            (:e posp)
                                            (:e pos-fix)
                                            (:e expt)))
                                    'nil))
                        'nil)))
                  'nil)
                 (cons
                  '///
                  (cons
                   (cons
                    'fty::deffixequiv
                    (cons
                     ungroup-lendian
                     (cons
                      ':hints
                      (cons
                       (cons
                        (cons
                         '"Goal"
                         (cons
                          ':in-theory
                          (cons
                           (cons
                            'quote
                            (cons
                                 (cons larger.digits-fix-correct
                                       (cons ungroup-lendian
                                             '(ungroup-lendian-of-dab-digit-list-fix-digits
                                                   (:e dab-base-fix)
                                                   (:e pos-fix)
                                                   (:e expt))))
                                 'nil))
                           'nil)))
                        'nil)
                       'nil))))
                   'nil)))))))))))))))
    (len-of-group-bendian-event
     (cons
      'defrule
      (cons
       len-of-group-bendian
       (cons
        (cons
           'equal
           (cons (cons 'len
                       (cons (cons group-bendian (cons digits 'nil))
                             'nil))
                 (cons (cons 'ceiling
                             (cons (cons 'len (cons digits 'nil))
                                   (cons exp 'nil)))
                       'nil)))
        (cons
         ':in-theory
         (cons
             (cons 'quote
                   (cons (cons group-bendian
                               '(len-of-group-bendian (:e pos-fix)))
                         'nil))
             'nil))))))
    (len-of-group-lendian-event
     (cons
      'defrule
      (cons
       len-of-group-lendian
       (cons
        (cons
           'equal
           (cons (cons 'len
                       (cons (cons group-lendian (cons digits 'nil))
                             'nil))
                 (cons (cons 'ceiling
                             (cons (cons 'len (cons digits 'nil))
                                   (cons exp 'nil)))
                       'nil)))
        (cons
         ':in-theory
         (cons
             (cons 'quote
                   (cons (cons group-lendian
                               '(len-of-group-lendian (:e pos-fix)))
                         'nil))
             'nil))))))
    (len-of-ungroup-bendian-event
     (cons
      'defrule
      (cons
       len-of-ungroup-bendian
       (cons
        (cons
         'equal
         (cons (cons 'len
                     (cons (cons ungroup-bendian (cons digits 'nil))
                           'nil))
               (cons (cons '*
                           (cons (cons 'len (cons digits 'nil))
                                 (cons exp 'nil)))
                     'nil)))
        (cons
         ':in-theory
         (cons
           (cons 'quote
                 (cons (cons ungroup-bendian
                             '(len-of-ungroup-bendian (:e pos-fix)))
                       'nil))
           'nil))))))
    (len-of-ungroup-lendian-event
     (cons
      'defrule
      (cons
       len-of-ungroup-lendian
       (cons
        (cons
         'equal
         (cons (cons 'len
                     (cons (cons ungroup-lendian (cons digits 'nil))
                           'nil))
               (cons (cons '*
                           (cons (cons 'len (cons digits 'nil))
                                 (cons exp 'nil)))
                     'nil)))
        (cons
         ':in-theory
         (cons
           (cons 'quote
                 (cons (cons ungroup-lendian
                             '(len-of-ungroup-lendian (:e pos-fix)))
                       'nil))
           'nil))))))
    (name-event
      (cons 'defxdoc
            (cons name
                  (append (and parents (list :parents parents))
                          (append (and short (list :short short))
                                  (and long (list :long long))))))))
   (cons
    'encapsulate
    (cons
     'nil
     (cons
      '(logic)
      (cons
       '(evmac-prepare-proofs)
       (cons
        group-bendian-event
        (cons
         group-lendian-event
         (cons
          ungroup-bendian-event
          (cons
           ungroup-lendian-event
           (cons
             len-of-group-bendian-event
             (cons len-of-group-lendian-event
                   (cons len-of-ungroup-bendian-event
                         (cons len-of-ungroup-lendian-event
                               (cons name-event 'nil))))))))))))))))