Leandro Facchinetti

Playing the Game with PLT Redex

We covered the basics of PLT Redex without going into programming-language theory. Instead, we used it to model a game of Peg Solitaire. We used terms to represent elements in the game: boards, pegs, spaces and paddings. We used patterns to match those terms as the basis of several definitions:

With these definitions in place, we used PLT Redex visualization tools to play Peg Solitaire. We then explored other features, including extra conditions for a clause to contribute to the output, unquoting, holes, testing and typesetting. We also discussed some limitations, including debugging, performance, and more advanced pattern matching; the lack of metaparameters, parallel reduction and higher-order metafunctions; how definition extensions do not reinterpret dependent definitions; how it can be difficult to customize typeset figures; and how PLT Redex is not appropriate for mechanized formal proofs.


You now know enough to read the more advanced material on PLT Redex, and understanding the tool will help you read papers in programming-language theory.

Acknowledgments

Thanks to the following people for providing feedback on a preliminary version of this article: P.C. Shyamshankar, Scott Moore, Allan Vital and Rafael da Silva Almeida.