version 0.7.1

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

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index e01f28eb3fcc1994f068dbc86926e6dff42a614c..57274e616446b3dab7b416c8db8f71f3aace8441 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,47 +25,30 @@
 
 open Printf;;
 
-ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
-
-(* the list of known coercions (MUST be transitively closed) *)
-let coercions = ref [
-  (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
-   UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
-   UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
-
-   (
-     UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
-     UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)",
-     UriManager.uri_of_string "cic:/CoRN/algebra/CFields/cf_crr.con"
-  
-    );
-    (
-     UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)",
-     UriManager.uri_of_string "cic:/CoRN/algebra/CGroups/CGroup.ind#xpointer(1/1)",
-     UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/cag_crr.con"
-  
-    );
-
-]
-;;
+let debug = false
+let debug_print = if debug then prerr_endline else ignore
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
-  try
-    let s,t,u = 
-      List.find (fun (s,t,_) -> 
-        UriManager.eq s src && 
-        UriManager.eq t tgt) 
-      !coercions 
-    in
-    prerr_endline (sprintf ":) TROVATA la coercion %s %s" 
-      (UriManager.name_of_uri src) 
-      (UriManager.name_of_uri tgt));
-    Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
-  with 
-    Not_found -> 
-      prerr_endline (sprintf ":( NON TROVATA la coercion %s %s" 
-        (UriManager.name_of_uri src) (UriManager.name_of_uri tgt));
+    try
+      let src = CicUtil.uri_of_term src in
+      let tgt = CicUtil.uri_of_term tgt in
+      let l = 
+        CoercDb.find_coercion 
+          (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) 
+      in
+      match l with
+      | [] -> debug_print ":( coercion non trovata"; None
+      | u::_ -> 
+          debug_print (
+            sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
+              (List.length l)
+              (UriManager.name_of_uri src) 
+              (UriManager.name_of_uri tgt)
+              (UriManager.name_of_uri u));
+              Some (CicUtil.term_of_uri u)
+    with Invalid_argument s -> 
+      debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
       None
 ;;
 
@@ -73,17 +56,9 @@ let look_for_coercion src tgt =
  * of new coercions to create. hte list elements are
  * (source, list of coercions to follow, target)
  *)
-let get_closure_coercions src tgt uri =
-  let c_from_tgt = 
-    List.filter (fun (f,_,_) -> 
-      UriManager.eq f tgt) 
-    !coercions   
-  in
-  let c_to_src = 
-    List.filter (fun (_,t,_) -> 
-      UriManager.eq t src) 
-    !coercions
-  in
+let get_closure_coercions src tgt uri coercions =
+  let c_from_tgt = List.filter (fun (f,_,_) -> UriManager.eq f tgt) coercions in
+  let c_to_src = List.filter (fun (_,t,_) -> UriManager.eq t src) coercions in
     (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
     (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
     (List.fold_left (
@@ -122,7 +97,7 @@ let generate_composite_closure c1 c2 univ =
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
-      prerr_endline (sprintf "Generated composite coercion:\n%s\n%s" 
+      debug_print (sprintf "Generated composite coercion:\n%s\n%s" 
         (CicPp.ppterm c) s);
       raise exn
   in
@@ -134,13 +109,13 @@ let generate_composite_closure c1 c2 univ =
 ;;
 
 (* removes from l the coercions that are in !coercions *)
-let filter_duplicates l =
+let filter_duplicates l coercions =
   List.filter (
       fun (src,_,tgt) ->
         not (List.exists (fun (s,t,u) -> 
           UriManager.eq s src && 
           UriManager.eq t tgt)
-        !coercions))
+        coercions))
   l
 
 (* given a new coercion uri from src to tgt returns 
@@ -148,8 +123,9 @@ let filter_duplicates l =
  *)
 let close_coercion_graph src tgt uri =
   (* check if the coercion already exists *)
-  let todo_list = get_closure_coercions src tgt uri in
-  let todo_list = filter_duplicates todo_list in
+  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 (
@@ -157,9 +133,7 @@ let close_coercion_graph src tgt uri =
           match l with
           | [] -> assert false 
           | he :: tl ->
-              let term_of_uri' uri = 
-                CicUtil.term_of_uri (UriManager.string_of_uri uri)
-              in
+              let term_of_uri' uri = CicUtil.term_of_uri uri in
               let first_step = 
                 Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
                   obj_attrs)
@@ -188,29 +162,8 @@ let close_coercion_graph src tgt uri =
                 ((src,tgt,c_uri),(c_uri,named_obj,u))
       ) todo_list)
   in
-  coercions := !coercions @ new_coercions;
+  List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]);
   new_coercions_obj
 ;;
 
-
-
-
-(* stupid case *)
-
-let l = close_coercion_graph 
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)")
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CRings/cr_crr.con")
-in
- List.iter (fun (u,o,g) -> 
-   prerr_endline (CicPp.ppobj o);
-   prerr_endline (UriManager.string_of_uri u);
-   prerr_endline "")
- l
- 
- 
-
 (* EOF *)