WhileyRewriteLanguage

WyRL is a domain specific rewrite language and code generator which has been custom developed for use within the Whiley Compiler. Specifically, WyRL is used to generate the Automated Theorem Prover used within Whiley.

Building

To build WyRL, you can run ant from the command-line:

> ant

Buildfile: WhileyRewriteLanguage/build.xml

compile-wyrl:
    [javac] Compiling 1 source file
     [wyrl] Compiling 0 wyrl file(s)
    [javac] Compiling 5 source files

build:
    [mkdir] Created dir: WhileyRewriteLanguage/tmp
      [jar] Building jar: WhileyRewriteLanguage/lib/wyrl-v0.3.34.jar
   [delete] Deleting directory WhileyRewriteLanguage/tmp
     [echo] =============================================
     [echo] BUILT: lib/wyrl-v0.3.34.jar
     [echo] =============================================

BUILD SUCCESSFUL
Total time: 3 seconds

Examples

There are several examples provided in the examples/ directory:

• Boolean Logic Simplifier. This simplifies formulae written in propositional logic. For example, it would simplify X||(Y||!Y) to X. For more, see here.

• Arithmetic Simplifier. This simplifies simple arithmetic expressions. For example, it would simplify y-y+(2*x)+(3*x) to 5*x. For more, see here.

• Recursive Types Simplifier. This simplifies types involving unions, intersections and negations and which may also be recursive. For example, it would simplify (int|!int)&int to int. For more, see here.

• Transitive Closure. This applies transitive closure to strict inequalities. For example, it would rewrite x < y,y < z to x < y, y < z, x < z. For more, see here.

• Quantifier Instantiater. This instantiates and simplifies boolean expressions involving quantifiers. For example, it would simplify fn(x,y) && forall X.!fn(X,X) to False. For more, see here.