Assignment Program Representation

Pt04
%TOC%

*Note*: You have to do this assignment individually.

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

---++ (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). You should disable the heuristic filters of SGLR in the invocation of =parse-unit= (and later =sglri=). Write some larger tests in separate =.plf= files and include them in the testsuite. We will use these separate files later.

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

---+++ 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).
  
------++ (C) Pretty-print table

Generate a pretty-print table =PLF.pp= for the language. Copy thisgenerated 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).

---+++ 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 following arguments to sdf2parenthesize (besides =-i= and
=-o=):
   * =--lang PLF=
   * =--omod PLF-parenthesize=
   * =-m PLF=

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>
$ rtg2sig -i PLF.rtg -o PLF.str
$ strc -i PLF-parenthesize.str -m io-PLF-parenthesize -Cl stratego-lib
</verbatim>

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

------++ (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. Apply the script to the syntax
definition developed above and to the examples and testsuites you have
defined.

---++ 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. Check that the result of both parses 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.

---+++ Email

Send your solution by email to =martin@cs.uu.nl= at least 15 minutes
before the lecture of Tuesday, i.e. 8:45. Please include the text
=pt-submit= in the topic of your email. 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=.

---++ Additional Resources

   * Overview of the available
   [[http://catamaran.labs.cs.uu.nl/twiki/pt/bin/view/Sdf/SdfDocumentation][documentation]]
   for SDF.

   * [[http://catamaran.labs.cs.uu.nl/dist/stratego/strategoxt-manual-unstable-latest/manual/][Stratego/XT Manual]]
      * [[http://catamaran.labs.cs.uu.nl/dist/stratego/strategoxt-manual-unstable-latest/manual/sdf-unit-testing.html][Unit Testing with parse-unit]]
      * [[http://catamaran.labs.cs.uu.nl/dist/stratego/strategoxt-manual-unstable-latest/manual/format-checking.html][Format Checking with format-check]]
      * [[http://catamaran.labs.cs.uu.nl/dist/stratego/strategoxt-manual-unstable-latest/manual/tool-ref.html][Manual pages of some Programs and Tools]]

   * [[http://www.tldp.org/LDP/abs/html/][Bash Shell Scripting Tutorial]]