		Search-engine friendly clone of the ACL2 documentation.

Splitgso-input-processing

Splitgso-process-inputs

Process the inputs.

Signature
(splitgso-process-inputs const-old const-new object-name object-filepath new-object1 new-object2 new-type1 new-type2 split-members wrld) → (mv erp tunits object-ident filepath? new-object1 new-object2 new-type1 new-type2 split-members const-new$)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: tunits — Type (and (transunit-ensemblep tunits) (transunit-ensemble-annop tunits)).; object-ident — Type (identp object-ident).; filepath? — Type (c$::filepath-optionp filepath?).; new-object1 — Type (ident-optionp new-object1).; new-object2 — Type (ident-optionp new-object2).; new-type1 — Type (ident-optionp new-type1).; new-type2 — Type (ident-optionp new-type2).; split-members — Type (ident-listp split-members).; const-new$ — Type (symbolp const-new$).

Definitions and Theorems

Function: splitgso-process-inputs

(defun splitgso-process-inputs
       (const-old const-new object-name
                  object-filepath new-object1 new-object2
                  new-type1 new-type2 split-members wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'splitgso-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (irr-transunit-ensemble)
     (c$::irr-ident)
     nil (c$::irr-ident)
     (c$::irr-ident)
     (c$::irr-ident)
     (c$::irr-ident)
     nil nil)
    ((unless (symbolp const-old))
     (reterr (msg "~x0 must be a symbol" const-old)))
    (tunits (constant-value const-old wrld))
    ((unless (transunit-ensemblep tunits))
     (reterr (msg "~x0 must be a translation unit ensemble."
                  const-old)))
    ((unless (transunit-ensemble-annop tunits))
     (reterr
        (msg "~x0 must be an annotated with validation information."
             const-old)))
    ((unless (or (not object-filepath)
                 (stringp object-filepath)))
     (reterr (msg "~x0 must be nil or a string"
                  object-filepath)))
    (object-filepath (and object-filepath
                          (filepath object-filepath)))
    ((unless (stringp object-name))
     (reterr (msg "~x0 must be a string" object-name)))
    (object-ident (ident object-name))
    ((unless (or (stringp new-object1)
                 (not new-object1)))
     (reterr (msg "~x0 must be a string or @('nil')"
                  new-object1)))
    (new-object1 (and new-object1 (ident new-object1)))
    ((unless (or (stringp new-object2)
                 (not new-object2)))
     (reterr (msg "~x0 must be a string or @('nil')"
                  new-object2)))
    (new-object2 (and new-object2 (ident new-object2)))
    ((unless (or (stringp new-type1)
                 (not new-type1)))
     (reterr (msg "~x0 must be a string or @('nil')"
                  new-type1)))
    (new-type1 (and new-type1 (ident new-type1)))
    ((unless (or (stringp new-type2)
                 (not new-type2)))
     (reterr (msg "~x0 must be a string or @('nil')"
                  new-type2)))
    (new-type2 (and new-type2 (ident new-type2)))
    ((unless (string-listp split-members))
     (reterr (msg "~x0 must be a string list"
                  split-members)))
    (split-members (ident-map split-members))
    ((unless (symbolp const-new))
     (reterr (msg "~x0 must be a symbol" const-new))))
   (retok tunits object-ident object-filepath
          new-object1 new-object2 new-type1
          new-type2 split-members const-new))))

Theorem: return-type-of-splitgso-process-inputs.tunits

(defthm return-type-of-splitgso-process-inputs.tunits
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (and (transunit-ensemblep tunits)
         (transunit-ensemble-annop tunits)))
  :rule-classes :rewrite)

Theorem: identp-of-splitgso-process-inputs.object-ident

(defthm identp-of-splitgso-process-inputs.object-ident
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (identp object-ident))
  :rule-classes :rewrite)

Theorem: filepath-optionp-of-splitgso-process-inputs.filepath?

(defthm filepath-optionp-of-splitgso-process-inputs.filepath?
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (c$::filepath-optionp filepath?))
  :rule-classes :rewrite)

Theorem: ident-optionp-of-splitgso-process-inputs.new-object1

(defthm ident-optionp-of-splitgso-process-inputs.new-object1
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (ident-optionp new-object1))
  :rule-classes :rewrite)

Theorem: ident-optionp-of-splitgso-process-inputs.new-object2

(defthm ident-optionp-of-splitgso-process-inputs.new-object2
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (ident-optionp new-object2))
  :rule-classes :rewrite)

Theorem: ident-optionp-of-splitgso-process-inputs.new-type1

(defthm ident-optionp-of-splitgso-process-inputs.new-type1
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (ident-optionp new-type1))
  :rule-classes :rewrite)

Theorem: ident-optionp-of-splitgso-process-inputs.new-type2

(defthm ident-optionp-of-splitgso-process-inputs.new-type2
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (ident-optionp new-type2))
  :rule-classes :rewrite)

Theorem: ident-listp-of-splitgso-process-inputs.split-members

(defthm ident-listp-of-splitgso-process-inputs.split-members
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (ident-listp split-members))
  :rule-classes :rewrite)

Theorem: symbolp-of-splitgso-process-inputs.const-new$

(defthm symbolp-of-splitgso-process-inputs.const-new$
  (b*
    (((mv acl2::?erp
          ?tunits ?object-ident ?filepath?
          ?new-object1 ?new-object2 ?new-type1
          ?new-type2 ?split-members ?const-new$)
      (splitgso-process-inputs const-old
                               const-new object-name object-filepath
                               new-object1 new-object2 new-type1
                               new-type2 split-members wrld)))
    (symbolp const-new$))
  :rule-classes :rewrite)