milestone in basic_2, λδ-2A reconstructed

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

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 1ca46db0bfd9538b3abb2d90e82b41762214213a..185ae53158f7cff7061382b12fbbc7f89f2974aa 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -314,8 +314,8 @@ and
              | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _)
              | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> 
                 (HLog.warn 
-                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^
-                "it is a duplicate of " ^ UriManager.string_of_uri u);
+                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
+                 "it is a duplicate of " ^ UriManager.string_of_uri u);
                 true) 
              | CoercDb.Sort s1, CoercDb.Sort s2 -> 
               (HLog.warn 
@@ -325,20 +325,30 @@ and
                  CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ 
                  CicPp.ppterm (Cic.Sort s2)); false)
              | _ -> 
+                let ty', _ = 
+                  CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) 
+                  CicUniv.oblivion_ugraph
+                in
+                if CicUtil.alpha_equivalence ty ty' then
                 (HLog.warn 
-                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^
-                "it is a duplicate of " ^ UriManager.string_of_uri u);
-                true))
+                ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
+                 "it is a duplicate of " ^ UriManager.string_of_uri u);
+                true)
+                else false
+                
+                )
          ul)
-      (CoercDb.to_list ())
+      (CoercDb.to_list (CoercDb.dump ()))
   in
   let cpos = no_args - arity - saturations - 1 in 
   if not add_composites then
-    (ignore(already_in_obj src_carr tgt_carr uri 
-      (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)));
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
-    []))
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); [])
   else
+    let _ = 
+      if already_in_obj src_carr tgt_carr uri
+       (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then
+        raise (AlreadyDefined uri);
+    in
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
        baseuri
@@ -348,18 +358,17 @@ and
       new_coercions 
     in
     (* update the DB *)
-    ignore(already_in_obj src_carr tgt_carr uri 
-      (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)));
-    List.iter 
-      (fun (src,tgt,uri,saturations,_,_,cpos) ->
-        CoercDb.add_coercion (src,tgt,uri,saturations,cpos)) 
-      new_coercions;
+    let lemmas = 
+      List.fold_left
+        (fun acc (src,tgt,uri,saturations,obj,arity,cpos) ->
+           CoercDb.add_coercion (src,tgt,uri,saturations,cpos);
+           let acc = add_obj uri obj pack_coercion_obj @ uri::acc in
+           acc)
+        [] new_coercions
+    in
     CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos);
-    (* add the composites obj and they eventual lemmas *)
-      (List.fold_left
-        (fun acc (_,tgt,uri,saturations,obj,arity,cpos) -> 
-          add_obj uri obj pack_coercion_obj @ uri::acc)
-        [] new_coercions)
+(*     CoercDb.prefer uri; *)
+    lemmas
 ;;