instruction-list is executed, the
prompt and that instruction will be printed, unless the global state
variable print-prompt-and-instr-flg is unbound or nil and the
parameter no-prompt-flg is supplied and not nil.
run the given list of instructions according to a multitude of
options
Major Section: PROOF-CHECKER-COMMANDS
Example: (sequence (induct p prove) t)See also the definitions of commands
do-all, do-strict, protect, and
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''.
Note: 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 (in the standard ACL2 sense), 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 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 erp and val (in 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
proof-checker'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 print-prompt-and-instr-flg is unbound or nil and the
parameter no-prompt-flg is supplied and not nil.