+ rc
+ in
+ let rc =
+ List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
+ in
+ let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
+
+ debug(lazy ("Hints:"^
+ String.concat "\n" (List.map
+ (fun (metasenv, (t1, t2), premises) ->
+ ("\t" ^ String.concat "; "
+ (List.map (fun (a,b) ->
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context a ^
+ " =?= "^
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context b)
+ premises) ^
+ " ==> "^
+ NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t1 ^
+ " = "^NCicPp.ppterm ~margin:max_int ~metasenv ~subst ~context t2))
+ rc)));
+
+ rc
+ end
+;;
+
+let pp_hint t p =
+ let context, t =
+ let rec aux ctx = function
+ | NCic.Prod (name, ty, rest) -> aux ((name, NCic.Decl ty) :: ctx) rest
+ | t -> ctx, t
+ in
+ aux [] t
+ in
+ let recproblems, concl =
+ let rec aux ctx = function
+ | NCic.LetIn (name,ty,bo,rest) -> aux ((name, NCic.Def(bo,ty))::ctx) rest
+ | t -> ctx, t
+ in
+ aux [] t
+ in
+ let buff = Buffer.create 100 in
+ let fmt = Format.formatter_of_buffer buff in
+(*
+ F.fprintf "@[<hov>"
+ F.fprintf "@[<hov>"
+(* pp_ctx [] context *)
+ F.fprintf "@]"
+ F.fprintf "@;"
+ F.fprintf "@[<hov>"
+(* pp_ctx context recproblems *)
+ F.fprintf "@]"
+ F.fprintf "\vdash@;";
+ NCicPp.ppterm ~fmt ~context:(recproblems@context) ~subst:[] ~metasenv:[];
+ F.fprintf "@]"
+ F.fprintf formatter "@?";
+ prerr_endline (Buffer.contents buff);
+*)
+()
+;;
+
+let generate_dot_file status fmt =
+ let module Pp = GraphvizPp.Dot in
+ let h_db, _ = status#uhint_db in
+ let names = ref [] in
+ let id = ref 0 in
+ let mangle l =
+ try List.assoc l !names
+ with Not_found ->
+ incr id;
+ names := (l,"node"^string_of_int!id) :: !names;
+ List.assoc l !names
+ in
+ let nodes = ref [] in
+ let edges = ref [] in
+ HDB.iter h_db (fun _key dataset ->
+ List.iter
+ (fun (precedence, l,r, hint) ->
+ let l =
+ Str.global_substitute (Str.regexp "\n") (fun _ -> "")
+ (NCicPp.ppterm
+ ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] l)
+ in
+ let r =
+ Str.global_substitute (Str.regexp "\n") (fun _ -> "")
+ (NCicPp.ppterm
+ ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] r)
+ in
+ let shint = "???" (*
+ string_of_int precedence ^ "..." ^
+ Str.global_substitute (Str.regexp "\n") (fun _ -> "")
+ (NCicPp.ppterm
+ ~margin:max_int ~metasenv:[] ~context:[] ~subst:[] hint)*)
+ in
+ nodes := (mangle l,l) :: (mangle r,r) :: !nodes;
+ edges := (mangle l, mangle r, shint, precedence, hint) :: !edges)
+ (HintSet.elements dataset);
+ );
+ List.iter (fun x, l -> Pp.node x ~attrs:["label",l] fmt) !nodes;
+ List.iter (fun x, y, l, _, _ ->
+ Pp.raw (Printf.sprintf "%s -- %s [ label=\"%s\" ];\n" x y "?") fmt)
+ !edges;
+ edges := List.sort (fun (_,_,_,p1,_) (_,_,_,p2,_) -> p1 - p2) !edges;
+ List.iter (fun x, y, _, p, l -> pp_hint l p) !edges;