|
|
|---|
|
|
|
|---|
Generate an updated symbol table according to executing a conditional statement.
(atc-gen-if/ifelse-inscope fn fn-guard
inscope then-inscope else-inscope
context new-context test-term then-term
else-term compst-var new-compst
then-new-compst else-new-compst
prec-tags thm-index names-to-avoid wrld)
→
(mv new-inscope events thm-index names-to-avoid)The
We generate proof builder instructions, in order to deal with the case split of the if in a controlled way.
Here we cannot use atc-gen-new-inscope, because we need to use more elaborate proof builder instructions than just a set of rules.
Function:
(defun atc-gen-if/ifelse-inscope-aux (fn fn-guard scope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (atc-symbol-varinfo-alistp scope) (atc-symbol-varinfo-alist-listp then-inscope) (atc-symbol-varinfo-alist-listp else-inscope) (atc-contextp context) (atc-contextp new-context) (symbolp compst-var) (atc-string-taginfo-alistp prec-tags) (posp thm-index) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-if/ifelse-inscope-aux)) (declare (ignorable __function__)) (b* (((when (endp scope)) (mv nil nil names-to-avoid)) ((cons var info) (car scope)) (type (atc-var-info->type info)) (externalp (atc-var-info->externalp info)) (type-pred (atc-type-to-recognizer type prec-tags)) (new-thm (pack fn '- var '-in-scope- thm-index)) ((mv new-thm names-to-avoid) (fresh-logical-name-with-$s-suffix new-thm nil names-to-avoid wrld)) (var/varptr (if (and (or (type-case type :pointer) (type-case type :array)) (not externalp)) (add-suffix-to-fn var "-PTR") var)) (formula1 (cons 'and (cons (cons 'objdesign-of-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons compst-var 'nil))) (cons (cons 'equal (cons (cons 'read-object (cons (cons 'objdesign-of-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons compst-var 'nil))) (cons compst-var 'nil))) (cons var/varptr 'nil))) (and (or (type-case type :pointer) (type-case type :array)) (not externalp) (cons (cons 'equal (cons (cons 'read-object (cons (add-suffix-to-fn var "-OBJDES") (cons compst-var 'nil))) (cons var 'nil))) 'nil)))))) (formula1 (atc-contextualize formula1 new-context fn fn-guard compst-var nil nil t wrld)) (formula2 (cons type-pred (cons var 'nil))) (formula2 (atc-contextualize formula2 new-context fn fn-guard nil nil nil nil wrld)) (formula (cons 'and (cons formula1 (cons formula2 'nil)))) (valuep-when-type-pred (atc-type-to-valuep-thm type prec-tags)) (not-flexiblep-thms (atc-type-to-notflexarrmem-thms type prec-tags)) (then-var-info (atc-get-var var then-inscope)) ((unless then-var-info) (raise "Internal error: ~x0 not in scope after 'then'." var) (mv nil nil nil)) (then-var-thm (atc-var-info->thm then-var-info)) (else-var-info (atc-get-var var else-inscope)) ((unless else-var-info) (raise "Internal error: ~x0 not in scope after 'else'." var) (mv nil nil nil)) (else-var-thm (atc-var-info->thm else-var-info)) (value-kind-thms (atc-string-taginfo-alist-to-value-kind-thms prec-tags)) (writer-return-thms (atc-string-taginfo-alist-to-writer-return-thms prec-tags)) (then-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons then-var-thm (cons 'read-object-of-enter-scope (cons 'read-object-of-update-object-same (cons 'objdesign-of-var-of-update-object-iff (cons 'objdesign-of-var-of-enter-scope-iff (cons 'update-object-of-update-object-same (cons 'read-object-of-update-object-disjoint (cons 'object-disjointp-commutative (cons 'update-object-of-enter-scope (cons 'compustate-frames-number-of-enter-scope-not-zero (cons 'compustatep-of-enter-scope (cons 'compustate-frames-number-of-update-object (cons 'read-object-of-objdesign-of-var-of-enter-scope (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'read-var-of-update-object (cons 'read-var-of-add-var (cons 'update-var-of-enter-scope (cons 'update-var-of-add-var (cons 'equal-of-ident-and-ident (cons '(:e str-fix) (cons 'exit-scope-of-enter-scope (cons 'compustatep-of-add-var (cons 'compustate-frames-number-of-add-var-not-zero (cons 'objdesign-of-var-of-add-var-iff (cons 'ident-fix-when-identp (cons 'identp-of-ident (cons 'read-object-of-objdesign-of-var-of-add-var (cons 'remove-flexible-array-member-when-absent (append not-flexiblep-thms (cons 'value-fix-when-valuep (cons valuep-when-type-pred (cons 'exit-scope-of-if* (cons 'objdesign-of-var-of-if*-when-both-objdesign-of-var (cons 'read-var-of-if* (cons 'read-var-of-enter-scope (cons 'acl2::if*-when-same (cons 'read-object-of-value-pointer->designator-of-if* (cons 'uchar-arrayp-of-uchar-array-write (cons 'schar-arrayp-of-schar-array-write (cons 'ushort-arrayp-of-ushort-array-write (cons 'sshort-arrayp-of-sshort-array-write (cons 'uint-arrayp-of-uint-array-write (cons 'sint-arrayp-of-sint-array-write (cons 'ulong-arrayp-of-ulong-array-write (cons 'slong-arrayp-of-slong-array-write (cons 'ullong-arrayp-of-ullong-array-write (cons 'sllong-arrayp-of-sllong-array-write (cons 'compustatep-of-update-object (append value-kind-thms (append writer-return-thms '(update-static-var-of-enter-scope compustatep-of-update-static-var compustate-frames-number-of-update-static-var compustate-frames-number-of-add-frame-not-zero objdesign-of-var-of-update-static-var-iff update-static-var-of-add-frame read-var-of-add-frame read-static-var-of-update-static-var compustate-frames-number-of-update-static-var compustatep-of-add-frame objdesign-of-var-of-add-frame-when-read-object-static read-object-of-objdesign-static (:t objdesign-static) read-static-var-of-add-frame mv-nth-of-cons (:e zp)))))))))))))))))))))))))))))))))))))))))))))))))))) 'nil)) 'nil))) 'nil)) (else-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons else-var-thm (cons 'read-object-of-enter-scope (cons 'read-object-of-update-object-same (cons 'objdesign-of-var-of-update-object-iff (cons 'objdesign-of-var-of-enter-scope-iff (cons 'update-object-of-update-object-same (cons 'read-object-of-update-object-disjoint (cons 'object-disjointp-commutative (cons 'update-object-of-enter-scope (cons 'compustate-frames-number-of-enter-scope-not-zero (cons 'compustatep-of-enter-scope (cons 'compustate-frames-number-of-update-object (cons 'read-object-of-objdesign-of-var-of-enter-scope (cons 'read-object-of-objdesign-of-var-to-read-var (cons 'read-var-of-update-object (cons 'read-var-of-add-var (cons 'update-var-of-enter-scope (cons 'update-var-of-add-var (cons 'equal-of-ident-and-ident (cons '(:e str-fix) (cons 'exit-scope-of-enter-scope (cons 'compustatep-of-add-var (cons 'compustate-frames-number-of-add-var-not-zero (cons 'objdesign-of-var-of-add-var-iff (cons 'ident-fix-when-identp (cons 'identp-of-ident (cons 'read-object-of-objdesign-of-var-of-add-var (cons 'remove-flexible-array-member-when-absent (append not-flexiblep-thms (cons 'value-fix-when-valuep (cons valuep-when-type-pred (cons 'exit-scope-of-if* (cons 'objdesign-of-var-of-if*-when-both-objdesign-of-var (cons 'read-var-of-if* (cons 'read-var-of-enter-scope (cons 'acl2::if*-when-same (cons 'read-object-of-value-pointer->designator-of-if* (cons 'uchar-arrayp-of-uchar-array-write (cons 'schar-arrayp-of-schar-array-write (cons 'ushort-arrayp-of-ushort-array-write (cons 'sshort-arrayp-of-sshort-array-write (cons 'uint-arrayp-of-uint-array-write (cons 'sint-arrayp-of-sint-array-write (cons 'ulong-arrayp-of-ulong-array-write (cons 'slong-arrayp-of-slong-array-write (cons 'ullong-arrayp-of-ullong-array-write (cons 'sllong-arrayp-of-sllong-array-write (cons 'compustatep-of-update-object (append value-kind-thms (append writer-return-thms '(update-static-var-of-enter-scope compustatep-of-update-static-var compustate-frames-number-of-update-static-var compustate-frames-number-of-add-frame-not-zero objdesign-of-var-of-update-static-var-iff update-static-var-of-add-frame read-var-of-add-frame read-static-var-of-update-static-var compustate-frames-number-of-update-static-var compustatep-of-add-frame objdesign-of-var-of-add-frame-when-read-object-static read-object-of-objdesign-static (:t objdesign-static) read-static-var-of-add-frame mv-nth-of-cons (:e zp)))))))))))))))))))))))))))))))))))))))))))))))))))) 'nil)) 'nil))) 'nil)) (instructions (cons (cons 'casesplit (cons (atc-contextualize test-term context nil nil nil nil nil nil wrld) 'nil)) (cons (cons 'claim (cons (atc-contextualize (cons 'test* (cons test-term 'nil)) context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(test*)))))) (cons '(drop 1) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons (cons 'if* (cons test-term (cons then-term (cons else-term 'nil)))) (cons then-term 'nil))) context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-true test*)))))) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons new-compst (cons then-new-compst 'nil))) context nil nil compst-var nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-true test*)))))) (cons (cons 'prove (cons ':hints (cons then-hints 'nil))) (cons (cons 'claim (cons (atc-contextualize (cons 'test* (cons (cons 'not (cons test-term 'nil)) 'nil)) context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(test*)))))) (cons '(drop 1) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons (cons 'if* (cons test-term (cons then-term (cons else-term 'nil)))) (cons else-term 'nil))) context nil nil nil nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-false test*)))))) (cons (cons 'claim (cons (atc-contextualize (cons 'equal (cons new-compst (cons else-new-compst 'nil))) context nil nil compst-var nil nil nil wrld) '(:hints (("Goal" :in-theory '(acl2::if*-when-false test*)))))) (cons (cons 'prove (cons ':hints (cons else-hints 'nil))) 'nil)))))))))))) ((mv event &) (evmac-generate-defthm new-thm :formula formula :instructions instructions :enable nil)) (new-info (change-atc-var-info info :thm new-thm)) (rest (cdr scope)) ((mv new-rest events names-to-avoid) (atc-gen-if/ifelse-inscope-aux fn fn-guard rest then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (mv (acons var new-info new-rest) (cons event events) names-to-avoid))))
Theorem:
(defthm atc-symbol-varinfo-alistp-of-atc-gen-if/ifelse-inscope-aux.new-scope (implies (atc-symbol-varinfo-alistp scope) (b* (((mv ?new-scope ?events ?names-to-avoid) (atc-gen-if/ifelse-inscope-aux fn fn-guard scope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (atc-symbol-varinfo-alistp new-scope))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-if/ifelse-inscope-aux.events (b* (((mv ?new-scope ?events ?names-to-avoid) (atc-gen-if/ifelse-inscope-aux fn fn-guard scope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-if/ifelse-inscope-aux.names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?new-scope ?events ?names-to-avoid) (atc-gen-if/ifelse-inscope-aux fn fn-guard scope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (symbol-listp names-to-avoid))) :rule-classes :rewrite)
Function:
(defun atc-gen-if/ifelse-inscope (fn fn-guard inscope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (atc-symbol-varinfo-alist-listp inscope) (atc-symbol-varinfo-alist-listp then-inscope) (atc-symbol-varinfo-alist-listp else-inscope) (atc-contextp context) (atc-contextp new-context) (symbolp compst-var) (atc-string-taginfo-alistp prec-tags) (posp thm-index) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-if/ifelse-inscope)) (declare (ignorable __function__)) (b* (((when (endp inscope)) (mv nil nil (1+ thm-index) names-to-avoid)) (scope (car inscope)) ((mv new-scope events names-to-avoid) (atc-gen-if/ifelse-inscope-aux fn fn-guard scope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld)) ((mv new-inscope more-events thm-index names-to-avoid) (atc-gen-if/ifelse-inscope fn fn-guard (cdr inscope) then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (mv (cons new-scope new-inscope) (append events more-events) thm-index names-to-avoid))))
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-if/ifelse-inscope.new-inscope (implies (atc-symbol-varinfo-alist-listp inscope) (b* (((mv ?new-inscope ?events ?thm-index ?names-to-avoid) (atc-gen-if/ifelse-inscope fn fn-guard inscope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (atc-symbol-varinfo-alist-listp new-inscope))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-if/ifelse-inscope.events (b* (((mv ?new-inscope ?events ?thm-index ?names-to-avoid) (atc-gen-if/ifelse-inscope fn fn-guard inscope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-if/ifelse-inscope.thm-index (implies (posp thm-index) (b* (((mv ?new-inscope ?events ?thm-index ?names-to-avoid) (atc-gen-if/ifelse-inscope fn fn-guard inscope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (posp thm-index))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-if/ifelse-inscope.names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?new-inscope ?events ?thm-index ?names-to-avoid) (atc-gen-if/ifelse-inscope fn fn-guard inscope then-inscope else-inscope context new-context test-term then-term else-term compst-var new-compst then-new-compst else-new-compst prec-tags thm-index names-to-avoid wrld))) (symbol-listp names-to-avoid))) :rule-classes :rewrite)