Lift a program from the current ACL2 environment to the meta level.
We lift all the known packages, along with the functions specified by symbol. In general there are too many functions in the ACL2 environment, so we only lift the specified functions. Care must be exercised so that the list of functions is closed with respect to calls.
(defun lift-program (fns state) (declare (xargs :stobjs (state))) (declare (xargs :guard (symbol-listp fns))) (let ((__function__ 'lift-program)) (declare (ignorable __function__)) (b* ((packages (lift-package-list (known-packages+ state))) (functions (lift-function-list fns (w state)))) (make-program :packages packages :functions functions))))
(defthm programp-of-lift-program (b* ((program (lift-program fns state))) (programp program)) :rule-classes :rewrite)