BIG FAT COMMIT REGARDING COERCIONS:

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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 1db8f0cfc2c7b8374b79ae334ef068da0cab6c83..9529375ae57a6b36c3317c45b8878ff24fa6932e 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -209,7 +209,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri =
+let add_coercion ~add_composites refinement_toolkit uri arity =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -225,23 +225,44 @@ let add_coercion ~add_composites refinement_toolkit uri =
    * should we saturate it with metas in case we insert it?
    * 
    *)
-  let extract_last_two_p ty =
+  let spline2list ty =
     let rec aux = function
-      | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> 
-          aux t
-      | Cic.Prod( _, src, tgt) -> src, tgt
-      | _ -> assert false
+      | Cic.Prod( _, src, tgt) -> src::aux tgt
+      | t -> [t]
     in
     aux ty
   in
+  let src_carr, tgt_carr = 
+    let list_remove_from_tail n l = 
+      let rec aux n = function
+        | hd::tl when n > 0 -> aux (n-1) tl
+        | l when n = 0 -> l
+        | _ -> assert false
+      in
+      aux n (List.rev l)
+    in
+    let types = spline2list coer_ty in
+    match arity, list_remove_from_tail arity types with
+    | 0,tgt::src::_ -> 
+        (* if ~delta is true, it is impossible to define an identity coercion *)
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+    | n,_::src::_ -> 
+        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+        CoercDb.Fun arity
+    | _ -> assert false    
+  in
   let already_in = 
      List.exists 
-      (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+      (fun (s,t,ul) -> 
+        List.exists 
+         (fun u -> 
+           UriManager.eq u uri && 
+           CoercDb.eq_carr s src_carr && 
+           CoercDb.eq_carr t tgt_carr) 
+         ul)
       (CoercDb.to_list ())
   in
-  let ty_src, ty_tgt = extract_last_two_p coer_ty in
-  let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
-  let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
   if not add_composites then
     (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
   else
@@ -317,10 +338,13 @@ let remove_coercion uri =
 
 let generate_projections refinement_toolkit uri fields =
  let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections = 
+   CicRecord.projections_of uri 
+     (List.map (fun (x,_,_) -> x) fields) 
+ in
   try
    List.iter2 
-    (fun (uri, name, bo) (_name, coercion) ->
+    (fun (uri, name, bo) (_name, coercion, arity) ->
       try
        let ty, ugraph =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
@@ -331,7 +355,8 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
-              let x = add_coercion ~add_composites:true refinement_toolkit uri
+              let x = 
+                add_coercion ~add_composites:true refinement_toolkit uri arity
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;