Assignment Program Representation

Introduction

In this assignment, you will use the infrastructure of Stratego/XT to implement a syntax definition, and generate a parser, tree grammar and pretty-printer for a small language of predicate logic formulae. Thus, you will implement all the components used in a program transformation pipeline, except for the actual transformations. The following are examples of predicate logic formulae in the language you will implement.

not (exists a : Man(a) /\ Woman(a))

forall a : forall b : not(a /\ b) <-> (not a \/ not b)

For documentation, use the part on The XT Transformation Tools in the Stratego/XT Manual. The Programs and Tools Reference might be helpful as well.

(A) Syntax Definition

Write a syntax definition that defines a syntax for predicate logic formulae such that the abstract syntax trees which it generates correspond to the abstract syntax defined by the tree grammar in the subsection 'Abstract Syntax'. Use at least two modules in your syntax definition. Create a shell script generate.sh. In this script, apply the parse table generator to generate a parse table from your syntax definition. If the parse table generator gives warnings, then fix these.

Testing

Use parse-unit testsuite(s) to test if your syntax definition defines the right language. Apply your testsuites in the same shell script (see resources if you are not familiar with shell scripting). Write some larger tests in separate .plf files and include them in the testsuite. We will use these separate files later.

(see Manual: Syntax Definition in SDF / Unit Testing of Syntax Definitions)

Disambiguation

You should solve all possible ambiguities in this syntax definition. For example, test if the formulae true is ambiguous and if so, solve this ambiguity.

The priorities of the operators are not specified, but some can be derived from the two examples. Just use your common sense for the cases where the priority is not defined by the examples. The same holds for associativity.

Feel free to add language features to illustrate more disambiguation problems.

(see Manual: Syntax Definition in SDF / Examples: Defining Lexical Syntax and Examples: Defining Context-Free Syntax)

Abstract Syntax

The abstract syntax of our predicate logic language is defined by the following tree grammar:

regular tree grammar
start Form
productions
  Form -> True()
        | False()
        | Prop(Id)
        | Pred(Id, FormList)
        | Not(Form)
        | And(Form, Form)
        | Or(Form, Form)
        | Equiv(Form, Form)
        | ForAll(Id, Form)
        | Exists(Id, Form)

  FormList -> <cons> (Form, FormList)
            | <nil> ()

  Id -> <string>

Thus, the syntax definition should parse the formulae mentioned in the introduction and produce the following abstract syntax trees:

Not(
  Exists("a"
  , And(
      Pred("Man", [Prop("a")])
    , Pred("Woman", [Prop("a")])
    )
  )
)

Forall("a"
, Forall("b"
  , Equiv(
      Not(And(Prop("a"),Prop("b")))
    , Or(Not(Prop("a")),Not(Prop("b")))
    )
  )
)

(B) Tree Grammar

Generate a tree grammar PLF.rtg from your syntax definition. The tree language defined by the generated tree grammar should be very similar to the tree grammar above. There will be some differences in the definition of lists. Try to find out how the definition of lists works in the generated rtg.

In your shell script, check that all the .plf files you created after parsing have the right format, i.e. conform to the generated tree grammar. You will probably get no errors. Just for fun, modify an abstract syntax tree by hand and see what the format-check tool does (optionally, use --vis to visualize the problem).

(see Manual: Trees, Terms, and Tree Grammars / Format Checking. Unfortunately, this chapter is not finished yet. Please use the information from the course slides for now.)

(C) Pretty-print table

Generate a pretty-print table PLF.pp for the language. Copy this generated pretty-print table to PLF-pretty.pp and adapt it to produce pretty formulae, or at least formulae that are parsed in the same way as the original.

Most pretty-print rules are trivial. Modify the pretty-print rules of the exists and forall constructs to produce a more fancy layout:

forall a :
  forall b :
    not(a /\ b) <-> not a \/ not b

Check the correctness of your pipeline (see the Script section for a more detailed description of this).

(see Manual: Pretty Printing with GPP

Parentheses

Most likely, you will have a problem with parentheses. Use the sdf2parenthesize tool to generate a Stratego program PLF-parenthesize.str that inserts Parenthetical nodes. Add a pretty-print rule for this constructor to the pretty-print table. Pass the argument -m PLF to sdf2parenthesize (besides -i and -o) to specify the main module in the syntax definition.

The parenthesize tool needs a so-called Stratego Signature, which you can generate from the .rtg using rtg2sig. We have not discussed Stratego compilation yet, so you get that part for free.

$ sdf2parenthesize -i PLF.def -o PLF-parenthesize.str -m PLF
$ rtg2sig -i PLF.rtg -o PLF.str
$ strc -i PLF-parenthesize.str -m io-PLF-parenthesize -la stratego-lib

You can now invoke PLF-parenthesize in your pipeline. It is an executable PLF ATerm to ATerm tool. For example:

$ echo "not (a /\ b)" | sglri -p PLF.tbl
Not(And(Prop("a"),Prop("b")))
$ echo "not (a /\ b)" | sglri -p PLF.tbl | ./PLF-parenthesize 
Not(Parenthetical(And(Prop("a"),Prop("b"))))

Note that this introduces a new constructor Parenthetical. You need to extend your pretty-print table to handle this new constructor.

(D) Script

Using the Stratego/XT tools, write a script that generates a packed syntax definition, a parse table, a tree grammar, a pretty-print table, and a parenthesize tool from the syntax definition. Then, for all files with extension .plf in the current working directory, it should parse, implode, pretty-print, and subsequently parse and implode the pretty-printed texts. Finally, it should check that the original abstract syntax trees and those produced from the pretty-printed files are equivalent.

The easiest way to do that, is to add some layout to the aterms using pp-aterm and diff the result of that. You can, for example, store the intermediate results in the following files:

• base.ast
• base.txt (pretty-printed ast)
• base-pretty.ast (parse of base.txt)
• base-pretty.txt (pp of base-pretty.ast)

So, the script should verify that base.ast and base-pretty.ast are equivalent.

Submission

Files

Submit the following files in a zip or tar.gz

• *.sdf: SDF modules
• *.plf: example files
• *.testsuite: parse-unit testsuites
• PLF-pretty.pp: modified pretty-print table
• generate.sh (the script)

Assuming that Stratego/XT is installed in the path, the script should generate:

• PLF.def
• PLF.tbl
• PLF.rtg
• PLF.pp
• PLF.str
• PLF-parenthesize.str

And for each base.plf file in the directory (should be extendable) the following pipeline should be checked: parse, pretty-print, parse, pretty-print.

Email

Send your solution by email to martin@cs.uu.nl. Please include the text pt-submit in the topic of your email (for my email filters). The same day, you will get a short notification that I've received your solution. If you don't get this reply, then please contact me.

Questions

After the lab session you can still send questions to pt@cs.uu.nl or join #stratego at irc.freenode.com.