		Search-engine friendly clone of the ACL2 documentation.

Wrap-fn-implementation

Code-ensemble-wrap-fn-multiple

Transform a code ensemble.

Signature
(code-ensemble-wrap-fn-multiple code targets) → (mv er? code$)
Arguments: code — Guard (code-ensemblep code).; targets — Guard (ident-ident-option-mapp targets).
Returns: er? — Type (maybe-msgp er?).; code$ — Type (code-ensemblep code$).

The target-name is the function to be wrapped. wrapper-name?, if it is non-nil, is the suggested name of the wrapper function. If no suggestion is provided, a name will be generated.

Definitions and Theorems

Function: code-ensemble-wrap-fn-multiple

(defun code-ensemble-wrap-fn-multiple (code targets)
  (declare (xargs :guard (and (code-ensemblep code)
                              (ident-ident-option-mapp targets))))
  (declare (xargs :guard (and (code-ensemble-annop code))))
  (b*
    (((reterr) (c$::code-ensemble-fix code))
     (targets (ident-ident-option-map-fix targets))
     ((when (omap::emptyp targets))
      (retok (c$::code-ensemble-fix code)))
     ((erp code)
      (code-ensemble-wrap-fn code (omap::head-key targets)
                             (omap::head-val targets)))
     ((unless (code-ensemble-unambp code))
      (retmsg$ "Internal error: code has not been disambiguated."))
     ((erp valid-transunits)
      (c$::valid-transunit-ensemble (code-ensemble->transunits code)
                                    (code-ensemble->ienv code)
                                    nil))
     ((unless (transunit-ensemble-annop valid-transunits))
      (retmsg$ "Internal error: code is invalid."))
     (code (change-code-ensemble code
                                 :transunits valid-transunits)))
    (code-ensemble-wrap-fn-multiple code (omap::tail targets))))

Theorem: maybe-msgp-of-code-ensemble-wrap-fn-multiple.er?

(defthm maybe-msgp-of-code-ensemble-wrap-fn-multiple.er?
  (b* (((mv ?er? ?code$)
        (code-ensemble-wrap-fn-multiple code targets)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: code-ensemblep-of-code-ensemble-wrap-fn-multiple.code$

(defthm code-ensemblep-of-code-ensemble-wrap-fn-multiple.code$
  (b* (((mv ?er? ?code$)
        (code-ensemble-wrap-fn-multiple code targets)))
    (code-ensemblep code$))
  :rule-classes :rewrite)

Theorem: code-ensemble-wrap-fn-multiple-of-code-ensemble-fix-code

(defthm code-ensemble-wrap-fn-multiple-of-code-ensemble-fix-code
 (equal (code-ensemble-wrap-fn-multiple (c$::code-ensemble-fix code)
                                        targets)
        (code-ensemble-wrap-fn-multiple code targets)))

Theorem: code-ensemble-wrap-fn-multiple-code-ensemble-equiv-congruence-on-code

(defthm
 code-ensemble-wrap-fn-multiple-code-ensemble-equiv-congruence-on-code
 (implies
      (c$::code-ensemble-equiv code code-equiv)
      (equal (code-ensemble-wrap-fn-multiple code targets)
             (code-ensemble-wrap-fn-multiple code-equiv targets)))
 :rule-classes :congruence)

Theorem: code-ensemble-wrap-fn-multiple-of-ident-ident-option-map-fix-targets

(defthm
 code-ensemble-wrap-fn-multiple-of-ident-ident-option-map-fix-targets
 (equal (code-ensemble-wrap-fn-multiple
             code
             (ident-ident-option-map-fix targets))
        (code-ensemble-wrap-fn-multiple code targets)))

Theorem: code-ensemble-wrap-fn-multiple-ident-ident-option-map-equiv-congruence-on-targets

(defthm
 code-ensemble-wrap-fn-multiple-ident-ident-option-map-equiv-congruence-on-targets
 (implies
      (ident-ident-option-map-equiv targets targets-equiv)
      (equal (code-ensemble-wrap-fn-multiple code targets)
             (code-ensemble-wrap-fn-multiple code targets-equiv)))
 :rule-classes :congruence)