		Search-engine friendly clone of the ACL2 documentation.

Split-fn-input-processing

Split-fn-process-inputs

Process the inputs.

Signature
(split-fn-process-inputs const-old const-new target new-fn split-point wrld) → (mv er? code const-new$ target$ new-fn$ split-point)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: er? — Type (maybe-msgp er?).; code — Type (code-ensemblep code).; const-new$ — Type (symbolp const-new$).; target$ — Type (identp target$).; new-fn$ — Type (identp new-fn$).; split-point — Type (natp split-point).

Definitions and Theorems

Function: split-fn-process-inputs

(defun split-fn-process-inputs
       (const-old const-new
                  target new-fn split-point wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (b* (((reterr)
        (irr-code-ensemble)
        nil (c$::irr-ident)
        (c$::irr-ident)
        0)
       ((unless (symbolp const-old))
        (retmsg$ "~x0 must be a symbol." const-old))
       (code (constant-value const-old wrld))
       ((unless (code-ensemblep code))
        (retmsg$ "~x0 must be a code ensemble."
                 const-old))
       ((unless (symbolp const-new))
        (retmsg$ "~x0 must be a symbol." const-new))
       ((unless (stringp target))
        (retmsg$ "~x0 must be a string." target))
       (target (ident target))
       ((unless (stringp new-fn))
        (retmsg$ "~x0 must be a string." new-fn))
       (new-fn (ident new-fn))
       ((unless (natp split-point))
        (retmsg$ "~x0 must be a natural number."
                 split-point)))
    (retok code
           const-new target new-fn split-point)))

Theorem: maybe-msgp-of-split-fn-process-inputs.er?

(defthm maybe-msgp-of-split-fn-process-inputs.er?
  (b* (((mv ?er? ?code ?const-new$
            ?target$ ?new-fn$ ?split-point)
        (split-fn-process-inputs const-old const-new
                                 target new-fn split-point wrld)))
    (maybe-msgp er?))
  :rule-classes :rewrite)

Theorem: code-ensemblep-of-split-fn-process-inputs.code

(defthm code-ensemblep-of-split-fn-process-inputs.code
  (b* (((mv ?er? ?code ?const-new$
            ?target$ ?new-fn$ ?split-point)
        (split-fn-process-inputs const-old const-new
                                 target new-fn split-point wrld)))
    (code-ensemblep code))
  :rule-classes :rewrite)

Theorem: symbolp-of-split-fn-process-inputs.const-new$

(defthm symbolp-of-split-fn-process-inputs.const-new$
  (b* (((mv ?er? ?code ?const-new$
            ?target$ ?new-fn$ ?split-point)
        (split-fn-process-inputs const-old const-new
                                 target new-fn split-point wrld)))
    (symbolp const-new$))
  :rule-classes :rewrite)

Theorem: identp-of-split-fn-process-inputs.target$

(defthm identp-of-split-fn-process-inputs.target$
  (b* (((mv ?er? ?code ?const-new$
            ?target$ ?new-fn$ ?split-point)
        (split-fn-process-inputs const-old const-new
                                 target new-fn split-point wrld)))
    (identp target$))
  :rule-classes :rewrite)

Theorem: identp-of-split-fn-process-inputs.new-fn$

(defthm identp-of-split-fn-process-inputs.new-fn$
  (b* (((mv ?er? ?code ?const-new$
            ?target$ ?new-fn$ ?split-point)
        (split-fn-process-inputs const-old const-new
                                 target new-fn split-point wrld)))
    (identp new-fn$))
  :rule-classes :rewrite)

Theorem: natp-of-split-fn-process-inputs.split-point

(defthm natp-of-split-fn-process-inputs.split-point
  (b* (((mv ?er? ?code ?const-new$
            ?target$ ?new-fn$ ?split-point)
        (split-fn-process-inputs const-old const-new
                                 target new-fn split-point wrld)))
    (natp split-point))
  :rule-classes :rewrite)