Assignment Program Representation

%TOC%

------++ 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.

<verbatim>
not (exists a : Man(a) /\ Woman(a))
</verbatim>

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

For documentation, use the part on [[%MANUAL%/tutorial-xt.html][The XT Transformation Tools]] in the [[%MANUAL%][Stratego/XT Manual]]. The [[%MANUAL%/tool-ref.html][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:

<verbatim>
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>
</verbatim>

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

<verbatim>
Not(
  Exists("a"
  , And(
      Pred("Man", [Prop("a")])
    , Pred("Woman", [Prop("a")])
    )
  )
)
</verbatim>

<verbatim>
Forall("a"
, Forall("b"
  , Equiv(
      Not(And(Prop("a"),Prop("b")))
    , Or(Not(Prop("a")),Not(Prop("b")))
    )
  )
)
</verbatim>

------++ (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:

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

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.

<verbatim>
$ 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
</verbatim>

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

<verbatim>
$ 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"))))
</verbatim>

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 [[irc://irc.freenode.com/#stratego][#stratego]] at
=irc.freenode.com=.