Improve output

lib/rethfl.ml

@@ -49,15 +49,15 @@ let report_times () =
 
 let main file =
   let psi, _ = Syntax.parse_file file in
-  Log.app begin fun m -> m ~header:"Input" "%a"
+  Log.info begin fun m -> m ~header:"Input" "%a"
     Print.(hflz_hes simple_ty_) psi
   end;
   let psi = Syntax.Trans.Simplify.hflz_hes psi in
-  Log.app begin fun m -> m ~header:"Simplified" "%a"
+  Log.info begin fun m -> m ~header:"Simplified" "%a"
     Print.(hflz_hes simple_ty_) psi
   end;
   let psi = Syntax.Trans.Peephole.hflz_hes psi in
-  Log.app begin fun m -> m ~header:"Peephole" "%a"
+  Log.info begin fun m -> m ~header:"Peephole" "%a"
     Print.(hflz_hes simple_ty_) psi
   end;
   let psi, top = Syntax.Trans.Preprocess.main psi in
@@ -69,7 +69,7 @@ let main file =
       begin
       (* remove disjunction *)
         let psi = Syntax.Trans.RemoveDisjunction.f psi top in
-        Log.app begin fun m -> m ~header:"RemoveDisj" "%a"
+        Log.info begin fun m -> m ~header:"RemoveDisj" "%a"
           Print.(hflz_hes simple_ty_) psi
         end;
         psi

lib/typing/chc.ml

@@ -3,14 +3,20 @@ open Rtype
 
 type ('head, 'body) chc = {head: 'head; body: 'body}
 
+let pp_chc ppf chc =
+  (* Maybe head <= body is better ?*)
+  Fmt.pf ppf "@[<2>%a =>@ %a@]" pp_refinement chc.body pp_refinement chc.head
+
 let print_chc chc = 
-  print_refinement chc.body;
-  Printf.printf " => ";
-  print_refinement chc.head
+  pp_chc Fmt.stdout chc;
+  Fmt.flush Fmt.stdout ()
+
+let pp_constraits ppf chcs =
+    Fmt.pf ppf "@[<v>%a@,@]" (Fmt.list pp_chc) chcs
 
-let rec print_constraints = function
-  | [] -> ()
-  | x::xs -> print_chc x; print_newline(); print_constraints xs
+let print_constraints chcs =
+  pp_constraits Fmt.stdout chcs;
+  Fmt.flush Fmt.stdout ()
 
 (* find x=e in the toplevel of CHC's body, and then replace it by True *)
 let rec find_and_cut_substs rt ids = match rt with 

lib/typing/chc_solver.ml

@@ -7,6 +7,10 @@ module Unix = Core_unix
 
 type solver = [`Spacer | `Hoice | `Fptprove | `Eldarica | `Liu]
 
+let log_src = Logs.Src.create ~doc:"Log for the CHC solver module" "CHC Solver"
+module Log = (val Logs.src_log log_src)
+
+
 let fptprove_path_env = "fptprove"
 
 type unsat_proof_node =
@@ -267,7 +271,7 @@ let parse_model model =
       | (name, args, x)::xs -> (name, args, simplify_def x) :: inner xs
     in inner defs
   in
-  print_string model;
+  Log.info (fun m -> m ~header: "Model" "%s" model);
   match Sexplib.Sexp.parse model with
   | Done(model, _) -> begin
     match model with

lib/typing/rhflz.ml

@@ -16,57 +16,29 @@ type t =
   | Arith  of Arith.t
   | Pred   of Formula.pred * Arith.t list
 
-let rec print_formula = function
-  | Bool x when x -> Printf.printf "tt"
-  | Bool _ -> Printf.printf "ff"
-  | Var x -> Printf.printf "%s" (Id.to_string x)
-  | Or (x, y, _, _) -> 
-    Printf.printf "(";
-    print_formula x;
-    Printf.printf " || ";
-    print_formula y;
-    Printf.printf ")";
-  | And (x, y, tx, ty) -> 
-    Printf.printf "(";
-    print_formula x;
-    print_string ":";
-    print_template tx;
-    Printf.printf " && ";
-    print_formula y;
-    print_string ":";
-    print_template ty;
-    Printf.printf ")";
-  | Abs (x, y) -> 
-    Printf.printf "(";
-    Printf.printf "\\";
-    print_rtype x.ty;
-    Printf.printf ".";
-    print_formula y;
-    Printf.printf ")"
-  | Forall (x, y, _) -> 
-    Printf.printf "(";
-    Printf.printf "∀";
-    print_rtype x.ty;
-    Printf.printf ".";
-    print_formula y;
-    Printf.printf ")"
-  | App (x, y, template) -> 
-    Printf.printf "(";
-    print_formula x;
-    Printf.printf " ";
-    print_formula y;
-    Printf.printf ")";
-  | Arith x ->
-    Print.arith Fmt.stdout x;
-    Fmt.flush Fmt.stdout () 
-  | Pred (x,[f1; f2]) -> 
-    Print.arith Fmt.stdout f1;
-    Print.pred Fmt.stdout x;
-    Print.arith Fmt.stdout f2;
-    Fmt.flush Fmt.stdout () ;
-  | Pred (x,_) -> 
-    Print.pred Fmt.stdout x;
-    Fmt.flush Fmt.stdout () 
+let rec pp_formula ppf = function
+  | Bool x when x -> Fmt.string ppf "tt"
+  | Bool _ -> Fmt.string ppf "ff"
+  | Var x -> Fmt.string ppf @@ Id.to_string x
+  | Or (x, y, _, _) ->
+    Fmt.pf ppf "(@[<hov 1>%a@ || %a@])" pp_formula x pp_formula y
+  | And (x, y, tx, ty) ->
+    Fmt.pf ppf "(@[<hov 1>%a:%a@ && %a:%a@])"
+      pp_formula x pp_template tx pp_formula y pp_template ty
+  | Abs (x, y) ->
+    Fmt.pf ppf "(@[<1>\\%a.@,%a@])" pp_rtype x.ty pp_formula y
+  | Forall (x, y, _) ->
+    Fmt.pf ppf "(@[<1>∀%a.@,%a@])" pp_rtype x.ty pp_formula y
+  | App (x, y, _) ->
+    Fmt.pf ppf "(@[<1>%a  %a@])" pp_formula x pp_formula y
+  | Arith x -> Fmt.pf ppf "(%a)" Print.arith x
+  | Pred (x,[f1; f2]) ->
+    Fmt.pf ppf "(%a%a%a)" Print.arith f1 Print.pred x Print.arith f2
+  | Pred (x,_) -> Print.pred ppf x
+
+let print_formula f =
+  pp_formula Fmt.stdout f;
+  Fmt.flush Fmt.stdout ()
 
 let rec is_simple p = match p with
   | And(x, y, _, _) | Or(x, y, _, _) -> (is_simple x && is_simple y)