		Search-engine friendly clone of the ACL2 documentation.

Wrap-fn-implementation

Code-ensemble-wrap-fn

Transform a code ensemble.

Signature
(code-ensemble-wrap-fn code target-name wrapper-name?) → (mv er? code$)
Arguments: code — Guard (code-ensemblep code).; target-name — Guard (identp target-name).; wrapper-name? — Guard (ident-optionp wrapper-name?).
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

(defun code-ensemble-wrap-fn (code target-name wrapper-name?)
  (declare (xargs :guard (and (code-ensemblep code)
                              (identp target-name)
                              (ident-optionp wrapper-name?))))
  (declare (xargs :guard (code-ensemble-annop code)))
  (b* (((reterr) (c$::code-ensemble-fix code))
       ((code-ensemble code) code)
       ((erp transunits)
        (transunit-ensemble-wrap-fn code.transunits
                                    target-name wrapper-name?)))
    (retok (change-code-ensemble code
                                 :transunits transunits))))

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

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

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

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

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

(defthm code-ensemble-wrap-fn-of-code-ensemble-fix-code
  (equal (code-ensemble-wrap-fn (c$::code-ensemble-fix code)
                                target-name wrapper-name?)
         (code-ensemble-wrap-fn code target-name wrapper-name?)))

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

(defthm code-ensemble-wrap-fn-code-ensemble-equiv-congruence-on-code
 (implies
  (c$::code-ensemble-equiv code code-equiv)
  (equal
      (code-ensemble-wrap-fn code target-name wrapper-name?)
      (code-ensemble-wrap-fn code-equiv target-name wrapper-name?)))
 :rule-classes :congruence)

Theorem: code-ensemble-wrap-fn-of-ident-fix-target-name

(defthm code-ensemble-wrap-fn-of-ident-fix-target-name
  (equal (code-ensemble-wrap-fn code (ident-fix target-name)
                                wrapper-name?)
         (code-ensemble-wrap-fn code target-name wrapper-name?)))

Theorem: code-ensemble-wrap-fn-ident-equiv-congruence-on-target-name

(defthm code-ensemble-wrap-fn-ident-equiv-congruence-on-target-name
 (implies
  (c$::ident-equiv target-name target-name-equiv)
  (equal
      (code-ensemble-wrap-fn code target-name wrapper-name?)
      (code-ensemble-wrap-fn code target-name-equiv wrapper-name?)))
 :rule-classes :congruence)

Theorem: code-ensemble-wrap-fn-of-ident-option-fix-wrapper-name?

(defthm code-ensemble-wrap-fn-of-ident-option-fix-wrapper-name?
  (equal (code-ensemble-wrap-fn code target-name
                                (ident-option-fix wrapper-name?))
         (code-ensemble-wrap-fn code target-name wrapper-name?)))

Theorem: code-ensemble-wrap-fn-ident-option-equiv-congruence-on-wrapper-name?

(defthm
 code-ensemble-wrap-fn-ident-option-equiv-congruence-on-wrapper-name?
 (implies
  (c$::ident-option-equiv wrapper-name? wrapper-name?-equiv)
  (equal
      (code-ensemble-wrap-fn code target-name wrapper-name?)
      (code-ensemble-wrap-fn code target-name wrapper-name?-equiv)))
 :rule-classes :congruence)