DRAFT: elpi2html using react

elpi_REPL.ml

@@ -215,7 +215,7 @@ let _ =
   Format.eprintf "@\nTypechecking time: %5.3f@\n%!" type_checking_time;
   Format.eprintf "Determinacy checking time: %5.3f@\n%!" det_checking_time;
   if !print_lprolog then begin
-    API.Pp.program Format.std_formatter prog;
+    API.Pp.program1 Format.std_formatter prog;
     Format.printf "\n\n%% query\n?- ";
     API.Pp.goal Format.std_formatter query;
     exit 0;

src/API.ml

@@ -264,6 +264,9 @@ module Pp = struct
   let program f c =
     let module R = (val !r) in let open R in
     Compiler.pp_program (fun ~pp_ctx ~depth -> Pp.uppterm ~pp_ctx depth [] ~argsdepth:0 [||]) f c
+  let program1 f c =
+    let module R = (val !r) in let open R in
+    Compiler.pp_program1 (fun ~pp_ctx ~depth -> Pp.uppterm ~pp_ctx depth [] ~argsdepth:0 [||]) f c
   let goal f c =
     let module R = (val !r) in let open R in
     Compiler.pp_goal (fun ~pp_ctx ~depth -> Pp.uppterm ~pp_ctx depth [] ~argsdepth:0 [||]) f c

src/API.mli

@@ -385,6 +385,7 @@ module Pp : sig
   val state : Format.formatter -> Data.state -> unit
 
   val program : Format.formatter -> Compile.program -> unit
+  val program1 : Format.formatter -> Compile.program -> unit
   val goal : Format.formatter -> Compile.query -> unit
 
   module Ast : sig

src/compiler/compiler.ml

