bitstruct

(in-package "FTY")

(include-book "fixtype")

(include-book "fixequiv")

(include-book "fty-parseutils")

(include-book "std/util/define" :dir :system)

(include-book "ihs/basic-definitions" :dir :system)

(include-book "basetypes")

(include-book "std/basic/arith-equiv-defs" :dir :system)

(include-book "bitstruct-theory")

(include-book "misc/without-waterfall-parallelism" :dir :system)

(local (include-book "centaur/bitops/equal-by-logbitp" :dir :system))

(local (include-book "centaur/bitops/ihsext-basics" :dir :system))

(local (include-book "arithmetic/top-with-meta" :dir :system))

(local (in-theory (disable part-install part-select)))

(program)

(def-primitive-aggregate bitstruct-field
  (name width
    lsb
    accessor
    updater
    type
    pred
    fix
    equiv
    fullp
    signedp
    rule-classes
    doc
    subfield-hierarchy
    kwd-alist))

(defconst *bitstruct-field-keywords*
  '(:accessor :updater :default :subfields :rule-classes))

(def-primitive-aggregate bitstruct
  (name fields
    width
    pred
    fix
    equiv
    xvar
    fullp
    kwd-alist
    orig-fields
    signedp
    inline
    defs-ruleset
    r-o-w-ruleset
    update-to-ctor-ruleset
    extra-binder-names
    equiv-under-mask))

(defconst *defbitstruct-keywords*
  '(:pred :fix :equiv :xvar :signedp :inline :fullp :parents :short :long :msb-first :extra-binder-names))

(define lookup-bitstruct
  (name bitstruct-table)
  (cond ((atom bitstruct-table) nil)
    ((eq name (caar bitstruct-table)) (cdar bitstruct-table))
    ((eq name
       (bitstruct->pred (cdar bitstruct-table))) (cdar bitstruct-table))
    (t (lookup-bitstruct name (cdr bitstruct-table)))))

(defines parse-bitstruct-subfields
  (define parse-bitstruct-subfields
    (subfield-treelst fields
      hier
      lsb
      x.name
      bitstruct-table)
    (if (atom fields)
      (and (consp subfield-treelst)
        (raise "Bad subfield tree: ran out of primary fields under ~x0"
          hier))
      (if (bitstruct-field->subfield-hierarchy (car fields))
        (parse-bitstruct-subfields subfield-treelst
          (cdr fields)
          hier
          lsb
          x.name
          bitstruct-table)
        (append (parse-bitstruct-subfield (car subfield-treelst)
            (car fields)
            hier
            lsb
            x.name
            bitstruct-table)
          (parse-bitstruct-subfields (cdr subfield-treelst)
            (cdr fields)
            hier
            lsb
            x.name
            bitstruct-table)))))
  (define parse-bitstruct-subsubfield
    (subfield-treelst field
      hier
      lsb
      x.name
      bitstruct-table)
    (b* (((bitstruct-field field)) (type (lookup-bitstruct field.type bitstruct-table))
        ((unless type) (raise "Didn't find bitstruct type for field ~x0 at ~x1"
            field.name
            hier))
        ((bitstruct type)))
      (parse-bitstruct-subfields subfield-treelst
        type.fields
        hier
        x.name
        (+ lsb field.lsb)
        bitstruct-table)))
  (define parse-bitstruct-subfield
    (subfield-tree field
      hier
      lsb
      x.name
      bitstruct-table)
    (b* (((unless subfield-tree) nil) ((bitstruct-field field))
        (hier (cons field hier))
        ((mv subfield-name sub-subfields) (if (consp subfield-tree)
            (mv (car subfield-tree)
              (parse-bitstruct-subsubfield (cdr subfield-tree)
                field
                hier
                lsb
                x.name
                bitstruct-table))
            (mv subfield-tree nil))))
      (cons (make-bitstruct-field :name subfield-name
          :width field.width
          :lsb (+ lsb field.lsb)
          :accessor (intern-in-package-of-symbol (cat (symbol-name x.name)
              "->"
              (symbol-name subfield-name))
            x.name)
          :updater (intern-in-package-of-symbol (cat "!"
              (symbol-name x.name)
              "->"
              (symbol-name subfield-name))
            x.name)
          :rule-classes field.rule-classes
          :type field.type
          :pred field.pred
          :fix field.fix
          :fullp t
          :equiv field.equiv
          :signedp field.signedp
          :subfield-hierarchy hier
          :kwd-alist nil)
        sub-subfields))))

(define parse-bitstruct-field
  (x lsb structname bitstruct-table)
  (b* (((unless (>= (len x) 2)) (raise "Malformed bitstruct field: must have at least a field name and a type: ~x0"
         x)) ((list* fieldname type rest) x)
      ((mv field-kwd-alist docs) (extract-keywords fieldname
          *bitstruct-field-keywords*
          rest
          nil))
      (doc (if (atom docs)
          nil
          (car docs)))
      ((unless (or (not doc) (stringp doc))) (raise "Found ~x0 in place of a doc string in bitstruct field ~x1"
          doc
          x))
      (accessor (getarg! :accessor (intern-in-package-of-symbol (cat (symbol-name structname)
              "->"
              (symbol-name fieldname))
            structname)
          field-kwd-alist))
      (updater (getarg! :updater (intern-in-package-of-symbol (cat "!"
              (symbol-name structname)
              "->"
              (symbol-name fieldname))
            structname)
          field-kwd-alist))
      (rule-classes (getarg :rule-classes :rewrite field-kwd-alist))
      (bitstruct (lookup-bitstruct type bitstruct-table))
      ((unless bitstruct) (raise "In field ~x0, ~x1 is not a valid bitstruct type"
          x
          type))
      ((bitstruct bitstruct))
      (field (make-bitstruct-field :name fieldname
          :width bitstruct.width
          :lsb lsb
          :fullp bitstruct.fullp
          :accessor accessor
          :updater updater
          :rule-classes rule-classes
          :type bitstruct.name
          :pred bitstruct.pred
          :fix bitstruct.fix
          :doc doc
          :equiv bitstruct.equiv
          :signedp bitstruct.signedp
          :kwd-alist field-kwd-alist))
      (subfield-treelst (getarg :subfields nil field-kwd-alist))
      (subfields (and subfield-treelst
          (parse-bitstruct-subfields subfield-treelst
            bitstruct.fields
            (list field)
            lsb
            structname
            bitstruct-table))))
    (cons field subfields)))

(table bitstruct-table
  'bit
  (make-bitstruct :name 'bit
    :width 1
    :pred 'bitp
    :fix 'bfix
    :equiv 'bit-equiv
    :fullp t))

(table bitstruct-table
  'boolean
  (make-bitstruct :name 'boolean
    :width 1
    :pred 'booleanp
    :fix 'bool-fix
    :equiv 'iff
    :fullp t))

(define parse-bitstruct-fields-aux
  (x lsb structname bitstruct-table)
  (b* (((when (atom x)) (mv nil lsb t)) (fields (parse-bitstruct-field (car x)
          lsb
          structname
          bitstruct-table))
      ((bitstruct-field field1) (car fields))
      ((mv rest width fullp) (parse-bitstruct-fields-aux (cdr x)
          (+ lsb field1.width)
          structname
          bitstruct-table)))
    (mv (append fields rest)
      width
      (and fullp field1.fullp))))

(define parse-bitstruct-fields
  (x lsb structname bitstruct-table)
  (if (natp x)
    (mv nil x t)
    (parse-bitstruct-fields-aux x
      lsb
      structname
      bitstruct-table)))

(define bitstruct-primary-fields->names
  (x)
  (if (atom x)
    nil
    (if (bitstruct-field->subfield-hierarchy (car x))
      (bitstruct-primary-fields->names (cdr x))
      (cons (bitstruct-field->name (car x))
        (bitstruct-primary-fields->names (cdr x))))))

(define bitstruct-fields->names
  (x)
  (if (atom x)
    nil
    (cons (bitstruct-field->name (car x))
      (bitstruct-fields->names (cdr x)))))

(define bitstruct-fields->accessors
  (x)
  (if (atom x)
    nil
    (cons (bitstruct-field->accessor (car x))
      (bitstruct-fields->accessors (cdr x)))))

(define parse-defbitstruct
  (x bitstruct-table)
  (b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed defbitstruct: ~x0: name must be a symbol"
          x))
      ((mv pre-/// post-///) (split-/// name args))
      ((mv kwd-alist fields) (extract-keywords name
          *defbitstruct-keywords*
          pre-///
          nil))
      ((when (atom fields)) (raise "In defbitstruct ~x0: List of fields is missing~%"
          name))
      ((when (consp (cdr fields))) (raise "In defbitstruct ~x0: More than one list of fields present~%"
          name))
      (orig-fields (car fields))
      (pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
            name)
          kwd-alist))
      (fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
            name)
          kwd-alist))
      (equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
            name)
          kwd-alist))
      (fullp (getarg :fullp t kwd-alist))
      (signedp (getarg :signedp nil kwd-alist))
      (inline (getarg :inline nil kwd-alist))
      (msb-first (getarg :msb-first nil kwd-alist))
      (xvar (or (getarg :xvar nil kwd-alist)
          (intern-in-package-of-symbol "X" name)))
      ((mv fields width fields-fullp) (parse-bitstruct-fields (if msb-first
            (rev orig-fields)
            orig-fields)
          0
          name
          bitstruct-table)))
    (make-bitstruct :name name
      :pred pred
      :fix fix
      :fullp (and fullp fields-fullp)
      :equiv equiv
      :width width
      :fields fields
      :xvar xvar
      :signedp signedp
      :inline inline
      :kwd-alist (list* (cons :///-events post-///) kwd-alist)
      :orig-fields orig-fields
      :defs-ruleset (intern-in-package-of-symbol (cat (symbol-name name) "-DEFS")
        name)
      :r-o-w-ruleset (intern-in-package-of-symbol (cat (symbol-name name) "-READ-OVER-WRITE")
        name)
      :update-to-ctor-ruleset (intern-in-package-of-symbol (cat (symbol-name name) "-UPDATERS-TO-CTOR")
        name)
      :equiv-under-mask (intern-in-package-of-symbol (cat (symbol-name equiv) "-UNDER-MASK")
        name))))

