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
  // subsorts Var > Lexp
  constructors
    Var    : String -> Var
    Lambda : Var * Lexp -> Lexp
    App    : Lexp * Lexp -> Lexp

Revision: r1.3 - 04 Jul 2003 - 07:25 - MartinBravenboer
Stratego > RecursivePattern
Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback