		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-init-inscope

Generate the initial symbol table for a C function.

Signature
(atc-gen-init-inscope fn fn-guard typed-formals prec-tags compst-var context names-to-avoid wrld) → (mv inscope events names-to-avoid)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; compst-var — Guard (symbolp compst-var).; context — Guard (atc-contextp context).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: inscope — Type (atc-symbol-varinfo-alist-listp inscope), given (atc-symbol-varinfo-alistp typed-formals).; events — Type (pseudo-event-form-listp events).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

The initial symbol table consists of a scope for static storage and a scope for automatic storage.

Definitions and Theorems

Function: atc-gen-init-inscope

(defun atc-gen-init-inscope
       (fn fn-guard typed-formals prec-tags
           compst-var context names-to-avoid wrld)
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-string-taginfo-alistp prec-tags)
                         (symbolp compst-var)
                         (atc-contextp context)
                         (symbol-listp names-to-avoid)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-gen-init-inscope))
   (declare (ignorable __function__))
   (b*
     (((mv scope-static
           events-static names-to-avoid)
       (atc-gen-init-inscope-static
            fn fn-guard typed-formals prec-tags
            compst-var context names-to-avoid wrld))
      ((mv scope-auto events-auto names-to-avoid)
       (atc-gen-init-inscope-auto fn fn-guard
                                  typed-formals prec-tags compst-var
                                  context names-to-avoid wrld)))
     (mv (list scope-auto scope-static)
         (append events-static events-auto)
         names-to-avoid))))

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

(defthm
     atc-symbol-varinfo-alist-listp-of-atc-gen-init-inscope.inscope
 (implies
      (atc-symbol-varinfo-alistp typed-formals)
      (b* (((mv ?inscope ?events ?names-to-avoid)
            (atc-gen-init-inscope fn fn-guard
                                  typed-formals prec-tags compst-var
                                  context names-to-avoid wrld)))
        (atc-symbol-varinfo-alist-listp inscope)))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-init-inscope.events

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

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

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