		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-fundef

Transform a function definition.

Signature
(simpadd0-fundef fundef gin state) → (mv new-fundef gout)
Arguments: fundef — Guard (fundefp fundef).; gin — Guard (simpadd0-ginp gin).
Returns: new-fundef — Type (fundefp new-fundef).; gout — Type (simpadd0-goutp gout).

We generate a theorem for the function only under certain conditions, including the fact that a theorem for the body was generated.

The generated theorem contains local theorems that are used in the proof of the main theorem. The local theorems are about the initial scope of the function, and about the parameters in the computation state at the beginning of the execution of the function body.

If the body of the function underwent no transformation, which we can see from the diffp component of simpadd0-gout, the theorem generated for the body just talks about its type, but the theorem for the function always involves an equality between c::exec-fun. If diffp is nil, we make use of a theorem from the language formalization that says that execution without function calls does not depend on the function environment: we instantiate that theorem for the body, using the old and new function environments.

Definitions and Theorems

Function: simpadd0-fundef-loop

(defun simpadd0-fundef-loop (thms fun)
 (declare (xargs :guard (and (symbol-listp thms)
                             (stringp fun))))
 (let ((__function__ 'simpadd0-fundef-loop))
  (declare (ignorable __function__))
  (b*
   (((when (endp thms)) nil)
    (thm (car thms))
    (lemma-instance
     (cons
      ':instance
      (cons
       thm
       (cons
        (cons
         'fun
         (cons
          (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
          'nil))
        '((compst0 compst))))))
    (more-lemma-instances (simpadd0-fundef-loop (cdr thms) fun)))
   (cons lemma-instance more-lemma-instances))))

Theorem: true-listp-of-simpadd0-fundef-loop

(defthm true-listp-of-simpadd0-fundef-loop
  (b* ((lemma-instances (simpadd0-fundef-loop thms fun)))
    (true-listp lemma-instances))
  :rule-classes :rewrite)

Function: simpadd0-fundef

(defun simpadd0-fundef (fundef gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (fundefp fundef)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (fundef-unambp fundef)))
 (let ((__function__ 'simpadd0-fundef))
  (declare (ignorable __function__))
  (b*
   (((fundef fundef) fundef)
    ((mv new-spec (simpadd0-gout gout-spec))
     (simpadd0-decl-spec-list fundef.spec gin state))
    (gin (simpadd0-gin-update gin gout-spec))
    ((mv new-declor (simpadd0-gout gout-declor))
     (simpadd0-declor fundef.declor gin state))
    (gin (simpadd0-gin-update gin gout-declor))
    ((mv new-decls (simpadd0-gout gout-decls))
     (simpadd0-decl-list fundef.decls gin state))
    (gin (simpadd0-gin-update gin gout-decls))
    ((unless (stmt-case fundef.body :compound))
     (raise
      "Internal error: the body of ~x0 is not a compound statement."
      (fundef-fix fundef))
     (mv (irr-fundef) (irr-simpadd0-gout)))
    (items (stmt-compound->items fundef.body))
    ((mv new-items (simpadd0-gout gout-body))
     (simpadd0-block-item-list items gin state))
    ((simpadd0-gin gin)
     (simpadd0-gin-update gin gout-body))
    (new-body (stmt-compound new-items))
    (new-fundef (make-fundef :extension fundef.extension
                             :spec new-spec
                             :declor new-declor
                             :asm? fundef.asm?
                             :attribs fundef.attribs
                             :decls new-decls
                             :body new-body))
    (gout-no-thm
     (make-simpadd0-gout
      :events (append gout-spec.events gout-declor.events
                      gout-decls.events gout-body.events)
      :thm-name nil
      :thm-index gin.thm-index
      :names-to-avoid gin.names-to-avoid
      :vartys
      (omap::update*
           gout-spec.vartys
           (omap::update*
                gout-declor.vartys
                (omap::update* gout-decls.vartys gout-body.vartys)))
      :diffp (or gout-spec.diffp gout-declor.diffp
                 gout-decls.diffp gout-body.diffp)))
    ((unless gout-body.thm-name)
     (mv new-fundef gout-no-thm))
    ((unless (fundef-formalp fundef))
     (mv new-fundef gout-no-thm))
    ((declor declor) fundef.declor)
    ((when (consp declor.pointers))
     (mv new-fundef gout-no-thm))
    ((unless (dirdeclor-case declor.direct :function-params))
     (mv new-fundef gout-no-thm))
    (params (dirdeclor-function-params->params declor.direct))
    (dirdeclor (dirdeclor-function-params->declor declor.direct))
    ((unless (dirdeclor-case dirdeclor :ident))
     (raise "Internal error: ~x0 is not just the function name."
            dirdeclor)
     (mv (irr-fundef) (irr-simpadd0-gout)))
    (fun (ident->unwrap (dirdeclor-ident->ident dirdeclor)))
    ((unless (stringp fun))
     (raise "Internal error: non-string identifier ~x0."
            fun)
     (mv (irr-fundef) (irr-simpadd0-gout)))
    ((mv erp ldm-params)
     (ldm-param-declon-list params))
    ((when erp) (mv new-fundef gout-no-thm))
    (type (block-item-list-type items))
    ((unless (type-formalp type))
     (raise "Internal error: function ~x0 returns ~x1."
            (fundef-fix fundef)
            type)
     (mv (irr-fundef) (irr-simpadd0-gout)))
    ((mv & ctype) (ldm-type type))
    ((mv okp
         args parargs arg-types arg-types-compst)
     (simpadd0-gen-from-params ldm-params gin))
    ((unless okp)
     (mv new-fundef gout-no-thm))
    ((mv init-scope-thm-event
         init-scope-thm-name)
     (simpadd0-gen-init-scope-thm
          ldm-params args parargs arg-types))
    ((mv param-thm-events param-thm-names)
     (simpadd0-gen-param-thms args arg-types-compst
                              arg-types ldm-params args))
    (thm-name (packn-pos (list gin.const-new '-thm-
                               gin.thm-index)
                         gin.const-new))
    (thm-index (1+ gin.thm-index))
    (formula
     (cons
      'b*
      (cons
       (cons
        (cons 'old
              (cons (cons 'quote
                          (cons (fundef-fix fundef) 'nil))
                    'nil))
        (cons
         (cons 'new
               (cons (cons 'quote (cons new-fundef 'nil))
                     'nil))
         (cons
          (cons
           'fun
           (cons
            (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
            'nil))
          (cons
           (cons '(mv old-result old-compst)
                 (cons (cons 'c::exec-fun
                             (cons 'fun
                                   (cons (cons 'list args)
                                         '(compst old-fenv limit))))
                       'nil))
           (cons
            (cons
                 '(mv new-result new-compst)
                 (cons (cons 'c::exec-fun
                             (cons 'fun
                                   (cons (cons 'list args)
                                         '(compst new-fenv limit))))
                       'nil))
            'nil)))))
       (cons
        (cons
         'implies
         (cons
          (cons 'and
                (append arg-types
                        '((equal (c::fun-env-lookup fun old-fenv)
                                 (c::fun-info-from-fundef
                                      (mv-nth 1 (ldm-fundef old))))
                          (equal (c::fun-env-lookup fun new-fenv)
                                 (c::fun-info-from-fundef
                                      (mv-nth 1 (ldm-fundef new))))
                          (not (c::errorp old-result)))))
          (cons
           (cons
            'and
            (cons
             '(not (c::errorp new-result))
             (cons
              '(equal old-result new-result)
              (cons
               '(equal old-compst new-compst)
               (cons
                'old-result
                (cons
                   (cons 'equal
                         (cons '(c::type-of-value old-result)
                               (cons (cons 'quote (cons ctype 'nil))
                                     'nil)))
                   'nil))))))
           'nil)))
        'nil))))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':expand
        (cons
         (cons
          (cons 'c::exec-fun
                (cons (cons 'quote (cons (c::ident fun) 'nil))
                      (cons (cons 'list args)
                            '(compst old-fenv limit))))
          (cons (cons 'c::exec-fun
                      (cons (cons 'quote (cons (c::ident fun) 'nil))
                            (cons (cons 'list args)
                                  '(compst new-fenv limit))))
                'nil))
         (cons
          ':use
          (cons
           (append
            (and
             (not gout-body.diffp)
             (cons
              (cons
               ':instance
               (cons
                'c::exec-block-item-list-without-calls
                (cons
                 (cons
                  'items
                  (cons
                   (cons
                    'mv-nth
                    (cons
                     '1
                     (cons
                         (cons 'ldm-block-item-list
                               (cons (cons 'quote (cons items 'nil))
                                     'nil))
                         'nil)))
                   'nil))
                 (cons
                  (cons
                   'compst
                   (cons
                    (cons
                     'c::push-frame
                     (cons
                      (cons
                       'c::frame
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
                        (cons
                         (cons
                          'list
                          (cons
                           (cons
                            'c::init-scope
                            (cons
                                (cons 'quote (cons ldm-params 'nil))
                                (cons (cons 'list args) 'nil)))
                           'nil))
                         'nil)))
                      '(compst)))
                    'nil))
                  '((fenv old-fenv)
                    (fenv1 new-fenv)
                    (limit (1- limit)))))))
              'nil))
            (cons
             init-scope-thm-name
             (append
              (simpadd0-fundef-loop param-thm-names fun)
              (cons
               (cons
                ':instance
                (cons
                 gout-body.thm-name
                 (cons
                  (cons
                   'compst
                   (cons
                    (cons
                     'c::push-frame
                     (cons
                      (cons
                       'c::frame
                       (cons
                        (cons
                         'mv-nth
                         (cons
                          '1
                          (cons
                           (cons 'ldm-ident
                                 (cons (cons 'ident (cons fun 'nil))
                                       'nil))
                           'nil)))
                        (cons
                         (cons
                          'list
                          (cons
                           (cons
                            'c::init-scope
                            (cons
                                (cons 'quote (cons ldm-params 'nil))
                                (cons (cons 'list args) 'nil)))
                           'nil))
                         'nil)))
                      '(compst)))
                    'nil))
                  (append (and (not gout-body.diffp)
                               '((fenv old-fenv)))
                          '((limit (1- limit)))))))
               'nil))))
           '(:in-theory '((:e c::fun-info->body$inline)
                          (:e c::fun-info->params$inline)
                          (:e c::fun-info->result$inline)
                          (:e c::fun-info-from-fundef)
                          (:e ident)
                          (:e ldm-block-item-list)
                          (:e ldm-fundef)
                          (:e ldm-ident)
                          (:e ldm-type)
                          (:e ldm-block-item-list)
                          (:e c::tyname-to-type)
                          (:e c::type-sint)
                          (:e c::block-item-list-nocallsp)
                          c::errorp-of-error)))))))
      'nil))
    (thm-event
     (cons
      'defruled
      (cons
       thm-name
       (cons
        formula
        (cons
         ':hints
         (cons
            hints
            (cons ':prep-lemmas
                  (cons (cons init-scope-thm-event param-thm-events)
                        'nil)))))))))
   (mv
    new-fundef
    (make-simpadd0-gout
      :events (append gout-spec.events
                      gout-declor.events gout-decls.events
                      gout-body.events (list thm-event))
      :thm-name thm-name
      :thm-index thm-index
      :names-to-avoid (cons thm-name gout-body.names-to-avoid)
      :vartys
      (omap::update*
           gout-spec.vartys
           (omap::update*
                gout-declor.vartys
                (omap::update* gout-decls.vartys gout-body.vartys)))
      :diffp (or gout-spec.diffp gout-declor.diffp
                 gout-decls.diffp gout-body.diffp))))))

Theorem: fundefp-of-simpadd0-fundef.new-fundef

(defthm fundefp-of-simpadd0-fundef.new-fundef
  (b* (((mv ?new-fundef ?gout)
        (simpadd0-fundef fundef gin state)))
    (fundefp new-fundef))
  :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-fundef.gout

(defthm simpadd0-goutp-of-simpadd0-fundef.gout
  (b* (((mv ?new-fundef ?gout)
        (simpadd0-fundef fundef gin state)))
    (simpadd0-goutp gout))
  :rule-classes :rewrite)

Theorem: fundef-unambp-of-simpadd0-fundef

(defthm fundef-unambp-of-simpadd0-fundef
  (b* (((mv ?new-fundef ?gout)
        (simpadd0-fundef fundef gin state)))
    (fundef-unambp new-fundef)))

Theorem: simpadd0-fundef-of-fundef-fix-fundef

(defthm simpadd0-fundef-of-fundef-fix-fundef
  (equal (simpadd0-fundef (fundef-fix fundef)
                          gin state)
         (simpadd0-fundef fundef gin state)))

Theorem: simpadd0-fundef-fundef-equiv-congruence-on-fundef

(defthm simpadd0-fundef-fundef-equiv-congruence-on-fundef
  (implies (c$::fundef-equiv fundef fundef-equiv)
           (equal (simpadd0-fundef fundef gin state)
                  (simpadd0-fundef fundef-equiv gin state)))
  :rule-classes :congruence)

Theorem: simpadd0-fundef-of-simpadd0-gin-fix-gin

(defthm simpadd0-fundef-of-simpadd0-gin-fix-gin
  (equal (simpadd0-fundef fundef (simpadd0-gin-fix gin)
                          state)
         (simpadd0-fundef fundef gin state)))

Theorem: simpadd0-fundef-simpadd0-gin-equiv-congruence-on-gin

(defthm simpadd0-fundef-simpadd0-gin-equiv-congruence-on-gin
  (implies (simpadd0-gin-equiv gin gin-equiv)
           (equal (simpadd0-fundef fundef gin state)
                  (simpadd0-fundef fundef gin-equiv state)))
  :rule-classes :congruence)