• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Transformation-tools
          • Simpadd0
            • Simpadd0-implementation
              • Simpadd0-event-generation
                • Simpadd0-exprs/decls/stmts
                • Simpadd0-fundef
                • Simpadd0-expr-cond
                • Simpadd0-expr-binary
                • Simpadd0-block-item-list-cons
                • Simpadd0-block-item-list-one
                • Simpadd0-block-item-stmt
                • Simpadd0-gen-expr-pure-thm
                • Simpadd0-expr-cast
                • Simpadd0-stmt-return
                • Simpadd0-gen-expr-asg-thm
                • Simpadd0-gen-stmt-thm
                • Simpadd0-gen-from-params
                • Simpadd0-gen-block-item-list-thm
                • Simpadd0-expr-unary
                • Simpadd0-gen-param-thms
                • Simpadd0-gen-block-item-thm
                • Simpadd0-expr-const
                • Simpadd0-stmt-expr
                • Simpadd0-gout
                • Simpadd0-expr-ident
                • Simpadd0-gen-init-scope-thm
                • Simpadd0-gin
                • Simpadd0-expr-paren
                • Simpadd0-vartys-from-valid-table
                • Simpadd0-extdecl-list
                • Simpadd0-transunit-ensemble
                • Simpadd0-filepath-transunit-map
                • Simpadd0-extdecl
                • Simpadd0-gen-var-assertions
                • Simpadd0-transunit
                • Simpadd0-code-ensemble
                • Simpadd0-join-vartys
                • C::compustate-has-var-with-type-p
                • Simpadd0-block-item-list-empty
                • Simpadd0-tyspecseq-to-type
                • Simpadd0-gin-update
                • Simpadd0-gen-everything
                • Irr-simpadd0-gout
              • Simpadd0-process-inputs-and-gen-everything
              • Simpadd0-fn
              • Simpadd0-input-processing
              • Simpadd0-macro-definition
            • Simpadd0-expr-option
            • Simpadd0-structdeclor-list
            • Simpadd0-structdecl-list
            • Simpadd0-spec/qual-list
            • Simpadd0-param-declon-list
            • Simpadd0-initdeclor-list
            • Simpadd0-dirabsdeclor-option
            • Simpadd0-dirabsdeclor
            • Simpadd0-desiniter-list
            • Simpadd0-absdeclor-option
            • Simpadd0-struni-spec
            • Simpadd0-structdeclor
            • Simpadd0-structdecl
            • Simpadd0-statassert
            • Simpadd0-spec/qual
            • Simpadd0-param-declor
            • Simpadd0-param-declon
            • Simpadd0-member-designor
            • Simpadd0-initer-option
            • Simpadd0-initdeclor
            • Simpadd0-genassoc-list
            • Simpadd0-genassoc
            • Simpadd0-expr
            • Simpadd0-enumspec
            • Simpadd0-enumer-list
            • Simpadd0-dirdeclor
            • Simpadd0-desiniter
            • Simpadd0-designor-list
            • Simpadd0-designor
            • Simpadd0-declor-option
            • Simpadd0-decl-spec-list
            • Simpadd0-decl-spec
            • Simpadd0-decl-list
            • Simpadd0-const-expr-option
            • Simpadd0-const-expr
            • Simpadd0-block-item-list
            • Simpadd0-align-spec
            • Simpadd0-absdeclor
            • Simpadd0-type-spec
            • Simpadd0-tyname
            • Simpadd0-stmt
            • Simpadd0-label
            • Simpadd0-initer
            • Simpadd0-expr-list
            • Simpadd0-enumer
            • Simpadd0-declor
            • Simpadd0-decl
            • Simpadd0-block-item
          • Splitgso
          • Constant-propagation
          • Specialize
          • Split-fn
          • Split-fn-when
          • Copy-fn
          • Split-all-gso
          • Rename
          • Utilities
        • Representation
        • Insertion-sort
        • Pack
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Riscv
      • Ethereum
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Simpadd0-event-generation

Simpadd0-join-vartys

Join two maps from identifiers to types.

Signature

(simpadd0-join-vartys vartys1 vartys2) → vartys

Arguments

vartys1 — Guard (ident-type-mapp vartys1).

vartys2 — Guard (ident-type-mapp vartys2).

Returns

vartys — Type (ident-type-mapp vartys).

This is used on maps that must be compatible, so we throw a hard error if that is not the case.

Definitions and Theorems

Function: simpadd0-join-vartys

(defun simpadd0-join-vartys (vartys1 vartys2)
 (declare (xargs :guard (and (ident-type-mapp vartys1)
                             (ident-type-mapp vartys2))))
 (let ((__function__ 'simpadd0-join-vartys))
  (declare (ignorable __function__))
  (b* ((vartys1 (ident-type-map-fix vartys1))
       (vartys2 (ident-type-map-fix vartys2)))
   (if (omap::compatiblep vartys1 vartys2)
       (omap::update* vartys1 vartys2)
    (raise
     "Internal error: ~
              incompatible variable-type maps ~x0 and ~x1"
     vartys1 vartys2)))))

Theorem: ident-type-mapp-of-simpadd0-join-vartys

(defthm ident-type-mapp-of-simpadd0-join-vartys
  (b* ((vartys (simpadd0-join-vartys vartys1 vartys2)))
    (ident-type-mapp vartys))
  :rule-classes :rewrite)

Theorem: simpadd0-join-vartys-of-ident-type-map-fix-vartys1

(defthm simpadd0-join-vartys-of-ident-type-map-fix-vartys1
  (equal (simpadd0-join-vartys (ident-type-map-fix vartys1)
                               vartys2)
         (simpadd0-join-vartys vartys1 vartys2)))

Theorem: simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys1

(defthm
    simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys1
  (implies (c$::ident-type-map-equiv vartys1 vartys1-equiv)
           (equal (simpadd0-join-vartys vartys1 vartys2)
                  (simpadd0-join-vartys vartys1-equiv vartys2)))
  :rule-classes :congruence)

Theorem: simpadd0-join-vartys-of-ident-type-map-fix-vartys2

(defthm simpadd0-join-vartys-of-ident-type-map-fix-vartys2
  (equal (simpadd0-join-vartys vartys1 (ident-type-map-fix vartys2))
         (simpadd0-join-vartys vartys1 vartys2)))

Theorem: simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys2

(defthm
    simpadd0-join-vartys-ident-type-map-equiv-congruence-on-vartys2
  (implies (c$::ident-type-map-equiv vartys2 vartys2-equiv)
           (equal (simpadd0-join-vartys vartys1 vartys2)
                  (simpadd0-join-vartys vartys1 vartys2-equiv)))
  :rule-classes :congruence)