(define bitstruct-accessor-term-logic-form
  (field xvar)
  (b* (((bitstruct-field field)) (logic-form-base `(part-select ,FTY::XVAR
          :low ,FTY::FIELD.LSB
          :width ,FTY::FIELD.WIDTH)))
    (cond ((eq field.pred 'booleanp) `(bit->bool ,FTY::LOGIC-FORM-BASE))
      (field.signedp `(logext ,FTY::FIELD.WIDTH ,FTY::LOGIC-FORM-BASE))
      (t logic-form-base))))

(define bitstruct-accessor-term-exec-form
  (fullwidth fullsigned field xvar)
  (b* (((bitstruct-field field)) (widthleft (- fullwidth field.lsb))
      (field-type (if field.signedp
          'signed-byte
          'unsigned-byte))
      (full-type (if fullsigned
          'signed-byte
          'unsigned-byte))
      (exec-form-base (if (eql field.lsb 0)
          `(the (,FTY::FULL-TYPE ,FTY::FULLWIDTH) ,FTY::XVAR)
          `(the (,FTY::FULL-TYPE ,FTY::WIDTHLEFT)
            (ash (the (,FTY::FULL-TYPE ,FTY::FULLWIDTH) ,FTY::XVAR)
              ,(- FTY::FIELD.LSB)))))
      (exec-form `(the (,FTY::FIELD-TYPE ,FTY::FIELD.WIDTH)
          ,(IF FTY::FIELD.SIGNEDP
     `(FTY::FAST-LOGEXT ,FTY::FIELD.WIDTH ,FTY::EXEC-FORM-BASE)
     `(LOGAND
       (THE (,FTY::FIELD-TYPE ,FTY::FIELD.WIDTH)
            ,(1- (EXPT 2 FTY::FIELD.WIDTH)))
       ,FTY::EXEC-FORM-BASE)))))
    (if (eq field.pred 'booleanp)
      `(bit->bool ,FTY::EXEC-FORM)
      exec-form)))

(define bitstruct-field-preds
  (fields xvar)
  (b* (((when (atom fields)) nil) ((bitstruct-field field) (car fields))
      (rest (bitstruct-field-preds (cdr fields) xvar))
      ((when field.fullp) rest))
    (cons `(,FTY::FIELD.PRED ,(FTY::BITSTRUCT-ACCESSOR-TERM-LOGIC-FORM FTY::FIELD FTY::XVAR))
      rest)))

(define bitstruct-pred
  (x)
  (b* (((bitstruct x)) (short (cat "Recognizer for @(see "
          (full-escape-symbol x.name)
          ") bit structures."))
      (def (if x.signedp
          `(signed-byte-p ,FTY::X.WIDTH ,FTY::X.XVAR)
          `(unsigned-byte-p ,FTY::X.WIDTH ,FTY::X.XVAR)))
      (field-preds (bitstruct-field-preds x.fields x.xvar))
      (base-def `(mbe :logic ,FTY::DEF
          :exec ,(IF FTY::X.SIGNEDP
     `(AND (INTEGERP ,FTY::X.XVAR)
           (<= ,(- (ASH 1 (1- FTY::X.WIDTH))) ,FTY::X.XVAR)
           (< ,FTY::X.XVAR ,(ASH 1 (1- FTY::X.WIDTH))))
     `(AND (FTY::NATP ,FTY::X.XVAR) (< ,FTY::X.XVAR ,(ASH 1 FTY::X.WIDTH))))))
      (full-def (if field-preds
          `(and ,FTY::BASE-DEF . ,FTY::FIELD-PREDS)
          base-def)))
    `(define ,FTY::X.PRED
      (,FTY::X.XVAR)
      :parents (,FTY::X.NAME)
      :short ,FTY::SHORT
      :progn t
      :guard-hints (("goal" :in-theory (enable unsigned-byte-p signed-byte-p)))
      ,FTY::FULL-DEF
      ///
      ,@(AND FTY::X.FULLP
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::X.PRED)
             (IF FTY::X.SIGNEDP
                 "-WHEN-SIGNED-BYTE-P"
                 "-WHEN-UNSIGNED-BYTE-P"))
            FTY::X.NAME)
          (FTY::IMPLIES ,FTY::DEF (,FTY::X.PRED ,FTY::X.XVAR)))))
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT
   (IF FTY::X.SIGNEDP
       "SIGNED-BYTE-P-WHEN-"
       "UNSIGNED-BYTE-P-WHEN-")
   (SYMBOL-NAME FTY::X.PRED))
  FTY::X.NAME)
        (implies (,FTY::X.PRED ,FTY::X.XVAR) ,FTY::DEF))
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT (SYMBOL-NAME FTY::X.PRED) "-COMPOUND-RECOGNIZER") FTY::X.NAME)
        (implies (,FTY::X.PRED ,FTY::X.XVAR)
          (,(IF FTY::X.SIGNEDP
     'INTEGERP
     'FTY::NATP) ,FTY::X.XVAR))
        :rule-classes :compound-recognizer))))

(define bitstruct-fields-fix
  (fields xvar)
  (b* (((when (atom fields)) xvar) ((bitstruct-field field) (car fields))
      ((when field.subfield-hierarchy) (bitstruct-fields-fix (cdr fields) xvar))
      (sel `(part-select ,FTY::XVAR
          :width ,FTY::FIELD.WIDTH
          :low ,FTY::FIELD.LSB))
      (signed (if field.signedp
          `(logext ,FTY::FIELD.WIDTH ,FTY::SEL)
          sel))
      (fix (if field.fullp
          signed
          `(,FTY::FIELD.FIX ,FTY::SIGNED)))
      ((when (atom (cdr fields))) fix))
    `(logapp ,FTY::FIELD.WIDTH
      ,FTY::FIX
      ,(FTY::BITSTRUCT-FIELDS-FIX (CDR FTY::FIELDS) FTY::XVAR))))

(define bitstruct-fix
  (x)
  (b* (((bitstruct x)) (short (cat "Fixing function for @(see "
          (full-escape-symbol x.name)
          ") bit structures."))
      (x-fields-fixed (if x.fullp
          x.xvar
          (bitstruct-fields-fix x.fields x.xvar)))
      (x-length-fixed (cond (x.signedp `(logext ,FTY::X.WIDTH ,FTY::X-FIELDS-FIXED))
          (t `(loghead ,FTY::X.WIDTH ,FTY::X-FIELDS-FIXED)))))
    `(define ,FTY::X.FIX
      ((,FTY::X.XVAR ,FTY::X.PRED))
      :guard-hints (("goal" :in-theory (enable loghead-identity
           logext-identity
           logext-part-select-at-0-identity
           ,@(AND (NOT FTY::X.FULLP) `(,FTY::X.PRED)))))
      :parents (,FTY::X.NAME)
      :short ,FTY::SHORT
      :returns (fixed ,FTY::X.PRED
        ,@(AND (NOT FTY::X.FULLP)
       `(:HINTS
         (("goal" :IN-THEORY
           (FTY::ENABLE ,FTY::X.PRED
            FTY::PART-SELECT-AT-0-OF-UNSIGNED-BYTE-IDENTITY
            FTY::LOGEXT-PART-SELECT-AT-0-IDENTITY))))))
      :progn t
      (mbe :logic ,FTY::X-LENGTH-FIXED :exec ,FTY::X.XVAR)
      ///
      (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (FTY::CAT (SYMBOL-NAME FTY::X.FIX) "-WHEN-" (SYMBOL-NAME FTY::X.PRED))
  FTY::X.NAME)
        (implies (,FTY::X.PRED ,FTY::X.XVAR)
          (equal (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR))
        :hints (("Goal" :in-theory (enable loghead-identity
             logext-identity
             logext-part-select-at-0-identity
             ,@(AND (NOT FTY::X.FULLP) `(,FTY::X.PRED))))))
      (local (in-theory (disable ,FTY::X.FIX)))
      (deffixtype ,FTY::X.NAME
        :pred ,FTY::X.PRED
        :fix ,FTY::X.FIX
        :equiv ,FTY::X.EQUIV
        :define t))))

(define bitstruct-fields->ctor-formals
  (fields)
  (if (atom fields)
    nil
    (b* (((bitstruct-field field) (car fields)) ((when field.subfield-hierarchy) (bitstruct-fields->ctor-formals (cdr fields))))
      (cons (list field.name field.pred)
        (bitstruct-fields->ctor-formals (cdr fields))))))

(define bitstruct-fields->ctor-fixes
  (fields)
  (if (atom fields)
    nil
    (b* (((bitstruct-field field) (car fields)) ((when field.subfield-hierarchy) (bitstruct-fields->ctor-fixes (cdr fields))))
      (cons `(,FTY::FIELD.NAME ,(IF (EQ FTY::FIELD.PRED 'FTY::BOOLEANP)
     `(BOOL->BIT ,FTY::FIELD.NAME)
     `(FTY::MBE :LOGIC (,FTY::FIELD.FIX ,FTY::FIELD.NAME) :EXEC
       ,FTY::FIELD.NAME)))
        (bitstruct-fields->ctor-fixes (cdr fields))))))

(define bitstruct-fields->ctor-body
  (fields signedp)
  (b* (((when (atom fields)) nil) ((bitstruct-field field) (car fields))
      (rest (bitstruct-fields->ctor-body (cdr fields)
          signedp))
      ((when field.subfield-hierarchy) rest)
      ((when (not rest)) (if (iff signedp field.signedp)
          field.name
          (if signedp
            `(logext ,FTY::FIELD.WIDTH ,FTY::FIELD.NAME)
            `(loghead ,FTY::FIELD.WIDTH ,FTY::FIELD.NAME)))))
    `(logapp ,FTY::FIELD.WIDTH ,FTY::FIELD.NAME ,REST)))

(define bitstruct-fields->defaults
  (fields)
  (if (atom fields)
    nil
    (b* (((bitstruct-field field) (car fields)) ((when field.subfield-hierarchy) (bitstruct-fields->defaults (cdr fields))))
      (cons (or (cdr (assoc :default field.kwd-alist))
          (if (eq field.pred 'booleanp)
            nil
            0))
        (bitstruct-fields->defaults (cdr fields))))))

(define bitstruct-ctor
  (x)
  (b* (((bitstruct x)) (fieldnames (bitstruct-primary-fields->names x.fields)))
    `(define ,FTY::X.NAME
      ,(FTY::BITSTRUCT-FIELDS->CTOR-FORMALS FTY::X.FIELDS)
      :parents nil
      :returns (,FTY::X.NAME ,FTY::X.PRED
        ,@(AND (NOT FTY::X.FULLP)
       `(:HINTS
         (("goal" :IN-THEORY
           (FTY::ENABLE ,FTY::X.PRED
            FTY::PART-SELECT-AT-0-OF-UNSIGNED-BYTE-IDENTITY
            FTY::LOGEXT-PART-SELECT-AT-0-IDENTITY))))))
      :progn t
      (b* ,(FTY::BITSTRUCT-FIELDS->CTOR-FIXES FTY::X.FIELDS)
        ,(FTY::BITSTRUCT-FIELDS->CTOR-BODY FTY::X.FIELDS FTY::X.SIGNEDP))
      ///
      (deffixequiv ,FTY::X.NAME)
      ,(STD::DA-MAKE-MAKER FTY::X.NAME FTY::FIELDNAMES
  (FTY::BITSTRUCT-FIELDS->DEFAULTS FTY::X.FIELDS))
      ,(STD::DA-MAKE-CHANGER FTY::X.NAME FTY::FIELDNAMES NIL))))

(define bitstruct-equiv-under-mask
  (x)
  (b* (((bitstruct x)) (xvar1 (intern-in-package-of-symbol (cat (symbol-name x.xvar) "1")
          x.name))
      (mask (intern-in-package-of-symbol "MASK" x.name)))
    `(define ,FTY::X.EQUIV-UNDER-MASK
      ((,FTY::X.XVAR ,FTY::X.PRED) (,FTY::XVAR1 ,FTY::X.PRED)
        (,FTY::MASK integerp))
      (int-equiv-under-mask (,FTY::X.FIX ,FTY::X.XVAR)
        (,FTY::X.FIX ,FTY::XVAR1)
        ,FTY::MASK))))

(define bitstruct-subfield-accessor-form
  (hier xvar)
  (b* (((when (atom hier)) xvar) (subterm (bitstruct-subfield-accessor-form (cdr hier)
          xvar))
      ((bitstruct-field field) (car hier)))
    `(,FTY::FIELD.ACCESSOR ,FTY::SUBTERM)))

(define bitstruct-subfield-accessor-fns
  (hier)
  (b* (((when (atom hier)) nil) ((bitstruct-field field) (car hier)))
    (cons field.accessor
      (bitstruct-subfield-accessor-fns (cdr hier)))))

(define bitstruct-field-accessor
  (field x)
  (b* (((bitstruct x)) ((bitstruct-field field))
      (short (cat "Access the "
          (full-escape-symbol field.name)
          " field of a @(see "
          (full-escape-symbol x.name)
          ") bit structure."))
      (logic-form (bitstruct-accessor-term-logic-form field
          x.xvar))
      (exec-form (bitstruct-accessor-term-exec-form x.width
          x.signedp
          field
          x.xvar))
      (logic-form (cond (field.subfield-hierarchy (bitstruct-subfield-accessor-form field.subfield-hierarchy
              x.xvar))
          (t logic-form)))
      (subfield-accs (bitstruct-subfield-accessor-fns field.subfield-hierarchy))
      (fieldnames (bitstruct-primary-fields->names x.fields)))
    `(define ,FTY::FIELD.ACCESSOR
      ((,FTY::X.XVAR ,FTY::X.PRED))
      :returns (,FTY::FIELD.NAME ,FTY::FIELD.PRED
        ,@(AND (NOT FTY::FIELD.FULLP)
       `(:HINTS
         (("goal" :IN-THEORY
           (FTY::ENABLE ,FTY::X.FIX
            FTY::PART-SELECT-AT-0-OF-UNSIGNED-BYTE-IDENTITY
            FTY::LOGEXT-PART-SELECT-AT-0-IDENTITY))))))
      :no-function t
      ,@(AND FTY::X.INLINE `(:INLINE ,FTY::X.INLINE))
      :parents (,FTY::X.NAME)
      :short ,FTY::SHORT
      ,@(AND FTY::FIELD.SUBFIELD-HIERARCHY '(:ENABLED T))
      :guard-hints (("goal" :in-theory (enable ,@(AND (NOT FTY::FIELD.FULLP) `(,FTY::X.PRED))
           ,@(AND (EQL FTY::FIELD.WIDTH 1)
       '(FTY::PART-SELECT-IS-LOGBIT FTY::LOGBIT-AT-ZERO-IS-LOGHEAD-OF-1
         FTY::UNSIGNED-BYTE-P-OF-BOOL->BIT FTY::SIGNED-BYTE-P-OF-BOOL->BIT))
           part-select-width-low-in-terms-of-loghead-and-logtail
           remove-inner-logext-from-logext-logtail-nest
           remove-outer-logtail-from-logtail-logext-nest . ,FTY::SUBFIELD-ACCS)))
      (mbe :logic (let ((,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR)))
          ,FTY::LOGIC-FORM)
        :exec ,FTY::EXEC-FORM)
      ///
      (add-to-ruleset ,FTY::X.DEFS-RULESET ,FTY::FIELD.ACCESSOR)
      (deffixequiv ,FTY::FIELD.ACCESSOR)
      ,@(AND (NOT FTY::FIELD.SUBFIELD-HIERARCHY)
       `((FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::FIELD.ACCESSOR) "-OF-"
             (SYMBOL-NAME FTY::X.NAME))
            FTY::X.NAME)
          (EQUAL (,FTY::FIELD.ACCESSOR (,FTY::X.NAME . ,FTY::FIELDNAMES))
                 ,(IF FTY::FIELD.SUBFIELD-HIERARCHY
                      (FTY::BITSTRUCT-SUBFIELD-ACCESSOR-FORM
                       (BUTLAST FTY::FIELD.SUBFIELD-HIERARCHY 1)
                       (FTY::BITSTRUCT-FIELD->NAME
                        (CAR (LAST FTY::FIELD.SUBFIELD-HIERARCHY))))
                      `(,FTY::FIELD.FIX ,FTY::FIELD.NAME)))
          ,@(AND (NOT FTY::FIELD.SUBFIELD-HIERARCHY)
                 `(:HINTS
                   (("Goal" :IN-THEORY
                     (FTY::ENABLE ,FTY::X.NAME
                      ,@(AND (NOT FTY::X.FULLP)
                             `(,FTY::X.FIX
                               FTY::PART-SELECT-AT-0-OF-UNSIGNED-BYTE-IDENTITY))))
                    (AND FTY::STABLE-UNDER-SIMPLIFICATIONP
                         '(:IN-THEORY
                           (FTY::ENABLE FTY::LOGEXT-PART-SELECT-AT-0-IDENTITY
                            LOGEXT-IDENTITY)))))))
         (FTY::LOCAL (FTY::IN-THEORY (FTY::ENABLE FTY::EQUAL-OF-BOOL->BIT)))
         (FTY::LOCAL
          (WITHOUT-WATERFALL-PARALLELISM
           (FTY::DEFTHM FTY::DEFBITSTRUCT-WRITE-WITH-MASK-LEMMA
            (FTY::IMPLIES
             (,FTY::X.EQUIV-UNDER-MASK ,FTY::X.XVAR FTY::Y
              ,(ASH (FTY::LOGMASK FTY::FIELD.WIDTH) FTY::FIELD.LSB))
             (EQUAL (,FTY::FIELD.ACCESSOR ,FTY::X.XVAR)
                    (,FTY::FIELD.ACCESSOR FTY::Y)))
            :HINTS
            (("goal" :IN-THEORY
              (FTY::ENABLE ,FTY::X.EQUIV-UNDER-MASK FTY::INT-EQUIV-UNDER-MASK
               FTY::EQUAL-OF-BIT->BOOL FTY::LOGAND-MASK-LOGXOR-EQUAL-0
               FTY::LOGAND-CONST-OF-LOGAPP
               ,@(AND (NOT FTY::FIELD.FULLP) `(,FTY::X.FIX))
               . ,FTY::SUBFIELD-ACCS))
             (FTY::BITSTRUCT-LOGBITP-REASONING)
             (AND FTY::STABLE-UNDER-SIMPLIFICATIONP
                  '(:IN-THEORY (FTY::ENABLE FTY::BOOL->BIT))))
            :RULE-CLASSES NIL)))
         (FTY::DEFTHM
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::FIELD.ACCESSOR) "-OF-WRITE-WITH-MASK")
            FTY::X.NAME)
          (FTY::IMPLIES
           (AND
            (FTY::BITSTRUCT-READ-OVER-WRITE-HYPS ,FTY::X.XVAR
             ,FTY::X.EQUIV-UNDER-MASK)
            (,FTY::X.EQUIV-UNDER-MASK ,FTY::X.XVAR FTY::Y FTY::MASK)
            (EQUAL
             (LOGAND (LOGNOT FTY::MASK)
                     ,(ASH (FTY::LOGMASK FTY::FIELD.WIDTH) FTY::FIELD.LSB))
             0))
           (EQUAL (,FTY::FIELD.ACCESSOR ,FTY::X.XVAR)
                  (,FTY::FIELD.ACCESSOR FTY::Y)))
          :HINTS
          (("goal" :IN-THEORY
            (FTY::ENABLE ,FTY::X.EQUIV-UNDER-MASK
             FTY::INT-EQUIV-UNDER-MASK-OF-SUBMASK)
            :USE FTY::DEFBITSTRUCT-WRITE-WITH-MASK-LEMMA))))))))

(define bitstruct-subfield-updater-form-aux
  (hier subfield-term xvar)
  (b* (((bitstruct-field field) (car hier)) (name1 (intern-in-package-of-symbol (cat (symbol-name field.name) "1")
          field.name))
      ((when (atom (cdr hier))) `(b* ((,FTY::FIELD.NAME (,FTY::FIELD.ACCESSOR ,FTY::XVAR)) (,FTY::NAME1 ,FTY::SUBFIELD-TERM))
          (,FTY::FIELD.UPDATER ,FTY::NAME1 ,FTY::XVAR)))
      (next-var (bitstruct-field->name (cadr hier)))
      (next-term `(b* ((,FTY::FIELD.NAME (,FTY::FIELD.ACCESSOR ,FTY::NEXT-VAR)) (,FTY::NAME1 ,FTY::SUBFIELD-TERM))
          (,FTY::FIELD.UPDATER ,FTY::NAME1 ,FTY::NEXT-VAR))))
    (bitstruct-subfield-updater-form-aux (cdr hier)
      next-term
      xvar)))

(define bitstruct-subfield-updater-form
  (hier field-var xvar)
  (b* (((bitstruct-field field) (car hier)) (next-var (bitstruct-field->name (cadr hier)))
      (next-term `(,FTY::FIELD.UPDATER ,FTY::FIELD-VAR ,FTY::NEXT-VAR)))
    (bitstruct-subfield-updater-form-aux (cdr hier)
      next-term
      xvar)))

(define bitstruct-subfield-updater-fns
  (hier)
  (b* (((when (atom hier)) nil) ((bitstruct-field field) (car hier)))
    (cons field.updater
      (bitstruct-subfield-updater-fns (cdr hier)))))

(define bitstruct-updater-term-exec-form
  (fullwidth fullsignedp field xvar)
  (b* (((bitstruct-field field)) (field-type (if field.signedp
          'signed-byte
          'unsigned-byte))
      (full-type (if fullsignedp
          'signed-byte
          'unsigned-byte))
      (mask (lognot (ash (logmask field.width) field.lsb)))
      (field-msb (+ field.lsb field.width))
      (mask-size (+ 1 field-msb))
      (fname (if (eq field.pred 'booleanp)
          `(bool->bit ,FTY::FIELD.NAME)
          field.name))
      (exec-form-ash-base (cond ((eql field.lsb 0) (if field.signedp
              `(the (unsigned-byte ,FTY::FIELD.WIDTH)
                (logand ,(1- (EXPT 2 FTY::FIELD.WIDTH))
                  (the (,FTY::FIELD-TYPE ,FTY::FIELD.WIDTH) ,FTY::FNAME)))
              `(the (,FTY::FIELD-TYPE ,FTY::FIELD.WIDTH) ,FTY::FNAME)))
          (field.signedp `(the (unsigned-byte ,FTY::FIELD-MSB)
              (ash (the (unsigned-byte ,FTY::FIELD.WIDTH)
                  (logand ,(1- (EXPT 2 FTY::FIELD.WIDTH))
                    (the (,FTY::FIELD-TYPE ,FTY::FIELD.WIDTH) ,FTY::FNAME)))
                ,FTY::FIELD.LSB)))
          (t `(the (,FTY::FIELD-TYPE ,FTY::FIELD-MSB)
              (ash (the (,FTY::FIELD-TYPE ,FTY::FIELD.WIDTH) ,FTY::FNAME)
                ,FTY::FIELD.LSB)))))
      (exec-form (let ((new-fullwidth (if fullsignedp
               (max fullwidth mask-size)
               fullwidth)))
          `(the (,FTY::FULL-TYPE ,FTY::NEW-FULLWIDTH)
            (logior (the (,FTY::FULL-TYPE ,FTY::NEW-FULLWIDTH)
                (logand (the (,FTY::FULL-TYPE ,FTY::FULLWIDTH) ,FTY::XVAR)
                  (the (signed-byte ,FTY::MASK-SIZE) ,FTY::MASK)))
              ,FTY::EXEC-FORM-ASH-BASE)))))
    exec-form))

(define bitstruct-field-updater
  (field x)
  (b* (((bitstruct x)) ((bitstruct-field field))
      (short (cat "Update the "
          (full-escape-symbol field.name)
          " field of a @(see "
          (full-escape-symbol x.name)
          ") bit structure."))
      (last-field (equal (+ field.lsb field.width) x.width))
      (logic-form-base `(part-install ,FTY::FIELD.NAME
          ,FTY::X.XVAR
          :width ,FTY::FIELD.WIDTH
          :low ,FTY::FIELD.LSB))
      (exec-form (bitstruct-updater-term-exec-form x.width
          x.signedp
          field
          x.xvar))
      (body (if field.subfield-hierarchy
          `(mbe :logic ,(FTY::BITSTRUCT-SUBFIELD-UPDATER-FORM FTY::FIELD.SUBFIELD-HIERARCHY
  FTY::FIELD.NAME FTY::X.XVAR)
            :exec ,(IF (AND FTY::LAST-FIELD FTY::X.SIGNEDP (NOT FTY::FIELD.SIGNEDP))
     `(FTY::FAST-LOGEXT ,FTY::X.WIDTH ,FTY::EXEC-FORM)
     FTY::EXEC-FORM))
          (b* ((body-base `(mbe :logic (b* ((,FTY::FIELD.NAME ,(IF (EQ FTY::FIELD.PRED 'FTY::BOOLEANP)
     `(BOOL->BIT ,FTY::FIELD.NAME)
     `(FTY::MBE :LOGIC (,FTY::FIELD.FIX ,FTY::FIELD.NAME) :EXEC
       ,FTY::FIELD.NAME))) (,FTY::X.XVAR (,FTY::X.FIX ,FTY::X.XVAR)))
                   ,FTY::LOGIC-FORM-BASE)
                 :exec ,FTY::EXEC-FORM)))
            (if (and last-field x.signedp)
              `(fast-logext ,FTY::X.WIDTH ,FTY::BODY-BASE)
              body-base))))
      (subfield-fns (append (bitstruct-subfield-accessor-fns field.subfield-hierarchy)
          (bitstruct-subfield-updater-fns field.subfield-hierarchy)))
      (new-x (intern-in-package-of-symbol (cat "NEW-" (symbol-name x.xvar))
          x.name))
      (type-incr-rule (if x.signedp
          'signed-byte-p-incr
          'unsigned-byte-p-incr))
      (type-incr-use-hint-1 `((:instance ,FTY::TYPE-INCR-RULE
           (a ,(IF (AND FTY::X.SIGNEDP (EQL FTY::FIELD.WIDTH 1))
     (+ 1 FTY::FIELD.WIDTH)
     FTY::FIELD.WIDTH))
           (x ,(IF (EQ FTY::FIELD.PRED 'FTY::BOOLEANP)
     `(FTY::BOOL->BIT ,FTY::FIELD.NAME)
     FTY::FIELD.NAME))
           (b ,(- FTY::X.WIDTH FTY::FIELD.LSB)))))
      (type-incr-use-hint-2 `((:instance ,FTY::TYPE-INCR-RULE
           (a ,(IF (AND FTY::X.SIGNEDP (EQL FTY::FIELD.WIDTH 1))
     (+ 1 FTY::FIELD.WIDTH)
     FTY::FIELD.WIDTH))
           (x ,(IF (EQ FTY::FIELD.PRED 'FTY::BOOLEANP)
     `(FTY::BOOL->BIT ,FTY::FIELD.NAME)
     FTY::FIELD.NAME))
           (b ,FTY::X.WIDTH))))
      (type-incr-use-hint-3 `((:instance ,FTY::TYPE-INCR-RULE
           (a ,FTY::X.WIDTH)
           (x ,FTY::X.XVAR)
           (b ,(+ 1 FTY::X.WIDTH))))))
    `(define ,FTY::FIELD.UPDATER
      ((,FTY::FIELD.NAME ,FTY::FIELD.PRED) (,FTY::X.XVAR ,FTY::X.PRED))
      ,@(AND (NOT FTY::FIELD.SUBFIELD-HIERARCHY)
       `(:RETURNS
         (,FTY::NEW-X ,FTY::X.PRED
          ,@(AND (NOT FTY::X.FULLP)
                 `(:HINTS
                   (("goal" :IN-THEORY
                     (FTY::ENABLE ,FTY::X.PRED ,FTY::X.FIX
                      FTY::PART-SELECT-AT-0-OF-UNSIGNED-BYTE-IDENTITY
                      FTY::LOGEXT-PART-SELECT-AT-0-IDENTITY))))))))
      :no-function t
      ,@(AND FTY::X.INLINE `(:INLINE ,FTY::X.INLINE))
      :parents (,FTY::X.NAME)
      :short ,FTY::SHORT
      :progn t
      ,@(AND FTY::FIELD.SUBFIELD-HIERARCHY '(:ENABLED T))
      :guard-hints (("goal" :in-theory (e/d (part-install-width-low-in-terms-of-logior-logmask-ash ,@(AND (EQL FTY::FIELD.WIDTH 1)
       '(FTY::LOGBIT-AT-ZERO-IS-LOGHEAD-OF-1 FTY::UNSIGNED-BYTE-P-OF-BOOL->BIT
         FTY::SIGNED-BYTE-P-OF-BOOL->BIT))
             ,@(AND (OR FTY::X.SIGNEDP FTY::FIELD.SIGNEDP)
       '(FTY::SIGNED-BYTE-P-+1
         FTY::SIGNED-BYTE-P-ONE-BIGGER-WHEN-UNSIGNED-BYTE-P))
             ,@(AND FTY::FIELD.SUBFIELD-HIERARCHY
       `(,@FTY::SUBFIELD-FNS
         FTY::SIMPLIFY-SUBFIELD-UPDATER-GUARD-EXPRESSION-WITH-INNER-LOGEXT
         FTY::SIMPLIFY-SUBFIELD-UPDATER-GUARD-EXPRESSION-WITH-MORE-LOGEXT
         FTY::REMOVE-INNER-LOGEXT-FROM-LOGEXT-LOGTAIL-NEST)))
           (,FTY::TYPE-INCR-RULE logand-with-negated-bitmask
             ,@(AND (EQL FTY::FIELD.WIDTH 1)
       (IF FTY::X.SIGNEDP
           '(FTY::SIGNED-BYTE-P-2-WHEN-BITP)
           '(FTY::UNSIGNED-BYTE-P-1-WHEN-BITP)))))
         :use (,@FTY::TYPE-INCR-USE-HINT-1 ,@FTY::TYPE-INCR-USE-HINT-2
           ,@FTY::TYPE-INCR-USE-HINT-3
           ,@(AND (EQL FTY::FIELD.WIDTH 1)
       `((:INSTANCE
          ,@(IF FTY::X.SIGNEDP
                `(FTY::SIGNED-BYTE-P-2-WHEN-BITP (FTY::X ,FTY::FIELD.NAME))
                `(FTY::UNSIGNED-BYTE-P-1-WHEN-BITP
                  (FTY::X ,FTY::FIELD.NAME)))))))))
      ,FTY::BODY
      ///
      (add-to-ruleset ,FTY::X.DEFS-RULESET ,FTY::FIELD.UPDATER)
      (deffixequiv ,FTY::FIELD.UPDATER)
      ,@(AND (NOT FTY::FIELD.SUBFIELD-HIERARCHY)
       `((FTY::DEFTHMD
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::FIELD.UPDATER) "-IS-"
             (SYMBOL-NAME FTY::X.NAME))
            FTY::X.NAME)
          (EQUAL (,FTY::FIELD.UPDATER ,FTY::FIELD.NAME ,FTY::X.XVAR)
                 (,(STD::DA-CHANGER-NAME FTY::X.NAME) ,FTY::X.XVAR
                  ,(FTY::INTERN$ (SYMBOL-NAME FTY::FIELD.NAME) "KEYWORD")
                  ,FTY::FIELD.NAME))
          :HINTS
          (("Goal" :IN-THEORY
            (FTY::ENABLE ,FTY::X.NAME
             ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
               (FTY::CAT (SYMBOL-NAME FTY::X.FIX) "-IN-TERMS-OF-"
                (SYMBOL-NAME FTY::X.NAME))
               FTY::X.NAME)))
           (AND FTY::STABLE-UNDER-SIMPLIFICATIONP
                '(:IN-THEORY
                  (FTY::ENABLE FTY::PART-INSTALL-IDENTITY
                   FTY::PART-INSTALL-IDENTITY-SIGNED LOGHEAD-IDENTITY
                   BITOPS::CANCEL-LOGHEAD-UNDER-LOGEXT)))))
         (FTY::DEFRET
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::FIELD.ACCESSOR) "-OF-"
             (SYMBOL-NAME FTY::FIELD.UPDATER))
            FTY::X.NAME)
          (EQUAL (,FTY::FIELD.ACCESSOR ,FTY::NEW-X)
                 (,FTY::FIELD.FIX ,FTY::FIELD.NAME))
          :HINTS
          (("Goal" :IN-THEORY
            (FTY::E/D (,FTY::FIELD.ACCESSOR) (,FTY::FIELD.UPDATER)))
           (AND FTY::STABLE-UNDER-SIMPLIFICATIONP
                '(:IN-THEORY (FTY::ENABLE ,FTY::FIELD.UPDATER)))))
         (WITHOUT-WATERFALL-PARALLELISM
          (FTY::DEFRET
           ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
             (FTY::CAT (SYMBOL-NAME FTY::FIELD.UPDATER) "-EQUIV-UNDER-MASK")
             FTY::X.NAME)
           (,FTY::X.EQUIV-UNDER-MASK ,FTY::NEW-X ,FTY::X.XVAR
            ,(IF FTY::LAST-FIELD
                 (LOGNOT (ASH -1 FTY::FIELD.LSB))
                 (LOGNOT
                  (ASH (FTY::LOGMASK FTY::FIELD.WIDTH) FTY::FIELD.LSB))))
           :HINTS
           (("Goal" :IN-THEORY
             (FTY::E/D (,FTY::X.EQUIV-UNDER-MASK FTY::INT-EQUIV-UNDER-MASK)
              (,FTY::FIELD.UPDATER)))
            (AND FTY::STABLE-UNDER-SIMPLIFICATIONP
                 '(:IN-THEORY (FTY::ENABLE ,FTY::FIELD.UPDATER)))
            (FTY::BITSTRUCT-LOGBITP-REASONING)))))))))

(define bitstruct-field-accessors
  (fields x)
  (if (atom fields)
    nil
    (cons (bitstruct-field-accessor (car fields) x)
      (bitstruct-field-accessors (cdr fields) x))))

(define bitstruct-field-updaters
  (fields x)
  (if (atom fields)
    nil
    (cons (bitstruct-field-updater (car fields) x)
      (bitstruct-field-updaters (cdr fields) x))))

(define bitstruct-debug-field-pairs
  (fields x)
  (b* (((when (atom fields)) nil) ((bitstruct x))
      ((bitstruct-field field) (car fields)))
    `(cons (cons ',FTY::FIELD.NAME
        ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
  (STR::CAT (SYMBOL-NAME FTY::X.XVAR) "." (SYMBOL-NAME FTY::FIELD.NAME))
  FTY::X.NAME))
      ,(FTY::BITSTRUCT-DEBUG-FIELD-PAIRS (CDR FTY::FIELDS) FTY::X))))

(define bitstruct-debugger
  (x)
  (b* (((bitstruct x)) (debug (intern-in-package-of-symbol (cat (symbol-name x.name) "-DEBUG")
          x.name)))
    `(define ,DEBUG
      ((,FTY::X.XVAR ,FTY::X.PRED))
      (b* (((,FTY::X.NAME ,FTY::X.XVAR)))
        ,(FTY::BITSTRUCT-DEBUG-FIELD-PAIRS FTY::X.FIELDS FTY::X)))))

(defun html-encode-str
  (x acc)
  (simple-html-encode-str x
    0
    (length x)
    acc))

(define bitstruct-field-xdoc
  (field acc state)
  (b* (((bitstruct-field field)) (acc (revappend-chars "<dt>" acc))
      ((mv name-str state) (fmt-to-str-orig field.name
          field.name
          state))
      (acc (html-encode-str name-str acc))
      (acc (b* (((when (eq field.type nil)) acc) (acc (revappend-chars " &mdash; @(see? " acc))
            (acc (revappend-chars (full-escape-symbol field.type)
                acc))
            (acc (revappend-chars ")" acc)))
          acc))
      (acc (revappend-chars "</dt>" acc))
      (acc (cons #\
 acc))
      (acc (b* (((when (or (not field.doc) (equal field.doc ""))) acc) (acc (revappend-chars "<dd>" acc))
            (acc (revappend-chars field.doc acc))
            (acc (revappend-chars "</dd>" acc))
            (acc (cons #\
 acc)))
          acc))
      (acc (cons #\
 acc)))
    (mv acc state)))

(define bitstruct-fields-xdoc
  (fields acc state)
  (b* (((when (atom fields)) (mv acc state)) ((mv acc state) (bitstruct-field-xdoc (car fields)
          acc
          state)))
    (bitstruct-fields-xdoc (cdr fields)
      acc
      state)))

(define bitstruct-xdoc-long
  (x state)
  (b* (((bitstruct x)) (long (or (cdr (assoc :long x.kwd-alist)) ""))
      (acc nil)
      (acc (revappend-chars "<p>This is a bitstruct type introduced by @(see fty::defbitstruct),"
          acc))
      (acc (revappend-chars " represented as a " acc))
      (acc (revappend-chars (if x.signedp
            "signed "
            "unsigned ")
          acc))
      (acc (revappend-chars (natstr x.width) acc))
      (acc (revappend-chars "-bit integer.</p>" acc))
      (acc (cons #\
 acc))
      ((mv acc state) (if (consp x.fields)
          (b* ((acc (revappend-chars "<h5>Fields</h5>" acc)) (acc (cons #\
 acc))
              (acc (revappend-chars "<dl>" acc))
              ((mv acc state) (bitstruct-fields-xdoc x.fields
                  acc
                  state))
              (acc (revappend-chars "</dl>" acc)))
            (mv acc state))
          (mv (revappend-chars "<p>This is an atomic/empty structure; it has no fields.</p>"
              acc)
            state)))
      (acc (revappend-chars long acc))
      (long (rchars-to-string acc)))
    (mv long state)))

(define bitstruct-events
  (x state)
  (b* (((bitstruct x)) ((mv long state) (bitstruct-xdoc-long x state))
      (field-accs (pairlis$ (bitstruct-fields->names x.fields)
          (bitstruct-fields->accessors x.fields)))
      (binder-alist (append field-accs
          (extra-binder-names->acc-alist (cdr (assoc :extra-binder-names x.kwd-alist))
            x.name))))
    (value `(with-output :off (event prove)
        :summary-off (:other-than form time)
        (defsection ,FTY::X.NAME
          :parents ,(OR (CDR (ASSOC :PARENTS FTY::X.KWD-ALIST))
     (XDOC::GET-DEFAULT-PARENTS (FTY::W FTY::STATE)) '(UNDOCUMENTED))
          :short ,(OR (CDR (ASSOC :SHORT FTY::X.KWD-ALIST))
     (FTY::CAT "An " (STR::NATSTR FTY::X.WIDTH) "-bit "
      (IF FTY::X.SIGNEDP
          "signed"
          "unsigned")
      " bitstruct type."))
          :long ,FTY::LONG
          (set-inhibit-warnings "non-rec" "disable" "subsume")
          (local (include-book "centaur/bitops/ihsext-basics" :dir :system))
          (local (include-book "centaur/bitops/equal-by-logbitp" :dir :system))
          (local (include-book "arithmetic/top-with-meta" :dir :system))
          (local (in-theory (disable unsigned-byte-p
                signed-byte-p
                part-select
                part-install
                bit->bool)))
          ,(FTY::BITSTRUCT-PRED FTY::X)
          ,(FTY::BITSTRUCT-FIX FTY::X)
          ,@(AND (CONSP FTY::X.FIELDS)
       (LIST `(FTY::DEF-RULESET! ,FTY::X.DEFS-RULESET NIL)
             (FTY::BITSTRUCT-CTOR FTY::X)
             (FTY::BITSTRUCT-EQUIV-UNDER-MASK FTY::X)))
          ,@(FTY::BITSTRUCT-FIELD-ACCESSORS FTY::X.FIELDS FTY::X)
          ,@(AND (CONSP FTY::X.FIELDS)
       `((FTY::DEFTHMD
          ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL
            (FTY::CAT (SYMBOL-NAME FTY::X.FIX) "-IN-TERMS-OF-"
             (SYMBOL-NAME FTY::X.NAME))
            FTY::X.NAME)
          (EQUAL (,FTY::X.FIX ,FTY::X.XVAR)
                 (,(STD::DA-CHANGER-NAME FTY::X.NAME) ,FTY::X.XVAR))
          :HINTS
          (("Goal" :IN-THEORY
            (FTY::ENABLE ,FTY::X.FIX ,FTY::X.NAME
             . ,(FTY::BITSTRUCT-FIELDS->ACCESSORS FTY::X.FIELDS)))
           (AND FTY::STABLE-UNDER-SIMPLIFICATIONP
                '(:IN-THEORY
                  (FTY::ENABLE FTY::LOGEXT-PART-SELECT-AT-0-IDENTITY
                   FTY::PART-SELECT-AT-0-OF-UNSIGNED-BYTE-IDENTITY)))))))
          ,@(FTY::BITSTRUCT-FIELD-UPDATERS FTY::X.FIELDS FTY::X)
          ,@(AND (CONSP FTY::X.FIELDS)
       `((DEF-B*-BINDER ,FTY::X.NAME :BODY
          (STD::DA-PATBIND-FN ',FTY::X.NAME ',FTY::BINDER-ALIST ARGS FORMS
           REST-EXPR))
         ,(FTY::BITSTRUCT-DEBUGGER FTY::X)))
          (table bitstruct-table ',FTY::X.NAME ',FTY::X))))))

