		Search-engine friendly clone of the ACL2 documentation.

Split-fn-when-implementation

Fundef-try-split-fn-when

Signature
(fundef-try-split-fn-when fundef triggers transunits) → (mv er? fundef1 fundef2)
Arguments: fundef — Guard (fundefp fundef).; triggers — Guard (ident-setp triggers).; transunits — Guard (transunit-ensemblep transunits).
Returns: er? — Type (maybe-msgp er?).; fundef1 — Type (fundefp fundef1).; fundef2 — Type (fundef-optionp fundef2).

Definitions and Theorems

Function: fundef-try-split-fn-when

(defun fundef-try-split-fn-when (fundef triggers transunits)
 (declare (xargs :guard (and (fundefp fundef)
                             (ident-setp triggers)
                             (transunit-ensemblep transunits))))
 (b*
  (((reterr) (irr-fundef) nil)
   (fundef (fundef-fix fundef))
   ((fundef fundef) fundef)
   ((declor fundef.declor) fundef.declor)
   (position? (block-item-list-try-split-fn-when
                   (comp-stmt->items fundef.body)
                   triggers))
   ((unless position?) (retok fundef nil))
   ((erp fun-name)
    (b* (((reterr) nil))
     (dirdeclor-case
          fundef.declor.direct
          :function-params
          (retok (c$::dirdeclor->ident fundef.declor.direct.declor))
          :function-names
          (retok (c$::dirdeclor->ident fundef.declor.direct.declor))
          :otherwise (retmsg$ "Malformed syntax.")))))
  (split-fn-fundef
       fun-name
       (transunit-ensemble-fresh-ident fun-name transunits)
       fundef position?)))

Theorem: maybe-msgp-of-fundef-try-split-fn-when.er?

(defthm maybe-msgp-of-fundef-try-split-fn-when.er?
  (b* (((mv ?er? ?fundef1 ?fundef2)
        (fundef-try-split-fn-when fundef triggers transunits)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: fundefp-of-fundef-try-split-fn-when.fundef1

(defthm fundefp-of-fundef-try-split-fn-when.fundef1
  (b* (((mv ?er? ?fundef1 ?fundef2)
        (fundef-try-split-fn-when fundef triggers transunits)))
    (fundefp fundef1))
  :rule-classes :rewrite)

Theorem: fundef-optionp-of-fundef-try-split-fn-when.fundef2

(defthm fundef-optionp-of-fundef-try-split-fn-when.fundef2
  (b* (((mv ?er? ?fundef1 ?fundef2)
        (fundef-try-split-fn-when fundef triggers transunits)))
    (fundef-optionp fundef2))
  :rule-classes :rewrite)