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



On Mon, Mar 22, 2010 at 11:54 PM, Rafal Kolanski <rafalk at cse.unsw.edu.au> wrote:
> I also want to generate the appropriate mixfix syntax for the new constant.
> I know how to do the transformation and how to declare syntax, but I need to
> get the syntax for a constant, e.g. "map_bp". I've been grepping through the
> source but can't see anything that returns a mixfix.
>
> In this case, I want to get out:
>        ("_ :→ _" [56,51] 56)
> so I can turn it into:
>        ("_ :→ -" [56] 56)
>
> Does anyone know how to do the syntax retrieval for a constant?

Hi Rafal,

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.

After more grepping, I did come across a function in
Pure/Syntax/syntax.ML that looks like what you want:

ML_val {* Syntax.guess_infix (Sign.syn_of @{theory}) @{const_syntax plus} *}

val it = SOME (Infixl ("+", 65)) : Mixfix.mixfix option

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.

- Brian





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