		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop

Generate a C loop from a recursive ACL2 function, with accompanying theorems.

Signature
(atc-gen-loop fn prec-fns prec-tags prec-objs proofs prog-const fn-thms fn-appconds appcond-thms print names-to-avoid state) → (mv erp events updated-prec-fns updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; proofs — Guard (booleanp proofs).; prog-const — Guard (symbolp prog-const).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; fn-appconds — Guard (symbol-symbol-alistp fn-appconds).; appcond-thms — Guard (keyword-symbol-alistp appcond-thms).; print — Guard (evmac-input-print-p print).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: events — Type (pseudo-event-form-listp events).; updated-prec-fns — Type (atc-symbol-fninfo-alistp updated-prec-fns), given (and (symbolp fn) (atc-symbol-fninfo-alistp prec-fns)).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

This is called if fn is a recursive target function. We process the function body as a loop term, and update the prec-fns alist with information about the function.

We also generate the measure function for fn here. See atc-gen-loop-measure-fn.

No C external declaration is generated for this function, because this function just represents a loop used in oher functions.

For now we do not generate a guard function for the guard of fn; also, we do not generate theorems for the formal parameters for now. We will change this soon.

Definitions and Theorems

Function: atc-gen-loop

(defun atc-gen-loop (fn prec-fns prec-tags prec-objs
                        proofs prog-const fn-thms fn-appconds
                        appcond-thms print names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (atc-symbol-fninfo-alistp prec-fns)
                             (atc-string-taginfo-alistp prec-tags)
                             (atc-string-objinfo-alistp prec-objs)
                             (booleanp proofs)
                             (symbolp prog-const)
                             (symbol-symbol-alistp fn-thms)
                             (symbol-symbol-alistp fn-appconds)
                             (keyword-symbol-alistp appcond-thms)
                             (evmac-input-print-p print)
                             (symbol-listp names-to-avoid))))
 (declare (xargs :guard (and (function-symbolp fn (w state))
                             (logicp fn (w state))
                             (irecursivep+ fn (w state))
                             (not (eq fn 'quote)))))
 (let ((__function__ 'atc-gen-loop))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil nil nil)
    (wrld (w state))
    ((mv measure-of-fn-event measure-of-fn
         measure-formals names-to-avoid)
     (if proofs (atc-gen-loop-measure-fn fn names-to-avoid state)
       (mv '(_) nil nil names-to-avoid)))
    ((mv fn-guard-event fn-guard names-to-avoid)
     (atc-gen-fn-guard fn names-to-avoid state))
    ((erp typed-formals
          formals-events names-to-avoid)
     (atc-typed-formals fn fn-guard prec-tags
                        prec-objs names-to-avoid wrld))
    (body (ubody+ fn wrld))
    ((erp (lstmt-gout loop))
     (atc-gen-loop-stmt
          body
          (make-lstmt-gin :context (make-atc-context :preamble nil
                                                     :premises nil)
                          :typed-formals typed-formals
                          :inscope (list typed-formals)
                          :fn fn
                          :fn-guard nil
                          :compst-var nil
                          :fenv-var nil
                          :limit-var nil
                          :measure-for-fn measure-of-fn
                          :measure-formals measure-formals
                          :prec-fns prec-fns
                          :prec-tags prec-tags
                          :prec-objs prec-objs
                          :thm-index 1
                          :names-to-avoid names-to-avoid
                          :proofs nil)
          state))
    (names-to-avoid loop.names-to-avoid)
    ((erp events
          natp-of-measure-of-fn-thm fn-result-thm
          fn-correct-thm names-to-avoid)
     (if proofs
      (b*
       (((reterr) nil nil nil nil nil)
        ((mv fn-result-events
             fn-result-thm names-to-avoid)
         (atc-gen-fn-result-thm fn nil loop.affect
                                typed-formals prec-fns prec-tags
                                prec-objs names-to-avoid state))
        (loop-test (stmt-while->test loop.stmt))
        (loop-body (stmt-while->body loop.stmt))
        ((mv exec-stmt-while-events
             exec-stmt-while-for-fn
             exec-stmt-while-for-fn-thm
             names-to-avoid)
         (atc-gen-exec-stmt-while-for-loop
              fn loop.stmt
              prog-const names-to-avoid wrld))
        ((mv natp-of-measure-of-fn-thm-event
             natp-of-measure-of-fn-thm
             names-to-avoid)
         (atc-gen-loop-measure-thm
              fn
              fn-appconds appcond-thms measure-of-fn
              measure-formals names-to-avoid wrld))
        ((erp termination-of-fn-thm-event
              termination-of-fn-thm names-to-avoid)
         (atc-gen-loop-termination-thm
              fn measure-of-fn measure-formals
              natp-of-measure-of-fn-thm
              names-to-avoid state))
        ((mv test-local-events
             correct-test-thm names-to-avoid)
         (atc-gen-loop-test-correct-thm
              fn typed-formals loop-test
              loop.test-term fn-thms prec-tags
              prec-objs names-to-avoid state))
        ((mv body-local-events
             correct-body-thm names-to-avoid)
         (atc-gen-loop-body-correct-thm
              fn typed-formals loop.affect loop-body
              loop.test-term loop.body-term prec-fns
              prec-tags prec-objs prog-const fn-thms
              loop.limit-body names-to-avoid state))
        ((mv correct-events print-event
             fn-correct-thm names-to-avoid)
         (atc-gen-loop-correct-thm
              fn typed-formals
              loop.affect loop-test loop-body prec-fns
              prec-tags prec-objs prog-const fn-thms
              fn-result-thm exec-stmt-while-for-fn
              exec-stmt-while-for-fn-thm
              termination-of-fn-thm
              natp-of-measure-of-fn-thm
              correct-test-thm correct-body-thm
              loop.limit-all names-to-avoid state))
        (progress-start?
         (and
             (evmac-input-print->= print :info)
             (cons (cons 'cw-event
                         (cons '"~%Generating the proofs for ~x0..."
                               (cons (cons 'quote (cons fn 'nil))
                                     'nil)))
                   'nil)))
        (progress-end? (and (evmac-input-print->= print :info)
                            '((cw-event " done.~%"))))
        (print-result? (and (evmac-input-print->= print :result)
                            (list print-event)))
        (events (append progress-start? (list fn-guard-event)
                        formals-events loop.events
                        (and measure-of-fn
                             (list measure-of-fn-event))
                        fn-result-events exec-stmt-while-events
                        (list natp-of-measure-of-fn-thm-event)
                        (list termination-of-fn-thm-event)
                        test-local-events
                        body-local-events correct-events
                        progress-end? print-result?)))
       (retok events
              natp-of-measure-of-fn-thm fn-result-thm
              fn-correct-thm names-to-avoid))
      (retok nil nil nil nil names-to-avoid)))
    (info
      (make-atc-fn-info
           :out-type nil
           :in-types
           (atc-var-info-list->type-list (strip-cdrs typed-formals))
           :loop? loop.stmt
           :affect loop.affect
           :extobjs nil
           :result-thm fn-result-thm
           :correct-thm fn-correct-thm
           :correct-mod-thm nil
           :measure-nat-thm natp-of-measure-of-fn-thm
           :fun-env-thm nil
           :limit loop.limit-all
           :guard nil)))
   (retok events (acons fn info prec-fns)
          names-to-avoid))))

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

(defthm pseudo-event-form-listp-of-atc-gen-loop.events
  (b* (((mv acl2::?erp ?events ?updated-prec-fns
            ?updated-names-to-avoid)
        (atc-gen-loop fn prec-fns
                      prec-tags prec-objs proofs prog-const
                      fn-thms fn-appconds appcond-thms
                      print names-to-avoid state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: atc-symbol-fninfo-alistp-of-atc-gen-loop.updated-prec-fns

(defthm atc-symbol-fninfo-alistp-of-atc-gen-loop.updated-prec-fns
  (implies (and (symbolp fn)
                (atc-symbol-fninfo-alistp prec-fns))
           (b* (((mv acl2::?erp ?events ?updated-prec-fns
                     ?updated-names-to-avoid)
                 (atc-gen-loop fn prec-fns
                               prec-tags prec-objs proofs prog-const
                               fn-thms fn-appconds appcond-thms
                               print names-to-avoid state)))
             (atc-symbol-fninfo-alistp updated-prec-fns)))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-loop.updated-names-to-avoid

(defthm symbol-listp-of-atc-gen-loop.updated-names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv acl2::?erp ?events ?updated-prec-fns
                     ?updated-names-to-avoid)
                 (atc-gen-loop fn prec-fns
                               prec-tags prec-objs proofs prog-const
                               fn-thms fn-appconds appcond-thms
                               print names-to-avoid state)))
             (symbol-listp updated-names-to-avoid)))
  :rule-classes :rewrite)