]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/coercGraph.ml
patch to calculate meets of a pair of carriers
[helm.git] / helm / software / components / library / coercGraph.ml
index 99ba33c33502c5f56f549d1bff2d716a103f7f4c..355c8019a80401f055b559f99f5352e154ea4022 100644 (file)
@@ -171,4 +171,51 @@ let is_composite t =
   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])))
+;;
+
 (* EOF *)