Proving touches

The proof process

Proving an expression (representing a touch) in GSiril can be done in two ways: either by using the prove statement, or with the -P command line option. Irrespective of how the proof is instigated, the process of proving an expression is the same. The expression is first separated into component parts (e.g. blocks of place notation, format strings, etc.) which are then proved sequentially.

The proof process builds up a list of all of the rows of the touch. Each time a block of place notation is proved, each changes in it is used to append an additional rows to the touch in the obvious manner. If the touch gets more than the permitted number of identical rows (as set by the -n command line option or the extents statement), a message is printed and the proof is halted. (This behaviour can be overridden by the conflict built-in symbol.

Built-in symbols

GSiril defines a number of special symbols that are used by the program to communicate the result of proving a touch. These symbols, and their initial values, are given below.

start    =;

everyrow =;
rounds   =;
conflict = "# rows ending in @", "Touch not completed due to false row$$";

abort    =;
finish   =;

true     = "# rows ending in @", "Touch is true";
notround = "# rows ending in @", "Is this OK?";
false    = "# rows ending in @", "Touch is false in $ rows";

The start symbol is proved as soon as the proof is started. It is often used to print the initial rounds, or to print column headings. Immediately after proving the touch (unless it was halted using the $$ string), the finish symbol is executed. This can be used to print any closing text required.

During proving, the everyrow symbol is executed for every row that is added to the touch; the rounds symbol is executed whenever rounds occurs in the composition; and the conflict symbol is executed whenever a row is repeated more times than is allowed. If a single row causes more than one of these symbols to be executed, then they are executed in the order they are described in the previous sentence.

If the search to be terminated by a $$ string (as, for example, the default conflict symbol does), the abort symbol is executed, and no further output is produced. Otherwise depending on whether the touch was true and came round, was true but didn't come round, or was false, the relevant one of true, notround or false gets executed.