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

For now we only generate a theorem if the function has all int parameters and a theorem was generated for the functions's body. The 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.

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 'c$::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 (c$::irr-fundef)
         (irr-simpadd0-gout)))
    (items (c$::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
        :vars (union gout-spec.vars
                     (union gout-declor.vars
                            (union gout-decls.vars gout-body.vars)))
        :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 (c$::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 (c$::dirdeclor-function-params->decl declor.direct))
    ((unless (dirdeclor-case dirdeclor :ident))
     (raise "Internal error: ~x0 is not just the function name."
            dirdeclor)
     (mv (c$::irr-fundef)
         (irr-simpadd0-gout)))
    (fun (ident->unwrap (c$::dirdeclor-ident->ident dirdeclor)))
    ((unless (stringp fun))
     (raise "Internal error: non-string identifier ~x0."
            fun)
     (mv (c$::irr-fundef)
         (irr-simpadd0-gout)))
    ((mv erp ldm-params)
     (c$::ldm-paramdecl-list params))
    ((when erp) (mv new-fundef gout-no-thm))
    ((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
                              arg-types-compst 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 'c$::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 (c$::ldm-fundef old))))
                       (equal (c::fun-env-lookup fun new-fenv)
                              (c::fun-info-from-fundef
                                   (mv-nth 1 (c$::ldm-fundef new))))
                       (not (c::errorp old-result)))))
          '((and (not (c::errorp new-result))
                 (equal old-result new-result)
                 (equal old-compst new-compst)
                 old-result
                 (equal (c::value-kind old-result)
                        :sint)))))
        '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
           (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 'c$::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))
                 '((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 c$::ldm-block-item-list)
                          (:e c$::ldm-fundef)
                          (:e c$::ldm-ident)
                          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)
        :vars (union gout-spec.vars
                     (union gout-declor.vars
                            (union gout-decls.vars gout-body.vars)))
        :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)