		Search-engine friendly clone of the ACL2 documentation.

Atc-theorem-generation

Atc-gen-vardecl-inscope

Generate an updated symbol table according to declaring a new local variable.

Signature
(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)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; inscope — Guard (atc-symbol-varinfo-alist-listp inscope).; context — Guard (atc-contextp context).; var — Guard (symbolp var).; type — Guard (typep type).; term — An untranslated term.; term-thm — Guard (symbolp term-thm).; compst-var — Guard (symbolp compst-var).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; thm-index — Guard (posp thm-index).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: new-inscope — Type (atc-symbol-varinfo-alist-listp new-inscope), given (atc-symbol-varinfo-alist-listp inscope).; new-context — Type (atc-contextp new-context), given (atc-contextp context).; events — Type (pseudo-event-form-listp events).; thm-index — Type (posp thm-index), given (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp 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.

Definitions and Theorems

Function: atc-gen-vardecl-inscope

(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: atc-symbol-varinfo-alist-listp-of-atc-gen-vardecl-inscope.new-inscope

(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: atc-contextp-of-atc-gen-vardecl-inscope.new-context

(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: pseudo-event-form-listp-of-atc-gen-vardecl-inscope.events

(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: posp-of-atc-gen-vardecl-inscope.thm-index

(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: symbol-listp-of-atc-gen-vardecl-inscope.names-to-avoid

(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)