moved coercion to library (work in progress)

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

diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml
index d99fc6f798f67f72ccbee796adc50b8bd0db1474..77c449e0480f58f9f7044e4e3d18f92b48f0cf72 100644 (file)
--- a/helm/ocaml/library/coercGraph.ml
+++ b/helm/ocaml/library/coercGraph.ml
@@ -207,4 +207,61 @@ let close_coercion_graph src tgt uri =
   new_coercions_obj
 ;;
 
+let coercion_hashtbl = UriManager.UriHashtbl.create 3
+
+let add_coercion ~basedir ~add_composites uri =
+ let coer_ty,_ =
+  CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
+   CicUniv.empty_ugraph 
+ in
+  (* we have to get the source and the tgt type uri
+   * in Coq syntax we have already their names, but
+   * since we don't support Funclass and similar I think
+   * all the coercion should be of the form
+   * (A:?)(B:?)T1->T2
+   * So we should be able to extract them from the coercion type
+   *)
+  let extract_last_two_p ty =
+    let rec aux = function
+      | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
+      | Cic.Prod( _, src, tgt) -> src, tgt
+      | _ -> assert false
+    in
+    aux ty
+  in
+  let ty_src,ty_tgt = extract_last_two_p coer_ty in
+  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
+    []
+
+let remove_coercion uri =
+ let uris =
+  try
+   let res = UriManager.UriHashtbl.find coercion_hashtbl uri in
+    UriManager.UriHashtbl.remove coercion_hashtbl uri;
+    res
+   with
+    Not_found -> assert false
+ in
+  List.iter LibrarySync.remove_obj uris
+
 (* EOF *)