Recursive Pattern
Stratego -- Strategies for Program Transformation
Recursive patterns is a
Stratego idiom for checking the format of terms by means of recursion and congruences. This idiom is useful for checking the conformance of terms to some signature. Moreover it can be used to check conformance to some subset of terms generated by a signature. For example, checking that some
abstract syntax tree corresponds to the desugared subset of the
abstract syntax.
Recursive patterns where first described in the
Strategic pattern matching paper.
A recursive pattern has the following format
strategies
LambdaExp =
rec x(
Var(is-string)
+ Lambda(Var(is-string), x)
+ App(x, x)
)
This recursive pattern assumes a signature that defines the constructors Var/1, Lambda/2 and App/2. For example as follows:
signature
sorts Lexp
constructors
Var : String -> Var
Lambda : Var * Lexp -> Lexp
App : Lexp * Lexp -> Lexp
: Var > Lexp
Stratego.RecursivePattern moved from Stratego.RecursivePatterns on 15 May 2003 - 13:16 by MartinBravenboer -
put it back