Email Gateway (Aug 18 2022 at 14:57): Email Gateway (Aug 18 2022 at 14:57):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Users and Gurus,
I have written a ML function which creates a new constant definition
based on the type of an old one, for example, the _any transform:
definition
"map_bp_any p ≡ λs. ∃v. map_bp p v s"
(where map_bp was also defined using "definition")
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?
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 14:57):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Email Gateway (Aug 18 2022 at 14:57):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
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
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.
This has been introduced by me to solve a technical issue concerning the
Haskabelle importer. I would not recommend to use this.
definition
"map_bp_any p ≡ λs. ∃v. map_bp p v s"
(where map_bp was also defined using "definition")
In this case, I want to get out:
("_ :→ _" [56,51] 56)
so I can turn it into:
("_ :→ -" [56] 56)
Can you provide me with a little more context? There are various ways
to deal with your problem, and the right way depends on how systematic
the desired behaviour can be described.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:59):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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!
Sincerely,
Rafal Kolanski.
Email Gateway (Aug 18 2022 at 14:59):From: Makarius <makarius@sketis.net>
I do not know of a proper way. There is a conceptual problem here, since
there is not "the" syntax for a constant. If the user writes something
like
definition c (mixfix) where "c = t"
then there is along way down to the internal syntax data structures. And
it is hard to interpret these later, and even harder to recover a
high-level notation declaration from that.
Also note that users could have there own notation/no_notation
declarations apart from that. The whole thing is subject to local
contexts and interpretations. The print mode is another degree of freedom
here.
Two many features, too many layers ...
Makarius
Last updated: Apr 18 2024 at 08:19 UTC