X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercGraph.ml;h=355c8019a80401f055b559f99f5352e154ea4022;hb=4609a07e2fe4343d94832fcaf0936223f83ba71c;hp=d3adfdb5f6566dcb1156ce7f26be64cf664d5a11;hpb=62f814b9b8c255abbdfcbf12d96f3a3b4e74d477;p=helm.git

diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index d3adfdb5f..355c8019a 100644
--- 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,42 +117,105 @@ 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
+  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 preamble = "
-    digraph g {
-      node [fontsize=9, width=.4, height=.4];
-      edge [fontsize=10]; 
-      \n" 
-  in
-  let conclusion = " } \n" in
-  let node_dsc carr =
+  let pp_description carr =
     match CoercDb.uri_of_carr carr with
-    | None -> ""
+    | None -> ()
     | Some uri ->
-        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])))
+;;
+
 (* EOF *)