Code to generate the rules for executing array subscript expressions.
Function:
(defun atc-exec-arrsub-rules-gen (atype) (declare (xargs :guard (typep atype))) (declare (xargs :guard (type-nonchar-integerp atype))) (let ((__function__ 'atc-exec-arrsub-rules-gen)) (declare (ignorable __function__)) (b* ((afixtype (integer-type-to-fixtype atype)) (apred (pack afixtype '-arrayp)) (atype-array-index-okp (pack afixtype '-array-index-okp)) (atype-array-read (pack afixtype '-array-read)) (value-array->elemtype-when-apred (pack 'value-array->elemtype-when- apred)) (value-array-read-when-apred (pack 'value-array-read-when- apred)) (name (pack 'exec-arrsub-when- apred)) (formula (cons 'implies (cons (cons 'and (cons '(equal ex (apconvert-expr-value (expr-value x objdes-x))) (cons '(expr-valuep ex) (cons '(equal a (expr-value->value ex)) (cons '(value-case a :pointer) (cons '(value-pointer-validp a) (cons (cons 'equal (cons '(value-pointer->reftype a) (cons (type-to-maker atype) 'nil))) (cons '(equal objdes (value-pointer->designator a)) (cons '(equal array (read-object objdes compst)) (cons (cons apred '(array)) (cons '(cintegerp y) (cons (cons atype-array-index-okp '(array y)) 'nil)))))))))))) (cons (cons 'equal (cons '(exec-arrsub (expr-value x objdes-x) (expr-value y objdes-y) compst) (cons (cons 'expr-value (cons (cons atype-array-read '(array y)) '((objdesign-element objdes (integer-from-cinteger y))))) 'nil))) 'nil)))) (event (cons 'defruled (cons name (cons formula (cons ':enable (cons (cons 'exec-arrsub (cons value-array->elemtype-when-apred (cons 'apconvert-expr-value-when-not-value-array (cons 'value-kind-not-array-when-cintegerp (cons 'value-integerp-when-cintegerp (cons atype-array-index-okp (cons 'integer-range-p (cons 'value-integer->get-when-cintegerp (cons value-array-read-when-apred 'nil))))))))) 'nil))))))) (mv name event))))
Theorem:
(defthm symbolp-of-atc-exec-arrsub-rules-gen.name (b* (((mv ?name acl2::?event) (atc-exec-arrsub-rules-gen atype))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-exec-arrsub-rules-gen.event (b* (((mv ?name acl2::?event) (atc-exec-arrsub-rules-gen atype))) (pseudo-event-formp event)) :rule-classes :rewrite)
Function:
(defun atc-exec-arrsub-rules-gen-loop (atypes) (declare (xargs :guard (type-listp atypes))) (declare (xargs :guard (type-nonchar-integer-listp atypes))) (let ((__function__ 'atc-exec-arrsub-rules-gen-loop)) (declare (ignorable __function__)) (b* (((when (endp atypes)) (mv nil nil)) ((mv name event) (atc-exec-arrsub-rules-gen (car atypes))) ((mv more-names more-events) (atc-exec-arrsub-rules-gen-loop (cdr atypes)))) (mv (cons name more-names) (cons event more-events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-arrsub-rules-gen-loop.names (b* (((mv ?names ?events) (atc-exec-arrsub-rules-gen-loop atypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-arrsub-rules-gen-loop.events (b* (((mv ?names ?events) (atc-exec-arrsub-rules-gen-loop atypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-arrsub-rules-gen-all nil (declare (xargs :guard t)) (let ((__function__ 'atc-exec-arrsub-rules-gen-all)) (declare (ignorable __function__)) (b* (((mv names events) (atc-exec-arrsub-rules-gen-loop *nonchar-integer-types*))) (cons 'progn (cons (cons 'defsection (cons 'atc-exec-arrsub-rules (cons ':short (cons '"Rules for executing array subscript expressions." (append events (cons (cons 'defval (cons '*atc-exec-arrsub-rules* (cons (cons 'quote (cons names 'nil)) 'nil))) 'nil)))))) 'nil)))))
Theorem:
(defthm pseudo-event-formp-of-atc-exec-arrsub-rules-gen-all (b* ((event (atc-exec-arrsub-rules-gen-all))) (pseudo-event-formp event)) :rule-classes :rewrite)