		Search-engine friendly clone of the ACL2 documentation.

Atc-theorem-generation

Atc-gen-enter-inscope

Generate an updated symbol table according to entering a new scope.

Signature
(atc-gen-enter-inscope fn fn-guard inscope context 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).; 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 computation state that updates it via enter-scope; we return the updated context. We use atc-gen-new-inscope to generate most of the new symbol table and then we add a new empty scope to it.

The theorems for the new symbol table are proved from the old ones using the rule that reduces objdesign-of-var and read-object of enter-scope to just objdesign-of-var and read-object. The hypothesis of that rule saying that there are frames is discharged via the rules in atc-compustate-frames-number-rules: the computation state that enter-scope is applied to always starts with add-frame or enter-scope or add-var; there may be other forms possible, which we will handle later. For pointers, we also need the rule that reduces read-object of the object designator of enter-scope to just read-object of enter-scope.

Definitions and Theorems

Function: atc-gen-enter-inscope

(defun atc-gen-enter-inscope
       (fn fn-guard inscope context 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 compst-var)
                         (atc-string-taginfo-alistp prec-tags)
                         (posp thm-index)
                         (symbol-listp names-to-avoid)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-enter-inscope))
  (declare (ignorable __function__))
  (b* ((premise (make-atc-premise-compustate
                     :var compst-var
                     :term (cons 'enter-scope
                                 (cons compst-var 'nil))))
       (new-context (atc-context-extend context (list premise)))
       (rules '(objdesign-of-var-of-enter-scope-iff
                    read-object-of-objdesign-of-var-of-enter-scope
                    compustate-frames-number-of-add-frame-not-zero
                    compustate-frames-number-of-enter-scope-not-zero
                    compustate-frames-number-of-add-var-not-zero
                    read-object-of-enter-scope))
       ((mv 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)))
    (mv (cons nil new-inscope)
        new-context events (1+ thm-index)
        names-to-avoid))))

Theorem: atc-symbol-varinfo-alist-listp-of-atc-gen-enter-inscope.new-inscope

(defthm
 atc-symbol-varinfo-alist-listp-of-atc-gen-enter-inscope.new-inscope
 (implies
   (atc-symbol-varinfo-alist-listp inscope)
   (b* (((mv ?new-inscope ?new-context
             ?events ?thm-index ?names-to-avoid)
         (atc-gen-enter-inscope fn fn-guard
                                inscope context 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-enter-inscope.new-context

(defthm atc-contextp-of-atc-gen-enter-inscope.new-context
 (implies
   (atc-contextp context)
   (b* (((mv ?new-inscope ?new-context
             ?events ?thm-index ?names-to-avoid)
         (atc-gen-enter-inscope fn fn-guard
                                inscope context 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-enter-inscope.events

(defthm pseudo-event-form-listp-of-atc-gen-enter-inscope.events
  (b* (((mv ?new-inscope ?new-context
            ?events ?thm-index ?names-to-avoid)
        (atc-gen-enter-inscope fn fn-guard
                               inscope context compst-var prec-tags
                               thm-index names-to-avoid wrld)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: posp-of-atc-gen-enter-inscope.thm-index

(defthm posp-of-atc-gen-enter-inscope.thm-index
 (implies
   (posp thm-index)
   (b* (((mv ?new-inscope ?new-context
             ?events ?thm-index ?names-to-avoid)
         (atc-gen-enter-inscope fn fn-guard
                                inscope context compst-var prec-tags
                                thm-index names-to-avoid wrld)))
     (posp thm-index)))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-enter-inscope.names-to-avoid

(defthm symbol-listp-of-atc-gen-enter-inscope.names-to-avoid
 (implies
   (symbol-listp names-to-avoid)
   (b* (((mv ?new-inscope ?new-context
             ?events ?thm-index ?names-to-avoid)
         (atc-gen-enter-inscope fn fn-guard
                                inscope context compst-var prec-tags
                                thm-index names-to-avoid wrld)))
     (symbol-listp names-to-avoid)))
 :rule-classes :rewrite)