		Search-engine friendly clone of the ACL2 documentation.

Defstruct-implementation

Defstruct-gen-fixing-term

Generate the fixing term for a member of a given type.

Signature
(defstruct-gen-fixing-term type) → term
Arguments: type — Guard (typep type).
Returns: term — An untranslated term.

This is used in defstruct-gen-fixer. We only the types allowed for structure memberd by defstruct.

Definitions and Theorems

Function: defstruct-gen-fixing-term

(defun defstruct-gen-fixing-term (type)
 (declare (xargs :guard (typep type)))
 (let ((__function__ 'defstruct-gen-fixing-term))
  (declare (ignorable __function__))
  (type-case
   type :void
   (raise "Internal error: type ~x0." type)
   :char
   (raise "Internal error: type ~x0." type)
   :schar '(schar-from-integer 0)
   :uchar '(uchar-from-integer 0)
   :sshort '(sshort-from-integer 0)
   :ushort '(ushort-from-integer 0)
   :sint '(sint-from-integer 0)
   :uint '(uint-from-integer 0)
   :slong '(slong-from-integer 0)
   :ulong '(ulong-from-integer 0)
   :sllong '(sllong-from-integer 0)
   :ullong '(ullong-from-integer 0)
   :struct
   (raise "Internal error: type ~x0." type)
   :pointer
   (raise "Internal error: type ~x0." type)
   :array
   (b* ((size (or type.size 1)))
    (type-case
     type.of
     :void (raise "Internal error: type ~x0." type)
     :char (raise "Internal error: type ~x0." type)
     :schar
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
            '(type-schar)
            (cons ':elements
                  (cons (cons 'repeat
                              (cons size '((schar-from-integer 0))))
                        'nil)))))
     :uchar
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
            '(type-uchar)
            (cons ':elements
                  (cons (cons 'repeat
                              (cons size '((uchar-from-integer 0))))
                        'nil)))))
     :sshort
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
           '(type-sshort)
           (cons ':elements
                 (cons (cons 'repeat
                             (cons size '((sshort-from-integer 0))))
                       'nil)))))
     :ushort
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
           '(type-ushort)
           (cons ':elements
                 (cons (cons 'repeat
                             (cons size '((ushort-from-integer 0))))
                       'nil)))))
     :sint
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons '(type-sint)
             (cons ':elements
                   (cons (cons 'repeat
                               (cons size '((sint-from-integer 0))))
                         'nil)))))
     :uint
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons '(type-uint)
             (cons ':elements
                   (cons (cons 'repeat
                               (cons size '((uint-from-integer 0))))
                         'nil)))))
     :slong
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
            '(type-slong)
            (cons ':elements
                  (cons (cons 'repeat
                              (cons size '((slong-from-integer 0))))
                        'nil)))))
     :ulong
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
            '(type-ulong)
            (cons ':elements
                  (cons (cons 'repeat
                              (cons size '((ulong-from-integer 0))))
                        'nil)))))
     :sllong
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
           '(type-sllong)
           (cons ':elements
                 (cons (cons 'repeat
                             (cons size '((sllong-from-integer 0))))
                       'nil)))))
     :ullong
     (cons
      'make-value-array
      (cons
       ':elemtype
       (cons
           '(type-ullong)
           (cons ':elements
                 (cons (cons 'repeat
                             (cons size '((ullong-from-integer 0))))
                       'nil)))))
     :struct (raise "Internal error: type ~x0." type)
     :pointer (raise "Internal error: type ~x0." type)
     :array (raise "Internal error: type ~x0." type))))))

Theorem: defstruct-gen-fixing-term-of-type-fix-type

(defthm defstruct-gen-fixing-term-of-type-fix-type
  (equal (defstruct-gen-fixing-term (type-fix type))
         (defstruct-gen-fixing-term type)))

Theorem: defstruct-gen-fixing-term-type-equiv-congruence-on-type

(defthm defstruct-gen-fixing-term-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (defstruct-gen-fixing-term type)
                  (defstruct-gen-fixing-term type-equiv)))
  :rule-classes :congruence)