Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / library / coercGraph.ml

diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml
index 77c449e0480f58f9f7044e4e3d18f92b48f0cf72..3862fcccc8904e206d6a47fc86bfca7eff68c35f 100644 (file)
--- a/helm/ocaml/library/coercGraph.ml
+++ b/helm/ocaml/library/coercGraph.ml
@@ -156,7 +156,7 @@ let filter_duplicates l coercions =
 
 let term_of_carr = function
   | CoercDb.Uri u -> CicUtil.term_of_uri u
-  | CoercDb.Sort _ -> assert false 
+  | CoercDb.Sort s -> Cic.Sort s
   | CoercDb.Term _ -> assert false
   
 (* given a new coercion uri from src to tgt returns 
@@ -167,49 +167,48 @@ let close_coercion_graph src tgt uri =
   let coercions = CoercDb.to_list () in
   let todo_list = get_closure_coercions src tgt uri coercions in
   let todo_list = filter_duplicates todo_list coercions in
-  let new_coercions, new_coercions_obj = 
-    List.split (
-      List.map (
-        fun (src, l , tgt) ->
-          match l with
-          | [] -> assert false 
-          | he :: tl ->
-              let first_step = 
-                Cic.Constant ("", 
-                  Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs)
-              in
-              let o,u = 
-                List.fold_left (fun (o,univ) coer ->
-                  match o with 
-                  | Cic.Constant (_,Some c,_,[],_) ->
-                      generate_composite_closure c (term_of_carr (CoercDb.Uri
-                      coer)) univ
-                  | _ -> assert false 
-                ) (first_step, CicUniv.empty_ugraph) tl
-              in
-              let name_src = CoercDb.name_of_carr src in
-              let name_tgt = CoercDb.name_of_carr tgt in
-              let name = name_tgt ^ "_of_" ^ name_src in
-              let buri = UriManager.buri_of_uri uri in
-              let c_uri = 
-                UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") 
-              in
-              let named_obj = 
-                match o with
-                | Cic.Constant (_,bo,ty,vl,attrs) ->
-                    Cic.Constant (name,bo,ty,vl,attrs)
+  let new_coercions = 
+    List.map (
+      fun (src, l , tgt) ->
+        match l with
+        | [] -> assert false 
+        | he :: tl ->
+            let first_step = 
+              Cic.Constant ("", 
+                Some (term_of_carr (CoercDb.Uri he)),
+                Cic.Sort Cic.Prop, [], obj_attrs)
+            in
+            let o,_ = 
+              List.fold_left (fun (o,univ) coer ->
+                match o with 
+                | Cic.Constant (_,Some c,_,[],_) ->
+                    generate_composite_closure c (term_of_carr (CoercDb.Uri
+                    coer)) univ
                 | _ -> assert false 
-              in
-                ((src,tgt,c_uri),(c_uri,named_obj,u))
-      ) todo_list)
+              ) (first_step, CicUniv.empty_ugraph) tl
+            in
+            let name_src = CoercDb.name_of_carr src in
+            let name_tgt = CoercDb.name_of_carr tgt in
+            let name = name_tgt ^ "_of_" ^ name_src in
+            let buri = UriManager.buri_of_uri uri in
+            let c_uri = 
+              UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") 
+            in
+            let named_obj = 
+              match o with
+              | Cic.Constant (_,bo,ty,vl,attrs) ->
+                  Cic.Constant (name,bo,ty,vl,attrs)
+              | _ -> assert false 
+            in
+              ((src,tgt,c_uri,named_obj))
+    ) todo_list
   in
-  List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]);
-  new_coercions_obj
+  new_coercions
 ;;
 
 let coercion_hashtbl = UriManager.UriHashtbl.create 3
 
-let add_coercion ~basedir ~add_composites uri =
+let add_coercion uri =
  let coer_ty,_ =
   CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
    CicUniv.empty_ugraph 
@@ -233,35 +232,47 @@ let add_coercion ~basedir ~add_composites uri =
   let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
   let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
   let new_coercions = close_coercion_graph src_uri tgt_uri uri in
-  let uris = ref [] in
-   if add_composites then
-    try
-     let lemmas =
-      List.fold_left
-       (fun lemmas (uri,o,_) ->
-         let lemmas' = LibrarySync.add_obj ~basedir uri o in
-          uris := uri :: !uris;
-          uri::lemmas'@lemmas
-       ) [] new_coercions;
-     in
-      UriManager.UriHashtbl.add coercion_hashtbl uri !uris;
-      lemmas
-    with
-     exn ->
-      List.iter LibrarySync.remove_obj !uris;
-      raise exn    
-   else
-    []
+  UriManager.UriHashtbl.add coercion_hashtbl uri 
+    (List.map (fun (_,_,uri,_) -> uri) new_coercions);
+  CoercDb.add_coercion (src_uri,tgt_uri,uri);
+  List.iter
+    (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
+    new_coercions;
+  List.map (fun (_,_,uri,o) -> uri,o) new_coercions
+  
 
 let remove_coercion uri =
- let uris =
   try
    let res = UriManager.UriHashtbl.find coercion_hashtbl uri in
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    res
+    CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
+    List.iter 
+      (fun u -> 
+        CoercDb.remove_coercion 
+          (fun (_,_,u1) -> UriManager.eq u u1)) 
+      res;
    with
-    Not_found -> assert false
- in
-  List.iter LibrarySync.remove_obj uris
+    Not_found -> ()
+
+let remove_all () =
+  CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
+let is_a_coercion t = 
+  try
+    let uri = CicUtil.uri_of_term t in
+    CoercDb.is_a_coercion uri
+  with Invalid_argument _ -> false
+
+let source_of t = 
+  try
+    let uri = CicUtil.uri_of_term t in
+    term_of_carr (fst (CoercDb.get_carr uri))
+  with Invalid_argument _ -> assert false (* t must be a coercion *)
+  
+let target_of t =
+  try
+    let uri = CicUtil.uri_of_term t in
+    term_of_carr (snd (CoercDb.get_carr uri))
+  with Invalid_argument _ -> assert false (* t must be a coercion *)
+    
 (* EOF *)