Appendix 3Parsing and printing of formulas
Although parsing and printing support is vital to making the programs in this book usable for experimentation, we have deferred a detailed discussion of how parsing and printing are done to the present appendix. This is partly because the material is fairly unexciting and rather peripheral to the main concerns of the book, and partly because, while first used in the propositional logic chapter, it actually covers full first-order logic and so doesn’t clearly fit at any point in the otherwise systematic sequence.
General parsing functions
We often need to parse infix operators of various kinds, e.g. the logical connectives like ==> and the arithmetic operators like +. For most of these we adopt a ...