Extending notations in CtCoq.

In this page, we explain how to obtain to display your mathematical formulas with elaborate notations like the ones used in the following figure:

To extend the mathematical notations you use when working with CtCoq you need to define a new pretty printer and tell CtCoq how to use it. To define a new pretty-printer you may have to learn the PPML language that is used to write pretty-printing specifications by reading the reference manual and user guide(a 370k postscript file). However, you may avoid this by simply modifying the example "user notation" file given in the CtCoq distribution. Below, we give a short checklist of the steps to follow to add simple notations using this method. Then, we give a very short tutorial on the capabilities of the PPML language, showing how to perform basic formatting and how to use your own fonts and colors.

Making and compiling your own pretty printing specification

To make your own pretty printing specification, we suggest you use the Centaur windows to edit a PPML file starting from the example given in the tape. Follow these instructions:

Choose the option "Editor" from the "View" pulldown from the Centaur top menu. This will create a Centaur editing window.
Choose the option "Read" from the "File" pulldown menu in this window's menubar. This will prompt you for a file name give the following answer:
```
<ctcoq-directory>/contrib/vernac-v10/pprinters/usernotations/vernac-usernotations.ppml
```
where <ctcoq-directory> is the directory where ctcoq is installed (if you don't know this directory, go in the xterm where you started ctcoq and type (car #:system:app-path) at the prompt
In this window, choose the "Beginner" option from the "Editing-Tools" pulldown menu from the menubar. This will open an editing tool, called a Ctmenu, that will enable you to insert instruction templates without worrying too much about the exact syntax.
Choose a chapter, by clicking on a "chapter " token. You should then be in a state that ressembles the following figure:
Type <Ctrl>-I. This will introduce a new place for your own notations. choose the "rule_s" option in the Ctmenu (by clicking on it). This will introduce an operator that can have an arbitrary number of rule subpterms. The Ctmenu will automatically introduce a rule, with the following aspect:
```
CFHC_PATT1 -> [<IDENT1 ID_NUMBER> ELEM];
```
You can now edit the various holes of this rule to construct the notations you want, the rest of the file will provide you with examples that you can follow. If you want to introduce several rules, just click on the "->" and type <Ctrl>-A to introduce a new rule schema.

When you are happy with your specification it must be compiled and stored on disk for the display machinery to use it. You must decide where the new notation specification will be stored. Let us suppose you want to put this specification in the sub-directory "resources/special" of your home directory. In this case, you must edit your main resource file to add the following resources:

Centaur.vernac.ppml.usernotations.Location: \
            resources/usernotations
Centaur.vernac.ppml.usernotations.Root: user
Centaur.vernac.ppml.usernotations.Mode: compiled

After this, you should save your modified specification as the file
<your-home-directory>/resources/usernotations/vernac-usernotations.ppml,
hit the option "Reset Resources" from the Centaur top menu, and hit the "Compile" option from the "PPML" pulldown in the editing window's menubar. You can then test your new notations by hitting the "Redraw" option from the "Display" menu in CtCoq windows.

Writing a PPML Specification

The PPML formalism has been in used for more than ten years in the Centaur system to write pretty printers for a variety of programming languages. It makes it possible to parameterize the line breaking policy, to use several colors and fonts, to use several display variants depending on the level of detail requested, to combine several specifications, to put parentheses only when needed, and to adapt the display mechanism to black and white screens. In this section we shall give an overview of these capabilities.

A Rule oriented formalism

A pretty printing specification is an ordered collection of rules associating tree patterns with formatting patterns. The order in the list is relevant as it resolves the ambiguity that may exist when an expression matches two patterns. We shall see that it also plays a key role to override a old notation with a new one. Here is an instance of a pretty-printing rule for the plus function binary operator:

 appc(ident 'plus',formula_ne_list(*x,*y)) ->
             [<hv> *x "+" *y ];

In this rule the tree pattern is the expression

appc(ident 'plus',formula_ne_list(*x,*y))

The tree patterns refer to the abstract syntax structure of the commands and expressions. For this reason, they are not written in the "regular" syntax of Coq expressions. This tree pattern matches any expression where a function is applied to two arguments. It is possible to write more complex tree patterns, like the following one that ranges over a finite case of variants:

appc(*f,formula_ne_list(*x,*y))
     where *f in {ident 'plus', ident 'mult'}

To know more about the capabilities of the pattern language in PPML, you are invited to consult the PPML documentation.

Formatting boxes

The right hand side of pretty-printing rules describes boxes. a box has the form

[<hv> ...]

The brackets delimit the contents of the box, the first element of the box, <hv> denotes a separator, indicating how the various elements will be placed with respect to each other. The various possible separators are the following ones:

<h dx>: All elements will be separated by dx units of space.
<v i, dy>: All elements will be formatted vertically, the second one will be indented of i and any two elements will be separated by dy blank lines
<hv dx, i, dy>: When all elements can fit on the same line while separated by dx units of space, they do. Otherwise, the first line is filled as much as possible and the second one is indented of i units of space and it is filled as much as possible and the following lines are vertically aligned with the second line. Two consecutive lines are separated by dy blank lines.
<hov dx, i, dy>: This separator behaves the same as the previous one, except that all the elements will be placed vertically if they don't fit on one line (so the lines will not be filled as much as possible anymore).

For any separator it is possible to omit the the arguments, thus <h>, <v>, <hv>, and <hov> are acceptable separators.

Displaying box elements

The elements of the box can be of several kinds, of which we describe only three:

byte strings: Byte strings can be arbitrary character strings, but they can also contain characters outside the ascii character set. For instance, printing a double arrow requires the character of rank 222 in the symbol font. This can be obtained by writing the string "\336" (336 is the octal representation of 222, two hundreds and twenty two).
resource class elements: A change in color or font can be obtained by indicating that a sub-box will be displayed with a different set of ressources, thus to actually pretty print a double arrow, you need to change to a set of resources that uses the symbol font. For instance, the class symbol is already used in CtCoq pretty printers. the following element will do the trick:

    in class = symbol : "\222"

If you omit to print this character string with this resource class you will obtain the character "Þ" which has the same rank in all the latin fonts.

To associate a font, a background color, and a foreground color to resource class, you need to add a few lines in your main ctcoq resource file (usually, the file ~/.centaur.rdb). For instance, suppose you want to use a german very large "ß" (the german sz character) in cyan color for some purpose, you simply insert the following text in your pretty-printing rule:

    in class = myclass : "\223"

Then, in the file ~/.centaur.rdb, you insert the following lines:

Centaur.formalism-vernac.Pprinter.Format.class-myclass.Foreground:\
 cyan
Centaur.formalism-vernac.Pprinter.Format.class-myclass.Font:\
 -adobe-new century schoolbook-medium-r-normal--34-*-*-*-*-*-*-*

Be very careful that the resource mechanism is very sensitive to mistyping. It happens very often that a requested font is not used because the resource is slightly erroneous.
recursive calls: You can insert any pattern variable in the right hand side of a pretty printing rule as long as this pattern variable appears in the left hand side. This means that the formatting will contain the result of displaying the corresponding subtree at the place of this variable.
context calls: It is possible to restrict the rules used to display a subterm by placing a context on the recursive call to the pretty printer. If there is such a context, the rule applied on this subterm will have to start with a "context pattern". Then the diplay of this subterm's subterms will proceed normally. This useful if you want the same data to be displayed differently in different circumstances. For instance, we want the identifier "plus" to be displayed as the word "plus" in most cases, and as the token "+" when it is used in a function call with two arguments, and we want to have the same for the identifier "mult" (this time with the token "*"). We achieved this result by typing the following three rules:

appc(*op,formula_ne_list(*x, *y)) where 
     *op in {ident 'plus', ident 'mult'} -> 
   [<hv> *x infixop::*op *y];

infixop::ident 'plus' -> [<h> "+" ];

infixop::ident 'mult' -> [<h> "*" ];

Choosing special characters

The two main sources of special characters are the "symbol" family of fonts and the characters whose codes are outside the ascii range in all other fonts. When you want to introduce a special character in your notations, you should first check what is available in these fonts. This is done by typing the following command to the Unix shell prompt:

xfd -fn -*-symbol-*-r-*-*-*-*-*-*-*-*-*

This will open a new window with the following aspect.:

By clicking on this window, you can get the octal code of the character of your choice. To choose a special character in a regular font, just type

xfd -fn -*-helvetica-*-r-*-*-*-*-*-*-*-*-*

You can also choose the size of the fonts you use by replacing the fifth star by a pixel size. To see the available pixel sizes for a given font on your X server, type the command xlsfonts at the Unix shell prompt. Once you have chosen a font, you can tell CtCoq to use it by a resource class, as described above.