Building a syntax tree

The Part 2 parser only checked a formula’s syntax. Give each nonterminal one extra argument, and the same rules build the tree in that schema:

atom(F, T, {"type": "var", "name": C})      :- char(F, C), prop_var(C), T = F + 1.
conj(F, T, {"type": "and", "args": [L, R]}) :- conj(F, M, L), char(M, "&"), lit(M + 1, T, R).

Parsing p & q now yields the tree itself:

{"type": "and", "args": [{"type": "var", "name": "p"}, {"type": "var", "name": "q"}]}
Nested objects and arrays: exactly JSON. The value type lets a rule assemble structured data and pass it along. Carried all the way to a theorem verdict, this is examples/parse-to-cnf.