• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Acre
      • Milawa
      • Smtlink
      • Aleobft
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
        • Transformation-tools
          • Deftrans
          • Simpadd0
          • Split-fn
          • Copy-fn
          • Specialize
          • Rename
          • Splitgso
            • Splitgso-implementation
              • Splitgso-process-inputs-and-gen-everything
              • Splitgso-fn
              • Splitgso-input-processing
                • Splitgso-process-inputs
                  • Ident-map
                • Splitgso-event-generation
                • Splitgso-macro-definition
            • Utilities
          • Pack
        • Java
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Riscv
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Bigmems
        • Builtins
        • Axe
        • Execloader
        • Solidity
        • Leo
        • Paco
        • Concurrent-programs
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Splitgso-input-processing

    Splitgso-process-inputs

    Process the inputs.

    Signature
    (splitgso-process-inputs const-old const-new 
                         object-name new-object1 new-object2 
                         new-type1 new-type2 split-members wrld) 
 
  → 
(mv erp filepath tunit object-ident 
    new-object1 new-object2 new-type1 
    new-type2 split-members const-new$)
    Arguments
    wrld — Guard (plist-worldp wrld).
    Returns
    filepath — Type (filepathp filepath).
    tunit — Type (transunitp tunit).
    object-ident — Type (identp object-ident).
    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 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)
     (filepath :irrelevant)
     (c$::irr-transunit)
     (c$::irr-ident)
     (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-old (acl2::constant-value const-old wrld))
    ((unless (transunit-ensemblep tunits-old))
     (reterr (msg "~x0 must be a translation unit ensemble."
                  const-old)))
    (tunits-map (transunit-ensemble->unwrap tunits-old))
    ((when (or (omap::emptyp tunits-map)
               (not (omap::emptyp (omap::tail tunits-map)))))
     (reterr
      (msg
       "~x0 must be a translation unit ensemble with at exactly
                      one translation unit"
       const-old)))
    (filepath (deftrans-filepath (omap::head-key tunits-map)
                                 "SPLITGSO"))
    (tunit (omap::head-val tunits-map))
    ((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 filepath tunit object-ident
          new-object1 new-object2 new-type1
          new-type2 split-members const-new))))

    Theorem: filepathp-of-splitgso-process-inputs.filepath

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

    Theorem: transunitp-of-splitgso-process-inputs.tunit

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

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

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

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

    (defthm identp-of-splitgso-process-inputs.new-object1
  (b* (((mv acl2::?erp
            c$::?filepath ?tunit ?object-ident
            ?new-object1 ?new-object2 ?new-type1
            ?new-type2 ?split-members ?const-new$)
        (splitgso-process-inputs const-old const-new object-name
                                 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
            c$::?filepath ?tunit ?object-ident
            ?new-object1 ?new-object2 ?new-type1
            ?new-type2 ?split-members ?const-new$)
        (splitgso-process-inputs const-old const-new object-name
                                 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
            c$::?filepath ?tunit ?object-ident
            ?new-object1 ?new-object2 ?new-type1
            ?new-type2 ?split-members ?const-new$)
        (splitgso-process-inputs const-old const-new object-name
                                 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
            c$::?filepath ?tunit ?object-ident
            ?new-object1 ?new-object2 ?new-type1
            ?new-type2 ?split-members ?const-new$)
        (splitgso-process-inputs const-old const-new object-name
                                 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
            c$::?filepath ?tunit ?object-ident
            ?new-object1 ?new-object2 ?new-type1
            ?new-type2 ?split-members ?const-new$)
        (splitgso-process-inputs const-old const-new object-name
                                 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
            c$::?filepath ?tunit ?object-ident
            ?new-object1 ?new-object2 ?new-type1
            ?new-type2 ?split-members ?const-new$)
        (splitgso-process-inputs const-old const-new object-name
                                 new-object1 new-object2 new-type1
                                 new-type2 split-members wrld)))
    (symbolp const-new$))
  :rule-classes :rewrite)