Code to generate the rules for executing the indirection unary operation.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)