diff options
Diffstat (limited to 'backend/LICMaux.ml')
| -rw-r--r-- | backend/LICMaux.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index ecc11a00..39e336eb 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -107,17 +107,20 @@ let inner_loops (f : coq_function) : PSet.t PTree.t = and predecessors = Kildall.make_predecessors f.fn_code RTL.successors_instr in PTree.map (filter_dominated_part predecessors) parts;; -let pp_pset oc s = +let pp_list pp_item oc l = output_string oc "{ "; let first = ref true in List.iter (fun x -> (if !first then first := false else output_string oc ", "); - Printf.printf "%d" x) - (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s))); + pp_item oc x) l; output_string oc " }";; +let pp_pset oc s = + pp_list (fun oc -> Printf.fprintf oc "%d") oc + (List.sort (fun x y -> y - x) (List.map P.to_int (PSet.elements s)));; + let print_dominated_parts oc f = List.iter (fun (header, nodes) -> Printf.fprintf oc "%d : %a\n" (P.to_int header) pp_pset nodes) |