]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/coercGraph.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_unification / coercGraph.ml
index c1056b6eca8a912c1ba9b0171ebcf368ea514a3a..d99fc6f798f67f72ccbee796adc50b8bd0db1474 100644 (file)
 
 open Printf;;
 
+type coercion_search_result = 
+  | SomeCoercion of Cic.term
+  | NoCoercion
+  | NotMetaClosed
+  | NotHandled of string Lazy.t
+
 let debug = false
-let debug_print = if debug then prerr_endline else ignore
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
 
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src 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
-      | [] -> prerr_endline ":( 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
+  try 
+    let l = 
+      CoercDb.find_coercion 
+        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) 
+    in
+    match l with
+    | [] -> 
+        debug_print 
+          (lazy 
+            (sprintf ":-( coercion non trovata da %s a %s" 
+              (CoercDb.name_of_carr src) 
+              (CoercDb.name_of_carr tgt)));
+        NoCoercion
+    | [u] -> 
+        debug_print (lazy (
+          sprintf ":-) TROVATA 1 coercion da %s a %s: %s" 
+            (CoercDb.name_of_carr src) 
+            (CoercDb.name_of_carr tgt)
+            (UriManager.name_of_uri u)));
+        SomeCoercion (CicUtil.term_of_uri u)
+    | u::_ -> 
+        debug_print (lazy (
+          sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
+            (List.length l)
+            (CoercDb.name_of_carr src) 
+            (CoercDb.name_of_carr tgt)
+            (UriManager.name_of_uri u)));
+        SomeCoercion (CicUtil.term_of_uri u)
+  with
+    | CoercDb.EqCarrNotImplemented s -> NotHandled s
+    | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
 ;;
 
+let look_for_coercion src tgt = 
+  let src_uri = CoercDb.coerc_carr_of_term src in
+  let tgt_uri = CoercDb.coerc_carr_of_term tgt in
+  look_for_coercion src_uri tgt_uri
+
 (* given the new coercion uri from src to tgt returns the list 
  * of new coercions to create. hte list elements are
  * (source, list of coercions to follow, target)
  *)
 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 (
-      fun l (s,_,u1) ->
-        ((List.map (fun (_,t,u2) ->
-          (s,[u1;uri;u2],t)
-        )c_from_tgt)@l) )
-    [] c_to_src)
+  let eq_carr s t = 
+    try
+      CoercDb.eq_carr s t
+    with
+    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+  in
+  match src,tgt with
+  | CoercDb.Uri _, CoercDb.Uri _ ->
+      let c_from_tgt = 
+        List.filter (fun (f,_,_) -> eq_carr f tgt) coercions 
+      in
+      let c_to_src = 
+        List.filter (fun (_,t,_) -> eq_carr 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 (
+          fun l (s,_,u1) ->
+            ((List.map (fun (_,t,u2) ->
+              (s,[u1;uri;u2],t)
+            )c_from_tgt)@l) )
+        [] c_to_src)
+  | _ -> [] (* do not close in case source or target is not an indty ?? *)
 ;;
 
 let obj_attrs = [`Class `Coercion; `Generated]
@@ -97,8 +133,8 @@ let generate_composite_closure c1 c2 univ =
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
-      debug_print (sprintf "Generated composite coercion:\n%s\n%s" 
-        (CicPp.ppterm c) s);
+      debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" 
+        (CicPp.ppterm c) (Lazy.force s)));
       raise exn
   in
   let cleaned_ty =
@@ -113,11 +149,16 @@ 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)
+          CoercDb.eq_carr s src && 
+          CoercDb.eq_carr t tgt)
         coercions))
   l
 
+let term_of_carr = function
+  | CoercDb.Uri u -> CicUtil.term_of_uri u
+  | CoercDb.Sort _ -> assert false 
+  | CoercDb.Term _ -> assert false
+  
 (* given a new coercion uri from src to tgt returns 
  * a list of (new coercion uri, coercion obj, universe graph) 
  *)
@@ -133,21 +174,21 @@ let close_coercion_graph src tgt uri =
           match l with
           | [] -> assert false 
           | he :: tl ->
-              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)
+                Cic.Constant ("", 
+                  Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs)
               in
               let o,u = 
-                List.fold_left (fun (o,u) coer ->
+                List.fold_left (fun (o,univ) coer ->
                   match o with 
                   | Cic.Constant (_,Some c,_,[],_) ->
-                      generate_composite_closure c (term_of_uri' coer) u
+                      generate_composite_closure c (term_of_carr (CoercDb.Uri
+                      coer)) univ
                   | _ -> assert false 
                 ) (first_step, CicUniv.empty_ugraph) tl
               in
-              let name_src = UriManager.name_of_uri src in
-              let name_tgt = UriManager.name_of_uri tgt 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 =