Bug fixed: inductive types were no longer removed from the environment during

[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 6f31cbd463453ec1abee6f0892da3cfc696b61eb..99ba33c33502c5f56f549d1bff2d716a103f7f4c 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,20 +117,21 @@ 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 fmt;
-  Pp.node "node" ~attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] fmt;
-  Pp.node "edge" ~attrs:["fontsize", "10"] fmt;
+  Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+    ~edge_attrs:["fontsize", "10"] fmt;
   let l = CoercDb.to_list () in
   let pp_description carr =
     match CoercDb.uri_of_carr carr with
@@ -146,5 +155,20 @@ 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
+;;
 
 (* EOF *)