• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Soft
        • Bv
        • Imp-language
        • C
          • Syntax-for-tools
          • Atc
          • Language
          • Representation
          • Transformation-tools
            • Deftrans
            • Simpadd0
            • Constant-propagation
            • Split-fn
            • Copy-fn
            • Specialize
            • Splitgso
              • Splitgso-implementation
                • Replace-field-access-filepath-transunit-map
                • Replace-field-access-transunit-ensemble
                • Replace-field-access-fundef
                • Replace-field-access-extdecl-list
                • Replace-field-access-ident-list
                • Replace-field-access-extdecl
                • Replace-field-access-transunit
                • Splitgso-process-inputs-and-gen-everything
                • Replace-field-access-ident
                • Replace-field-access-const
                • Splitgso-fn
                • Match-simple-declor-ident
                • Splitgso-input-processing
                  • Splitgso-process-inputs
                    • Ident-map
                  • Splitgso-event-generation
                  • Splitgso-macro-definition
              • Rename
              • Utilities
            • Pack
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Number-theory
          • Cryptography
          • Lists-light
          • Builtins
          • Axe
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • 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) (c$::transunit-ensemble-annop tunits)) .
    object-ident — Type (identp object-ident).
    filepath? — Type (c$::filepath-optionp filepath?).
    new-object1 — Type (identp new-object1).
    new-object2 — Type (identp new-object2).
    new-type1 — Type (identp new-type1).
    new-type2 — Type (identp 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)
     (c$::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 (acl2::constant-value const-old wrld))
    ((unless (transunit-ensemblep tunits))
     (reterr (msg "~x0 must be a translation unit ensemble."
                  const-old)))
    ((unless (c$::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 (stringp new-object1))
     (reterr (msg "~x0 must be a string" new-object1)))
    (new-object1 (ident new-object1))
    ((unless (stringp new-object2))
     (reterr (msg "~x0 must be a string" new-object2)))
    (new-object2 (ident new-object2))
    ((unless (stringp new-type1))
     (reterr (msg "~x0 must be a string" new-type1)))
    (new-type1 (ident new-type1))
    ((unless (stringp new-type2))
     (reterr (msg "~x0 must be a string" new-type2)))
    (new-type2 (ident new-type2))
    ((unless (string-listp split-members))
     (reterr (msg "~x0 must be a string" 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)
         (c$::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: identp-of-splitgso-process-inputs.new-object1

    (defthm identp-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)))
    (identp new-object1))
  :rule-classes :rewrite)

    Theorem: identp-of-splitgso-process-inputs.new-object2

    (defthm identp-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)))
    (identp new-object2))
  :rule-classes :rewrite)

    Theorem: identp-of-splitgso-process-inputs.new-type1

    (defthm identp-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)))
    (identp new-type1))
  :rule-classes :rewrite)

    Theorem: identp-of-splitgso-process-inputs.new-type2

    (defthm identp-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)))
    (identp 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)