		Search-engine friendly clone of the ACL2 documentation.

4v-sexpr-to-faig

4v-sexpr-to-faig-list

Convert a sexpr list into a faig list.

Definitions and Theorems

Function: 4v-sexpr-to-faig-list-fn1

(defun 4v-sexpr-to-faig-list-fn1 (x onoff optimizep)
  "Assumes ONOFF is fast."
  (declare (xargs :guard t))
  (if optimizep (4v-sexpr-to-faig-opt-list x onoff)
    (4v-sexpr-to-faig-plain-list x onoff)))

Function: 4v-sexpr-to-faig-list-fn

(defun 4v-sexpr-to-faig-list-fn (x onoff optimizep)
 "Assumes ONOFF is fast."
 (declare (xargs :guard t))
 (mbe
   :logic
   (if (atom x)
       nil
     (cons (4v-sexpr-to-faig-fn (car x)
                                onoff optimizep)
           (4v-sexpr-to-faig-list-fn (cdr x)
                                     onoff optimizep)))
   :exec
   (with-fast-alist onoff
                    (4v-sexpr-to-faig-list-fn1 x onoff optimizep))))

Theorem: 4v-sexpr-to-faig-list-fn1-removal

(defthm 4v-sexpr-to-faig-list-fn1-removal
  (equal (4v-sexpr-to-faig-list-fn1 x onoff optimizep)
         (4v-sexpr-to-faig-list-fn x onoff optimizep)))

Theorem: alistp-of-4v-sexpr-to-faig-list-fn

(defthm alistp-of-4v-sexpr-to-faig-list-fn
  (alistp (4v-sexpr-to-faig-list-fn x onoff optimize))
  :rule-classes :type-prescription)

Theorem: len-of-4v-sexpr-to-faig-list-fn

(defthm len-of-4v-sexpr-to-faig-list-fn
  (equal (len (4v-sexpr-to-faig-list-fn x onoff optimize))
         (len x)))

Theorem: faig-eval-list-of-4v-sexpr-to-faig

(defthm faig-eval-list-of-4v-sexpr-to-faig
  (equal (faig-eval-list (4v-sexpr-to-faig-list-fn x onoff optimize)
                         env)
         (faig-eval-list (4v-sexpr-to-faig-plain-list x onoff)
                         env)))

Subtopics

Sfaiglist: A simplified version of 4v-sexpr-to-faig-list that constructs its own onoff list out of the variables of the sexprs.