9. Constructor explanations

Constructor explanations are used to access and query the semantic (constructor) level of the Mizar formulas. See section Constructors and user symbols, for more on constructors.

Constructor information can help a lot, especially in a situation when one is not sure how Mizar is resolving overloaded symbols. Also, searching on the level of constructors is often more useful than searching on the level of symbols.

9.1 How Constructor explanations work

Since the translation of the Mizar article to constructor level is nontrivial, we use Mizar itself to get access to that level rather than emulating that process in MizarMode. Currently, Mizar produces intermediate files when processing an article, and it is through these intermediate files that we can gain access to the desired linguistic level.

This has some drawbacks:

1. Mizar has to be run before the constructor info is available.
2. We have to ensure synchronization of the editing buffer with the intermediate file containing the constructor information.
3. When the “@proof” keyword is used to prevent proof checking, the constructor-level information is not available for the nonchecked part of article.

We solve the second problem by attaching the constructor information to the formulas in the editing buffer as a text property. This attachment is done immediately after verifying. The places where this property is attached are clickable with <S-down-mouse-3> (mizar-show-constrs-other-window), which displays the constructor information for that place. The constructor information is translated according to mizar-expl-kind) in the buffer *Constructors list*.

Putting the constructor info into the editing buffer usually slows down the verifying functions, since more work is being done by Emacs than without constructor explanations. Nonetheless, for articles of average size the slowdown is insignificant. If one wishes to use constructor explanations while working on large articles, the “@proof” construct, See section Proof checking, since it focuses the verification process by ignoring certain parts of the article, may be useful.

9.2 Getting Constructor explanations

<S-down-mouse-3>

mizar-show-constrs-other-window

To use constructor explanations, set the Verbosity in the menu to any value different from “none”. (This influences the value of the variables mizar-do-expl and mizar-expl-kind.)

If you are new to constructor explanations, we recommend that you also enable the option Underline explanation points. When this option is enabled, the places in the buffer where constructor explanations are available will be clearly visible. As was explained before, one must run Mizar on the article that one is working on before constructor explanations will be in effect, See section How Constructor explanations work.

User Option: mizar-do-expl

Use constructor explanations.
Put constructor format of 'by' items as properties after verifier run. The constructor representation can then be displayed (according to the value of ‘mizar-expl-kind’) and queried.

The default value is nil.

User Option: mizar-expl-kind

Variable controlling the display of constructor representation of formulas.
Has effect iff ‘mizar-do-expl’ is non-nil. Possible values are now

'sorted for sorted list of constructors in absolute notation. 'constructors for list of constructors in absolute notation, 'mmlquery behaves as 'sorted, but constructors are inserted directly into the mmlquery input buffer. The mmlquery interpreter has to be installed for this, see ‘mmlquery-program-name’. 'translate for expanded formula in absolute notation, 'raw for the internal Mizar representation, 'xml for xml internal Mizar representation

The values 'xml and 'raw are for debugging only, do not use them to get constructor explanations.

The default value is sorted.

User Option: mizar-underline-expls

If t, the clickable explanation spots in mizar buffer are underlined.
Has effect iff ‘mizar-do-expl’ is non-nil.

The default value is nil.

Command: mizar-show-constrs-other-window event

Show constructors of the inference that was just clicked on.
The constructors are translated according to the variable ‘mizar-expl-kind’, and shown in the buffer *Constructors list* or mmlquery if ‘mizar-expl-kind’ is 'mmlquery. The variable ‘mizar-do-expl’ should be non-nil.

9.3 Using Constructor explanations

Once you have a constructor explanation (stored in the buffer *Constructors list*) for a given formula you can get useful information.

Available operations now include

• Browsing the semantically disambiguated MMLQuery abstract (GABs, see below)
• Asking MML Query (See section MML Query,) for the meaning of a constructor.
• Using tags (See section Browsing Functions,) to see the definition of a constructor.
• Sending the whole formula to the Mizar Proof Advisor, See section Mizar Proof Advisor.

The MMLQuery abstracts (GABs) are now the preferred browsing methods, however they are not yet distributed with Mizar. They are downloadable from Grezgorz Bancerek’s site http://merak.pb.bialystok.pl/mmlquery/downloads/. The detailed description is at http://kti.mff.cuni.cz/~urban/integration.pdf.

The following special keybindings are available in the buffer *Constructors list*.

<mouse-3>

mizar-mouse-cstr-tag

M-.

mizar-kbd-cstr-tag

<mouse-2>

mizar-mouse-ask-query

RET

mizar-kbd-ask-query

C-c C-c

mizar-ask-advisor

Command: mizar-mouse-cstr-tag event

Find the definition of the mmlquery resource we clicked on.

Command: mizar-kbd-cstr-tag pos

Find the definition of the mmlquery resource at position pos.

Command: mizar-mouse-ask-query event

Ask MML Query about the mmlquery resource we clicked on.

Command: mizar-kbd-ask-query pos

Ask MML Query about the mmlquery resource at position pos.

Command: mizar-ask-advisor

Send the contents of the *Constr Explanations* buffer to Mizar Proof Advisor.
Resulting advice is shown in the buffer *Proof Advice*, where normal tag-browsing keyboard bindings can be used to view the suggested references.

This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.