seq - ACL2 Book

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

other

(defsection seq
  :parents (macro-libraries)
  :short "<i>Seq</i> is a macro language for applying actions to a stream."
  :long "<p>In this context, a <i>stream</i> is any data structure that we want
to update in an essentially sequential/single-threaded way.  It might be a
stobj, but it could also be a regular ACL2 list or some other kind of
structure.  For example, in the @(see vl) Verilog parser, we typically use seq
to traverse a list of tokens, which are regular ACL2 objects.</p>

<p>Meanwhile, an <i>action</i> is some operation which typically inspects the
stream, and then returns a triple of the form @('(mv error val stream)').  When
the action is successful, @('error') is @('nil'), @('stream') is the updated
stream, and @('val') is perhaps some piece of information that was gleaned from
running this action.  For instance, in the Verilog parser we may take a token
out of the stream and put it into val.</p>

<p>But an action may also fail, in which case it should set @('error') to some
non-nil value, typically an error message produced by @(see msg).</p>

<p>A Seq program is introduced by writing:</p>

@({
    (seq <stream> ... statements ...)
})

<p>Where @('stream') is the name of the stream to operate on and update, and
the valid statements are described below.  Every Seq program evaluates to an
@('(mv error val stream)') triple.</p>

<p>Some examples of using Seq can be found in @('misc/seq-examples.lsp').</p>


<h3>The Basic Assignment Statement</h3>

<p>In many ways, Seq resembles a loop-free, imperative programming language
with a mechanism to throw exceptions.  Seq programs are written as blocks of
statements, and the fundamental statement is assignment:</p>

@({
    (var := (action ... <stream>))
})

<p>Such an assignment statement has two effects when action is successful:</p>

<ol>
<li>It binds var to the val produced by the action, and</li>
<li>It rebinds stream to the updated stream produced by the action</li>
</ol>

<p>But action may also fail, in which case the failure stops execution of the
current block and we propagate the error upwards throughout the entire Seq
program.</p>


<h3>Alternative Forms of Assignment</h3>

<p>We have a couple of additional assignment statements.  The first variant
simply allows you to ignore the val produced by an action, and is written:</p>

@({
     (:= (action ... <stream>))
})

<p>The second variant allows you to destructure the val produced by the action,
and is written:</p>

@({
     ((foo . bar) := (action ... <stream>))
})

<p>@('NIL') has a special meaning in this second form, and can be used to
"drop" parts of val which are not interesting.  For example, if action
produces the value (1 . 2), and you write:</p>

@({
     ((foo . nil) := action)
})

<p>Then @('foo') will be bound to 1 and the "2" part of val will be
inaccessible.</p>

<p>(Usually unnecessary): In place of @(':=') in any of the above, one can also
write:</p>

<ul>
<li>@(':w=') &mdash; weak length decrease</li>
<li>@(':s=') &mdash; strong length decrease</li>
</ul>

<p>These act the same as @(':='), except that they add some @('(mbe :logic
...)')-only checks that ensure that the returned stream has a weakly lower or
strongly lower @(tsee len) than the stream going into the action.  This
is sometimes needed when using Seq in mutually-recursive functions.</p>


<h3>Conditional Execution</h3>

<p>A block can be only conditionally executed by wrapping it in a <b>when</b>
or <b>unless</b> clause.  For example:</p>

@({
    (when (integerp x)
      (foo := (action1 ...)
      (bar := (action2 ...)))

    (unless (consp x)
      (foo := (action ...)))
})

<p>This causes the bindings for @('foo') and @('bar') only to be executed when
the condition evaluates to non-@('nil').</p>


<h3>Return Statements</h3>

<p>The final statement of a Seq program must be a return statement, and "early"
return statements can also occur as the last statement of a when or unless
block.  There are two versions of the return statement.</p>

@({
    (return expr)
    (return-raw action)
})

<p>Either one of these causes the entire Seq program to exit.  In the first
form, @('expr') is expected to evaluate to a regular ACL2 object, and the result
of the Seq program will be @('(mv nil expr stream)').</p>

<p>In the second form, @('action') is expected to itself evaluate to an @('(mv
error val stream)') tuple, and the Seq program returns this value verbatim.</p>


<h3>Backtracking</h3>

<p>We also provide another macro, <b>seq-backtrack</b>, which cannot be used on
STOBJs, but can be used with regular, applicative structures.  The general form
is:</p>

@({
    (seq-backtrack stream block1 block2 ...)
})

<p>This macro has the following effect.  First, we try to run @('block1').  If
it succeeds, we return the @('(mv error val new-stream)') that it returns.
Otherwise, we start again with the initial @('stream') and try to run the
remaining blocks, in order.  If none of the blocks succeed, we return the
@('(mv error val new-stream)') encountered by the final block.</p>


<h3>Other Resources</h3>

<p>While Seq is convenient in certain cases, the @(see b*) macro is generally
more flexible.</p>

<p>See also @(see seqw), an expanded version of @(see seq) that supports the
creation of warnings while processing the stream.</p>")

other

(program)

seq-name-pfunction

(defun seq-name-p
  (x)
  (declare (xargs :guard t))
  (cond ((not (symbolp x)) (cw "Error: ~x0 cannot be used as a variable name.~%" x))
    ((eq x t) (cw "Error: t cannot be used as a variable name.~%"))
    ((equal (symbol-package-name x) "KEYWORD") (cw "Error: ~x0 cannot be used as a variable name.~%" x))
    (t t)))

seq-aux-nametree-pfunction

(defun seq-aux-nametree-p
  (x)
  (declare (xargs :guard t))
  (if (consp x)
    (and (seq-aux-nametree-p (car x))
      (seq-aux-nametree-p (cdr x)))
    (seq-name-p x)))

seq-flatten-nametreefunction

(defun seq-flatten-nametree
  (x)
  (declare (xargs :guard (seq-aux-nametree-p x)))
  (if (consp x)
    (append (seq-flatten-nametree (car x))
      (seq-flatten-nametree (cdr x)))
    (if (not x)
      nil
      (list x))))

seq-nametree-pfunction

(defun seq-nametree-p
  (x)
  (declare (xargs :guard t))
  (and (seq-aux-nametree-p x)
    (or (no-duplicatesp (seq-flatten-nametree x))
      (cw "Error: the nametree ~x0 contains duplicates.~%" x))))

seq-nametree-to-let-bindingsfunction

(defun seq-nametree-to-let-bindings
  (x path)
  (declare (xargs :guard (seq-nametree-p x)))
  (if (consp x)
    (append (seq-nametree-to-let-bindings (car x) `(car ,PATH))
      (seq-nametree-to-let-bindings (cdr x) `(cdr ,PATH)))
    (if (not x)
      nil
      (list (list x path)))))

seq-bind-pfunction

(defun seq-bind-p
  (x)
  (declare (xargs :guard t))
  (and (consp x)
    (if (member-eq (first x) '(:= :w= :s=))
      (and (or (true-listp x)
          (cw "Error: Expected assignment to be a true-listp. ~x0.~%"
            x))
        (or (= (length x) 2)
          (cw "Error: Expected assignment to have length 2. ~x0.~%" x)))
      (and (consp (cdr x))
        (member-eq (second x) '(:= :w= :s=))
        (or (true-listp x)
          (cw "Error: Expected assignment to be a true-listp. ~x0.~%"
            x))
        (or (= (length x) 3)
          (cw "Error: Expected assignment to have length 3. ~x0.~%" x))
        (or (seq-nametree-p (first x))
          (cw "Error: Expected assignment to have a name-tree. ~x0.~%"
            x))))))

seq-return-pfunction

(defun seq-return-p
  (x)
  (declare (xargs :guard t))
  (and (consp x)
    (or (eq (car x) 'return) (eq (car x) 'return-raw))
    (or (true-listp x)
      (cw "Error: Expected return to be a true-listp. ~x0.~%" x))
    (or (= (length x) 2)
      (cw "Error: Expected return to have length 2. ~x0.~%" x))))

seq-when-pmutual-recursion

(mutual-recursion (defun seq-when-p
    (x)
    (declare (xargs :guard t))
    (and (consp x)
      (eq (car x) 'when)
      (or (true-listp x)
        (cw "Error: "when" must be a true-listp. ~x0.~%" x))
      (or (>= (length x) 3)
        (cw "Error: "when" must have at least length 3. ~x0.~%" x))
      (seq-block-p (cddr x) nil)))
  (defun seq-unless-p
    (x)
    (declare (xargs :guard t))
    (and (consp x)
      (eq (car x) 'unless)
      (or (true-listp x)
        (cw "Error: "unless" must be a true-listp. ~x0.~%" x))
      (or (>= (length x) 3)
        (cw "Error: "unless" must have at least length 3. ~x0.~%"
          x))
      (seq-block-p (cddr x) nil)))
  (defun seq-block-p
    (x toplevelp)
    (declare (xargs :guard t))
    (cond ((atom x) (cw "Error: expected a block, but found ~x0.~%" x))
      ((atom (cdr x)) (if toplevelp
          (or (seq-return-p (car x))
            (cw "Error: top-level block must end with a return ~
                       statement, but ends with ~x0.~%"
              x))
          (or (seq-bind-p (car x))
            (seq-when-p (car x))
            (seq-unless-p (car x))
            (seq-return-p (car x))
            (cw "Error: invalid final block statement: ~x0.~%" (car x)))))
      (t (and (or (seq-bind-p (car x))
            (seq-when-p (car x))
            (seq-unless-p (car x))
            (cw "Error: invalid interior block statement: ~x0.~%"
              (car x)))
          (seq-block-p (cdr x) toplevelp))))))

seq-bind-namesfunction

(defun seq-bind-names
  (x)
  (declare (xargs :guard (seq-bind-p x)))
  (if (member-eq (car x) '(:= :w= :s=))
    nil
    (seq-flatten-nametree (first x))))

seq-when-namesmutual-recursion

(mutual-recursion (defun seq-when-names
    (x)
    (declare (xargs :guard (seq-when-p x)))
    (seq-block-names (cddr x) nil))
  (defun seq-unless-names
    (x)
    (declare (xargs :guard (seq-unless-p x)))
    (seq-block-names (cddr x) nil))
  (defun seq-stmt-names
    (x)
    (declare (xargs :guard (or (seq-bind-p x)
          (seq-when-p x)
          (seq-unless-p x)
          (seq-return-p x))))
    (cond ((seq-bind-p x) (seq-bind-names x))
      ((seq-when-p x) (seq-when-names x))
      ((seq-unless-p x) (seq-unless-names x))
      ((seq-return-p x) nil)))
  (defun seq-block-names
    (x toplevelp)
    (declare (xargs :guard (seq-block-p x toplevelp)))
    (if (atom (cdr x))
      (seq-stmt-names (car x))
      (append (seq-stmt-names (car x))
        (seq-block-names (cdr x) toplevelp)))))

seq-process-bindfunction

(defun seq-process-bind
  (x stream rest)
  (declare (xargs :guard (and (seq-bind-p x) (seq-name-p stream))))
  (cond ((eq (car x) :=) (let ((action (second x)))
        `(mv-let (!!!error !!!val ,STREAM)
          ,ACTION
          (if !!!error
            (mv !!!error !!!val ,STREAM)
            (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)
            ,ACTION
            (cond (!!!error (mv !!!error !!!val ,STREAM))
              ((not (mbt (,(CASE (CAR X) (:S= '<) (:W= '<=)) (len ,STREAM)
                     (len !!!stream)))) (prog2$ (er hard?
                    'seq-process-bind
                    "SEQ count failed for (~x0 ~x1.)~%"
                    ',(CAR X)
                    ',ACTION)
                  (mv "SEQ count failure." nil ,STREAM)))
              (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)
                ,ACTION
                (if !!!error
                  (mv !!!error ,NAMETREE ,STREAM)
                  (check-vars-not-free (!!!error !!!val !!!stream) ,REST))))
            ((:w= :s=) `(let ((!!!stream ,STREAM))
                (mv-let (!!!error ,NAMETREE ,STREAM)
                  ,ACTION
                  (cond (!!!error (mv !!!error ,NAMETREE ,STREAM))
                    ((not (mbt (,(CASE TYPE (:S= '<) (:W= '<=)) (len ,STREAM)
                           (len !!!stream)))) (prog2$ (er hard?
                          'seq-process-bind
                          "SEQ count failed for (~x0 ~x1 ~x2.)~%"
                          ',NAMETREE
                          ',TYPE
                          ',ACTION)
                        (mv "SEQ count failure." nil ,STREAM)))
                    (t (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))))
          (case type
            (:= `(mv-let (!!!error !!!val ,STREAM)
                ,ACTION
                (if !!!error
                  (mv !!!error !!!val ,STREAM)
                  (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)
                  ,ACTION
                  (cond (!!!error (mv !!!error !!!val ,STREAM))
                    ((not (mbt (,(CASE TYPE (:S= '<) (:W= '<=)) (len ,STREAM)
                           (len !!!stream)))) (prog2$ (er hard?
                          'seq-process-bind
                          "SEQ count failed for (~x0 ~x1 ~x2.)~%"
                          ',NAMETREE
                          ',TYPE
                          ',ACTION)
                        (mv "SEQ count failure." nil ,STREAM)))
                    (t (let ,(SEQ-NAMETREE-TO-LET-BINDINGS NAMETREE '!!!VAL)
                        (check-vars-not-free (!!!error !!!val !!!stream) ,REST)))))))))))))

seq-list-ends-with-returnpfunction

(defun seq-list-ends-with-returnp
  (x)
  (declare (xargs :guard (consp x)))
  (if (atom (cdr x))
    (seq-return-p (car x))
    (seq-list-ends-with-returnp (cdr x))))

seq-make-let-pairs-for-whenfunction

(defun seq-make-let-pairs-for-when
  (names)
  (declare (xargs :guard t))
  (cond ((atom names) nil)
    ((atom (cdr names)) (list `(,(CAR NAMES) (car !!!val))))
    (t (list* `(,(CAR NAMES) (car !!!val))
        `(!!!val (cdr !!!val))
        (seq-make-let-pairs-for-when (cdr names))))))

seq-process-unlessmutual-recursion

(mutual-recursion (defun seq-process-unless
    (x stream rest)
    (declare (xargs :guard (and (seq-unless-p x) (seq-name-p stream))))
    (let ((condition (second x)) (subblock (cddr x)))
      (seq-process-when (list* 'when `(not ,CONDITION) subblock)
        stream
        rest)))
  (defun seq-process-when
    (x stream rest)
    (declare (xargs :guard (and (seq-when-p x) (seq-name-p stream))))
    (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
            ,(SEQ-PROCESS-BLOCK SUBBLOCK STREAM NIL)
            ,REST))
        ((not bound-in-subblock) `(mv-let (!!!error !!!val ,STREAM)
            (if ,CONDITION
              ,(SEQ-PROCESS-BLOCK SUBBLOCK STREAM NIL)
              (mv nil nil ,STREAM))
            (if !!!error
              (mv !!!error !!!val ,STREAM)
              (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))
              (new-subblock (append subblock (list return-stmt)))
              (rebindings (seq-make-let-pairs-for-when bound-in-subblock)))
            `(mv-let (!!!error !!!val ,STREAM)
              (if ,CONDITION
                ,(SEQ-PROCESS-BLOCK NEW-SUBBLOCK STREAM NIL)
                ,RETURN-EXPANSION)
              (if !!!error
                (mv !!!error !!!val ,STREAM)
                (let* ,REBINDINGS
                  (check-vars-not-free (!!!error !!!val) ,REST)))))))))
  (defun seq-process-stmt
    (x stream 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))))
    (cond ((seq-bind-p x) (seq-process-bind x stream rest))
      ((seq-when-p x) (seq-process-when x stream rest))
      ((seq-unless-p x) (seq-process-unless x stream rest))
      (t (let ((type (first x)) (value (second x)))
          (cond ((eq type 'return) `(mv nil ,VALUE ,STREAM))
            ((eq type 'return-raw) value))))))
  (defun seq-process-block
    (x stream toplevelp)
    (declare (xargs :guard (and (seq-block-p x toplevelp) (seq-name-p stream))))
    (if (atom (cdr x))
      (seq-process-stmt (car x) stream `(mv nil nil ,STREAM))
      (let ((rest (seq-process-block (cdr x) stream toplevelp)))
        (seq-process-stmt (car x) stream rest)))))

seq-make-initial-let-pairsfunction

(defun seq-make-initial-let-pairs
  (names)
  (declare (xargs :guard t))
  (if (atom names)
    nil
    (cons `(,(CAR NAMES) nil)
      (seq-make-initial-let-pairs (cdr names)))))

seq-fnfunction

(defun seq-fn
  (stream block)
  (declare (xargs :guard (and (seq-name-p stream) (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))
      ,(SEQ-PROCESS-BLOCK BLOCK STREAM T))))

seqmacro

(defmacro seq (stream &rest block) (seq-fn stream block))

seq-block-list-pfunction

(defun seq-block-list-p
  (x toplevelp)
  (declare (xargs :guard t))
  (if (atom x)
    (eq x nil)
    (and (seq-block-p (car x) toplevelp)
      (seq-block-list-p (cdr x) toplevelp))))

seq-backtrack-fnfunction

(defun seq-backtrack-fn
  (stream blocks)
  (declare (xargs :guard (and (seq-name-p stream)
        (seq-block-list-p blocks t)
        (consp blocks))))
  (if (atom (cdr blocks))
    `(seq ,STREAM . ,(CAR BLOCKS))
    `(mv-let (!!!error !!!val updated-stream)
      (seq ,STREAM . ,(CAR BLOCKS))
      (if (not !!!error)
        (mv !!!error !!!val updated-stream)
        (check-vars-not-free (!!!error !!!val)
          ,(SEQ-BACKTRACK-FN STREAM (CDR BLOCKS)))))))

seq-backtrackmacro

(defmacro seq-backtrack
  (stream &rest blocks)
  (seq-backtrack-fn stream blocks))