[isabelle] precedences and orderings



Dear Isabelle users,

I've been wondering how easy it is to implement, and how useful people
would find, a different mechanism for defining precedence: something
based on partial orderings instead of numerical values. (I believe that
 the underlying representation is a search tree anyway...)

I'm thinking of something like:

consts "*" :: "N => N => N" (infixr [> "="])
consts "+" :: "N => N => N" (infixr [< "*", > "="])
consts "^" :: "N => N => N" (infixr [> "*"])
consts "++" :: "N => N => N" (infixr [= "+"])

where the [> "X"] makes the constant have greater precedence than X. [<
"X"], less than and [= "X"] equal to X. I think this would be a nicer
way to specify them... what do you think?

There is a little question as to the treatment of less well defined
situations, such as:

consts "a" :: "N => N => N" (infixr [> "="])
consts "b" :: "N => N => N" (infixr [> "a"])
consts "c" :: "N => N => N" (infixr [> "b"])
consts "x" :: "N => N => N" (infixr [< "c"])

in particular, how does "x" relate to "a" and "b"? I suggest that when
such ambiguity arises "x" would be given precedence equal to the nearest
element less than "c". Similarly for greater than: it could be
interpreted, when ambiguity arises, as 'just a little bigger than': the
same as the nearest next value.

Cycles should obviously produce errors. :)

Do any of you know of something like this in other systems? I do not
know much about parsing, so perhaps there is some reason why such
approaches are not implemented... ? (if so, I'd like to know!)

cheers,
lucas





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