Leandro Facchinetti

Playing the Game with PLT Redex

From all the PLT Redex forms for manipulating with terms, we begin with the metafunction because it is the most familiar—it is just a function on terms. We define a metafunction with the define-metafunction form including patterns that match the input terms, and templates to compute the output terms:

(define-metafunction <language>
  <contract>
  [(<metafunction> <pattern> ...) <template>]
  ...)

A metafunction is similar to define/match in that it compares the inputs to patterns and executes the first clause that matches. More generally, it is similar to forms for multi-way conditionals, for example, case and cond.

When we introduced patterns, we noted that they are to terms as regular expressions are to strings, and we used the redex-match? form to recognize terms the same way we can use regular expressions to match strings. Continuing that analogy, a metafunction is similar to a search-and-replace with regular expressions including capture groups.

In programming languages, metafunctions are the small utilities, for example, substituting variables for their values (a metafunction generally notated as program-fragment[variable\value]), and evaluating primitive operators (a metafunction generally named δ).


We define a metafunction to invert a position:

metafunctions.rkt

#lang racket
(require redex "terms.rkt" "languages.rkt")

(define-metafunction peg-solitaire
  invert/position : position -> position
  [(invert/position peg) ]
  [(invert/position space) ]
  [(invert/position padding) padding])

In the listing above, we define the invert/position metafunction for the peg-solitaire language. Its input and output are positions. The invert/position metafuction compares the input to each of the patterns in turn: peg, space, and padding. The first pattern that matches determines the metafunction output: , , and ·, respectively. The last clause exemplifies how a name in the pattern (padding) is available in the template.

We use a metafunction by applying it on terms:

(test-equal (term (invert/position ))
            (term ))
(test-equal (term (invert/position ))
            (term ))
(test-equal (term (invert/position ·))
            (term ·))

We can call a metafunction from any place in which a term might appear, including the definition of another metafunction. To illustrate this, consider the following metafunction that inverts a whole board by calling invert/position on each position:

(define-metafunction peg-solitaire
  invert/board : board -> board
  [(invert/board ([position ...] ...))
   ([(invert/position position) ...] ...)])

The invert/board metafunction matches its input to the pattern ([position ...] ...), which represents boards. Its output is the result of calling invert/position on each position: the ellipses (...) after the metafunction call mean “map over the positions with the metafunction invert/position.” The following is an example of calling the invert/board metafunction with the initial-board:

(test-equal (term (invert/board initial-board))
            (term ((· ·    · ·)
                   (· ·    · ·)
                   (      )
                   (      )
                   (      )
                   (· ·    · ·)
                   (· ·    · ·))))

We defined two metafunctions in this section only for illustration—we do not use them to play the game. But the digression is over, because in the next section we cover reduction relations, which we use to model Peg Solitaire moves.