@@ -2495,6 +2495,131 @@ let pp_program (pp : pp_ctx:pp_ctx -> depth:int -> _) fmt (compiler_state, { Ass
   Format.fprintf fmt "@]"
 ;;
 
+let pp_program1 (pp : pp_ctx:pp_ctx -> depth:int -> Fmt.formatter -> term -> unit) fmt (compiler_state, { Assembled.clauses=cl; signature; symbols }) =
+  let pp_ctx = {
+    uv_names = ref (IntMap.empty, 0);
+    table = SymbolMap.compile symbols;
+  } in
+
+  let cnt = ref 0 in
+  let get () = incr cnt; !cnt in
+
+  let pp_const ~depth t = Format.asprintf "%a" (pp ~depth ~pp_ctx) t in
+
+  let pp_clause_loc (cl:clause) = Format.(asprintf "%a" (pp_print_option Loc.pp) cl.loc) in
+
+  let module JSON = struct 
+    type j = Trace_ppx_runtime.Runtime.j (*= J : (F.formatter -> 'a -> unit) * 'a -> j*)
+    module JSON = Trace_ppx_runtime.Runtime.JSON
+    open JSON 
+
+    let pp_id_cnt id cnt : j = JSON.( J(pp_d, ["id", (J(pp_s, id):j); "cnt", J(pp_d, cnt)]))
+
+    let rec pp_main fmt (l: (string option * constant * clause) list) : unit =
+      Format.fprintf fmt "@[<hov 2>%a@]" pp_d ["clauses", J(pp_a, List.map (pp_card ~depth:0) l)]
+
+    and pp_card ~depth (graft,pname,cl:string option * constant * clause) : j =
+      J(pp_d, [
+        ("id", J (pp_s, "card"));
+        ("predicate", J (pp_s, pp_const ~depth (Const pname)));
+        ("title", J (pp_s, pp_clause_loc cl));
+        ("cnt", J (pp_clause ~depth, (pname,cl)));
+      ])
+
+    and pp_names ~map ~depth names =
+      let old = List.map (fun k -> k, C.Map.find_opt k map) names in
+      let clean map2 = List.fold_left (fun map (v,id) -> match id with None -> map | Some e -> C.Map.add v e map) map old in
+      clean, List.fold_left_map (fun (map:'a C.Map.t) (n:constant) -> 
+        let id = get () in
+        let m = C.Map.add n id map in
+        m, pp_id_cnt "var" ["name", J(pp_s, pp_const ~depth (Const n)); "varId", J(pp_i, id) ]) map names 
+
+    and is_infix ~depth c =
+      let s = (Format.asprintf "%a" (pp ~depth ~pp_ctx) (Const c)) in
+      let is_math c = List.mem c ['<';'>';'='] in
+      List.exists (fun prefix -> String.starts_with ~prefix s) [";";"=";"<";">";"&";"*";"/";"+";"-";"^"] || 
+        (String.length s > 2 && is_math s.[1] && is_math s.[2]) ||
+          (String.length s > 1 && is_math s.[1]) || s = "is"
+
+    and is_infixb = function
+      | Eq | Impl | ImplBang | RImpl | And -> true
+      | Pi | Sigma | Cut | Match | Findall | Delay | Host _ -> false
+
+    and builtin2str = Data.Term.show_builtin_predicate (fun ?table x -> "TODO")
+
+    and pp_atom ~map ~depth (tm:term) : 'a C.Map.t * j =
+      let pp_id x y = (x,(J(pp_s, y):j)) in
+      let pp_b x y = (x,(J(pp_b, y):j)) in
+      let rec grab_list = function
+        | Cons (x,xs) -> let xs, b = grab_list xs in (x::xs), b
+        | Nil -> [], None
+        | x -> [], Some x
+      in
+      match tm with
+      | Discard -> map, J(pp_d, [pp_id "id" "discard"])
+      | Builtin (b, []) ->
+          map, J(pp_d, ["id", J(pp_s,"const"); "cnt", J(pp_s, builtin2str b)])
+      | Builtin (b, bo) ->
+          let map, cnt = pp_atoms ~map ~depth bo in
+          let cnt : j = J(pp_a, J(pp_d, ["id", J(pp_s,"const"); "cnt", J(pp_s, builtin2str b)]) :: cnt) in
+          map, J(pp_d, [pp_id "id" "app"; pp_b "is_infix" (is_infixb b); "cnt", cnt])
+      | Cons _ -> 
+          let l, b = grab_list tm in
+          let map, cnt = pp_atoms ~map ~depth l in
+          let cnt : j = J(pp_a, J(pp_d, ["id", J(pp_s,"const"); "cnt", J(pp_s, "::")]) :: cnt) in
+          map, J(pp_d, [pp_id "id" "app"; pp_b "is_infix" true; "cnt", cnt])
+      | Nil -> map, J(pp_d, ["id", J(pp_s,"const"); "cnt", J(pp_s, "[]")])
+      | Const x when x < 0 -> map, J(pp_d, ["id", J(pp_s,"const"); "cnt", J(pp_s, pp_const ~depth tm)])
+      | Const x -> map, pp_id_cnt "var" ["name", J(pp_s, pp_const ~depth tm); "varId", J(pp_i, C.Map.find x map) ]
+      | App (x, hd, tl) -> 
+          let map, cnt = pp_atoms ~map ~depth (Const x :: hd ::tl) in
+          let cnt : j = J(pp_a, cnt) in
+          map, J(pp_d, [pp_id "id" "app"; pp_b "is_infix" (is_infix ~depth x); "cnt", cnt])
+      | Lam t ->
+          let clean, (map, names) = pp_names ~map ~depth [depth] in
+          let map, body = pp_atom ~map ~depth:(depth+1) t in
+          clean map, pp_id_cnt "quantification" 
+          [
+            "type", J (pp_s, "binder");
+            "names", J(pp_a, names);
+            "body", J(pp_a, [body])
+          ]
+      | CData c -> 
+        let s = Format.asprintf "%a" (pp ~pp_ctx ~depth) tm in
+        let s = Re.Str.(global_replace (regexp "\\(\194\\|\171\\|\187\\)") "") s in
+        map, J(pp_d, ["id", J(pp_s, "string"); "cnt", J(pp_s, s)])
+      | AppArg (hd, laaa) ->
+          let map = if C.Map.mem hd map then map else C.Map.add hd (get ()) map in
+          map, J(pp_d, ["id", J(pp_s,"var"); "cnt", J(pp_d, ["name", J(pp_s, pp_const ~depth (AppArg (hd, []))); "varId", J(pp_i, C.Map.find hd map)])])
+      | Arg (hd, _) -> 
+          let map = if C.Map.mem hd map then map else C.Map.add hd (get ()) map in
+          map, J(pp_d, ["id", J(pp_s,"var"); "cnt", J(pp_d, ["name", J(pp_s, pp_const ~depth (AppArg (hd, []))); "varId", J(pp_i, C.Map.find hd map)])])
+
+      | UVar (_, _) ->  anomaly "pp_atom: UVar assert false"
+      | AppUVar (_, _) -> anomaly "pp_atom: AppUVar assert false"
+
+    and pp_atoms ~map ~depth l : 'a C.Map.t * j list = 
+      let map, args = List.fold_left_map (fun a e -> pp_atom ~depth ~map:a e) map l in 
+      map, args
+
+    and pp_clause ~depth fmt (pname, cl) : unit =
+      let pp_hyps ~map ~depth l : 'a C.Map.t * j = 
+        match l with
+        | [] -> map, J (pp_a, [])
+        | [x] -> pp_atom ~map ~depth x
+        | l -> pp_atom ~map ~depth (Builtin (And, l))
+      in
+      let map, args = pp_atom ~map:C.Map.empty ~depth (match cl.args with [] -> Const pname | x::xs -> mkApp pname x xs) in
+      let map, hyps = pp_hyps ~map ~depth cl.hyps in
+      (pp_d fmt [
+        ("id", J (pp_s, "clause"));
+        ("cnt", J (pp_d, [ "hyp", hyps; "args", args ]));
+      ]);;
+
+  end in
+  let clauses = handle_clause_graftin cl in
+  JSON.pp_main fmt clauses ;;
+
 let pp_goal pp fmt {  WithMain.compiler_state; initial_goal; symbols } =
   let pp_ctx = {
     uv_names = ref (IntMap.empty, 0);

src/compiler/compiler.mli

@@ -53,6 +53,7 @@ val optimize_query : query -> executable
 val relocate_closed_term : from:symbol_table -> to_:program -> term -> (term, string) Stdlib.Result.t
 
 val pp_program : (pp_ctx:pp_ctx -> depth:int -> Format.formatter -> term -> unit) -> Format.formatter -> program -> unit
+val pp_program1 : (pp_ctx:pp_ctx -> depth:int -> Format.formatter -> term -> unit) -> Format.formatter -> program -> unit
 val pp_goal : (pp_ctx:pp_ctx -> depth:int -> Format.formatter -> term -> unit) -> Format.formatter -> query -> unit
 
 val elpi_language : Compiler_data.Scope.language

trace/runtime/runtime.ml

@@ -190,6 +190,7 @@ let exit ~runtime_id k tailcall e time =
   end
 
 (* Json *)
+module JSON = struct
 let pp_s fmt s =
   Format.fprintf fmt "%S" s
 
@@ -199,6 +200,9 @@ let pp_i fmt i =
 let pp_f fmt f =
   Format.fprintf fmt "%f" f
 
+let pp_b fmt f = 
+  Format.fprintf fmt "%b" f
+
 let pp_kv fmt = function
   | k, J(pp_v, v) -> F.fprintf fmt "%a : %a" pp_s k pp_v v
 
@@ -210,12 +214,12 @@ let rec pp_comma_l fmt pp = function
   | x :: xs -> F.fprintf fmt ","; pp fmt x; pp_comma_l fmt pp xs
 
 let pp_a fmt (l : j list) =
-  F.fprintf fmt "[";
+  F.fprintf fmt "@[<hov 2>[";
   begin match l with
   | [] -> ()
   | x :: l -> pp_j fmt x; pp_comma_l fmt pp_j l
   end;
-  F.fprintf fmt "]"
+  F.fprintf fmt "]@]"
 
 
 module JSON_STRING_ENCODING = struct
@@ -306,6 +310,7 @@ let print_json fmt  = (); fun { runtime_id; goal_id; kind; name; step; payload }
   ];
   F.pp_print_newline fmt ();
   F.pp_print_flush fmt ()
+end
 
 (* TTY *)
 let tty_formatter_maxcols = ref 80
@@ -322,16 +327,16 @@ let pplist ppelem f l =
 let print_tty fmt = (); fun { runtime_id; goal_id; kind; name; step; payload } ->
   match kind with
   | Start ->
-    F.fprintf fmt "%s %d {{{@[<hov1> %a@]\n%!" name step (pplist pp_j) payload
+    F.fprintf fmt "%s %d {{{@[<hov1> %a@]\n%!" name step (pplist JSON.pp_j) payload
   | Stop { cause; time } ->
     F.fprintf fmt "}}} %s  (%.3fs)\n%!" cause time
   | Info ->
     let () = F.fprintf fmt "  @[<hov 2>rid:%d step:%d gid:%d %s =@ " runtime_id step goal_id name in
     let () = match payload with
       | [] -> ()
       | j :: payload ->
-        let () = F.fprintf fmt "%a@," pp_j j in
-        F.fprintf fmt "@[<hov 0>%a@]" (pplist pp_j) payload in
+        let () = F.fprintf fmt "%a@," JSON.pp_j j in
+        F.fprintf fmt "@[<hov 0>%a@]" (pplist JSON.pp_j) payload in
     F.fprintf fmt "@]\n%!"
 
 let () = printer := print_tty F.err_formatter
@@ -344,7 +349,7 @@ let set_trace_output format formatter =
       F.pp_set_margin formatter !tty_formatter_maxcols;
       printer := print_tty formatter
   | JSON ->
-      printer := print_json formatter
+      printer := JSON.print_json formatter
 
 let output_file = ref None
 

trace/runtime/runtime.mli

@@ -27,3 +27,25 @@ val usage: string
 (* prints here *)
 type trace_format = TTY | JSON
 val set_trace_output : trace_format -> Format.formatter -> unit
+
+module JSON : sig
+  val pp_s : Format.formatter -> string -> unit
+  val pp_b : Format.formatter -> bool -> unit
+  val pp_i : Format.formatter -> int -> unit
+  val pp_f : Format.formatter -> float -> unit
+  val pp_kv : Format.formatter -> string * j -> unit
+  val pp_j : Format.formatter -> j -> unit
+
+  val pp_comma_l :
+    Format.formatter ->
+    (Format.formatter -> 'a -> unit) ->
+    'a list ->
+    unit
+
+  val pp_a : Format.formatter -> j list -> unit
+  val pp_d : Format.formatter -> (string * j) list -> unit
+
+  module JSON_STRING_ENCODING : sig
+    val write_string_body : Buffer.t -> string -> unit
+  end
+end