*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle operator precedence*From*: Holger Gast <gast at informatik.uni-tuebingen.de>*Date*: Tue, 06 Nov 2012 12:58:16 +0100*In-reply-to*: <20121105195910.GA14984@laptop-hbl.localdomain>*References*: <20121105142302.GA10786@laptop-hbl.localdomain> <CAAMXsiaSBptcj3swFrbBFAOZdZ=iSZhJRQEwbC5wBLeRy_v7QQ@mail.gmail.com> <20121105195910.GA14984@laptop-hbl.localdomain>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

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

**References**:**[isabelle] Isabelle operator precedence***From:*Holger Blasum

**Re: [isabelle] Isabelle operator precedence***From:*Brian Huffman

**Re: [isabelle] Isabelle operator precedence***From:*Holger Blasum

- Previous by Date: Re: [isabelle] looking for some measure.union_inter theorem
- Next by Date: Re: [isabelle] Exporting Proof Terms to Text File
- Previous by Thread: Re: [isabelle] Isabelle operator precedence
- Next by Thread: Re: [isabelle] Isabelle operator precedence
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list