		Search-engine friendly clone of the ACL2 documentation.

Defstv

Defstv-main

Main error checking and processing of an STV.

Signature
(defstv-main &key mod name inputs outputs internals overrides) → pstv
Arguments: mod — Guard (good-esim-modulep mod).; name — Guard (symbolp name).
Returns: pstv — Type (equal (processed-stv-p pstv) (if pstv t nil)), given (force (symbolp name)).

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.

Definitions and Theorems

Function: defstv-main-fn

(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)))

Theorem: return-type-of-defstv-main

(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)