Re: [mizar] Question on parsing term expression with "qua".

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi Josef,

First of all, thanks for the answer!

> I have not looked at the actual Mizar parser code for this (and do not
> know it at the moment). I'd like to ask Andrzej (the chairman of Assoc. of
> Mizar Users) if I can answer here public questions like this by looking at
> the Mizar code (I promised not to publish it six years ago). Andrzej?

I think that the rules like this is the part of language definition (like the 
overloading rules in C++, for example), and I hope that the language 
defintion is open, though the pascal code for parser is closed. :)

Michael Nedzelsky

On Wed, 1 Nov 2006 02:51 am, Josef Urban wrote:
> Hi Michael,
>
> since no one else is answering, here is an example which could clarify
> such issues (the symbols Relation and bool are used just not to define new
> vocabulary with some Foomode and Foofunc).
>
> environ vocabularies RELAT_1; begin
>
> definition
> mode Relation means :DRel1: not contradiction;
> existence;
> end;
>
> definition
> let X be Relation;
> mode Relation of X -> Relation means not contradiction;
> correctness by DRel1;
> end;
>
> definition
> let X be Relation;
> func bool X -> set means it = X;
> correctness;
> let Y be Relation of X;
> func bool Y -> Relation means it = Y;
> correctness;
> end;
>
> reserve Y for Relation, V for Relation of Y, Z for Relation of V;
>
>
> bool (Z qua Relation of V qua Relation) is Relation;
> bool (Z qua Relation of (V qua Relation)) is Relation;
> bool ((Z qua Relation of V) qua Relation) is Relation;
>
> ::>                                                 *4
> ::> 4: This inference is not accepted
>
> I have not looked at the actual Mizar parser code for this (and do not
> know it at the moment). I'd like to ask Andrzej (the chairman of Assoc. of
> Mizar Users) if I can answer here public questions like this by looking at
> the Mizar code (I promised not to publish it six years ago). Andrzej?
>
> Josef
>
> On Tue, 31 Oct 2006, Michael Nedzelsky wrote:
> > Hi all,
> >
> > If we have the term expression like the following:
> >
> >  term_1 qua mode_1 of term_2 qua type_1
> >
> > it can be parsed in two ways:
> >
> > 1)   term_1 qua (mode_1 of term_2  qua type_1)
> > 2)  (term_1 qua  mode_1 of term_2) qua type_1
> >
> > What are the current rules for disambiguation in this situation?
> >
> > Michael Nedzelsky
> >
> >
> > --
> > This message has been scanned for viruses and
> > dangerous content by MailScanner, and is
> > believed to be clean.


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.