Main error checking and processing of an STV.
This is the main part of defstv.
We split this out into its own function for advanced users who need a non-event based way to introduce symbolic test vectors.
This does only the STV processing. We don't deal here with generating documentation, creating autohyps macros, etc.
(defun defstv-main-fn (mod name inputs outputs internals overrides) (declare (xargs :guard (and (good-esim-modulep mod) (symbolp name)))) (let ((__function__ 'defstv-main)) (declare (ignorable __function__)) (b* ((mod (or mod (raise "No :mod was specified."))) (- (or (and (gpl :n mod) (symbolp (gpl :n mod))) (raise "Alleged module doesn't have a non-nil symbol :n field? ~ Is this a proper ESIM module?"))) (inputs (if (true-list-listp inputs) inputs (raise ":inputs are not even a true-list-listp"))) (outputs (if (true-list-listp outputs) outputs (raise ":outputs are not even a true-list-listp"))) (internals (if (true-list-listp internals) internals (raise ":internals are not even a true-list-listp"))) (overrides (if (true-list-listp overrides) overrides (raise ":overrides are not even a true-list-listp"))) (stv (make-stvdata :overrides overrides :inputs inputs :outputs outputs :internals internals)) (preprocessed-stv (time$ (let* ((stv (stv-widen stv)) (stv (stv-expand stv mod))) stv) :msg "; stv preprocessing: ~st sec, ~sa bytes~%" :mintime 1/2)) (compiled-stv (time$ (stv-compile preprocessed-stv mod) :msg "; stv compilation: ~st sec, ~sa bytes~%" :mintime 1/2)) ((unless compiled-stv) (raise "stv-compile failed?")) (mod (stv-cut-module (compiled-stv->override-paths compiled-stv) mod)) (processed-stv (time$ (stv-process name stv compiled-stv mod) :msg "; stv processing: ~st sec, ~sa bytes~%" :mintime 1/2)) ((unless processed-stv) (raise "stv-process failed?"))) processed-stv)))
(defthm return-type-of-defstv-main (implies (force (symbolp name)) (b* ((pstv (defstv-main-fn mod name inputs outputs internals overrides))) (equal (processed-stv-p pstv) (if pstv t nil)))) :rule-classes :rewrite)