Re: [CZT-Devel] CZT Parser(s) - Circus extension

[Leo F. <le...@cs...>]

Hi Tim,

>> What I would like to do is to integrate the code of this parser 
>> within the parsing structure available in the CZT.
>> As far as I could understand, there are some XML template files and 
>> the ant build script that generates the parser codes.
>> Is there a kind of GnAST for generating parsers as well, or is it a 
>> sort of XML transformation that is necessary?
>
> The parser is written using an XML file. There is a base Z-part to the 
> parser file, and rules for Z extensions are put between tags. For 
> example, in the Object-Z parser, Object-Z paras/exprs etc are put 
> between <add:oz> </add:oz> tags. Petra has set up some neat trick in 
> the ant script that generates Object-Z and TCOZ CUP grammars from this 
> file.  The parser XML file is in parser/templates/Parser.xml

thanks for that. I will study this closely soon and will try to include 
the Circus productions there.
I guess that I need to include another branch in the ant task Petra 
produced to cover circus, is that right?
I mean, once I have included a new production into the XML files, what 
are the steps to follow to produce the parser class?
I know I need to run java cup over the cup file and so on, but since we 
are using XML and ant (something I haven't come across before),
what to do in the ant script? Just include something like

  <target name="generate-circus-parser"
    depends="circus-parser, circus-lparser, circus-uparser, 
circus-parserutils"/>

(plus the related targets) and then run the ant scripts?

>>  From the ant script it seems more like the. If that is so, what are 
>> the files I need to modify to take the Circus CUP into account?
>
> Most of the files in the parser/templates directory I think. You will 
> need to edit the scanner (which is implement over several XML files), 
> as well as the parser grammar.

Ok.

>> I know a little about CUP and grammars, but never used them. I am 
>> aware that dealing with CUP is not a task as easy as creating the 
>> Circus.xsd file.
>> It includes all that shift/reduction rules and conflicts to be 
>> solved. As the Z standard is already implemented in the CZT and some 
>> examples of extension are available,
>> I am assuming that including Circus CUP productions is somehow  
>> straightforward. Am I being overoptimisitic?
>> Is there anyone interested in helping doing this integration?
>
> A lot of the precedence problems are Z related, and from what I know 
> of CSP, a CSP extension to Z shouldn't be too difficult (as far 
> parsing goes) if it's built on a Z parser.

That is my intuition too.

> I'm just looking at your Circus XML schema, and I think you can do a 
> few things in there to make the transition easier. For starters, I 
> don't think you really need CircusSect or CircusPara. The best 
> solution would be to have channel, channel set, and process paragraphs 
> extend Z:Para. Even though you comment that Circus paragraphs are not 
> allowed within process definitions, the parser grammar can restrict 
> this. This simplifies the AST classes, and any other tools that use 
> them (e.g. less classes to write visitor methods for, and also you can 
> write tools such as a circus typechecker by extending the visitor 
> classes in the Z typechecker).

That is right. I was discussing this with Petra in another e-mail. I 
guess that is right.
When I wrote the schema, I followed the CUP grammar productions as well 
as the BNF of Circus I had at hand.
At first I thought they insisted on the differentiation of CircusPara, 
but with a closer look at the CUP file and your suggestions,
I could see that this differention is not the case. The confusion 
perhaps came from the fact that although Circus is a superset of Z,
the CUP grammar assumes Circus as a superclass of Z and not the other 
way round like the CZT does!

> If you remove these classes, then the parser becomes much easier to 
> extend too. You add the three new paragraphs to the "paragraph" rule 
> in the grammar, and then add a new rule called "processExpr" or 
> something (I guess processes aren't really expressions but something 
> along those lines). The "processExpr" rule will be straightforward 
> because this will not conflict with any of the Z rules, and also, it 
> is VERY similar to several of the Z, Object-Z, and TCOZ rules already 
> in the parser :)

I am pleased to hear that! Parsing is not really my first priority at 
the moment, but I am really interested in integrating Circus with the CZT.
And since I just recieve the working Circus parser, I thought to have a 
go at it using the CZT facilities.

> So firstly, I suggest you check the parser project out from the CVS 
> server and have a look how it is designed. Then try to add some of the 
> Circus extensions, but add only a few at a time, and then make sure 
> they work before continuing.
> I'm happy to answer any questions you have. I wrote most of the Z and 
> Object-Z grammar that are there, and Petra wrote most of the 
> supporting code and the scanner, so between us we should be able to 
> help with any problems.

Great! I will try those out soon and I let you know.

> Regards,
> Tim

Best regards,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Computer Science @ York University
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------