		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-recognizer-conjuncts

Generate conjuncts for a member in the recognizer of the structures.

Signature
(defstruct-gen-recognizer-conjuncts memtype) → terms
Arguments: memtype — Guard (member-typep memtype).
Returns: terms — A list of untranslated terms.
Type (true-listp terms).

This is used by defstruct-gen-recognizer. For each member, there is one or more conjunct that constrains its value. An integer member has just one conjunct saying that the value satisfies the predicate that recognizes those integer values. A non-flexible array member has two conjuncts, one saying that the value is an array of the appropriate type, and one saying that the length of the array is the one indicated in the type. A flexible array member has just one conjunct saying that the value is an array of the appropriate type.

The value of the member is retrieved via value-struct-read-aux (see value-struct-read), which is a lookup function on member values (and perhaps it should be renamed to something better than an aux(iliary) function).

Definitions and Theorems

Function: defstruct-gen-recognizer-conjuncts

(defun defstruct-gen-recognizer-conjuncts (memtype)
 (declare (xargs :guard (member-typep memtype)))
 (let ((__function__ 'defstruct-gen-recognizer-conjuncts))
  (declare (ignorable __function__))
  (b* ((name (member-type->name memtype))
       (type (member-type->type memtype)))
   (type-case
    type
    :void (raise "Internal error: type ~x0." type)
    :char (raise "Internal error: type ~x0." type)
    :schar
    (cons (cons 'scharp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :uchar
    (cons (cons 'ucharp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :sshort
    (cons (cons 'sshortp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :ushort
    (cons (cons 'ushortp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :sint
    (cons (cons 'sintp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :uint
    (cons (cons 'uintp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :slong
    (cons (cons 'slongp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :ulong
    (cons (cons 'ulongp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :sllong
    (cons (cons 'sllongp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :ullong
    (cons (cons 'ullongp
                (cons (cons 'value-struct-read-aux
                            (cons (cons 'quote (cons name 'nil))
                                  '((value-struct->members x))))
                      'nil))
          'nil)
    :struct (raise "Internal error: type ~x0." type)
    :pointer (raise "Internal error: type ~x0." type)
    :array
    (type-case
     type.of
     :void (raise "Internal error: type ~x0." type)
     :char (raise "Internal error: type ~x0." type)
     :schar
     (cons
      (cons 'schar-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'schar-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :uchar
     (cons
      (cons 'uchar-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'uchar-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :sshort
     (cons
      (cons 'sshort-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'sshort-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :ushort
     (cons
      (cons 'ushort-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'ushort-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :sint
     (cons
      (cons 'sint-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'sint-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :uint
     (cons
      (cons 'uint-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'uint-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :slong
     (cons
      (cons 'slong-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'slong-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :ulong
     (cons
      (cons 'ulong-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'ulong-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :sllong
     (cons
      (cons 'sllong-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'sllong-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :ullong
     (cons
      (cons 'ullong-arrayp
            (cons (cons 'value-struct-read-aux
                        (cons (cons 'quote (cons name 'nil))
                              '((value-struct->members x))))
                  'nil))
      (and
       type.size
       (cons
        (cons
         'equal
         (cons
              (cons 'ullong-array-length
                    (cons (cons 'value-struct-read-aux
                                (cons (cons 'quote (cons name 'nil))
                                      '((value-struct->members x))))
                          'nil))
              (cons type.size 'nil)))
        'nil)))
     :struct (raise "Internal error: type ~x0." type)
     :pointer (raise "Internal error: type ~x0." type)
     :array (raise "Internal error: type ~x0." type))))))

Theorem: true-listp-of-defstruct-gen-recognizer-conjuncts

(defthm true-listp-of-defstruct-gen-recognizer-conjuncts
  (b* ((terms (defstruct-gen-recognizer-conjuncts memtype)))
    (true-listp terms))
  :rule-classes :rewrite)

Theorem: defstruct-gen-recognizer-conjuncts-of-member-type-fix-memtype

(defthm
      defstruct-gen-recognizer-conjuncts-of-member-type-fix-memtype
 (equal
      (defstruct-gen-recognizer-conjuncts (member-type-fix memtype))
      (defstruct-gen-recognizer-conjuncts memtype)))

Theorem: defstruct-gen-recognizer-conjuncts-member-type-equiv-congruence-on-memtype

(defthm
 defstruct-gen-recognizer-conjuncts-member-type-equiv-congruence-on-memtype
 (implies
      (member-type-equiv memtype memtype-equiv)
      (equal (defstruct-gen-recognizer-conjuncts memtype)
             (defstruct-gen-recognizer-conjuncts memtype-equiv)))
 :rule-classes :congruence)