X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=13596c84e27e696b91168d8c2086da8cdeeea0fd;hb=76ec6b95c6f462f7fdedf0bc87354fb874ef4a46;hp=fd89f77c8f7e89744e7a745bd8ff16f5df094b79;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index fd89f77c8..13596c84e 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -128,8 +128,7 @@ let save_object_to_disk uri obj ugraph univlist =
 
 let typecheck_obj =
  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri)
-  (Unshare.fresh_types obj)
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
  let profiler = HExtlib.profile "add_obj.index_obj" in
@@ -139,12 +138,9 @@ let index_obj =
 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 (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
-    then
-      refinement_toolkit.RT.pack_coercion_obj obj
-    else
-      obj 
+    if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None
+    then refinement_toolkit.RT.pack_coercion_obj obj
+    else obj 
   in
   let dbd = LibraryDb.instance () in
   if CicEnvironment.in_library uri then
@@ -160,8 +156,10 @@ let add_single_obj uri obj refinement_toolkit =
       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
       (univ_time *. 100. /. total_time) (total_time) (univ_time)
       (UriManager.name_of_uri uri));*)
-    let _, ugraph, univlist = 
-      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+    let obj, ugraph, univlist = 
+      try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
+      with CicEnvironment.Object_not_found _ -> assert false
+    in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       try
@@ -243,7 +241,7 @@ let generate_elimination_principles uri refinement_toolkit =
   
 let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
-  CoercDb.remove_coercion (fun (_,_,_,_) -> true)
+  CoercDb.remove_coercion (fun _ -> true)
 
 let stack = ref [];;
 
@@ -293,7 +291,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     in
     aux ty
   in
-  let src_carr, tgt_carr = 
+  let src_carr, tgt_carr, no_args = 
     let get_classes arity saturations l = 
       (* this is the ackerman's function revisited *)
       let rec aux = function
@@ -311,18 +309,19 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     in
     let types = spine2list coer_ty in
     let src,tgt = get_classes arity saturations types in
-     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
-     match tgt with
-        None -> assert false
-      | Some `Funclass -> CoercDb.Fun arity
-      | Some (`Class tgt) ->
-         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0,
+     (match tgt with
+     | None -> assert false
+     | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity
+     | Some (`Class tgt) ->
+         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0),
+     List.length types - 1
   in
   let already_in_obj src_carr tgt_carr uri obj = 
      List.exists 
       (fun (s,t,ul) -> 
         List.exists 
-         (fun u,_ -> 
+         (fun u,_,_ -> 
            let bo = 
             match obj with 
             | Cic.Constant (_, Some bo, _, _, _) -> bo
@@ -342,8 +341,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
          ul)
       (CoercDb.to_list ())
   in
+  let cpos = no_args - arity - saturations - 1 in 
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
     UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
     [])
   else
@@ -352,22 +352,24 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        baseuri
     in
     let new_coercions = 
-      List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
+      List.filter (fun (s,t,u,_,obj,_,_) -> not(already_in_obj s t u obj))
       new_coercions 
     in
-    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
+    let composite_uris = 
+      List.map (fun (_,_,uri,_,_,_,_) -> uri) new_coercions 
+    in
     (* update the DB *)
     List.iter 
-      (fun (src,tgt,uri,saturations,_,_) ->
-        CoercDb.add_coercion (src,tgt,uri,saturations)) 
+      (fun (src,tgt,uri,saturations,_,_,cpos) ->
+        CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) 
       new_coercions;
-    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
         List.fold_left
-          (fun acc (_,tgt,uri,saturations,obj,arity) -> 
+          (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> 
             add_single_obj uri obj refinement_toolkit;
-             (uri,arity,saturations)::acc) 
+             (uri,arity,saturations,cpos)::acc) 
           [] new_coercions
     in
     (* store that composite_uris are related to uri. the first component is
@@ -398,10 +400,11 @@ let remove_coercion uri =
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
     CoercDb.remove_coercion 
-      (fun (_,_,u,_) -> UriManager.eq uri u);
+      (fun (_,_,u,_,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
-      (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
+      (fun u -> 
+         CoercDb.remove_coercion (fun (_,_,u1,_,_) -> UriManager.eq u u1))
       composites_in_db;
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
@@ -441,7 +444,7 @@ let generate_projections refinement_toolkit uri fields =
   prerr_endline "---";
 *)
               (*CSC: I throw the arity away. See comment above *)
-              List.map (fun u,_,_ -> u) x
+              List.map (fun u,_,_,_ -> u) x
             end
           else  
             []
@@ -479,31 +482,31 @@ let
       List.fold_right
        (fun (name,idx,ty,bo) (n,uris) ->
          if name = name_to_avoid then
-          (n+1,uris)
+          (n-1,uris)
          else
           let uri =
            UriManager.uri_of_string
             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
-          let bo = Cic.Fix (n,funs) in 
+	  let bo = Cic.Fix (n-1,funs) in 
           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-           add_single_obj uri obj refinement_toolkit;
-           (n+1,uri::uris)
-       ) funs (1,[]))
+           (add_single_obj uri obj refinement_toolkit;
+           (n-1,uri::uris)))
+       funs (List.length funs,[]))
   | Cic.CoFix (_,funs) ->
      snd (
       List.fold_right
        (fun (name,ty,bo) (n,uris) ->
          if name = name_to_avoid then
-          (n+1,uris)
+          (n-1,uris)
          else
           let uri =
            UriManager.uri_of_string
             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
-          let bo = Cic.CoFix (n,funs) in 
+          let bo = Cic.CoFix (n-1,funs) in 
           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
            add_single_obj uri obj refinement_toolkit;
-           (n+1,uri::uris)
-       ) funs (1,[]))
+           (n-1,uri::uris)
+       ) funs (List.length funs,[]))
   | _ -> assert false
 
 let add_obj refinement_toolkit uri obj =