		Search-engine friendly clone of the ACL2 documentation.

Svtv-chase

Svtv-chase-repl1

Re-enter the svtv-chase read-eval-print loop, with no change to the environment or SVTV.

Signature
(svtv-chase-repl1 &key (moddb 'moddb) (aliases 'aliases) (svtv-chase-data 'svtv-chase-data) (state 'state)) → (mv new-svtv-chase-data new-state)
Arguments: moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: svtv-chase-repl1-fn

(defun svtv-chase-repl1-fn (moddb aliases svtv-chase-data state)
 (declare (xargs :stobjs (moddb aliases svtv-chase-data state)))
 (declare (xargs :guard (moddb-ok moddb)))
 (declare
  (xargs
   :guard
   (and
    (open-input-channel-p *standard-oi*
                          :object state)
    (< (svtv-chase-data->modidx svtv-chase-data)
       (moddb->nmods moddb))
    (<=
     (moddb-mod-totalwires (svtv-chase-data->modidx svtv-chase-data)
                           moddb)
     (aliass-length aliases)))))
 (let ((__function__ 'svtv-chase-repl1))
  (declare (ignorable __function__))
  (b*
   (((mv exitp svtv-chase-data state)
     (svtv-chase-rep))
    ((when exitp)
     (cw!
      "~%Exiting SVTV-CHASE.  You may execute ~x0 to re-enter or ~x1 ~
              to change the simulation inputs.~%"
      '(svtv-chase-repl)
      '(svtv-chase-update env))
     (mv svtv-chase-data state)))
   (svtv-chase-repl1))))

Theorem: nth-of-svtv-chase-repl1

(defthm nth-of-svtv-chase-repl1
 (b* (((mv ?new-svtv-chase-data ?new-state)
       (svtv-chase-repl1-fn moddb aliases svtv-chase-data state)))
  (implies
   (not
      (member-equal (nfix n)
                    (list *svtv-chase-data->smartp*
                          *svtv-chase-data->stack*
                          *svtv-chase-data->sigtype*
                          *svtv-chase-data->vars*
                          *svtv-chase-data->expr*
                          *svtv-chase-data->print-with-mask-mode*
                          *svtv-chase-data->print-overrides-mode*)))
   (equal (nth n new-svtv-chase-data)
          (nth n svtv-chase-data)))))