		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-init-scope-thms

Generate the theorems about the initial scope of a function execution.

Signature
(atc-gen-init-scope-thms fn fn-guard typed-formals prec-tags context-preamble prog-const fn-fun-env-thm compst-var fenv-var names-to-avoid state) → (mv expand-event expand-thm scopep-event scopep-thm omap-update-nest init-formals 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).; context-preamble — Guard (true-listp context-preamble).; prog-const — Guard (symbolp prog-const).; fn-fun-env-thm — Guard (symbolp fn-fun-env-thm).; compst-var — Guard (symbolp compst-var).; fenv-var — Guard (symbolp fenv-var).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: expand-event — Type (pseudo-event-formp expand-event).; expand-thm — Type (symbolp expand-thm).; scopep-event — Type (pseudo-event-formp scopep-event).; scopep-thm — Type (symbolp scopep-thm).; omap-update-nest — An untranslated term.; init-formals — Type (symbol-listp init-formals), given (atc-symbol-varinfo-alistp typed-formals).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp names-to-avoid).

We generate one theorem saying what the initial scope expands to, and one theorem saying that the expansion satisfies scopep.

We also return the omap::update nest term that describes the initial scope, for use in subsequent theorems.

Definitions and Theorems

Function: atc-gen-init-scope-thms

