Email Gateway (Aug 22 2022 at 20:40): Email Gateway (Aug 22 2022 at 20:40):From: Daniel Kirchner <daniel@ekpyron.org>
Dear Isabelle mailing list,
Is there a reason why the ML function "Syntax_Phases.parsetree_to_ast" is not
exposed as public API?
I haven't seen another way to translate a parse tree to an AST or to further
process a parse tree in any way using the ML API for that matter. It looks
like the exposed API allows to generate a parse tree, but I haven't seen a way
to continue from there. Currently I work around that problem by just copying
"Syntax_Phases.parsetree_to_ast", but that's of course not particularly nice.
Or am I missing another way to do this?
To provide some background for the question:
I'm currently working on implementing a custom parser for inner syntax packed
in string constants for implementing an embedded object logic with a syntactic
structure that cannot be parsed otherwise (e.g. single letter identifiers with
no whitespace delimiters, etc., requiring a customized parsing process). The
idea is to end up with a syntax like " ⊨ ''<formula of embedded logic>'' ".
This is already working quite well, basically using "Syntax.tokenize ->
Syntax.parse -> Syntax_Phases.parsetree_to_ast" with some custom adjustments
between the steps, but unfortunately "Syntax_Phases.parsetree_to_ast" seems to
be private to "Syntax_Phases" at the moment.
On a related note: packing formulas in custom syntax plus a string constant is
the only way to prevent the parsing process from trying to parse children first
and to be able to intervene on string or token level using a
"parse_ast_translation", right? The otherwise very great tutorial at https://
nms.kcl.ac.uk/christian.urban/Cookbook/ is unfortunately still lacking
information on parse translations and generally on intervening on the inner
syntax parsing process - in fact I'm considering to contribute to it once my
own project is done.
Best wishes,
Daniel Kirchner
signature.asc
Email Gateway (Aug 22 2022 at 20:41):From: Makarius <makarius@sketis.net>
I've seen this and was somewhat worried about it, because it means that
I have again explain more things about how Isabelle really works.
People who prefer a non-canonical view on Isabelle are free to do that,
but I will not support it.
Makarius
Email Gateway (Aug 22 2022 at 20:43):From: Makarius <makarius@sketis.net>
On 26/09/2019 15:58, Daniel Kirchner wrote:
Is there a reason why the ML function "Syntax_Phases.parsetree_to_ast" is not
exposed as public API?
Usually to prevent violation of implicit structural assumptions about
the system. Note that many of these modules are more open than they
should. Low-level tinkering with "syntax phases" is unlikely to work out
properly -- now and in the longer run.
It requires very careful study of the overall situation to figure out if
previously unintended applications of certain modules can be made official.
I'm currently working on implementing a custom parser for inner syntax packed
in string constants for implementing an embedded object logic with a syntactic
structure that cannot be parsed otherwise (e.g. single letter identifiers with
no whitespace delimiters, etc., requiring a customized parsing process). The
idea is to end up with a syntax like " ⊨ ''<formula of embedded logic>'' ".
This is already working quite well, basically using "Syntax.tokenize ->
Syntax.parse -> Syntax_Phases.parsetree_to_ast" with some custom adjustments
between the steps, but unfortunately "Syntax_Phases.parsetree_to_ast" seems to
be private to "Syntax_Phases" at the moment.
The standard way to embed sublanguages is via cartouches, e.g. see
Isabelle2019/HOL/ex/Cartouche_Examples.thy for some experiments and
examples.
This does not solve the problem of imitation the Isabelle term language.
At some point there might be more official ways to do that, e.g.
something like antiquotations with control symbol and cartouch within terms.
The otherwise very great tutorial at https://
nms.kcl.ac.uk/christian.urban/Cookbook/ is unfortunately still lacking
information on parse translations and generally on intervening on the inner
syntax parsing process - in fact I'm considering to contribute to it once my
own project is done.
That document is "fan-fiction". In its early years, I tried to
contribute to it and rectify its somewhat misleading approach at
"Isabelle system hacking", but I've given up on it long ago.
Makarius
signature.asc
Email Gateway (Aug 22 2022 at 20:44):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
At an earlier stage of this document there was a chapter on parsing. I
have two copies of pdf versions of the document, of which one says
Jeremy Dawson wrote the first version of chapter 5 about parsing.
and the other (I think more recent) says
Jeremy Dawson wrote the first version of chapter ?? about parsing.
I understood this to indicate that parsing in Isabelle had changed so
significantly that the chapter was no longer useful, and that the
authors of these changes failed to update the documentation.
Unfortunately I can't recall enough about the chapter to tell whether it
would have given exactly what you want.
(I have no idea what "fan-fiction" or the somewhat misleading approach
at "Isabelle system hacking" mean)
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 20:49):From: "Urban, Christian via Cl-isabelle-users" <cl-isabelle-users@lists.cam.ac.uk>
Thanks for the praise from everybody....I would have interpreted "darkfic"
as criticism. ;o)
Anyway, if anybody likes to contribute "fix-fic" [*], you download the sources, make
changes and send back the diffs. Norbert Schirmer did this recently by getting
the fan-fiction back into a compilable state with Isabelle 2019. All praise to him!
Best wishes,
Christian
[*] https://en.m.wikipedia.org/wiki/Fan_fiction
Email Gateway (Aug 22 2022 at 20:50):From: Tobias Nipkow <nipkow@in.tum.de>
I would like to congratulate Christian on his sense of humour!
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC