X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.ml;h=0041685ef212d62d68e2c1bd453ad840cb263360;hb=78c5dec8c544c2ab9c2e19663444d50ac97e3812;hp=e9a123ad8a411781733a6dd50d3660ecee6ddf97;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index e9a123ad8..0041685ef 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/components/tactics/closeCoercionGraph.ml
@@ -33,39 +33,32 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  * (source, list of coercions to follow, target)
  *)
 let get_closure_coercions src tgt uri coercions =
-  let enrich (uri,sat) tgt =
+  let enrich (uri,sat,_) tgt =
    let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
     uri,sat,arity
   in
   let uri = enrich uri tgt in
   let eq_carr ?exact s t = 
-    debug_print (lazy(CoercDb.name_of_carr s^" VS "^CoercDb.name_of_carr t));
-    try
-            let rc = CoercDb.eq_carr ?exact s t in
-            debug_print(lazy(string_of_bool rc));
-            rc
-    with
-    | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> 
-        debug_print (lazy("false"));            
-        false
+    debug_print(lazy(CoercDb.string_of_carr s^" VS "^CoercDb.string_of_carr t));
+    let rc = CoercDb.eq_carr ?exact s t in
+    debug_print(lazy(string_of_bool rc));
+    rc
   in
   match src,tgt with
   | CoercDb.Uri _, CoercDb.Uri _ ->
-                  debug_print (lazy ("Uri, Uri4"));
+      debug_print (lazy ("Uri, Uri4"));
       let c_from_tgt = 
         List.filter 
           (fun (f,t,_) -> 
-                  
-                  debug_print (lazy ("Uri, Uri3"));
-                  eq_carr f tgt (*&& not (eq_carr t src)*)) 
+             debug_print (lazy ("Uri, Uri3"));
+             eq_carr f tgt) 
           coercions 
       in
       let c_to_src = 
         List.filter 
           (fun (f,t,_) -> 
-                  
-                  debug_print (lazy ("Uri, Uri2"));
-                  eq_carr t src (*&& not (eq_carr f tgt)*)) 
+             debug_print (lazy ("Uri, Uri2"));
+             eq_carr t src) 
           coercions 
       in
         (HExtlib.flatten_map 
@@ -249,9 +242,9 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       | (i,_,_)::_ when i = n -> acc
       | _::tl -> position_of n (acc + 1) tl
     in
-    let saturations_res = 
+    let saturations_res, position_of_meta_to_be_coerced = 
       match meta_to_be_coerced with
-      | None -> 0
+      | None -> 0,0
       | Some meta_to_be_coerced -> 
           debug_print
             (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced));
@@ -259,10 +252,11 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
             position_of meta_to_be_coerced 0 sorted in
           debug_print (lazy ("POSITION_OF_META_TO_BE_COERCED: " ^
             string_of_int position_of_meta_to_be_coerced));
-          List.length sorted - position_of_meta_to_be_coerced - 1
+          List.length sorted - position_of_meta_to_be_coerced - 1,
+          position_of_meta_to_be_coerced
     in
     debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res));
-    sorted, saturations_res
+    sorted, saturations_res, position_of_meta_to_be_coerced
   in
   let namer l n = 
     let l = List.map (function Cic.Name s -> s | _ -> "A") l in
@@ -287,7 +281,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
   let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in
   debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c));
   let old_insert_coercions = !CicRefine.insert_coercions in
-  let c, metasenv, univ, saturationsres =
+  let c, metasenv, univ, saturationsres, cpos =
     try
       CicRefine.insert_coercions := false;
       let term, ty, metasenv, ugraph = 
@@ -303,7 +297,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       in
       debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
       debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv));
-      let body_metasenv, saturationsres =
+      let body_metasenv, saturationsres, cpos =
        order_body_menv term body_metasenv c1_pis c2_pis
       in
       debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv));
