Re: [isabelle] Isabelle operator precedence



Hi Holger,

> Now, for the cherry on the cake:
> Where both parameters are equal (e.g. in the next line) 
> 	any[51] ">" any[51] => "\<^const>Orderings.ord_class_greater" (50)
> Or the first one is larger than the second (rarely encountered, 
> 	but existing, e.g.)
> 	logic[81] "respects" logic[80] => "\<^const>Equiv_Relations.RESPECTS" (80)
> what does it mean for associativity?
The point to realize is that numeric priorities generalize (or unify)
the associativity & precedence scheme by yacc et al.

The details can be found in Sec. 7.4.2 "Mixfix Syntax" of the
"The Isabelle/Isar Reference Manual"
(available as  "isabelle doc isar-ref" in Isabelle2012;
previously Sec. 6.1. of the "Old Isabelle Reference Manual").

The idea is straightforward: each non-terminal in the grammar
is annotated with an additional numeric priority, and
that priority restricts possible expansions. In a production

  ... ->  ... A^p ...

the non-terminal A^p is expanded only by rules  A^q -> ... where q >= p.

One can think of it as "that occurrence of A requires an
expansion at least 'as strong' / 'binding as tightly' as p".

In the "usual" case

  A^p -> A^q <op> A^r

<op> then appears to be / is in effect

- non-associative   if p < q  and p < r
  because the production itself does not match

- left-associative  if q <= p and p < r
  because the production can be re-applied
  only on the left-hand side of the operator

- right-associative if p < q  and p <= r
  because the production can be re-applied
  only on the right-hand side of the operator.

Excuse the length of the mail,
I am rather partial to parsers :)

--
Holger









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.