search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
694 stars 123 forks source link

RFE: XML export of model's parse tree #246

Closed cmsmcq closed 2 months ago

cmsmcq commented 3 months ago

In Alloy 6.1.0, the Execute menu includes a choice to Show Parse Tree, which opens a tree-display widget. This is convenient for clarifying just how some possibly problematic expression has been parsed.

Is it possible to export the parse tree to XML?

The instance viewer has the possibility to export an instance to XML, but although the exported instance includes the source code for the model in question, it does not include the parse tree.

If not currently possible, I propose adding this facility as a possible enhancement.

Motivation

For what it's worth, the use case I have in mind is that of a user like myself who would like to process Alloy models and has no desire (or perhaps just no time) to become a Java programmer.

I have transcribed the Alloy grammar into 'invisible XML' (ixml) and ixml processors can use that grammar to parse most Alloy models and produce XML representations of them. But I am finding it difficult to match the behavior of the Analyzer's parser exactly using purely grammatical means: if there is a way to write an unambiguous grammar that matches the shift/reduce conflict resolution in CUP (and yacc), I do not know what it is. So sometimes my grammar requires additional parentheses on inputs accepted by the Analyzer.

Writing an unambiguous grammar to accept the same language as an ambiguous grammar and produce parse trees that match (for some suitable definition of match) the trees chosen by yacc/CUP-style operator precedence rules is an interesting problem, but it's a digression from the work I want to do with Alloy models.

pkriens commented 3 months ago

Its open source ... you can submit a PR and if it does not interfere with the other code and it is ok we can integrate it.

cmsmcq commented 3 months ago

Thank you for the invitation. I've already explained why I am unlikely to be in a position to submit a pull request within this lifetime, so I will take your response as a polite way of saying you do not find the request for enhancement compelling.

pkriens commented 3 months ago

a polite way of saying you do not find the request for enhancement compelling. :-) I understood that you did no wanted to write Java code to interact with the AST for your apps, but it is now clarified that you do not want to learn this beautiful language at all!

I guess the key thing it is not compelling enough for me to spend my own time on. However, it is really compelling for you, you can always hire me.

grayswandyr commented 3 months ago

Writing an unambiguous grammar to accept the same language as an ambiguous grammar and produce parse trees that match (for some suitable definition of match) the trees chosen by yacc/CUP-style operator precedence rules is an interesting problem, but it's a digression from the work I want to do with Alloy models.

I don't think it's possible to produce an LL or LR grammar for Alloy as some context is needed in certain situations. This is currently solved by using what's usually called a "lexer hack".

cmsmcq commented 3 months ago

I don't think it's possible to produce an LL or LR grammar for Alloy as some context is needed in certain situations. This is currently solved by using what's usually called a "lexer hack".

Thank you for the observation. The syntax specification in Appendix B of Software Abstractions and the syntax specification for Alloy 6 don't mention any particularly tricky lexical rules, so I wonder if you can elaborate at all. The only lexical issues I have encountered so far relate to whitespace and reserved words -- both familiar enough problems when rendering into ixml a grammar which expects an upstream lexer. So my grammar does require whitespace in some places where the Analyzer's parser makes it optional.

Since ixml processors accept any context-free grammar, there is no requirement that the grammar be LL or LR; making it unambiguous is desirable for practical purposes but not required by ixml.

grayswandyr commented 3 months ago

See https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.core/parser/Alloy.cup#L17 and https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompFilter.java#L106 . Essentially, there are ambiguities related to tokens corresponding to distinct terminals (e.g. some is a multiplicity, a relation qualifier and a quantifier) and to arrows with multiplicities (notice these may appear in any expression, not only in the type of a field). In both cases, some context is needed to know in which case you are. When using an LR/LALR parser, the classic approach is to "intercept" tokens with a so-called "lexer hack".

pkriens commented 2 months ago

@cmsmcq I guess we can move this to abyeance?

cmsmcq commented 2 months ago

Grayswandyr writes:

See https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.core/parser/Alloy.cup#L17 and https://github.com/AlloyTools/org.alloytools.alloy/blob/master/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompFilter.java#L106 . Essentially, there are ambiguities related to tokens corresponding to distinct terminals (e.g. some is a multiplicity, a relation qualifier and a quantifier) and to arrows with multiplicities (notice these may appear in any expression, not only in the type of a field). In both cases, some context is needed to know in which case you are. ...

Thank you for the clarification. The code you point to reassures me: none of the phenomena identified actually leads to ambiguity, and none seems to be an issue for the grammar I am writing.

pkriens asks:

I guess we can move this to abyeance?

I think so. If money to support the RFE becomes available, I'll contact you privately.