@@ -340,7 +334,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
       debug_print (lazy ("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
       debug_print (lazy ("####################"));
       CicRefine.insert_coercions := old_insert_coercions;
-      term, metasenv, ugraph, saturationsres
+      term, metasenv, ugraph, saturationsres, cpos
     with
     | CicRefine.RefineFailure s 
     | CicRefine.Uncertain s -> debug_print s; 
@@ -350,7 +344,7 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ=
         CicRefine.insert_coercions := old_insert_coercions;
         raise exn
   in
-  c, metasenv, univ, saturationsres, arity2
+  c, metasenv, univ, saturationsres, arity2, cpos
 ;;
 
 let build_obj c univ arity =
@@ -372,16 +366,18 @@ let build_obj c univ arity =
 (* removes from l the coercions that are in !coercions *)
 let filter_duplicates l coercions =
   List.filter (
-      fun (src,l1,tgt) ->
-        not (List.exists (fun (s,t,l2) -> 
-          CoercDb.eq_carr s src && 
-          CoercDb.eq_carr t tgt &&
-          try 
-            List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2
-          with
-          | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false)
-        coercions))
+   fun (src,l1,tgt) ->
+     not (List.exists (fun (s,t,l2) -> 
+       CoercDb.eq_carr s src && 
+       CoercDb.eq_carr t tgt &&
+       try 
+         List.for_all2 (fun (u1,_,_) (u2,_,_) -> UriManager.eq u1 u2) l1 l2
+       with
+       | Invalid_argument "List.for_all2" -> 
+           debug_print (lazy("XXX")); false)
+     coercions))
   l
+;;
 
 let mangle s t l = 
   (*List.fold_left
@@ -429,7 +425,7 @@ let number_if_already_defined buri name l =
 let close_coercion_graph src tgt uri saturations baseuri =
   (* check if the coercion already exists *)
   let coercions = CoercDb.to_list () in
-  let todo_list = get_closure_coercions src tgt (uri,saturations) coercions in
+  let todo_list = get_closure_coercions src tgt (uri,saturations,0) coercions in
   debug_print (lazy("composed " ^ string_of_int (List.length todo_list)));
   let todo_list = filter_duplicates todo_list coercions in
   try
@@ -437,47 +433,46 @@ let close_coercion_graph src tgt uri saturations baseuri =
       List.fold_left 
         (fun acc (src, l , tgt) ->
           try 
-            (match l with
+            match l with
             | [] -> assert false 
             | (he,saturations1,arity1) :: tl ->
                 let first_step = 
-                  Cic.Constant ("", 
-                   Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+                  Cic.Constant ("", Some (CicUtil.term_of_uri he),
                     Cic.Sort Cic.Prop, [], obj_attrs arity1),
                   saturations1,
-                  arity1
+                  arity1,0
                 in
                 let o,_ = 
                   List.fold_left (fun (o,univ) (coer,saturations2,arity2) ->
                     match o with 
-                    | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 ->
-                        let t, menv, univ, saturationsres, arityres = 
+                    | Cic.Constant (_,Some u,_,[],_),saturations1,arity1,_ ->
+                        let t, menv, univ, saturationsres, arityres, cposres = 
                           generate_composite' (u,saturations1,arity1) 
-                            (CoercDb.term_of_carr (CoercDb.Uri coer),
+                            (CicUtil.term_of_uri coer,
                              saturations2, arity2) [] [] univ
                         in
                         if (menv = []) then
                           HLog.warn "MENV non empty after composing coercions";
                         let o,univ = build_obj t univ arityres in
-                         (o,saturationsres,arityres),univ
+                         (o,saturationsres,arityres,cposres),univ
                     | _ -> assert false 
                   ) (first_step, CicUniv.oblivion_ugraph) tl
                 in
-                let name_src = CoercDb.name_of_carr src in
-                let name_tgt = CoercDb.name_of_carr tgt in
+                let name_src = CoercDb.string_of_carr src in
+                let name_tgt = CoercDb.string_of_carr tgt in
                 let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) l in
                 let name = mangle name_tgt name_src by in
                 let c_uri = 
                   number_if_already_defined baseuri name 
-                    (List.map (fun (_,_,u,_,_,_) -> u) acc) 
+                    (List.map (fun (_,_,u,_,_,_,_) -> u) acc) 
                 in
-                let named_obj,saturations,arity = 
+                let named_obj,saturations,arity,cpos = 
                   match o with
-                  | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity ->
-                      Cic.Constant (name,bo,ty,vl,attrs),saturations,arity
+                  | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity,cpos ->
+                      Cic.Constant (name,bo,ty,vl,attrs),saturations,arity,cpos
                   | _ -> assert false 
                 in
-                  (src,tgt,c_uri,saturations,named_obj,arity))::acc
+                  (src,tgt,c_uri,saturations,named_obj,arity,cpos)::acc
           with UnableToCompose -> acc
       ) [] todo_list
     in
@@ -490,7 +485,7 @@ CicCoercion.set_close_coercion_graph close_coercion_graph;;
 (* generate_composite (c2 (c1 s)) in the universe graph univ
  * both living in the same context and metasenv *)
 let generate_composite c1 c2 context metasenv univ sat1 sat2 =
- let a,b,c,_,_ =
+ let a,b,c,_,_,_ =
   generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ
  in
   a,b,c