Serious bug fixed: arities of coercions in the .moo files were not computed

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf..4e64e6badc369c21d92e83d96c9719a4d72f1caa 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -111,7 +111,7 @@ let add_single_obj uri obj refinement_toolkit =
   let module RT = RefinementTool in
   let obj = 
     if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
-       not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+       not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
     then
       refinement_toolkit.RT.pack_coercion_obj obj
     else
@@ -211,7 +211,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri arity =
+let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -270,6 +270,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity =
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+       baseuri
     in
     let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
     if already_in then
@@ -292,9 +293,10 @@ let add_coercion ~add_composites refinement_toolkit uri arity =
         let lemmas = 
           if add_composites then
             List.fold_left
-              (fun acc (_,_,uri,obj) -> 
+              (fun acc (_,tgt,uri,obj) -> 
                 add_single_obj uri obj refinement_toolkit;
-                uri::acc) 
+                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+                 (uri,arity)::acc) 
               [] new_coercions
           else
             []
@@ -357,14 +359,19 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+              (*CSC: I think there is a bug here. The composite coercions
+                are not remembered in the .moo file. Thus they are re-generated
+                every time. Right? *)
               let x = 
                 add_coercion ~add_composites:true refinement_toolkit uri arity
+                (UriManager.buri_of_uri uri)
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
   prerr_endline "---";
 *)
-              x
+              (*CSC: I throw the arity away. See comment above *)
+              List.map fst x
             end
           else  
             []