ACL2-PC::SEQUENCE

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