Why has this taken so long, even though the new code is still unproven (i.e. the proof hasn't progressed beyond chapter 4)?
The Visitor pattern turned out to be quite a nut to crack. Bob has used templated
accept() methods. This means a concrete visitor can choose to return whatever type it needs -- the example AST printer returns a string, but later in the book, other types might come in handy. Unfortunately, in Ada generic functions cannot be overloaded, so I couldn't copy this approach. I tried to code around this restriction only to discover I didn't really understand the Visitor pattern (which I hadn't encountered before).
After some searching, I found an Ada implementation by Matthew Heaney. He, too, uses generics, but in a different way. The gist is that instead of returning a value, the Visitor type ("object") stores the data internally -- this is not a problem because the abstract visitor type is extended (subclassed) anyway -- and can then be queried by the caller. There seems to be a bit more boilerplate code, but most of this is written by Lox's source code generator, so this is no real problem.
The second nut stems from a shortcoming in current prover technology: Gnatprove cannot deal with aliasing (i.e. writing to one variable changes the value of another), and therefore access variables (pointers) are not allowed in SPARK. This is not as large a problem as it may seem since Ada programmers use access variables very sparingly. But the abstract syntax tree has nodes containing other nodes, so some kind of reference is needed.
I have decided to store all Exprs in a Formal_Indefinite_Vector (a container supplied by the standard library) and refer to them by their index in the vector.
I am quite satisfied with how far lox-spark has come, this is a good way to start the weekend.
What's next? Obviously, the new code needs to be annotated and proven. Also, chapter six has been out for almost two weeks, so there's still more code to be written. I haven't yet decided on where to start, so maybe I'll take advantage of git and do both in parallel.Kein Kommentar