How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

Question

Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages".

On PDF page 28 you'll see an OCaml implementation of eval1. Which I assumed is like a recursive single-step evaluator?

See the directory Dots' first tutorial / project D code. As you see I have a fully functioning grammar at least of the syntax. Now I'm wondering if we convert the pegged ParseTree into some other internal format? Or do we try to operate on ParseTree's themselves and then finally pretty print a result?

For example, one evaluation rule is E-BetaBoolT: if true then s:Term else t:Term |-> s, where here |-> is the evalutation relation.

So if for example I decided to convert true to a bool and throw away the pegged ParseTree, then it seems like it would 1) harder to implement because you have to write a 1-1 correspondence of classes with your grammar rules at least. And 2) it's going to be full of bugs and error prone, thus making your math kernel buggy which can't happen as is enforced in practice.

On the other hand manipulating someone else's ParseTree seems tacky. Though, it seems like an efficient enough structure. So I'm wondering, what would be the advantages of converting to a second type or layer of software? Would the ParseTree method be significantly slower?

   NumbersAndBooleans:
      Term <- IfThenElse(Term) / Successor(Value) / 
              Predecessor(Value) / IsZero(Value) / Value
      IfThenElse(T) < "if" T "then" T "else" T
      Successor(V) < "succ" V
      Predecessor(V) < "pred" V    
      IsZero(V) < "iszero" V     
      Value <- True / False / Zero
      True <- "true"
      False <- "false"
      Zero <- "0"

There is my grammar, and I am able to produce parse trees from it. But I don't know what to do with the parse trees to "evaluate" them.

How I'm currently implementing if-then-else evaluator:

// Inside class IfThenElse that inherits from Term abstract class
override Value evaluate() const {
      if (if_cond.evaluate().is_true)
      {
         // Pierce book: if true then t2 else t3 -> t2 (E-BOOLBETAT)
         return then_part.evaluate();
      }
      else {
         // Pierce book: if false then t2 else t3 -> t3 (E-BOOLBETAF)
         return else_part.evaluate();
      }
   }

Answer 1

Faithfully implementing textbook small-step semantics is not necessarily the best way to implement an interpreter. Large step semantics is often more intuitive and direct, as it amounts to a straightforward recursive fold of the syntax tree.

As for organizing datatypes, it is often a good idea to evaluate (pre-processed) syntax trees to values, which are defined as a separate datatype. For example, a common technique for evaluating λ-abstractions is to form closures (terms together with their local runtime environment), and those are not expressible in the original syntax.

The Programming languages zoo has simple examples of techniques:

• Small-step semantics for a functional language miniml evaluates syntax trees back to syntax trees, see eval.ml. (There is also a separate compiler.)

• Large-step semantics for a functional language minihaskell evaluates syntax trees to a value datatype, see interpret.ml

For more advanced techniques I highly recommend Andras Kovacs's work:

• smalltt demonstrating techniques for high-performance elaboration with dependent types.
• The elaboration zoo includes a series of Haskell implementations for elaborating dependently typed languages. There are accompanying videos.