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.