Filtering...

seqw

books/misc/seqw

Included Books

seq
other
(in-package "ACL2")
include-book
(include-book "seq")
other
(defsection seqw
  :parents (seq)
  :short "An alternative implementation of the Seq language which allows for
warnings to be implicitly collected and stored in a list as your program
executes."
  :long "<p>As background see @(see seq); here we only describe the differences
between Seqw and Seq.</p>

<p>The difference is quite straightforward:</p>

<ul>

<li>Whereas a Seq program has the form @('(seq <stream> ...)'), a Seqw program
instead has one additional argument, @('(seqw <stream> <warnings> ...)'), where
@('<warnings>') is the name of a <i>warnings structure</i> (see below).</li>

<li>Whereas every Seq action returns @('(mv error val stream)'), each Seqw action
instead returns @('(mv error val stream warnings)'), where warnings is the
updated warnings structure.</li>

<li>Similarly, every Seqw program returns @('(mv error val stream warnings)')
instead of @('(mv error val stream)').</li>

</ul>

<p>What is a warnings structure?  When we use Seqw, we generally accumulate
warnings into a list, so our actions just cons new warnings into this list
when desired.  But Seqw itself imposes no particular constraints on what
a warnings structure is, and generally the way in which a warning is updated
is determined by the actions of the program rather than by Seqw itself.</p>

<p>For examples of using SEQW, see the file @('misc/seqw-examples.lsp').</p>")
other
(program)
seqw-process-bindfunction
(defun seqw-process-bind
  (x stream warnings rest)
  (declare (xargs :guard (and (seq-bind-p x)
        (seq-name-p stream)
        (seq-name-p warnings))))
  (cond ((eq (car x) :=) (let ((action (second x)))
        `(mv-let (!!!error !!!val ,STREAM ,WARNINGS)
          ,ACTION
          (if !!!error
            (mv !!!error !!!val ,STREAM ,WARNINGS)
            (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))
    ((or (eq (car x) :w=) (eq (car x) :s=)) (let ((action (second x)))
        `(let ((!!!stream ,STREAM))
          (mv-let (!!!error !!!val ,STREAM ,WARNINGS)
            ,ACTION
            (cond (!!!error (mv !!!error !!!val ,STREAM ,WARNINGS))
              ((not (mbt (,(CASE (CAR X) (:S= '<) (:W= '<=)) (len ,STREAM)
                     (len !!!stream)))) (prog2$ (er hard?
                    "SEQW count failed for (~x0 ~x1.)~%"
                    ',(CAR X)
                    ',ACTION)
                  (mv "SEQW count failure." nil !!!stream ,WARNINGS)))
              (t (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))))
    (t (let* ((nametree (first x)) (type (second x)) (action (third x)))
        (if (and nametree (symbolp nametree))
          (case type
            (:= `(mv-let (!!!error ,NAMETREE ,STREAM ,WARNINGS)
                ,ACTION
                (if !!!error
                  (mv !!!error ,NAMETREE ,STREAM ,WARNINGS)
                  (check-vars-not-free (!!!error !!!val !!!stream) ,REST))))
            ((:w= :s=) `(let ((!!!stream ,STREAM))
                (mv-let (!!!error ,NAMETREE ,STREAM ,WARNINGS)
                  ,ACTION
                  (cond (!!!error (mv !!!error ,NAMETREE ,STREAM ,WARNINGS))
                    ((not (mbt (,(CASE TYPE (:S= '<) (:W= '<=)) (len ,STREAM)
                           (len !!!stream)))) (prog2$ (er hard?
                          "SEQW count failed for (~x0 ~x1 ~x2.)~%"
                          ',NAMETREE
                          ',TYPE
                          ',ACTION)
                        (mv "SEQW count failure." nil !!!stream ,WARNINGS)))
                    (t (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))))
          (case type
            (:= `(mv-let (!!!error !!!val ,STREAM ,WARNINGS)
                ,ACTION
                (if !!!error
                  (mv !!!error !!!val ,STREAM ,WARNINGS)
                  (let ,(SEQ-NAMETREE-TO-LET-BINDINGS NAMETREE '!!!VAL)
                    (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))
            ((:w= :s=) `(let ((!!!stream ,STREAM))
                (mv-let (!!!error !!!val ,STREAM ,WARNINGS)
                  ,ACTION
                  (cond (!!!error (mv !!!error !!!val ,STREAM ,WARNINGS))
                    ((not (mbt (,(CASE TYPE (:S= '<) (:W= '<=)) (len ,STREAM)
                           (len !!!stream)))) (prog2$ (er hard?
                          "SEQW count failed for (~x0 ~x1 ~x2.)~%"
                          ',NAMETREE
                          ',TYPE
                          ',ACTION)
                        (mv "SEQW count failure." nil !!!stream ,WARNINGS)))
                    (t (let ,(SEQ-NAMETREE-TO-LET-BINDINGS NAMETREE '!!!VAL)
                        (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))))))))))
seqw-process-unlessmutual-recursion
(mutual-recursion (defun seqw-process-unless
    (x stream warnings rest)
    (declare (xargs :guard (and (seq-unless-p x)
          (seq-name-p stream)
          (seq-name-p warnings))))
    (let ((condition (second x)) (subblock (cddr x)))
      (seqw-process-when (list* 'when `(not ,CONDITION) subblock)
        stream
        warnings
        rest)))
  (defun seqw-process-when
    (x stream warnings rest)
    (declare (xargs :guard (and (seq-when-p x)
          (seq-name-p stream)
          (seq-name-p warnings))))
    (let* ((condition (second x)) (subblock (cddr x))
        (ends-with-returnp (seq-list-ends-with-returnp subblock))
        (bound-in-subblock (seq-block-names subblock nil)))
      (cond (ends-with-returnp `(if ,CONDITION
            ,(SEQW-PROCESS-BLOCK SUBBLOCK STREAM WARNINGS NIL)
            ,REST))
        ((not bound-in-subblock) `(mv-let (!!!error !!!val ,STREAM ,WARNINGS)
            (if ,CONDITION
              ,(SEQW-PROCESS-BLOCK SUBBLOCK STREAM WARNINGS NIL)
              (mv nil nil ,STREAM ,WARNINGS))
            (if !!!error
              (mv !!!error !!!val ,STREAM ,WARNINGS)
              (check-vars-not-free (!!!error !!!val) ,REST))))
        (t (let* ((return-stmt `(return (list ,@BOUND-IN-SUBBLOCK))) (return-expansion `(mv nil (list ,@BOUND-IN-SUBBLOCK) ,STREAM ,WARNINGS))
              (new-subblock (append subblock (list return-stmt)))
              (rebindings (seq-make-let-pairs-for-when bound-in-subblock)))
            `(mv-let (!!!error !!!val ,STREAM ,WARNINGS)
              (if ,CONDITION
                ,(SEQW-PROCESS-BLOCK NEW-SUBBLOCK STREAM WARNINGS NIL)
                ,RETURN-EXPANSION)
              (if !!!error
                (mv !!!error !!!val ,STREAM ,WARNINGS)
                (let* ,REBINDINGS
                  (check-vars-not-free (!!!error !!!val) ,REST)))))))))
  (defun seqw-process-stmt
    (x stream warnings rest)
    (declare (xargs :guard (and (or (seq-bind-p x)
            (seq-when-p x)
            (seq-unless-p x)
            (seq-return-p x))
          (seq-name-p stream)
          (seq-name-p warnings))))
    (cond ((seq-bind-p x) (seqw-process-bind x stream warnings rest))
      ((seq-when-p x) (seqw-process-when x stream warnings rest))
      ((seq-unless-p x) (seqw-process-unless x stream warnings rest))
      (t (let ((type (first x)) (value (second x)))
          (cond ((eq type 'return) `(mv nil ,VALUE ,STREAM ,WARNINGS))
            ((eq type 'return-raw) value))))))
  (defun seqw-process-block
    (x stream warnings toplevelp)
    (declare (xargs :guard (and (seq-block-p x toplevelp)
          (seq-name-p stream)
          (seq-name-p warnings))))
    (if (atom (cdr x))
      (seqw-process-stmt (car x)
        stream
        warnings
        `(mv nil nil ,STREAM ,WARNINGS))
      (let ((rest (seqw-process-block (cdr x) stream warnings toplevelp)))
        (seqw-process-stmt (car x) stream warnings rest)))))
seqw-fnfunction
(defun seqw-fn
  (stream warnings block)
  (declare (xargs :guard (and (seq-name-p stream)
        (seq-name-p warnings)
        (seq-block-p block t))))
  (let* ((names (seq-block-names block t)) (initial-bindings (seq-make-initial-let-pairs (remove-duplicates names))))
    `(let ,INITIAL-BINDINGS
      (declare (ignorable ,@NAMES))
      ,(SEQW-PROCESS-BLOCK BLOCK STREAM WARNINGS T))))
seqwmacro
(defmacro seqw
  (stream warnings &rest block)
  (seqw-fn stream warnings block))
seqw-backtrack-fnfunction
(defun seqw-backtrack-fn
  (stream warnings blocks)
  (declare (xargs :guard (and (seq-name-p stream)
        (seq-name-p warnings)
        (seq-block-list-p blocks t)
        (consp blocks))))
  (if (atom (cdr blocks))
    `(seqw ,STREAM ,WARNINGS . ,(CAR BLOCKS))
    `(mv-let (!!!error !!!val updated-stream updated-warnings)
      (seqw ,STREAM ,WARNINGS . ,(CAR BLOCKS))
      (if (not !!!error)
        (mv !!!error !!!val updated-stream updated-warnings)
        (check-vars-not-free (!!!error !!!val)
          ,(SEQW-BACKTRACK-FN STREAM WARNINGS (CDR BLOCKS)))))))
seqw-backtrackmacro
(defmacro seqw-backtrack
  (stream warnings &rest blocks)
  (seqw-backtrack-fn stream warnings blocks))