back to mmj2
Comments?
Following is a brief sketch of my ASCII typesetting plan for use with the mmj2 Proof Assistant GUI. Problem: to render a Metamath formula using ASCII ======= in a way that facilitates comprehension. Stipulations: ============= 1) The formula has a parse tree (aka "exprRPN"); 2) The output goes into a StringBuffer with a specified left hand indentation and a right hand margin (both numbers given in terms of number of characters); 3) The rendered formula StringBuffer will be displayed using a fixed width font of a size that is compatible with the given right hand margin (it fits, in other words); 4) Carriage returns are inserted into the StringBuffer to start new lines and space characters are used for horizontal positioning of symbols. 5) If any errors are encountered the formula is not "pretty printed" but is just output symbol by symbol into the given margins (an error message should be sent to the error log however); 6) This solution and the resulting code are independent of any subsequent typesetting efforts involving MathML, etc. Strategy: ========= Because Metamath accomodates infix, postfix prefix and combinations of these syntax categories, it is impossible for any one "pretty-printing" algorithm to satisfy all users of all varieties of Metamath databases. Therefore, a default scheme shall be provided (Method A) and a RunParm will be provided allowing the user to specify a different default ASCII typesetting method for an input Metamath file. In addition, the user shall be able to specify exceptions to the default method for specific syntax axioms. For example: ASCIITypesetDefault,A ASCIITypesetMethod,B,wi,wbr,weq ASCIITypesetMethod,C,blah,blahblah,blahblahblah Method A: ======== Default Method A is very primitive. It operates recursively starting at the root node of the formula's parse tree. 1) At a given parse node the subtree expression is formatted as a single line within the left hand indentation and right hand margin.
2) If the length of the formatted expression overflows the right hand margin: 1. The symbols prior to the first variable in the node's syntax axiom are printed 2. Each variable subtree is formatted using Method A, using left hand indentation parameters such that all variable expressions are aligned vertically 3. The constant symbols, if any, following each variable expression subtree is formatted. Here is an example of Method A output for Theorem ser1absdiflem using very narrow margins to illustrate the method (it also uses the "Fencing Symbol Doublespacing" scheme that is described below): |- ( ( A e. NN /\ B e. NN ) -> ( abs ` ( ( ( + seq1 F ) ` ( A + B ) ) - ( ( + seq1 F ) ` A ) ) ) <_ ( ( ( + seq1 G ) ` ( A + B ) ) - ( ( + seq1 G ) ` A ) ) ) ExprRPN for ser1absdiflem: cA cn wcel cB cn wcel wa cA cB caddc co caddc cF cseq1 co cfv cA caddc cF cseq1 co cfv cmin co cabs cfv cA cB caddc co caddc cG cseq1 co cfv cA caddc cG cseq1 co cfv cmin co cle wbr wi Fencing Symbol Doublespacing: ============================ Finally, to (minimally) improve readability of formulas with nested "fencing" symbols (parentheses, brackets, etc), the following RunParm is provided which will insert an extra space character outside of an inner fencing symbol if adjacent to a nesting fencing symbol: ASCIITypesetFencingSpacing,(,) (where the pair of "fencing" symbols are provided and multiple "ASCIITypesetFencingSpacing" RunParms may be input.)
Original Source in set.mm:
mdsymlem5 $p |- ( ( q e. Atoms /\ r e. Atoms ) -> ( -. q = p -> ( ( p (_ ( q vH r ) /\ ( q (_ A /\ r (_ B ) ) -> ( ( ( c e. CH /\ A (_ c ) /\ p e. Atoms ) -> ( p (_ c -> p (_ ( ( c i^i B ) vH A ) ) ) ) ) ) $=
QED Proof Step Generated by BatchMMJ?2 using RunParm? "PrintStatementDetails?,mdsymlem5":
qed:107:com24
|- ( ( q e. Atoms /\ r e. Atoms ) -> ( -. q = p -> ( ( p (_ ( q vH r ) /\ ( q (_ A /\ r (_ B ) ) -> ( ( ( c e. CH /\ A (_ c ) /\ p e. Atoms ) -> ( p (_ c -> p (_ ( ( c i^i B ) vH A ) ) ) ) ) )
ExprRPN? Printed By BatchMMJ?2 using RunParm? "ProofAsstExportToFile?,mdsymlem5,mdsymlem5.txt,new,unified,NotRandomized?,Print"
mdsymlem1.vq cv cat wcel mdsymlem1.vr cv cat wcel wa mdsymlem1.vq cv mdsymlem1.vp cv wceq wn mdsymlem1.vp cv mdsymlem1.vq cv mdsymlem1.vr cv chj co wss mdsymlem1.vq cv cA wss mdsymlem1.vr cv cB wss wa wa mdsymlem1.vc cv cch wcel cA mdsymlem1.vc cv wss wa mdsymlem1.vp cv cat wcel wa mdsymlem1.vp cv mdsymlem1.vc cv wss mdsymlem1.vp cv mdsymlem1.vc cv cB cin cA chj co wss wi wi wi wi wi
Notation Syntax Axioms Used in ExprRPN?:
wi $a wff ( ph -> ps ) $. wn $a wff -. ph $. wa $a wff ( ph /\ ps ) $. wcel $a wff A e. B $. wceq $a wff A = B $. wss $a wff A (_ B $. co $a class ( A F B ) $. cin $a class ( A i^i B ) $.
Typeset Version of mdsymlem5 with ruler (Parms: infix; break overflow; align var @ op 1; left col=10; right col=79):
1 2 3 4 5 6 7 8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |- ( ( q e. Atoms /\ r e. Atoms ) -> ( -. q = p -> ( ( p (_ ( q vH r ) /\ ( q (_ A /\ r (_ B ) ) -> ( ( ( c e. CH /\ A (_ c ) /\ p e. Atoms ) -> ( p (_ c -> p (_ ( ( c i^i B ) vH A ) ) ) ) ) )
With Double-spaced Fencing:
1 2 3 4 5 6 7 8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |- ( ( q e. Atoms /\ r e. Atoms ) -> ( -. q = p -> ( ( p (_ ( q vH r ) /\ ( q (_ A /\ r (_ B ) ) -> ( ( ( c e. CH /\ A (_ c ) /\ p e. Atoms ) -> ( p (_ c -> p (_ ( ( c i^i B ) vH A ) ) ) ) ) )
Typeset Version of mdsymlem5 with ruler (Parms: infix; break overflow; 2-col align cnst&var @ sym 1; left col=10; right col=79):
1 2 3 4 5 6 7 8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |- ( ( q e. Atoms /\ r e. Atoms ) -> ( -. q = p -> ( ( p (_ ( q vH r ) /\ ( q (_ A /\ r (_ B ) ) -> ( ( ( c e. CH /\ A (_ c ) /\ p e. Atoms ) -> ( p (_ c -> p (_ ( ( c i^i B ) vH A ) ) ) ) ) )
With Double-spaced Fencing:
1 2 3 4 5 6 7 8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |- ( ( q e. Atoms /\ r e. Atoms ) -> ( -. q = p -> ( ( p (_ ( q vH r ) /\ ( q (_ A /\ r (_ B ) ) -> ( ( ( c e. CH /\ A (_ c ) /\ p e. Atoms ) -> ( p (_ c -> p (_ ( ( c i^i B ) vH A ) ) ) ) ) )
This is definitely easier to read than the set.mm source. :) Question: why has it chosen '->' to break on and not '/\', 'e.' etc.? Does it break on those too, if the line becomes too long? --norm 18-May-2006