		Search-engine friendly clone of the ACL2 documentation.

Sfaig

Sfaiglist-make-faigenv

For use with sfaiglist, translates sexpr environments into equivalent faig environments.

Signature
(sfaiglist-make-faigenv sexprs env) → faig-env
Arguments: sexprs — The list of 4v-sexprs.; env — A sexpr-env to evaluate them under.
Returns: faig-env — The corresponding faig environment.

Definitions and Theorems

Function: sfaiglist-make-faigenv

(defun sfaiglist-make-faigenv (sexprs env)
  (declare (xargs :guard t))
  (let ((__function__ 'sfaiglist-make-faigenv))
    (declare (ignorable __function__))
    (b* ((vars (4v-sexpr-vars-1pass-list sexprs))
         (onoff (num-varmap vars 0))
         (env (4v-sexpr-alist-extract vars env)))
      (sig-al-to-svar-al (4v-alist->faig-const-alist env)
                         onoff))))

Theorem: faig-eval-list-of-sfaiglist-make-faigenv

(defthm faig-eval-list-of-sfaiglist-make-faigenv
 (b* ((faigs (sfaiglist sexprs))
      (faig-env (sfaiglist-make-faigenv sexprs env)))
  (equal
       (faig-eval-list faigs faig-env)
       (4v-list->faig-const-list (4v-sexpr-eval-list sexprs env)))))