- let buf = Buffer.create 10240 in
- let fmt = Format.formatter_of_buffer buf in
- Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
- ~edge_attrs:["fontsize", "10"] fmt;
- let l = CoercDb.to_list () in
- let pp_description carr =
- match carr with
- | CoercDb.Uri uri ->
- Pp.node (CoercDb.string_of_carr carr)
- ~attrs:["href", UriManager.string_of_uri uri] fmt
- | _ -> ()
+ if List.exists (fun (_,t,_) -> CoercDb.string_of_carr t = "Type") l then
+ Format.fprintf fmt "subgraph cluster_rest { style=\"filled\";
+ color=\"white\"; label=<%s>; labelloc=\"b\"; %s; }\n"
+ ("<FONT POINT-SIZE=\"10.0\"><TABLE BORDER=\"1\" CELLBORDER=\"1\" >
+ <TR><TD BGCOLOR=\"gray95\">Source</TD>
+ <TD BGCOLOR=\"gray95\">Target</TD>
+ <TD BGCOLOR=\"gray95\">Arrows</TD></TR>"^
+ String.concat "</TR>"
+ (List.map
+ (fun (src,tgt,ul) ->
+ let src_name = CoercDb.string_of_carr src in
+ let tgt_name = CoercDb.string_of_carr tgt in
+ let names =
+ List.map (fun (u,_,_) ->
+ UriManager.name_of_uri u ^
+ (match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+ when List.exists ((=) (`Flavour `Variant)) attrs -> "*"
+ | _ -> "")
+ ) ul
+ in
+ "<TR><TD>" ^ src_name ^ "</TD><TD>" ^ tgt_name ^ "</TD><TD>" ^
+ String.concat ", " names ^ "</TD>")
+ (List.sort (fun (x,y,_) (x1,y1,_) ->
+ let rc = compare x x1 in
+ if rc = 0 then compare y y1 else rc) l))
+ ^ "</TR></TABLE></FONT>")
+ (String.concat ";" ["Type"]);
+ let type_uri u =
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u)
+ CicUniv.oblivion_ugraph
+ in
+ ty
+ in
+ let deref_coercion u =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph u with
+ | Cic.Constant (_,Some (Cic.Const (u',_)),_,_,attrs), _
+ when List.exists ((=) (`Flavour `Variant)) attrs ->
+ UriManager.name_of_uri u'
+ | Cic.Constant (_,Some t,_,_,_), _ when
+ let rec is_id = function
+ | Cic.Lambda (_,_,t) -> is_id t
+ | Cic.Rel _ -> true
+ | _ -> false
+ in is_id t -> "ID"
+ | _ -> UriManager.name_of_uri u