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