patch to calculate meets of a pair of carriers

diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml
index f06035604535dcd5a132f2667292f6318dc15fd2..d7ad886b2c8fa33a07213faf7ea8b98bb9e974b4 100644 (file)
--- a/components/library/cicCoercion.ml
+++ b/components/library/cicCoercion.ml
@@ -99,7 +99,7 @@ let generate_composite_closure rt c1 c2 univ arity =
     let len,names = aux [] 0 t in
     let len = len - arity in
     List.fold_left 
-      (fun (n,l) x -> if n <= len then n+1,l@[x] else n,l) (0,[]) 
+      (fun (n,l) x -> if n < len then n+1,l@[x] else n,l) (0,[]) 
       names
   in
   let compose c1 nc1 c2 nc2 =
@@ -194,8 +194,8 @@ let generate_composite_closure rt c1 c2 univ arity =
   debug_print (lazy ("\nCOMPOSING"));
   debug_print (lazy (" c1= "^CicPp.ppterm c1 ^"  :  "^ CicPp.ppterm c1_ty));
   debug_print (lazy (" c2= "^CicPp.ppterm c2 ^"  :  "^ CicPp.ppterm c2_ty));
-  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty arity in 
-  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 in
+  let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in 
+  let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity in
   let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
   let spline_len = saturations_for_c1 + saturations_for_c2 in
   let c = mk_lambda_spline c (namer (names_c1 @ names_c2)) spline_len in

diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml
index 99ba33c33502c5f56f549d1bff2d716a103f7f4c..355c8019a80401f055b559f99f5352e154ea4022 100644 (file)
--- a/components/library/coercGraph.ml
+++ b/components/library/coercGraph.ml
@@ -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 *)

diff --git a/components/library/coercGraph.mli b/components/library/coercGraph.mli
index 9e99d68f8cf02321645a9c4e3e88f3835070d779..7468d4699ce1cba63ba9acd4d6475ce73b56eebf 100644 (file)
--- a/components/library/coercGraph.mli
+++ b/components/library/coercGraph.mli
@@ -46,8 +46,11 @@ val is_a_coercion_to_funclass: Cic.term -> int option
  * a constant applyed that is marked with (`Class `Coercion) *)
 val is_composite: Cic.term -> bool
 
-
 val source_of: Cic.term -> Cic.term
 
 val generate_dot_file: unit -> string
 
+val meets : 
+  CoercDb.coerc_carr -> CoercDb.coerc_carr -> 
+    (CoercDb.coerc_carr * UriManager.uri * UriManager.uri) list
+