- sprintf "%s [href=\"%s\"]"
- (CoercDb.name_of_carr carr) (UriManager.string_of_uri uri) in
- let data = List.fold_left
- (fun acc (src,tgt,cl) ->
- List.fold_left
- (fun acc c ->
- let src_name = CoercDb.name_of_carr src in
- let tgt_name = CoercDb.name_of_carr tgt in
- acc ^ src_name ^ " -> "
- ^ tgt_name ^ " [label=\"" ^ UriManager.name_of_uri c
- ^ "\",href=\"" ^ UriManager.string_of_uri c
- ^ "\"];\n"
- ^ node_dsc src ^ node_dsc tgt)
- acc cl)
- "" l
- in
- preamble ^ data ^ conclusion
-
+ Pp.node (CoercDb.name_of_carr carr)
+ ~attrs:["href", UriManager.string_of_uri uri] fmt in
+ List.iter
+ (fun (src, tgt, cl) ->
+ let src_name = CoercDb.name_of_carr src in
+ let tgt_name = CoercDb.name_of_carr tgt in
+ pp_description src;
+ pp_description tgt;
+ List.iter
+ (fun c ->
+ Pp.edge src_name tgt_name
+ ~attrs:[ "label", UriManager.name_of_uri c;
+ "href", UriManager.string_of_uri c ]
+ fmt)
+ cl)
+ l;
+ Pp.trailer fmt;
+ Buffer.contents buf
+;;
+
+let is_composite t =
+ try
+ let uri =
+ match t with
+ | Cic.Appl (he::_) -> CicUtil.uri_of_term he
+ | _ -> CicUtil.uri_of_term t
+ in
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | Cic.Constant (_,_, _, _, attrs),_ ->
+ List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
+ | _ -> false
+ with Invalid_argument _ -> false
+;;
+
+let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;
+
+let splat e l = List.map (fun x -> e, x) l;;
+
+let get_coercions_to carr =
+ let l = CoercDb.to_list () in
+ List.flatten
+ (HExtlib.filter_map
+ (fun (src,tgt,cl) ->
+ if CoercDb.eq_carr tgt carr then Some (splat src cl) else None)
+ l)
+;;
+
+let get_coercions_from carr =
+ let l = CoercDb.to_list () in
+ List.flatten
+ (HExtlib.filter_map
+ (fun (src,tgt,cl) ->
+ if CoercDb.eq_carr src carr then Some (splat tgt cl) else None)
+ l)
+;;
+
+let intersect l1 l2 =
+ let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
+ uniq (List.filter is_in_l1 l2)
+;;
+
+let grow s =
+ uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
+;;
+
+let lb c =
+ let l = get_coercions_from c in
+ function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
+;;
+
+let rec min acc = function
+ | c::tl ->
+ if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
+ | [] -> acc
+;;
+
+let meets left right =
+ let u = UriManager.uri_of_string "cic:/foo.con" in
+ min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
+;;
+