(define defbitstruct-fn
  (args state)
  (b* ((bitstruct-table (table-alist 'bitstruct-table (w state))) (x (parse-defbitstruct args bitstruct-table)))
    (bitstruct-events x state)))

(defmacro defbitstruct
  (&rest args)
  `(make-event (defbitstruct-fn ',FTY::ARGS state)))

(defxdoc defbitstruct
  :parents (fty)
  :short "Define a bitvector type with accessors for its fields."
  :long "<p>This macro defines a bitstruct type.  A bitstruct can either be a
base type, which is a single fixed-width integer, or a product type containing
fields that are bits, Booleans, or other bitstructs.  Such a product is
represented as a single integer produced by concatenating all the fields
together, where the first field is least significant.</p>

<h5>Examples:</h5>

<p>A bitstruct can be made up of single bits and Booleans.  (The difference is
only in the return type of the accessors and the input type of the updaters;
the representation is the same.)  The fields are ordered LSB first, so @('a')
is bit 0 of the representation and @('c') is bit 2.  This defines a predicate,
fixing function, accessors, and a constructor similar to @('defprod'), but also
updaters such as @('!foo->a').</p> @({
 (defbitstruct foo
   ((a bitp)
    (b booleanp)
    (c bitp)))
})

<p>A bitstruct can also contain fields that are other bitstructs.  Here, the
first field is a @('foo'), which is three bits wide, so the @('b') and @('c')
fields are bits 3 and 4, respectively.  Also, since @(':signedp t') was
specified, the representation is signed: the product is represented as a 5-bit
signed integer rather than a 5-bit natural.</p>
@({
 (defbitstruct bar
   ((myfoo foo-p)
    (b booleanp)
    (c bitp))
   :signedp t)
 })

<p>A bitstruct can also be defined without any fields, giving only a
width. These are mainly useful as fields of other bitstructs.  This makes sense
when the individual bits aren't meaningful, and their combined value is what's
important.  This defines a rounding-control as a 2-bit unsigned value.</p>
@({
 (defbitstruct rounding-control 2)
 })

<p>Sometimes we may want to nest one bitstruct inside another, but also
directly access the fields of the internal struct.  Providing the
@(':subfields') keyword causes defbitstruct to produce direct accessors and
updaters for the subfields of the nested struct.  The following definition of
@('mxcsr') produces the usual accessors and updaters including @('mxcsr->flags')
and @('mxcsr->masks'), but also @('mxcsr->ie') and @('mxcsr->im'), etc.</p>
@({
 (defbitstruct fp-flags
   ((ie bitp)
    (de bitp)
    (ze bitp)
    (oe bitp)
    (ue bitp)
    (pe bitp)))

 (defbitstruct mxcsr
   ((flags fp-flags :subfields (ie de ze oe ue pe))
    (daz bitp)
    (masks fp-flags :subfields (im dm zm om um pm))
    (rc  rounding-control)
    (ftz bitp)))
 })

<h5>Syntax</h5>
<p>A @('defbitstruct') form is one of:</p>
@({
 (defbitstruct typename fields [ options ] )
 })
<p>or</p>
@({
 (defbitstruct typename width [ options ] ).
 })
<p>The syntax of fields is described below.</p>

<h5>Top-level options</h5>

<ul>

<li>@(':pred'), @(':fix'), @(':equiv') -- override the default names (foo-p,
foo-fix, and foo-equiv) for the predicate, fixing function, and equivalence
relation.</li>

<li>@(':parents'), @(':short'), @(':long') -- provide xdoc for the bitstruct</li>

<li>@(':signedp') -- when true, represents the structure as a signed integer
rather than an unsigned one.  (Signed and unsigned fields can be used inside
unsigned and signed bitstructs -- they are simply sign- or zero-extended as
necessary when accessed.)</li>

<li>@(':msb-first') -- when non-NIL, reverses the order of the top-level fields,
it does not reverse @(':subfield') accessors/updaters.</li>

<li>@(':extra-binder-args') -- a list of symbols that, in addition to the
fields, will be accessible through the generated B* binder once corresponding
accessor functions are defined.  For example if we define a bitstruct @('foo')
with @(':extra-binder-args (bar)'), then once the function @('foo->bar') is
defined, the B* binder @('(b* (((foo x))) ...)') will allow access to
@('(foo->bar x)') via variable @('x.bar').</li>

</ul>

<h5>Field Syntax</h5>
<p>A field has the following form:</p>
@({
 (fieldname type [ docstring ] [ options ... ] )
 })

<p>The type can be either a predicate or type name, i.e., @('bit') or
@('bitp'), and must refer to either a single-bit type (bit or boolean) or a
previously-defined bitstruct type.  The docstring is a string which may contain
xdoc syntax.</p>

<h5>Field Options</h5>
<ul>

<li>@(':accessor'), @(':updater') -- override the default names
@('struct->field'), @('!struct->field') for the accessor and updater
functions.</li>

<li>@(':default') -- change the default value for the field in the
@('make-foo') macro.  The default default is NIL for Boolean fields and 0 for
everything else.</li>

<li>@(':rule-classes') -- override the rule classes of the accessor function's
return type theorem.  The default is @(':rewrite'); it may be appealing to use
@(':type-prescription'), but typically the type prescription for the accessor
should be determined automatically anyway.</li>

<li>@(':subfields') -- Indicates that accessors and updaters should be created
for subfields of this field, and gives their subfield names.  See the section
on subfields below.</li> </ul>

<h5>Subfields</h5>

<p>The @(':subfields') field option may only be used on a field whose type is
itself a bitstruct type containing fields.  The value of the @(':subfields')
argument should be a list of @('subfield_entries'), according to the following
syntax:</p>
 @({ subfield_entry ::= name | ( name ( subfield_entry ... ) ) })

<p>Each top-level entry corresponds to a subfield of the field type.  If the
entry uses the second syntax, which itself has a list of entries, those entries
correspond to sub-subfields of the subfield type.  For example:</p>

@({
 (defbitstruct innermost
   ((aa bitp)
    (bb bitp)))

 (defbitstruct midlevel
   ((ii innermost :subfields (iaa ibb))
    (qq bitp)
    (jj innermost :subfields (jaa jbb))))

 (defbitstruct toplevel
   ((ss innermost :subfields (saa sbb))
    (tt midlevel  :subfields ((tii (tiaa tibb))
                              tqq
                              tjj))))
 })

<p>For the @('toplevel') bitstruct, this generates the following subfield
accessors, in addition to the direct accessors @('toplevel->ss') and
@('toplevel->tt'):</p>

@({
 (toplevel->saa x)    == (innermost->aa (toplevel->ss x))
 (toplevel->sbb x)    == (innermost->bb (toplevel->ss x))
 (toplevel->tii x)    == (midlevel->ii (toplevel->tt x))
 (toplevel->tiaa x)   == (innermost->aa (midlevel->ii (toplevel->tt x)))
 (toplevel->tibb x)   == (innermost->bb (midlevel->ii (toplevel->tt x)))
 (toplevel->tqq x)    == (midlevel->qq (toplevel->tt x))
 (toplevel->tjj x)    == (midlevel->jj (toplevel->tt x))
 })
")

(defconst *fixtype-to-bitstruct-keywords*
  '(:width :signedp :fullp))

(define fixtype-to-bitstruct-fn
  (name args wrld)
  (b* (((fixtype fty) (find-fixtype name
         (get-fixtypes-alist wrld))) ((mv kwd-alist rest) (extract-keywords name
          *fixtype-to-bitstruct-keywords*
          args
          nil))
      ((when rest) (raise "Extra arguments to fixtype-to-bitstruct: ~x0"
          rest))
      (width (cdr (assoc :width kwd-alist)))
      ((unless width) (raise "Must specify :width for fixtype-to-bitstruct"))
      (signedp (getarg :signedp nil kwd-alist))
      (fullp (getarg :fullp nil kwd-alist))
      (bitstruct (make-bitstruct :name fty.name
          :pred fty.pred
          :fix fty.fix
          :equiv fty.equiv
          :width width
          :signedp signedp
          :fullp fullp)))
    `(table bitstruct-table
      ',FTY::FTY.NAME
      ',FTY::BITSTRUCT)))

(defmacro fixtype-to-bitstruct
  (name &rest args)
  `(make-event (fixtype-to-bitstruct-fn ',FTY::NAME
      ',FTY::ARGS
      (w state))))

(logic)