X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercGraph.ml;h=99ba33c33502c5f56f549d1bff2d716a103f7f4c;hb=f7ef9307f419376e5db085d59ad79487010ec123;hp=6d7a670efc688d641f2927ce62e03af1600f6076;hpb=bdf989481462c1185c9cbbfdd4b31d13aa4352b3;p=helm.git

diff --git a/helm/software/components/library/coercGraph.ml b/helm/software/components/library/coercGraph.ml
index 6d7a670ef..99ba33c33 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,32 +117,58 @@ 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 pippo {
-      node [fontsize=9, width=.4, height=.4];
-      edge [fontsize=10]; 
-      \n" 
-  in
-  let conclusion = " } \n" in
-  let data = List.fold_left 
-    (fun acc (src,tgt,cl) -> 
-      List.fold_left 
-        (fun acc c ->
-          acc ^ CoercDb.name_of_carr src ^ " -> " ^ 
-          CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^ 
-          "\"];\n")
-        acc cl)
-      "" l 
-  in
-  preamble ^ data ^ conclusion
-  
+  let pp_description carr =
+    match CoercDb.uri_of_carr carr with
+    | None -> ()
+    | Some uri ->
+        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
+;;
+
 (* EOF *)