X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FcloseCoercionGraph.ml;h=7ed3c36e6b86d24d4a46b753a750e11597d919c0;hb=b0a6c05decc9f0e731f70cfc5ae5350ae4046b79;hp=d558c0ef030e6a1af2ff864b243dc1af410637ea;hpb=83c41ad650a2736acf27ccae820923157283c6db;p=helm.git diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml index d558c0ef0..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 @@ -152,11 +165,40 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= | t -> t in let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in + let rec metas_of_term_and_types t = + let metas = CicUtil.metas_of_term t in + let types = + List.flatten + (List.map + (fun (i,_) -> try + let _,_,ty = CicUtil.lookup_meta i body_metasenv in metas_of_term_and_types ty + with CicUtil.Meta_not_found _ -> []) + metas) + in + metas @ types + in + let sorted_metas_of_term world t = + let metas = metas_of_term_and_types t in + (* this check should be useless *) + let metas = List.filter (fun (i,_)->List.exists (fun (j,_,_) -> j=i) world) metas in + let order_metas metasenv metas = + let module OT = struct type t = int let compare = Pervasives.compare end in + let module S = HTopoSort.Make (OT) in + let dep i = + try + let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in + let metas = List.map fst (CicUtil.metas_of_term ty) in + HExtlib.list_uniq (List.sort Pervasives.compare metas) + with Not_found -> [] + in + S.topological_sort (List.map (fun (i,_) -> i) metas) dep + in + order_metas world metas + in let metas_that_saturate l = List.fold_left (fun (acc,n) t -> - let metas = CicUtil.metas_of_term t in - let metas = List.map fst metas in + let metas = sorted_metas_of_term body_metasenv t in let metas = List.filter (fun i -> List.for_all (fun (j,_) -> j<>i) acc) metas in let metas = List.map (fun i -> i,n) metas in @@ -176,12 +218,24 @@ 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 - let meta2no = fst (metas_that_saturate (l_c2_b @ l_c1 @ l_c2_a)) in + (* BIG HACK ORRIBLE: + * it should be (l_c2_b @ l_c1 @ l_c2_a), but in this case sym (eq_f) gets + * \A,B,f,x,y,Exy and not \B,A,f,x,y,Exy + * as an orrible side effect, the other composites get a type lyke + * \A,x,y,Exy,B,f with 2 saturations + *) + let meta2no = fst (metas_that_saturate (l_c1 @ l_c2_b @ l_c2_a)) in let sorted = List.sort (fun (i,ctx1,ty1) (j,ctx1,ty1) -> @@ -195,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 @@ -235,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 = @@ -318,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 @@ -369,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 = @@ -427,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 ;;