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
But an action may also fail, in which case it should set
A Seq program is introduced by writing:
(seq <stream> ... statements ...)
Some examples of using Seq can be found in
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:
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.
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>))
((foo . nil) := action)
(Usually unnecessary): In place of
These act the same as
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
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
In the second form,
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
While Seq is convenient in certain cases, the b* macro is generally more flexible.