X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FcloseCoercionGraph.ml;h=7ed3c36e6b86d24d4a46b753a750e11597d919c0;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=95b9fd6e04f04a100746d316a95059fe264eae15;hpb=864b6ef1956a312e5401a8705bcf7cf0cccf4e9f;p=helm.git diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml index 95b9fd6e0..7ed3c36e6 100644 --- a/components/tactics/closeCoercionGraph.ml +++ b/components/tactics/closeCoercionGraph.ml @@ -39,21 +39,33 @@ let get_closure_coercions src tgt uri coercions = 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 - CoercDb.eq_carr ?exact s t + let rc = CoercDb.eq_carr ?exact s t in + debug_print(lazy(string_of_bool rc)); + rc with - | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false + | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> + debug_print (lazy("false")); + false in match src,tgt with | CoercDb.Uri _, CoercDb.Uri _ -> + debug_print (lazy ("Uri, Uri4")); let c_from_tgt = List.filter - (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) + (fun (f,t,_) -> + + debug_print (lazy ("Uri, Uri3")); + eq_carr f tgt (*&& not (eq_carr t src)*)) coercions in let c_to_src = List.filter - (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) + (fun (f,t,_) -> + + debug_print (lazy ("Uri, Uri2")); + eq_carr t src (*&& not (eq_carr f tgt)*)) coercions in (HExtlib.flatten_map @@ -70,6 +82,7 @@ let get_closure_coercions src tgt uri coercions = (fun (_,t,u2l) -> HExtlib.flatten_map (fun u1 -> + debug_print (lazy ("Uri, Uri1")); if eq_carr ~exact:true s t || eq_carr ~exact:true s tgt || eq_carr ~exact:true src t @@ -122,8 +135,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= names in let compose c1 nc1 c2 nc2 = - Cic.Appl (CicSubstitution.lift 1 c2 :: mk_implicits (nc2 - sat2 - 1) @ - Cic.Appl (CicSubstitution.lift 1 c1 :: mk_implicits nc1 ) :: + Cic.Appl ((*CicSubstitution.lift 1*) c2 :: mk_implicits (nc2 - sat2 - 1) @ + Cic.Appl ((*CicSubstitution.lift 1*) c1 :: mk_implicits nc1 ) :: mk_implicits sat2) in let rec create_subst_from_metas_to_rels n = function @@ -205,8 +218,14 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= let meta_to_be_coerced = try match List.nth l_c1 (c1_pis - sat1 - 1) with - | Cic.Meta (i,_) -> i - | _ -> assert false + | Cic.Meta (i,_) -> Some i + | t -> + debug_print + (lazy("meta_to_be_coerced: " ^ CicPp.ppterm t)); + debug_print + (lazy("c1_pis: " ^ string_of_int c1_pis ^ + " sat1:" ^ string_of_int sat1)); + None with Failure _ -> assert false in @@ -230,15 +249,20 @@ 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 - debug_print - (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced)); - let position_of_meta_to_be_coerced = - 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)); - debug_print (lazy ("SATURATIONS: " ^ - string_of_int (List.length sorted - position_of_meta_to_be_coerced - 1))); - sorted, List.length sorted - position_of_meta_to_be_coerced - 1 + let saturations_res = + match meta_to_be_coerced with + | None -> 0 + | Some meta_to_be_coerced -> + debug_print + (lazy ("META_TO_BE_COERCED: " ^ string_of_int meta_to_be_coerced)); + let position_of_meta_to_be_coerced = + 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 + in + debug_print (lazy ("SATURATIONS: " ^ string_of_int saturations_res)); + sorted, saturations_res in let namer l n = let l = List.map (function Cic.Name s -> s | _ -> "A") l in @@ -270,6 +294,8 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= CicRefine.type_of_aux' metasenv context c univ in debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term)); + debug_print(lazy("COMPOSED REFINED (pretty): "^ + CicMetaSubst.ppterm_in_context [] ~metasenv term context)); (* let metasenv = order_metasenv metasenv in *) (* debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *) let body_metasenv, lambdas_metasenv = @@ -353,7 +379,7 @@ let filter_duplicates l coercions = try List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2 with - | Invalid_argument "List.for_all2" -> false) + | Invalid_argument "List.for_all2" -> debug_print (lazy("XXX")); false) coercions)) l @@ -404,6 +430,7 @@ 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 + debug_print (lazy("composed " ^ string_of_int (List.length todo_list))); let todo_list = filter_duplicates todo_list coercions in try let new_coercions = @@ -462,9 +489,9 @@ 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 sat2 = +let generate_composite c1 c2 context metasenv univ sat1 sat2 = let a,b,c,_,_ = - generate_composite' (c1,0,0) (c2,sat2,0) context metasenv univ + generate_composite' (c1,sat1,0) (c2,sat2,0) context metasenv univ in a,b,c ;;