		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-indir-rules-generation

Code to generate the rules for executing the indirection unary operation.

Definitions and Theorems

Function: atc-exec-indir-rules-gen

(defun atc-exec-indir-rules-gen (type)
 (declare (xargs :guard (typep type)))
 (declare (xargs :guard (type-nonchar-integerp type)))
 (let ((__function__ 'atc-exec-indir-rules-gen))
  (declare (ignorable __function__))
  (b*
   ((fixtype (integer-type-to-fixtype type))
    (pred (pack fixtype 'p))
    (name (pack 'exec-indir-when- pred))
    (hyps
     (cons
      'and
      (cons
       (atc-syntaxp-hyp-for-expr-pure 'x)
       (cons
        '(valuep x)
        (cons
         '(value-case x :pointer)
         (cons
          '(value-pointer-validp x)
          (cons
           (cons 'equal
                 (cons '(value-pointer->reftype x)
                       (cons (type-to-maker type) 'nil)))
           (cons
                '(unop-case op :indir)
                (cons '(equal objdes (value-pointer->designator x))
                      (cons '(equal val (read-object objdes compst))
                            (cons (cons pred '(val)) 'nil)))))))))))
    (formula
         (cons 'implies
               (cons hyps
                     '((equal (exec-unary op (expr-value x objdes-x)
                                          compst)
                              (expr-value val objdes))))))
    (hints
     '(("Goal" :in-theory
               (enable exec-unary exec-indir
                       apconvert-expr-value-when-not-value-array))))
    (event (cons 'defruled
                 (cons name
                       (cons formula
                             (cons ':hints (cons hints 'nil)))))))
   (mv name event))))

Theorem: symbolp-of-atc-exec-indir-rules-gen.name

(defthm symbolp-of-atc-exec-indir-rules-gen.name
  (b* (((mv ?name acl2::?event)
        (atc-exec-indir-rules-gen type)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-atc-exec-indir-rules-gen.event

(defthm pseudo-event-formp-of-atc-exec-indir-rules-gen.event
  (b* (((mv ?name acl2::?event)
        (atc-exec-indir-rules-gen type)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Function: atc-exec-indir-rules-loop

(defun atc-exec-indir-rules-loop (types)
  (declare (xargs :guard (type-listp types)))
  (declare (xargs :guard (type-nonchar-integer-listp types)))
  (let ((__function__ 'atc-exec-indir-rules-loop))
    (declare (ignorable __function__))
    (b* (((when (endp types)) (mv nil nil))
         ((mv name event)
          (atc-exec-indir-rules-gen (car types)))
         ((mv names events)
          (atc-exec-indir-rules-loop (cdr types))))
      (mv (cons name names)
          (cons event events)))))

Theorem: symbol-listp-of-atc-exec-indir-rules-loop.names

(defthm symbol-listp-of-atc-exec-indir-rules-loop.names
  (b* (((mv ?names ?events)
        (atc-exec-indir-rules-loop types)))
    (symbol-listp names))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-exec-indir-rules-loop.events

(defthm pseudo-event-form-listp-of-atc-exec-indir-rules-loop.events
  (b* (((mv ?names ?events)
        (atc-exec-indir-rules-loop types)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Function: atc-exec-indir-rules-gen-all

(defun atc-exec-indir-rules-gen-all nil
 (declare (xargs :guard t))
 (let ((__function__ 'atc-exec-indir-rules-gen-all))
  (declare (ignorable __function__))
  (b* (((mv names events)
        (atc-exec-indir-rules-loop *nonchar-integer-types*)))
   (cons
    'defsection
    (cons
     'atc-exec-indir-rules
     (cons
      ':short
      (cons
       '"Rules for executing the indirection unary operation."
       (append
        events
        (cons
         (cons
            'defval
            (cons '*atc-exec-indir-rules*
                  (cons (cons 'quote
                              (cons (append names '((:e unop-kind)))
                                    'nil))
                        'nil)))
         'nil)))))))))

Theorem: pseudo-event-formp-of-atc-exec-indir-rules-gen-all

(defthm pseudo-event-formp-of-atc-exec-indir-rules-gen-all
  (b* ((event (atc-exec-indir-rules-gen-all)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)