ENH: convert syntax tree to JSON

- API: add command-line option `--json-ast`

Author: johnyf

src/backend/prep.ml

@@ -897,6 +897,21 @@ let expand_enabled_cdot ob
     print_obl_and_msg ob (
         "Proof obligation before `Expr.Action.expand_action_operators`:\n");
     let expr = expr_from_obl ob in
+    (* Print syntax tree if requested. *)
+    if !Params.dumps_json_ast then begin
+        let visitor =
+            object (self: 'self)
+            inherit [unit] Expr.Visit.json_map
+            end in
+        let cx = ((), Deque.empty) in
+        let json_str = visitor#expr cx expr in
+        print_string (
+            "------------\n\
+            JSON output:\n\n" ^
+            json_str ^
+            "\n\n========\n\n")
+        end;
+    (* expand action operators *)
     let expr: Expr.T.expr = begin
         if expand_enabled || expand_cdot then begin
             let cx = Deque.empty in

src/expr.mli

@@ -308,6 +308,42 @@ module Visit : sig
       method rename : ctx -> hyp -> Util.hint -> hyp * Util.hint
       method renames : ctx -> hyp list -> Util.hint list -> hyp list * Util.hint list
   end
+
+  val hyps_of_bounds: bounds -> hyp list
+
+  class virtual ['s] json_map: object
+      method expr:
+          's scx -> expr -> string
+      method sel:
+          's scx -> sel -> string
+      method sequent:
+          's scx -> sequent -> string
+      method defn:
+          's scx -> defn -> string
+      method defns:
+          's scx -> defn list ->
+              's scx * string
+      method bounds: 's scx -> bounds ->
+          's scx * string
+      method bound: 's scx -> bound ->
+          's scx * string
+      method exspec:
+          's scx -> exspec -> string
+      method instance:
+          's scx -> instance -> string
+      method hyp:
+          's scx -> hyp -> 's scx * string
+      method hyps:
+          's scx -> hyp Deque.dq ->
+              's scx * string
+      method adj:
+          's scx -> hyp -> 's scx
+      method adjs:
+          's scx -> hyp list -> 's scx
+  end
+  val format_parameter:
+      Util.hint * shape -> string
+  val json_of_ast: ctx -> expr -> string
 end;;
 
 module Eq : sig