From 2f026e261c6a842300070b25240c1790240dfe69 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sat, 14 Dec 2024 10:53:49 +0900 Subject: [PATCH 1/7] add pretty printers for rtype --- lib/typing/rtype.ml | 94 ++++++++++++++++++++------------------------- 1 file changed, 41 insertions(+), 53 deletions(-) diff --git a/lib/typing/rtype.ml b/lib/typing/rtype.ml index 440f166..1b53961 100644 --- a/lib/typing/rtype.ml +++ b/lib/typing/rtype.ml @@ -16,21 +16,16 @@ let generate_top_template args = created := true; (id_top, args) -let rec print_ariths = function - | [] -> () - | [x] -> - Print.arith Fmt.stdout x; - Fmt.flush Fmt.stdout () ; - | x::xs -> - Print.arith Fmt.stdout x; - Fmt.flush Fmt.stdout () ; - print_string ","; - print_ariths xs - -let print_template (id, l) = - Printf.printf "X%d(" id; - print_ariths l; - print_string ")" +let pp_template ppf (id, l) = + let pp_ariths = + let unbreakable_comma ppf () = Fmt.string ppf "," in + Print.list ~sep:unbreakable_comma Print.arith + in + Fmt.pf ppf "X%d(%a)" id pp_ariths l + +let print_template t = + pp_template Fmt.stdout t; + Fmt.flush Fmt.stdout () type rint = | RId of [`Int] Id.t @@ -63,49 +58,42 @@ let rec clone_type_with_new_pred ints = function RArrow(clone_type_with_new_pred ints x, clone_type_with_new_pred ints y) | x -> x -let print_rint = function - | RId x -> - Print.id Fmt.stdout x; - Fmt.flush Fmt.stdout () - | RArith x -> - Print.arith Fmt.stdout x; - Fmt.flush Fmt.stdout () - -let rec print_refinement = function - | RTrue -> Printf.printf "tt" - | RFalse -> Printf.printf "ff" +let pp_rint ppf = function + | RId x -> Print.id ppf x + | RArith x -> Print.arith ppf x + +let print_rint x = + pp_rint Fmt.stdout x; + Fmt.flush Fmt.stdout () + +let rec pp_refinement ppf = function + | RTrue -> Fmt.string ppf "tt" + | RFalse -> Fmt.string ppf "ff" | RPred (x,[f1; f2]) -> - Print.arith Fmt.stdout f1; - Print.pred Fmt.stdout x; - Print.arith Fmt.stdout f2; - Fmt.flush Fmt.stdout () ; - | RPred (x,_) -> - Print.pred Fmt.stdout x; - Fmt.flush Fmt.stdout () ; + Fmt.pf ppf "%a%a%a" Print.arith f1 Print.pred x Print.arith f2 + | RPred (x,_) -> Print.pred ppf x | RAnd(x, y) -> - print_string "("; - print_refinement x; - Printf.printf " /\\ "; - print_refinement y; - print_string ")"; + let pp_v ppf (x, y) = Fmt.pf ppf "%a@ /\\ %a" pp_refinement x pp_refinement y in + Fmt.pf ppf "%a" (Fmt.parens pp_v) (x, y) | ROr(x, y) -> - print_string "("; - print_refinement x; - Printf.printf " \\/ "; - print_refinement y; - print_string ")"; - | RTemplate t -> print_template t - -let rec print_rtype = function - | RBool r -> Printf.printf "*["; print_refinement r; Printf.printf "]" + let pp_v ppf (x, y) = Fmt.pf ppf "%a@ \\/ %a" pp_refinement x pp_refinement y in + Fmt.pf ppf "%a" (Fmt.parens pp_v) (x, y) + | RTemplate t -> pp_template ppf t + +let print_refinement x = + pp_refinement Fmt.stdout x; + Fmt.flush Fmt.stdout () + +let rec pp_rtype ppf = function + | RBool r -> Fmt.pf ppf "*[%a]" pp_refinement r | RArrow(x, y) -> - print_string "("; - print_rtype x; - Printf.printf " -> "; - print_rtype y; - print_string ")"; - | RInt x -> print_rint x; Printf.printf ": int" + let pp_v ppf (x, y) = Fmt.pf ppf "%a ->@ %a" pp_rtype x pp_rtype y in + Fmt.pf ppf "%a" (Fmt.parens pp_v) (x, y) + | RInt x -> Fmt.pf ppf "%a: int" pp_rint x +let print_rtype x = + pp_rtype Fmt.stdout x; + Fmt.flush Fmt.stdout () let rint2arith = function | RId x -> Arith.Var(x) From 192a9650d5f19db5663210899f0b80560ff2adbe Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sat, 14 Dec 2024 12:41:32 +0900 Subject: [PATCH 2/7] add pretty printers for constraints --- lib/typing/chc.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/lib/typing/chc.ml b/lib/typing/chc.ml index 2f33534..8168676 100644 --- a/lib/typing/chc.ml +++ b/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 "@[%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 From b1061f3ea37b3352068ad54ce7241cd2232c58ad Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sat, 14 Dec 2024 15:19:25 +0900 Subject: [PATCH 3/7] add pretty printer for rhflz --- lib/typing/rhflz.ml | 74 ++++++++++++++------------------------------- 1 file changed, 23 insertions(+), 51 deletions(-) diff --git a/lib/typing/rhflz.ml b/lib/typing/rhflz.ml index b3f75b4..5399aeb 100644 --- a/lib/typing/rhflz.ml +++ b/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 "(@[%a@ || %a@])" pp_formula x pp_formula y + | And (x, y, tx, ty) -> + Fmt.pf ppf "(@[%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) From 64eacbfb4d59c2402b56e49af25a17aca428f324 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sun, 15 Dec 2024 11:12:45 +0900 Subject: [PATCH 4/7] logging for rinfer --- lib/typing/rinfer.ml | 140 +++++++++++++++++-------------------------- 1 file changed, 54 insertions(+), 86 deletions(-) diff --git a/lib/typing/rinfer.ml b/lib/typing/rinfer.ml index 34a79c6..b4e4370 100644 --- a/lib/typing/rinfer.ml +++ b/lib/typing/rinfer.ml @@ -7,6 +7,8 @@ open Rethfl_syntax open Chc module Parser = P +let log_src = Logs.Src.create ~doc:"Debug log for refinemnet type inference" "Rinfer" +module Log = (val Logs.src_log log_src) (* timer*) let measure_time f = @@ -170,33 +172,33 @@ let rec infer_formula track formula env m ints = end let infer_rule track (rule: hes_rule) env (chcs: (refinement, refinement) chc list): (refinement, refinement) chc list = - print_newline(); - print_newline(); - print_string "infering new formula: "; - Printf.printf "%s = " rule.var.name; - print_formula rule.body; - print_newline(); - (* infer type of rule.body using env *) - let (t, m) = infer_formula track rule.body env chcs [] in - (* generate constraint that inferred type `t` is subtype of var type *) - let m = subtype t rule.var.ty m in - print_string "[Result]\n"; - print_constraints m; - m - -let rec infer_hes ?(track=false) (hes: hes) env (accum_constraints: (refinement, refinement) chc list): (refinement, refinement) chc list = match hes with - | [] -> accum_constraints + Log.info begin fun m -> + m ~header:"Infering new formula" "%s = %a" rule.var.name pp_formula rule.body + end; + + let (t, cs) = infer_formula track rule.body env chcs [] in + let cs = subtype t rule.var.ty cs in + + Log.info begin fun m -> + m ~header:"Constraints" "%a" pp_constraits cs + end; + + cs + +let rec infer_hes ?(track=false) (hes: hes) env (accum: (refinement, refinement) chc list): (refinement, refinement) chc list = match hes with + | [] -> accum | rule::xs -> - infer_rule track rule env accum_constraints |> infer_hes ~track:track xs env + infer_rule track rule env accum |> infer_hes ~track:track xs env -let rec print_hes = function - | [] -> () - | hes_rule::xs -> - print_string hes_rule.var.name; - print_string " "; - print_rtype hes_rule.var.ty; - print_newline (); - print_hes xs +let pp_env ppf env = + let env = IdMap.to_alist env in + let pp_v ppf (id, ty) = Fmt.pf ppf "%s: %a" id.Id.name pp_rtype ty in + Fmt.pf ppf "@[%a@.@]" (Fmt.list pp_v) env + + +let print_env env = + pp_env Fmt.stdout env; + Fmt.flush Fmt.stdout () let rec dnf_size = function | [] -> 0 @@ -207,7 +209,8 @@ let rec dnf_size = function let simplify = normalize -let print_derived_refinement_type is_dual_chc hes constraints = + +let print_derived_refinement_type is_dual_chc (env : Rtype.t IdMap.t) constraints = let rec gen_name_type_map constraints m = match constraints with | [] -> m | (id, args, body)::xs -> @@ -215,8 +218,9 @@ let print_derived_refinement_type is_dual_chc hes constraints = in let m = gen_name_type_map constraints Rid.M.empty - |> Rid.M.map (fun (args, fml) -> args, if is_dual_chc then Rtype.dual fml else fml) in - let rec subst_ids map t = + |> Rid.M.map (fun (args, fml) -> args, if is_dual_chc then Rtype.dual fml else fml) + in + let rec subst_ids map t = match map with | [] -> t | (src, dst):: xs -> @@ -236,15 +240,7 @@ let print_derived_refinement_type is_dual_chc hes constraints = RBool(body') | x -> x in - let rec inner = - let open Rhflz in - function - | [] -> [] - | rule::hes -> - let rule = {rule with var={rule.var with ty=translate_ty rule.var.ty}} in - rule :: inner hes - in - inner hes + IdMap.map env ~f:translate_ty (* Algorithm Input: hes(simply typed) env top @@ -296,7 +292,9 @@ let infer hes env top = | `Unknown -> `Unknown and infer_main ?(size=1) hes env top = (* 1. generate constraints *) - print_hes hes; + Log.info begin fun m -> + m ~header:"Initial types" "%a" pp_env env + end; let top_pred = get_top @@ Rethfl_syntax.Id.(top.ty) in let constraints = infer_hes hes env [{head=RTemplate(top_pred); body=RTrue}] in (*print_constraints constraints;*) @@ -307,18 +305,22 @@ let infer hes env top = let simplified = simplify constraints in let size = dnf_size simplified in - Printf.printf "[Size] %d\n" size; + Log.info begin fun m -> + m ~header:"Size of constraints" "%d" size + end; if size > 1 then begin (* この辺使ってなさそう、size<=1っぽい *) let dual = List.map Chc.dual constraints in let simplified_dual = simplify dual in let size_dual = dnf_size simplified_dual in - Printf.printf "[Dual Size] %d\n" size_dual; let min_size = if size < size_dual then size else size_dual in let target = if size < size_dual then simplified else simplified_dual in let use_dual = size >= size_dual in - + Log.info begin fun m -> + m ~header:"Use dual?" + "Using the %s CHC because the size of the dual formula is %d" (if use_dual then "dual" else "original") size_dual + end; (* let target' = expand target in print_string "remove or or\n"; print_constraints target'; *) @@ -329,7 +331,7 @@ let infer hes env top = | _ -> begin *) if min_size > 1 then (print_string "[Warning]Some definite clause has or-head\n";flush stdout) - else (print_string "easy\n"; flush stdout); + else (); if min_size > 1 then (* if size > 1 /\ dual_size > 1 *) use_dual, call_solver_with_timer target Chc_solver.(`Fptprove) @@ -347,9 +349,12 @@ let infer hes env top = match x with | Ok(x) -> let open Rethfl_options in - let hes = print_derived_refinement_type is_dual_chc hes x in + let env = print_derived_refinement_type is_dual_chc env x in if !Typing.show_refinement then - print_hes hes + begin + print_string "Refinement types:\n"; + print_env env + end else () | Error(s) -> Printf.printf "%s\n" s @@ -360,27 +365,6 @@ let infer hes env top = | `Unknown -> `Unknown -let print_refinements (constraints: (int * [> `Int ] Id.t list * refinement) list) = - print_endline "[Refinements]"; - List.iter (fun (i, ids, ref) -> ( - Printf.printf "[constraint %d]\n%s\n" i ([%derive.show: [> `Int ] Id.t list] ids); - (* List.iter (fun x -> Printf.printf "%s " (Id.show x)) ids; *) - print_refinement ref; - print_newline (); - () - )) constraints; - print_endline "[Refinements end]" - - -let print_env (env: Rtype.t IdMap.t) = - print_string "[print_env:start]\n"; - Rethfl_syntax.IdMap.iteri env ~f:(fun ~key:key ~data:data -> ( - Printf.printf "%s[ID=%d]: " key.name key.id; - print_rtype data; - print_newline () - )); - print_string "[print_env:end]\n" - type annotation_config = { annotated_func: string; annotated_type: Rtype.t; [@opaque] @@ -389,14 +373,6 @@ type annotation_config = { } [@@deriving show] - -let rec string_of_rty_skeleton (rty: Rtype.t) = - match rty with - | RArrow(x, y) -> "RArrow("^ (string_of_rty_skeleton x)^", "^( string_of_rty_skeleton y)^")" - | RBool(_) -> "RBool(RTrue)" - | RInt(_) -> "RInt(RId Rethfl_syntax.Id.(gen ~name:\"x\" `Int))" - - let dependent_funs f (hes : Rhflz.hes) = let fvs f = let { Rhflz.body; _ } = List.find (fun { Rhflz.var; _ } -> Id.eq f var) hes in @@ -450,35 +426,27 @@ let annotation_of file hes = let infer_based_on_annotations hes (env: Rtype.t IdMap.t) top file = let annotation = annotation_of file hes in - print_env env; - let env = Rethfl_syntax.IdMap.mapi env ~f:(fun ~key:id ~data:rty -> ( - if id.name = annotation.annotated_func + if id.Id.name = annotation.annotated_func then annotation.annotated_type else rty )) in - print_env env; - let hes = List.filter (fun x -> x.var.name <> annotation.annotated_func && List.exists (fun s -> s = x.var.name) annotation.dependencies_toplevel) hes in - print_hes hes; - infer hes env top - + + infer hes env top + let check_annotation hes env file = let annotation = annotation_of file hes in - print_env env; - (* replace the types in the type environment by the given annotation *) let env = Rethfl_syntax.IdMap.mapi env ~f:(fun ~key:id ~data:rty -> ( - if id.name = annotation.annotated_func + if id.Id.name = annotation.annotated_func then annotation.annotated_type else rty )) in - print_env env; - (* get the annotated function *) let top = (List.find (fun x -> x.var.name = annotation.annotated_func) hes).var in From f5de1980efbe12d8f4afd4376a0f328b4592b17a Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Sun, 15 Dec 2024 11:13:49 +0900 Subject: [PATCH 5/7] change the log level from app to info in main --- lib/rethfl.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/rethfl.ml b/lib/rethfl.ml index ec6dc37..7925672 100644 --- a/lib/rethfl.ml +++ b/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 From 078538b3ac21615181577ec88a6d512c451a1d18 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Wed, 1 Jan 2025 18:25:24 +0900 Subject: [PATCH 6/7] logging for rtype --- lib/typing/rtype.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/lib/typing/rtype.ml b/lib/typing/rtype.ml index 1b53961..68be54f 100644 --- a/lib/typing/rtype.ml +++ b/lib/typing/rtype.ml @@ -3,6 +3,8 @@ open Rid open Rresult +let log_src = Logs.Src.create ~doc:"Debug log for refinemnet types" "RType" +module Log = (val Logs.src_log log_src) let id_source = ref 0 let id_top = 0 @@ -48,10 +50,12 @@ let generate_rtemplate args = RTemplate(generate_id(), args) (* clone *) let rec clone_type_with_new_pred ints = function | RBool(RTemplate(_, _)) -> RBool(RTemplate(generate_id (), ints)) - | RBool(_) -> begin - print_endline "[Info]: Replacing non-template refinement"; + | RBool(_) -> + Log.info + begin fun m -> + m "[Info]: Replacing non-template refinement" + end; RBool(RTemplate(generate_id (), ints)) - end | RArrow(RInt(RId(id)), y) -> RArrow(RInt(RId(id)), clone_type_with_new_pred (Arith.Var(id)::ints) y) | RArrow(x, y) -> From 734e3dd139b7648068b5ea1095f1be2ddcba2679 Mon Sep 17 00:00:00 2001 From: Ken Sakayori Date: Fri, 20 Dec 2024 21:58:49 +0900 Subject: [PATCH 7/7] logging for chc_solver --- lib/typing/chc_solver.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/lib/typing/chc_solver.ml b/lib/typing/chc_solver.ml index 154b1d0..46d669a 100644 --- a/lib/typing/chc_solver.ml +++ b/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