• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
          • 4v-sexpr-compose-alist
          • 4v-nsexpr-p-4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 4v-sexprs

4v-sexpr-compose

Alternate substitution operation for 4v-sexprs.

(4v-sexpr-compose x al) is takes a sexpr, x, and a fast alist al that binds variables to sexprs.

We construct a new sexpr by copying x, except that we unconditionally replace every variable in x with its binding in al, regardless of whether such a binding actually exists. Any unbound variables are just replaced by NIL, which in our semantics always evaluates to X.

We memoize this function, but this only helps when you are composing with the same alist. We don't use :forget t because you frequently want to compose several related expressions under the same alist, as in 4v-sexpr-restrict-alist. So, you'll generally need to manage clearing the memoization table yourself.

Definitions and Theorems

Function: 4v-sexpr-compose

(defun 4v-sexpr-compose (x al)
  (declare (xargs :guard t))
  (if (atom x)
      (and x
           (let ((look (hons-get x al)))
             (and look (cdr look))))
    (hons (car x)
          (4v-sexpr-compose-list (cdr x) al))))

Function: 4v-sexpr-compose-list

(defun 4v-sexpr-compose-list (x al)
  (declare (xargs :guard t))
  (if (atom x)
      x
    (hons (4v-sexpr-compose (car x) al)
          (4v-sexpr-compose-list (cdr x) al))))

Function: 4v-sexpr-compose-memoize-condition

(defun 4v-sexpr-compose-memoize-condition (x al)
  (declare (ignorable x al)
           (xargs :guard 't))
  (and (consp x) (consp (cdr x))))

Theorem: 4v-sexpr-eval-4v-sexpr-compose

(defthm 4v-sexpr-eval-4v-sexpr-compose
  (equal (4v-sexpr-eval (4v-sexpr-compose x al)
                        env)
         (4v-sexpr-eval x (4v-sexpr-eval-alist al env))))

Theorem: 4v-sexpr-eval-list-4v-sexpr-compose-list

(defthm 4v-sexpr-eval-list-4v-sexpr-compose-list
  (equal (4v-sexpr-eval-list (4v-sexpr-compose-list x al)
                             env)
         (4v-sexpr-eval-list x (4v-sexpr-eval-alist al env))))

Subtopics

4v-sexpr-compose-alist

Extension of 4v-sexpr-compose to alists.

4v-nsexpr-p-4v-sexpr-compose