Generate an updated symbol table according to declaring a new local variable.
(atc-gen-vardecl-inscope fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld) → (mv new-inscope new-context events thm-index names-to-avoid)
The context is updated with a let binding for the variable followed by a let binding for the computation state; we return the updated context. We use atc-gen-new-inscope to generate most of the new symbol table and then we add the new variable (to the innermost scope), along with a theorem for the new variable. The term to which the variable is bound is passed as argument here, along with its associated theorem, which we use in the generated hints.
Function:
(defun atc-gen-vardecl-inscope (fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (atc-symbol-varinfo-alist-listp inscope) (atc-contextp context) (symbolp var) (typep type) (symbolp term-thm) (symbolp compst-var) (atc-string-taginfo-alistp prec-tags) (posp thm-index) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-vardecl-inscope)) (declare (ignorable __function__)) (b* ((var-premise (make-atc-premise-cvalue :var var :term term)) (cs-premise-term (cons 'add-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons var (cons compst-var 'nil))))) (cs-premise (make-atc-premise-compustate :var compst-var :term cs-premise-term)) (new-context (atc-context-extend context (list var-premise cs-premise))) (rules '(objdesign-of-var-of-enter-scope-iff objdesign-of-var-of-add-var-iff read-object-of-objdesign-of-var-of-add-var read-object-of-objdesign-of-var-of-enter-scope ident-fix-when-identp identp-of-ident equal-of-ident-and-ident (:e str-fix) read-object-of-add-var)) ((mv new-inscope new-inscope-events names-to-avoid) (atc-gen-new-inscope fn fn-guard inscope new-context compst-var rules prec-tags thm-index names-to-avoid wrld)) (var-in-scope-thm (pack fn '- var '-in-scope- thm-index)) (thm-index (1+ thm-index)) ((mv var-in-scope-thm names-to-avoid) (fresh-logical-name-with-$s-suffix var-in-scope-thm nil names-to-avoid wrld)) (type-pred (atc-type-to-recognizer type prec-tags)) (var-in-scope-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 'nil))) 'nil)))) (var-in-scope-formula1 (atc-contextualize var-in-scope-formula1 new-context fn fn-guard compst-var nil nil t wrld)) (var-in-scope-formula2 (cons type-pred (cons var 'nil))) (var-in-scope-formula2 (atc-contextualize var-in-scope-formula2 new-context fn fn-guard nil nil nil nil wrld)) (var-in-scope-formula (cons 'and (cons var-in-scope-formula1 (cons var-in-scope-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)) (var-in-scope-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'objdesign-of-var-of-add-var-iff (cons 'read-object-of-objdesign-of-var-of-add-var (cons 'ident-fix-when-identp (cons 'identp-of-ident (cons 'equal-of-ident-and-ident (cons '(:e str-fix) (cons 'remove-flexible-array-member-when-absent (append not-flexiblep-thms (cons 'value-fix-when-valuep (cons valuep-when-type-pred (cons term-thm 'nil))))))))))) 'nil)) 'nil))) 'nil)) ((mv var-in-scope-event &) (evmac-generate-defthm var-in-scope-thm :formula var-in-scope-formula :hints var-in-scope-hints :enable nil)) (varinfo (make-atc-var-info :type type :thm var-in-scope-thm :externalp nil)) (new-inscope (atc-add-var var varinfo new-inscope))) (mv new-inscope new-context (append new-inscope-events (list var-in-scope-event)) thm-index names-to-avoid))))
Theorem:
(defthm atc-symbol-varinfo-alist-listp-of-atc-gen-vardecl-inscope.new-inscope (implies (atc-symbol-varinfo-alist-listp inscope) (b* (((mv ?new-inscope ?new-context ?events ?thm-index ?names-to-avoid) (atc-gen-vardecl-inscope fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld))) (atc-symbol-varinfo-alist-listp new-inscope))) :rule-classes :rewrite)
Theorem:
(defthm atc-contextp-of-atc-gen-vardecl-inscope.new-context (implies (atc-contextp context) (b* (((mv ?new-inscope ?new-context ?events ?thm-index ?names-to-avoid) (atc-gen-vardecl-inscope fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld))) (atc-contextp new-context))) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-vardecl-inscope.events (b* (((mv ?new-inscope ?new-context ?events ?thm-index ?names-to-avoid) (atc-gen-vardecl-inscope fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-vardecl-inscope.thm-index (implies (posp thm-index) (b* (((mv ?new-inscope ?new-context ?events ?thm-index ?names-to-avoid) (atc-gen-vardecl-inscope fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld))) (posp thm-index))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-vardecl-inscope.names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?new-inscope ?new-context ?events ?thm-index ?names-to-avoid) (atc-gen-vardecl-inscope fn fn-guard inscope context var type term term-thm compst-var prec-tags thm-index names-to-avoid wrld))) (symbol-listp names-to-avoid))) :rule-classes :rewrite)