From 143c10b37e360a1d115904c46a954e86904ee203 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 8 Sep 2007 23:41:54 +0000 Subject: [PATCH] the order of abstraction is now correct, but there is an orrible hack to make eq_OF_eq have the right type. --- .../components/tactics/closeCoercionGraph.ml | 41 +++++++++++++++++-- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index d558c0ef0..95b9fd6e0 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -152,11 +152,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 @@ -181,7 +210,13 @@ let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= 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) -> -- 2.39.2