Description of the parse_file(lines_tup) SETL procedure

This procedure reads and parses a raw scenario file, converting it to the "digested" set of files used during subsequent logical checking of the scenario. These are: theory_data_file, theorem_sno_map_file, theorem_map_file, suppose_not_file, digested_proof_file, definition_tup_file. (See [Click]).

The work of this procedure is complete when these files have been written. All the files are written in readable "plain text" format.

The main file read to check various kinds of inferences in the verifier is "digested_proof_file".

Once syntax analysis is successful, this routine does various more detailed semi-syntactic, semi-semantic checks.

We allow segments of the scenario file input to be indicated by special lines starting with --BEGIN HERE and --PAUSE HERE (which suspends analysis of scenario lines); also --END HERE, which terminates scenario processing.

Lines can be grouped together into single logical lines by including a "Â" (option l) mark at the end. Over the web this is å

Comment lines starting with -- are ignored.

Definitions must start with either "Def " or "Def:".

Theorems must start with either "Theorem " or "Theorem:".
Theorem statements can contain a prefixed comment in square brackets, as in

Theorem 251: [Zorn's Lemma] .... Proof:...
Theorems without a number are given dummy numbers of the form "TUnnn";
Theorem statements must consist either of a single extended line, or of two or more such lines, the first containing the theorem comment in square brackets.

Proofs must start with "Proof:"

We now start to assemble (extended) lines into sections, which can be either definition_sections, theorem_sections, proof_sections, etc., or unused_sections. Section starts are marked by the appearance of one of the significant marks "Def ","Def:","Theorem ","Theorem:", or "Proof:" Definition and theorem sections are also terminated by the first empty line after their opening, and all following lines without one of the above headers are skipped.

These sections are collected into an overall tuple called "sections"; the indices of elements of various kinds (theorems, definitions, proofs, etc.) are collected into auxiliary tuples called

Note that the apply_sections comprise all def_sections.

Description of the take_section(now_in,current_section) SETL procedure

This routine is called whenever a prior section is ended by the start of a new section. It collects all the sections into an overall tuple called "sections", and also (depending on their type) collects their section numbers into auxiliary tuples called def_sections, theorem_sections, theory_sections, apply_sections, enter_sections, and proof_sections

This routine also keeps track of incomplete or missing proofs.