Re: [isabelle] How do I retrieve the mixfix syntax of a constant?

Hi Brian,

Brian Huffman wrote:
This is not as simple as it might seem, because mixfixes for
top-level constants are not actually stored anywhere. I did some
grepping of my own, and I found that when you declare a top-level
mixfix, it ultimately gets passed to Mixfix.syn_ext_consts (defined
in Pure/Syntax/mixfix.ML). This function converts the mixfix into a syn_ext, which is a lower-level representation that is closer to what
 actually gets stored in the theory data.

It is indeed not at all simple. I ended up just writing out the mixfix representation by hand for the base constants, and they doing transforms on that.

Purely out of interest, do you know how one can get the syn_ext for a constant?

Evidently it is named "guess_infix" because it reconstructs a higher-level "mixfix" value by looking at the low-level productions stored in the theory's grammar. So it might not always succeed if there is anything unusual about the syntax for the given constant.
> [...]
According to the mercurial repository, this function was added by Florian Haftmann in April 2008; maybe he could tell us more about its
 expected behavior.

As Florian indicated, that path doesn't look very stable. From examining it, it seems the underlying syntax representation requires more time to comprehend than I have.

Thanks for the advice!


Rafal Kolanski.

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