ACL2-pc::sequence
(meta)
run the given list of instructions according to a multitude of
options
Example:
(sequence (induct p prove) t)
This is a very general command that is used to define other sequencing
commands; see ACL2-pc::do-all, ACL2-pc::do-strict, ACL2-pc::protect, and ACL2-pc::succeed.
General Form:
(sequence
instruction-list
&optional
strict-flg protect-flg success-expr no-prompt-flg no-restore-flg)
Each instruction in the list instruction-list is run, and the
instruction ``succeeds'' if every instruction in instruction-list
``succeeds''. However, it might ``succeed'' even if some instructions in the
list ``fail''; more generally, the various arguments control a number of
aspects of the running of the instructions. All this is explained in the
paragraphs below. First we embark on a general discussion of the instruction
interpreter, including the notions of ``succeed'' and ``fail''.
Remark: The arguments are not evaluated, except (in a sense)
for success-expr, as described below.
Each primitive and meta instruction can be thought of as returning an error-triple, say (erp val state). An instruction (primitive or meta)
``succeeds'' if erp is nil and val is not nil; otherwise
it ``fails''. (When we use the words ``succeed'' or ``fail'' in this
technical sense, we'll always include them in double quotes.) If an
instruction ``fails,'' we say that the failure is ``soft'' if erp is
nil; otherwise the failure is ``hard''. The sequence command gives
the user control over how to treat ``success'' and ``failure'' when sequencing
instructions, though we have created a number of handy macro commands for this
purpose, notably do-all, do-strict and protect.
Here is precisely what happens when a sequence instruction is run.
The instruction interpreter is run on the instructions supplied in the
argument instruction-list (in order). The interpreter halts the first
time there is a hard ``failure.'' except that if strict-flg is supplied
and not nil, then the interpreter halts the first time there is any
``failure.'' The error triple (erp val state) returned by the
sequence instruction is the triple returned by the last instruction
executed (or, the triple (nil t state) if instruction-list is
nil), except for the following provision. If success-expr is
supplied and not nil, then it is evaluated with the state global
variables pc-erp and pc-val (in the "ACL2" package) bound to the
corresponding components of the error triple returned (as described above).
At least two values should be returned, and the first two of these will be
substituted for erp and val in the triple finally returned by
sequence. For example, if success-expr is (mv erp val), then
no change will be made to the error triple, and if instead it is (mv nil
t), then the sequence instruction will ``succeed''.
That concludes the description of the error triple returned by a
sequence instruction, but it remains to explain the effects of the
arguments protect-flg and no-prompt-flg.
If protect-flg is supplied and not nil and if also the
instruction ``fails'' (i.e., the error component of the triple is not nil
or the value component is nil), then the state is reverted so that the
interactive proof-builder's state (including the behavior of restore) is
set back to what it was before the sequence instruction was executed.
Otherwise, unless no-restore-flg is set, the state is changed so that the
restore command will now undo the effect of this sequence
instruction (even if there were nested calls to sequence).
Finally, as each instruction in instruction-list is executed, the
prompt and that instruction will be printed, unless the global state variable
pc-print-prompt-and-instr-flg is unbound or nil and the parameter
no-prompt-flg is supplied and not nil.
