patch to calculate meets of a pair of carriers

[helm.git] / helm / software / components / library / coercGraph.ml

diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index 40d6281252c58de143736f3e6aaaa9248c13d570..355c8019a80401f055b559f99f5352e154ea4022 100644 (file)
--- a/helm/software/components/library/coercGraph.ml
+++ b/helm/software/components/library/coercGraph.ml
@@ -37,7 +37,7 @@ let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion src tgt =
+let look_for_coercion' src tgt =
   let arity_of con =
     try
       let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
@@ -77,8 +77,16 @@ let look_for_coercion src tgt =
          None -> NoCoercion
        | Some ul ->
           let cl = List.map CicUtil.term_of_uri ul in
+          let funclass_arityl = 
+            let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+            List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+          in
           let arityl = List.map arity_of cl in
-          let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+          let argsl = 
+            List.map2 
+              (fun arity fn_arity -> 
+                mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl
+          in
           let newtl =
             List.map2 
               (fun args c -> 
@@ -96,7 +104,7 @@ let look_for_coercion src tgt =
 let look_for_coercion src tgt = 
   let src_uri = CoercDb.coerc_carr_of_term src in
   let tgt_uri = CoercDb.coerc_carr_of_term tgt in
-  look_for_coercion src_uri tgt_uri
+  look_for_coercion' src_uri tgt_uri
 
 let is_a_coercion t = 
   try
@@ -109,13 +117,15 @@ let source_of t =
     let uri = CicUtil.uri_of_term t in
     CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
   with Invalid_argument _ -> assert false (* t must be a coercion *)
-  
-let target_of t =
+
+let is_a_coercion_to_funclass t =
   try
     let uri = CicUtil.uri_of_term t in
-    CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
-  with Invalid_argument _ -> assert false (* t must be a coercion *)
-    
+    match snd (CoercDb.get_carr uri) with
+    | CoercDb.Fun i -> Some i
+    | _ -> None
+  with Invalid_argument _ -> None
+  
 let generate_dot_file () =
   let module Pp = GraphvizPp.Dot in
   let buf = Buffer.create 10240 in
@@ -145,5 +155,67 @@ let generate_dot_file () =
     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])))
+;;
 
 (* EOF *)