On Thu, Nov 7, 2019 at 2:44 AM Giovanni Mascellani <[email protected]>
wrote:
> Hi,
>
> Il 07/11/19 03:18, Mario Carneiro ha scritto:
> > Neither; it means that any time a particular infixy constant appears, it
> > must have the same precedence. That is, if you have a notation x $e.$ A
> > and another notation ${$ x $e.$ A $|$ ph $}$, then $e.$ must be given
> > the same precedence in both appearances.
>
> Ok, so the reason for this is that when you found a constant while
> parsing at a certain minimum precedence level, you immediately know if
> you have to branch out or not, without having to know if the surrounding
> constructor is an infix or a notation? Or is there something deeper?
>
You can't actually tell during parsing (without backtracking) if you have
actually found the notation constant or the infix constant when you see
this; that is, if you have { x e. A | ph } it might actually be { (x e. A)
| ph } and you won't notice that this doesn't parse until you get to the
"|". (And besides the fact that they are slower, we don't want to backtrack
because then we lose all claim of unambiguity.) The typing prevents this in
the case of { x e. A | ph } (since x can only be a single token) but that's
not available during parsing.
The trick that is used to prevent this is to force the user to put
precedences on *constants* (and check consistency of a given constant
across all its uses), but then use precedences on *variables* for the
actual parsing process. That is, you write
(${$:max) x ($e.$:20) A ($|$:25) ph ($}$:0)
but the parser actually uses
(${$ (x:21) $e.$ (A:26) $|$ (ph:1) $}$ : max)
where the numbers indicate the precedence level associated to the CFG
nonterminal. Notice that the precedences are increased by 1 (I think you
could also do this with a special n+epsilon precedence); this is to ensure
that when parsing (x:21), the operator "infixl $e.$ prec 20", which
contributes the CFG rule ((x:20) $e.$ (A:21) : 20), is not applicable at
the location of the x in the set abstraction, so { (x e. A) e. A | ph }
will never be considered a valid parse.
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSuDNJ%3Dm9fobhze%3DWrCbvfSFdC_EqmeA9%2BuXZYVS87SuYw%40mail.gmail.com.
