WebHome
Education Page
Description
Schedule
Slides
Assignments

Center
Master Program
Assignment Program Representation

Pt03
The following are examples of predicate logic formulae:

<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 consisting of modules PLF and PLID that
describe predicate logic formulae such that the abstract syntax trees
which it generates correspond to the terms generated by the following
signature:

<verbatim>
module PLF
imports PLID
signature
  constructors
    Prop   : Id -> Form
    Pred   : Id * List(Form) -> Form
    Not    : Form -> Form
    And    : Form * Form -> Form
    Or     : Form * Form -> Form
    Equiv  : Form * Form -> Form
    ForAll : Id * Form -> Form
    Exists : Id * Form -> Form
</verbatim>

Thus, the syntax definition should parse the formulae above 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) Signature

Generate a signature from the syntax definition. Adapt the syntax
definition such that the generated module PLF.str exactly matches the
signature above.
   
------+++ (C) Pretty-print tables

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.

------+++ (D) Script

Using the Stratego/XT tools, write a script that generates a complete
syntax definition, a parse table, a signature, and a pretty-print
table 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 sample formulae; write some more examples.

------++ Submission

Submit the following files

   * PLF.sdf
   * PLID.sdf
   * *.plf
   * PLF-pretty.pp
   * generate.sh (the script)

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

   * PLF.def
   * PLF.tbl
   * PLF.str (equivalent to the one above)
   * PLID.str

And for each base.plf file in the directory (should be extendable) the
following files

   * base.asfix
   * base.ast
   * base.txt
   * base.abox
   * base-pretty.txt
   * base-pretty.ast

The script should verify that base.ast and base-pretty.ast are equivalent.