Stratego -- Strategies for Program Transformation

A format checker is a strategy that checks the well-formedness of an term.
Format checkers can check more properties than can just be described using signatures. For example, checking that a term is normalized in a certain way.

Format checkers can be defined easily using RecursivePattern. Consider the following signature of a simple expression language:

signature sorts Exp constructors Var : String -> Exp Add : Exp * Exp -> Exp Mul : Exp * Exp -> Exp

The following format checking strategy `Exp`

checks that
a term is a well-formed `Exp`

term.

strategies Exp = Var(is-string) + Add(Exp, Exp) + Mul(Exp, Exp)

It is also possible to check more strict properties such as being an additive expression (if that is a term), i.e., an expression consisting of additions on top and multiplications within. No addition should occur as a sub-term of a multiplication. The following strategy definition is a more concise way of expressing this property:

AdditiveExp = rec a(Add(a, a) + rec m(Mul(m, m) + Var(is-string)))

Note that the use of the `rec`

RecursionOperator makes the definition
more concise (without it an additional strategy definition would be needed).

-- EelcoVisser - 28 Nov 2001

The compile-time generation of a WellFormednessChecker^{?} for a given term or sort is suggested as a possible upcoming feature of Stratego.

-- MartinBravenboer - 08 Dec 2001

The generation of a FormatChecker from an AlgebraicSignature is supported in StrategoRelease09 . The tool sig2fc^{?} can be used to generate a FormatChecker for a valid AlgebraicSignature .

-- MartinBravenboer - 14 Jan 2003