9. Constructor explanations

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

Constructor information can help a lot, if you are not sure, how Mizar resolves some overloaded symbols. Constructors are also more useful for searching, than the text-level (vocabulary) 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, and take that information from an intermediate file produced by Mizar during verification.

This has some drawbacks:

• Mizar has to be run before the constructor info is available.
• We have to ensure synchronization of the editing buffer with the intermediate file containing the constructor information.
• 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 editing buffer as text property immediately after verifying. Places with this property are then clickable with <S-down-mouse-3> (mizar-show-constrs-other-window), which displays the constructor information for that place (translated according to variable mizar-expl-kind) in buffer *Constructors list* in other window. That way, the constructor information usually remains relevant even after most editing operations.

Putting the constructor info into the editing buffer can slow down the verifying functions in Emacs, but for articles of average size the slowdown is not significant. Fot large articles, the "@proof" construct, See section 5.1 Proof checking, can help to prevent using this feature at large.

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 this, better also check the option Underline explanation points, so that you know where to look for the clickable spots. You have to run Mizar first, for the explanation points to appear, See section 9.1 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, 'expanded for expansion of clusters,

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

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 you click 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 get a constructor explanation of a given formula in the buffer *Constructors list*, you can use it to get various useful information.

Available operations now include

• Browsing the semantically disambiguated MMLQuery abstract (GABs, see below)
• Asking MML Query (See section 10. MML Query,) for meaning of a constructor.
• Using tags (See section 6. Browsing Functions,) to see the definition of a constructor.
• Sending the whole formula to Mizar Proof Advisor, See section 11. 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.