(defun atc-gen-init-scope-thms
       (fn fn-guard
           typed-formals prec-tags context-preamble
           prog-const fn-fun-env-thm compst-var
           fenv-var names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (symbolp fn)
                         (symbolp fn-guard)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-string-taginfo-alistp prec-tags)
                         (true-listp context-preamble)
                         (symbolp prog-const)
                         (symbolp fn-fun-env-thm)
                         (symbolp compst-var)
                         (symbolp fenv-var)
                         (symbol-listp names-to-avoid))))
 (let ((__function__ 'atc-gen-init-scope-thms))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((mv omap-update-nest init-formals)
     (atc-gen-omap-update-formals typed-formals))
    (formals (strip-cars typed-formals))
    (expand-thm (pack fn '-init-scope-expand))
    ((mv expand-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          expand-thm nil names-to-avoid wrld))
    (info-var (genvar$ 'atc "INFO" nil formals state))
    (formal-thms
         (atc-var-info-list->thm-list (strip-cdrs typed-formals)))
    (expand-formula
     (cons
      'implies
      (cons
       (cons
        'and
        (cons
         (cons 'compustatep
               (cons compst-var 'nil))
         (cons
          (cons
               'equal
               (cons fenv-var
                     (cons (cons 'init-fun-env
                                 (cons (cons 'preprocess
                                             (cons prog-const 'nil))
                                       'nil))
                           'nil)))
          (cons
           (cons
            'equal
            (cons
               info-var
               (cons (cons 'fun-env-lookup
                           (cons (cons 'ident
                                       (cons (symbol-name fn) 'nil))
                                 (cons fenv-var 'nil)))
                     'nil)))
           (append context-preamble
                   (cons (cons fn-guard formals) 'nil))))))
       (cons
        (cons
           'equal
           (cons (cons 'init-scope
                       (cons (cons 'fun-info->params
                                   (cons info-var 'nil))
                             (cons (cons 'list init-formals) 'nil)))
                 (cons omap-update-nest 'nil)))
        'nil))))
    (flexible-thms
         (atc-string-taginfo-alist-to-flexiblep-thms prec-tags))
    (value-kind-thms
         (atc-string-taginfo-alist-to-value-kind-thms prec-tags))
    (valuep-thms
         (atc-string-taginfo-alist-to-valuep-thms prec-tags))
    (type-of-value-thms
         (atc-string-taginfo-alist-to-type-of-value-thms prec-tags))
    (type-to-quoted-thms
        (atc-string-taginfo-alist-to-type-to-quoted-thms prec-tags))
    (pointer-type-to-quoted-thms (atc-string-taginfo-alist-to-pointer-type-to-quoted-thms
                                      prec-tags))
    (expand-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            fn-fun-env-thm
            (cons
             '(:e fun-info->params)
             (cons
              'init-scope-when-consp
              (cons
               '(:e param-declonp)
               (append
                formal-thms
                (cons
                 'valuep-when-ucharp
                 (cons
                  'valuep-when-scharp
                  (cons
                   'valuep-when-ushortp
                   (cons
                    'valuep-when-sshortp
                    (cons
                     'valuep-when-uintp
                     (cons
                      'valuep-when-sintp
                      (cons
                       'valuep-when-ulongp
                       (cons
                        'valuep-when-slongp
                        (cons
                         'valuep-when-ullongp
                         (cons
                          'valuep-when-sllongp
                          (append
                           valuep-thms
                           (cons
                            'value-kind-when-ucharp
                            (cons
                             'value-kind-when-scharp
                             (cons
                              'value-kind-when-ushortp
                              (cons
                               'value-kind-when-sshortp
                               (cons
                                'value-kind-when-uintp
                                (cons
                                 'value-kind-when-sintp
                                 (cons
                                  'value-kind-when-ulongp
                                  (cons
                                   'value-kind-when-slongp
                                   (cons
                                    'value-kind-when-ullongp
                                    (cons
                                     'value-kind-when-sllongp
                                     (append
                                      value-kind-thms
                                      (cons
                                       'type-of-value-when-ucharp
                                       (cons
                                        'type-of-value-when-scharp
                                        (cons
                                         'type-of-value-when-ushortp
                                         (cons
                                          'type-of-value-when-sshortp
                                          (cons
                                           'type-of-value-when-uintp
                                           (cons
                                            'type-of-value-when-sintp
                                            (cons
                                             'type-of-value-when-ulongp
                                             (cons
                                              'type-of-value-when-slongp
                                              (cons
                                               'type-of-value-when-ullongp
                                               (cons
                                                'type-of-value-when-sllongp
                                                (cons
                                                 'type-of-value-when-value-pointer
                                                 (append
                                                  type-of-value-thms
                                                  (append
                                                   type-to-quoted-thms
                                                   (append
                                                    pointer-type-to-quoted-thms
                                                    (cons
                                                     'not-flexible-array-member-p-when-ucharp
                                                     (cons
                                                      'not-flexible-array-member-p-when-scharp
                                                      (cons
                                                       'not-flexible-array-member-p-when-ushortp
                                                       (cons
                                                        'not-flexible-array-member-p-when-sshortp
                                                        (cons
                                                         'not-flexible-array-member-p-when-uintp
                                                         (cons
                                                          'not-flexible-array-member-p-when-sintp
                                                          (cons
                                                           'not-flexible-array-member-p-when-ulongp
                                                           (cons
                                                            'not-flexible-array-member-p-when-slongp
                                                            (cons
                                                             'not-flexible-array-member-p-when-ullongp
                                                             (cons
                                                              'not-flexible-array-member-p-when-sllongp
                                                              (cons
                                                               'not-flexible-array-member-p-when-value-pointer
                                                               (cons
                                                                'not-flexible-array-member-p-when-value-struct
                                                                (append
                                                                 flexible-thms
                                                                 '(remove-flexible-array-member-when-absent
                                                                   value-fix-when-valuep
                                                                   (:e
                                                                    param-declon-to-ident+tyname)
                                                                   mv-nth-of-cons
                                                                   (:e
                                                                    zp)
                                                                   (:e
                                                                    tyname-to-type)
                                                                   (:e
                                                                    adjust-type)
                                                                   value-listp-of-cons
                                                                   (:e
                                                                    value-listp)
                                                                   (:e
                                                                    init-scope)
                                                                   (:e
                                                                    scopep)
                                                                   (:e
                                                                    type-uchar)
                                                                   (:e
                                                                    type-schar)
                                                                   (:e
                                                                    type-ushort)
                                                                   (:e
                                                                    type-sshort)
                                                                   (:e
                                                                    type-uint)
                                                                   (:e
                                                                    type-sint)
                                                                   (:e
                                                                    type-ulong)
                                                                   (:e
                                                                    type-slong)
                                                                   (:e
                                                                    type-ullong)
                                                                   (:e
                                                                    type-sllong)
                                                                   (:e
                                                                    type-pointer)
                                                                   omap::assoc-of-update
                                                                   (:e
                                                                    omap::assoc)
                                                                   scopep-of-update
                                                                   omap-update-of-const-identifier
                                                                   (:e
                                                                    identp)
                                                                   (:e
                                                                    ident->name)
                                                                   identp-of-ident
                                                                   equal-of-ident
                                                                   (:e
                                                                    str-fix))))))))))))))))))))))))))))))))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv expand-event &)
     (evmac-generate-defthm expand-thm
                            :formula expand-formula
                            :hints expand-hints
                            :enable nil))
    (scopep-thm (pack fn '-init-scope-scopep))
    ((mv scopep-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          scopep-thm nil names-to-avoid wrld))
    (scopep-formula
     (cons
      'implies
      (cons
          (cons 'and
                (cons (cons 'compustatep
                            (cons compst-var 'nil))
                      (append context-preamble
                              (cons (cons fn-guard formals) 'nil))))
          (cons (cons 'scopep
                      (cons omap-update-nest 'nil))
                'nil))))
    (valuep-thms
         (atc-string-taginfo-alist-to-valuep-thms prec-tags))
    (scopep-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'scopep-of-update
            (cons
             '(:e scopep)
             (cons
              'identp-of-ident
              (append
               formal-thms
               (cons
                'valuep-when-ucharp
                (cons
                 'valuep-when-scharp
                 (cons
                  'valuep-when-ushortp
                  (cons
                   'valuep-when-sshortp
                   (cons
                    'valuep-when-uintp
                    (cons
                     'valuep-when-sintp
                     (cons
                         'valuep-when-ulongp
                         (cons 'valuep-when-slongp
                               (cons 'valuep-when-ullongp
                                     (cons 'valuep-when-sllongp
                                           valuep-thms))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv scopep-event &)
     (evmac-generate-defthm scopep-thm
                            :formula scopep-formula
                            :hints scopep-hints
                            :enable nil)))
   (mv expand-event expand-thm
       scopep-event scopep-thm omap-update-nest
       init-formals names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-init-scope-thms.expand-event

(defthm pseudo-event-formp-of-atc-gen-init-scope-thms.expand-event
  (b* (((mv ?expand-event ?expand-thm ?scopep-event
            ?scopep-thm ?omap-update-nest
            ?init-formals ?names-to-avoid)
        (atc-gen-init-scope-thms
             fn fn-guard
             typed-formals prec-tags context-preamble
             prog-const fn-fun-env-thm compst-var
             fenv-var names-to-avoid state)))
    (pseudo-event-formp expand-event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-init-scope-thms.expand-thm

(defthm symbolp-of-atc-gen-init-scope-thms.expand-thm
  (b* (((mv ?expand-event ?expand-thm ?scopep-event
            ?scopep-thm ?omap-update-nest
            ?init-formals ?names-to-avoid)
        (atc-gen-init-scope-thms
             fn fn-guard
             typed-formals prec-tags context-preamble
             prog-const fn-fun-env-thm compst-var
             fenv-var names-to-avoid state)))
    (symbolp expand-thm))
  :rule-classes :rewrite)

Theorem: pseudo-event-formp-of-atc-gen-init-scope-thms.scopep-event

(defthm pseudo-event-formp-of-atc-gen-init-scope-thms.scopep-event
  (b* (((mv ?expand-event ?expand-thm ?scopep-event
            ?scopep-thm ?omap-update-nest
            ?init-formals ?names-to-avoid)
        (atc-gen-init-scope-thms
             fn fn-guard
             typed-formals prec-tags context-preamble
             prog-const fn-fun-env-thm compst-var
             fenv-var names-to-avoid state)))
    (pseudo-event-formp scopep-event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-init-scope-thms.scopep-thm

(defthm symbolp-of-atc-gen-init-scope-thms.scopep-thm
  (b* (((mv ?expand-event ?expand-thm ?scopep-event
            ?scopep-thm ?omap-update-nest
            ?init-formals ?names-to-avoid)
        (atc-gen-init-scope-thms
             fn fn-guard
             typed-formals prec-tags context-preamble
             prog-const fn-fun-env-thm compst-var
             fenv-var names-to-avoid state)))
    (symbolp scopep-thm))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-init-scope-thms.init-formals

(defthm symbol-listp-of-atc-gen-init-scope-thms.init-formals
  (implies (atc-symbol-varinfo-alistp typed-formals)
           (b* (((mv ?expand-event ?expand-thm ?scopep-event
                     ?scopep-thm ?omap-update-nest
                     ?init-formals ?names-to-avoid)
                 (atc-gen-init-scope-thms
                      fn fn-guard
                      typed-formals prec-tags context-preamble
                      prog-const fn-fun-env-thm compst-var
                      fenv-var names-to-avoid state)))
             (symbol-listp init-formals)))
  :rule-classes :rewrite)

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

(defthm symbol-listp-of-atc-gen-init-scope-thms.names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv ?expand-event ?expand-thm ?scopep-event
                     ?scopep-thm ?omap-update-nest
                     ?init-formals ?names-to-avoid)
                 (atc-gen-init-scope-thms
                      fn fn-guard
                      typed-formals prec-tags context-preamble
                      prog-const fn-fun-env-thm compst-var
                      fenv-var names-to-avoid state)))
             (symbol-listp names-to-avoid)))
  :rule-classes :rewrite)