Code to generate the rules for executing cast operations.
The hints expand
exec-cast,
convert-integer-value,
value-integer, and
value-integer->get,
which produces something like
Function:
(defun atc-exec-cast-rules-gen (dtype stype) (declare (xargs :guard (and (typep dtype) (typep stype)))) (declare (xargs :guard (and (type-nonchar-integerp dtype) (type-nonchar-integerp stype)))) (let ((__function__ 'atc-exec-cast-rules-gen)) (declare (ignorable __function__)) (b* ((dfixtype (integer-type-to-fixtype dtype)) (sfixtype (integer-type-to-fixtype stype)) (spred (pack sfixtype 'p)) (name (pack 'exec-cast-of- dfixtype '-when- spred)) (dtyname (type-to-tyname dtype)) (dtype-from-stype (pack dfixtype '-from- sfixtype)) (dtype-from-stype-okp (pack dtype-from-stype '-okp)) (guardp (and (not (equal dtype stype)) (or (type-case dtype :schar) (and (type-case dtype :sshort) (not (member-eq (type-kind stype) '(:schar)))) (and (type-case dtype :sint) (not (member-eq (type-kind stype) '(:schar :sshort)))) (and (type-case dtype :slong) (not (member-eq (type-kind stype) '(:schar :sshort :sint)))) (and (type-case dtype :sllong) (not (member-eq (type-kind stype) '(:schar :sshort :sint :slong))))))) (hyps (cons 'and (cons (atc-syntaxp-hyp-for-expr-pure 'x) (cons (cons spred '(x)) (and guardp (cons (cons dtype-from-stype-okp '(x)) 'nil)))))) (rhs (if (equal dtype stype) 'x (cons dtype-from-stype '(x)))) (formula (cons 'implies (cons hyps (cons (cons 'equal (cons (cons 'exec-cast (cons (cons 'quote (cons dtyname 'nil)) '((expr-value x objdes)))) (cons (cons 'expr-value (cons rhs '(nil))) 'nil))) 'nil)))) (hints (cons ':enable (cons (cons 'exec-cast (cons 'eval-cast (cons 'convert-integer-value (cons 'value-integer (append *atc-value-integer->get-rules* (cons 'integer-type-rangep (cons 'integer-type-min (cons 'integer-type-max (cons 'value-schar-to-schar-from-integer (cons 'value-uchar-to-uchar-from-integer (cons 'value-sshort-to-sshort-from-integer (cons 'value-ushort-to-ushort-from-integer (cons 'value-sint-to-sint-from-integer (cons 'value-uint-to-uint-from-integer (cons 'value-slong-to-slong-from-integer (cons 'value-ulong-to-ulong-from-integer (cons 'value-sllong-to-sllong-from-integer (cons 'value-ullong-to-ullong-from-integer (cons 'uchar-from-integer-mod (cons 'ushort-from-integer-mod (cons 'uint-from-integer-mod (cons 'ulong-from-integer-mod (cons 'ullong-from-integer-mod (cons 'schar-integerp-alt-def (cons 'uchar-integerp-alt-def (cons 'sshort-integerp-alt-def (cons 'ushort-integerp-alt-def (cons 'sint-integerp-alt-def (cons 'uint-integerp-alt-def (cons 'slong-integerp-alt-def (cons 'ulong-integerp-alt-def (cons 'sllong-integerp-alt-def (cons 'ullong-integerp-alt-def (append (and (not (equal dtype stype)) (list dtype-from-stype)) (append (and guardp (list dtype-from-stype-okp)) '(apconvert-expr-value-when-not-value-array value-kind-when-ucharp value-kind-when-scharp value-kind-when-ushortp value-kind-when-sshortp value-kind-when-uintp value-kind-when-sintp value-kind-when-ulongp value-kind-when-slongp value-kind-when-ullongp value-kind-when-sllongp ifix not-errorp-when-expr-valuep not-errorp-when-valuep valuep-when-ucharp valuep-when-scharp valuep-when-ushortp valuep-when-sshortp valuep-when-uintp valuep-when-sintp valuep-when-ulongp valuep-when-slongp valuep-when-ullongp valuep-when-sllongp value-integerp value-unsigned-integerp value-signed-integerp)))))))))))))))))))))))))))))))))))) '(:disable ((:e tau-system)))))) (event (cons 'defruled (cons name (cons formula hints))))) (mv name event))))
Theorem:
(defthm symbolp-of-atc-exec-cast-rules-gen.name (b* (((mv ?name acl2::?event) (atc-exec-cast-rules-gen dtype stype))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-exec-cast-rules-gen.event (b* (((mv ?name acl2::?event) (atc-exec-cast-rules-gen dtype stype))) (pseudo-event-formp event)) :rule-classes :rewrite)
Function:
(defun atc-exec-cast-rules-gen-loop-stypes (dtype stypes) (declare (xargs :guard (and (typep dtype) (type-listp stypes)))) (declare (xargs :guard (and (type-nonchar-integerp dtype) (type-nonchar-integer-listp stypes)))) (let ((__function__ 'atc-exec-cast-rules-gen-loop-stypes)) (declare (ignorable __function__)) (b* (((when (endp stypes)) (mv nil nil)) ((mv name event) (atc-exec-cast-rules-gen dtype (car stypes))) ((mv names events) (atc-exec-cast-rules-gen-loop-stypes dtype (cdr stypes)))) (mv (cons name names) (cons event events)))))
Theorem:
(defthm symbol-listp-of-atc-exec-cast-rules-gen-loop-stypes.names (b* (((mv ?names ?events) (atc-exec-cast-rules-gen-loop-stypes dtype stypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-cast-rules-gen-loop-stypes.events (b* (((mv ?names ?events) (atc-exec-cast-rules-gen-loop-stypes dtype stypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-cast-rules-gen-loop-dtypes (dtypes stypes) (declare (xargs :guard (and (type-listp dtypes) (type-listp stypes)))) (declare (xargs :guard (and (type-nonchar-integer-listp dtypes) (type-nonchar-integer-listp stypes)))) (let ((__function__ 'atc-exec-cast-rules-gen-loop-dtypes)) (declare (ignorable __function__)) (b* (((when (endp dtypes)) (mv nil nil)) ((mv names events) (atc-exec-cast-rules-gen-loop-stypes (car dtypes) stypes)) ((mv names1 events1) (atc-exec-cast-rules-gen-loop-dtypes (cdr dtypes) stypes))) (mv (append names names1) (append events events1)))))
Theorem:
(defthm symbol-listp-of-atc-exec-cast-rules-gen-loop-dtypes.names (b* (((mv ?names ?events) (atc-exec-cast-rules-gen-loop-dtypes dtypes stypes))) (symbol-listp names)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-exec-cast-rules-gen-loop-dtypes.events (b* (((mv ?names ?events) (atc-exec-cast-rules-gen-loop-dtypes dtypes stypes))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Function:
(defun atc-exec-cast-rules-gen-all nil (declare (xargs :guard t)) (let ((__function__ 'atc-exec-cast-rules-gen-all)) (declare (ignorable __function__)) (b* (((mv names events) (atc-exec-cast-rules-gen-loop-dtypes *nonchar-integer-types* *nonchar-integer-types*))) (cons 'progn (cons (cons 'defsection (cons 'atc-exec-cast-rules (cons ':short (cons '"Rules for executing casts." (append events (cons (cons 'defval (cons '*atc-exec-cast-rules* (cons (cons 'quote (cons names 'nil)) 'nil))) 'nil)))))) 'nil)))))
Theorem:
(defthm pseudo-event-formp-of-atc-exec-cast-rules-gen-all (b* ((event (atc-exec-cast-rules-gen-all))) (pseudo-event-formp event)) :rule-classes :rewrite)