		Search-engine friendly clone of the ACL2 documentation.

Macro-libraries

Seq

Seq is a macro language for applying actions to a stream.

In this context, a stream 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 vl Verilog parser, we typically use seq to traverse a list of tokens, which are regular ACL2 objects.

Meanwhile, an action 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.

But an action may also fail, in which case it should set error to some non-nil value, typically an error message produced by msg.

A Seq program is introduced by writing:

(seq <stream> ... statements ...)

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.

Some examples of using Seq can be found in misc/seq-examples.lsp.

The Basic Assignment Statement

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:

(var := (action ... <stream>))

Such an assignment statement has two effects when action is successful:

It binds var to the val produced by the action, and
It rebinds stream to the updated stream produced by the action

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.

Alternative Forms of Assignment

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:

(:= (action ... <stream>))

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

((foo . bar) := (action ... <stream>))

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:

((foo . nil) := action)

Then foo will be bound to 1 and the "2" part of val will be inaccessible.

(Usually unnecessary): In place of := in any of the above, one can also write:

:w= — weak length decrease
:s= — strong length decrease

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 len than the stream going into the action. This is sometimes needed when using Seq in mutually-recursive functions.

Conditional Execution

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

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

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

This causes the bindings for foo and bar only to be executed when the condition evaluates to non-nil.

Return Statements

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.

(return expr)
(return-raw action)

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

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.

Backtracking

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

(seq-backtrack stream block1 block2 ...)

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.

Other Resources

While Seq is convenient in certain cases, the b* macro is generally more flexible.

See also seqw, an expanded version of seq that supports the creation of warnings while processing the stream.

Subtopics

Seqw: An alternative implementation of the Seq language which allows for warnings to be implicitly collected and stored in a list as your program executes.