• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-fixpoint-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Moddb
      • Svex-compilation
      • Svmods
        • Address
        • Wire
        • Module
        • Lhs
        • Svar-add-namespace
        • Path
        • Design
        • Modinst
        • Lhs-add-namespace
        • Modalist
        • Path-add-namespace
        • Modname->submodnames
        • Name
        • Svex-alist-addr-p
        • Constraintlist-addr-p
        • Svar-map-addr-p
        • Lhspairs-addr-p
        • Assigns-addr-p
        • Modname
        • Lhs-addr-p
        • Lhatom-addr-p
        • Modhier-measure
        • Modhier-list-measure
        • Attributes
        • Modhier-list-measure-aux
        • Modhier-loopfreelist-p
        • Modhier-loopfree-p
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svmods

Lhs-add-namespace

Signature

(lhs-add-namespace namespace x) → xx

Arguments

namespace — Guard (name-p namespace).

x — Guard (lhs-p x).

Returns

xx — Type (and (lhs-p xx) (svarlist-addr-p (lhs-vars xx))).

Definitions and Theorems

Function: lhs-add-namespace

(defun
 lhs-add-namespace (namespace x)
 (declare (xargs :guard (and (name-p namespace) (lhs-p x))))
 (declare (xargs :guard (svarlist-addr-p (lhs-vars x))))
 (let
  ((__function__ 'lhs-add-namespace))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) nil)
    ((lhrange first) (lhrange-fix (car x))))
   (cons
    (lhatom-case
     first.atom
     :z first
     :var
     (change-lhrange
        first
        :atom
        (change-lhatom-var
             first.atom
             :name (svar-add-namespace namespace first.atom.name))))
    (lhs-add-namespace namespace (cdr x))))))

Theorem: return-type-of-lhs-add-namespace

(defthm return-type-of-lhs-add-namespace
        (b* ((xx (lhs-add-namespace namespace x)))
            (and (lhs-p xx)
                 (svarlist-addr-p (lhs-vars xx))))
        :rule-classes :rewrite)

Theorem: lhs-add-namespace-of-name-fix-namespace

(defthm lhs-add-namespace-of-name-fix-namespace
        (equal (lhs-add-namespace (name-fix namespace)
                                  x)
               (lhs-add-namespace namespace x)))

Theorem: lhs-add-namespace-name-equiv-congruence-on-namespace

(defthm lhs-add-namespace-name-equiv-congruence-on-namespace
        (implies (name-equiv namespace namespace-equiv)
                 (equal (lhs-add-namespace namespace x)
                        (lhs-add-namespace namespace-equiv x)))
        :rule-classes :congruence)

Theorem: lhs-add-namespace-of-lhs-fix-x

(defthm lhs-add-namespace-of-lhs-fix-x
        (equal (lhs-add-namespace namespace (lhs-fix x))
               (lhs-add-namespace namespace x)))

Theorem: lhs-add-namespace-lhs-equiv-congruence-on-x

(defthm lhs-add-namespace-lhs-equiv-congruence-on-x
        (implies (lhs-equiv x x-equiv)
                 (equal (lhs-add-namespace namespace x)
                        (lhs-add-namespace namespace x-equiv)))
        :rule-classes :congruence)