From: Enrico Tassi Date: Fri, 5 Jan 2007 11:36:41 +0000 (+0000) Subject: Added check for duplicate (convertible) composite coercions, X-Git-Tag: 0.4.95@7852~681 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=40a6a2eb15bc50a7fe8f47704ea0244bc9d18ef5;p=helm.git Added check for duplicate (convertible) composite coercions, that are not added anymore. Nicer api for meets used by unification. --- diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index a7a3a1674..912ae1e8e 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -628,51 +628,44 @@ let res = metasenv (C.Appl l1) (C.Appl l2) ugraph | _ -> raise exn) else - let meets = CoercGraph.meets car1 car2 in + let meets = + CoercGraph.meets metasenv subst context car1 car2 + in (match meets with | [] -> raise exn - | _::_::_ -> -prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); -let m1::m2::_ = meets in -prerr_endline ("M1 = " ^ CoercDb.name_of_carr m1 ^ "\nM2 = " ^ CoercDb.name_of_carr m2); -assert false - | [m] -> + | (carr,metasenv,to1,to2)::xxx -> + (match xxx with + [] -> () + | (m2,_,c2,c2')::_ -> + let m1,_,c1,c1' = carr,metasenv,to1,to2 in + let unopt = + function Some (_,t) -> CicPp.ppterm t + | None -> "id" + in + HLog.warn + ("There are two minimal joins of "^ + CoercDb.name_of_carr car1^" and "^ + CoercDb.name_of_carr car2^": " ^ + CoercDb.name_of_carr m1 ^ " via "^unopt c1^" + "^ + unopt c1'^" and " ^ CoercDb.name_of_carr m2^" via "^ + unopt c2^" + "^unopt c2')); let last_tl1',(subst,metasenv,ugraph) = - match last_tl1 with - | Cic.Meta (i1,l1) - when not (CoercDb.eq_carr m car1) -> - (match - CoercGraph.look_for_coercion' metasenv subst - context m car1 - with - | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_) - -> - last, - fo_unif_subst test_equality_only subst context + match last_tl1,to1 with + | Cic.Meta (i1,l1),Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context metasenv coerced last_tl1 ugraph - | _ -> -prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); -assert false) - | _ -> last_tl1,(subst,metasenv,ugraph) in + | _ -> last_tl1,(subst,metasenv,ugraph) + in let last_tl2',(subst,metasenv,ugraph) = - match last_tl2 with - Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) -> - (match - CoercGraph.look_for_coercion' metasenv subst - context m car2 - with - (*CSC: bu here: I am considering only the first one*) - | CoercGraph.SomeCoercion ((metasenv,last,coerced)::_) - -> - last, - fo_unif_subst test_equality_only subst context + match last_tl2,to2 with + | Cic.Meta (i2,l2),Some (last,coerced) -> + last, + fo_unif_subst test_equality_only subst context metasenv coerced last_tl2 ugraph - | _ -> -prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); -assert false) - | _ -> last_tl2,(subst,metasenv,ugraph) + | _ -> last_tl2,(subst,metasenv,ugraph) in -(*DEBUGGING ONLY: + (*DEBUGGING ONLY: prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); *) let subst,metasenv,ugraph = diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml index 70e90af52..37ded8ee0 100644 --- a/components/cic_unification/coercGraph.ml +++ b/components/cic_unification/coercGraph.ml @@ -39,6 +39,30 @@ type coercion_search_result = let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () +let saturate_coercion ul metasenv subst context = + let cl = List.map CicUtil.term_of_uri ul in + let funclass_arityl = + let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in + List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl + in + let freshmeta = CicMkImplicit.new_meta metasenv subst in + List.map2 + (fun arity c -> + let ty,_ = + CicTypeChecker.type_of_aux' ~subst metasenv context c + CicUniv.empty_ugraph in + let _,metasenv,args,lastmeta = + TermUtil.saturate_term freshmeta metasenv context ty arity in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + metasenv, Cic.Meta (lastmeta-1,irl), + match args with + [] -> c + | _ -> Cic.Appl (c::args) + ) funclass_arityl cl +;; + (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion' metasenv subst context src tgt = try @@ -64,31 +88,7 @@ let look_for_coercion' metasenv subst context src tgt = in (match uri with None -> NoCoercion - | Some ul -> - let cl = List.map CicUtil.term_of_uri ul in - let funclass_arityl = - let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in - List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl - in - let freshmeta = CicMkImplicit.new_meta metasenv subst in - let newtl = - List.map2 - (fun arity c -> - let ty,_ = - CicTypeChecker.type_of_aux' ~subst metasenv context c - CicUniv.empty_ugraph in - let _,metasenv,args,lastmeta = - TermUtil.saturate_term freshmeta metasenv context ty arity in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - metasenv, Cic.Meta (lastmeta-1,irl), - match args with - [] -> c - | _ -> Cic.Appl (c::args) - ) funclass_arityl cl - in - SomeCoercion newtl) + | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) with | CoercDb.EqCarrNotImplemented s -> NotHandled s | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed @@ -150,51 +150,114 @@ let is_composite t = with Invalid_argument _ -> false ;; -let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);; +let coerced_arg l = + match l with + | [] | [_] -> assert false + | c::_ when not (CoercDb.is_a_coercion' c) -> assert false + | c::tl -> + let arity = + match CoercDb.is_a_coercion_to_funclass c with None -> 0 | Some a -> a + in + (* decide a decent structure for coercion carriers so that all this stuff is + * useless *) + let pi = + (* this calculation is not complete, since we have strange carriers *) + let rec count_pi = function + | Cic.Prod(_,_,t) -> 1+ (count_pi t) + | _ -> 0 + in + let uri = CicUtil.uri_of_term c in + match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + | Cic.Constant (_, _, ty, _, _) -> count_pi ty + | _ -> assert false + in + try Some (List.nth tl (pi - arity)) with Invalid_argument _ -> None +;; + +(************************* meet calculation stuff ********************) +let eq_uri_opt u1 u2 = + match u1,u2 with + | Some u1, Some u2 -> UriManager.eq u1 u2 + | None,Some _ | Some _, None -> false + | None, None -> true +;; + +let eq_carr_uri (c1,u1) (c2,u2) = CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2;; + +let eq_carr_uri_uri (c1,u1,u11) (c2,u2,u22) = + CoercDb.eq_carr c1 c2 && eq_uri_opt u1 u2 && eq_uri_opt u11 u22 +;; + +let uniq = HExtlib.list_uniq ~eq:eq_carr_uri;; + +let uniq2 = HExtlib.list_uniq ~eq:eq_carr_uri_uri;; -let splat e l = List.map (fun x -> e, x) l;; +let splat e l = List.map (fun x -> e, Some x) l;; +(* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_to carr = let l = CoercDb.to_list () in - List.flatten - (HExtlib.filter_map - (fun (src,tgt,cl) -> - if CoercDb.eq_carr tgt carr then Some (splat src cl) else None) - l) + let splat_coercion_to carr (src,tgt,cl) = + if CoercDb.eq_carr tgt carr then Some (splat src cl) else None + in + let l = List.flatten (HExtlib.filter_map (splat_coercion_to carr) l) in + l ;; +(* : carr -> (carr * uri option) where the option is always Some *) let get_coercions_from carr = let l = CoercDb.to_list () in - List.flatten - (HExtlib.filter_map - (fun (src,tgt,cl) -> - if CoercDb.eq_carr src carr then Some (splat tgt cl) else None) - l) + let splat_coercion_from carr (src,tgt,cl) = + if CoercDb.eq_carr src carr then Some (splat tgt cl) else None + in + List.flatten (HExtlib.filter_map (splat_coercion_from carr) l) ;; +(* intersect { (s1,u1) | u1:s1->t1 } { (s2,u2) | u2:s2->t2 } + * gives the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } *) let intersect l1 l2 = - let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in - uniq (List.filter is_in_l1 l2) + let is_in_l1 (x,u2) = + HExtlib.filter_map + (fun (src,u1) -> + if CoercDb.eq_carr x src then Some (src,u1,u2) else None) + l1 + in + uniq2 (List.flatten (List.map is_in_l1 l2)) ;; -let grow s = - uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s) +(* grow tgt gives all the (src,u) such that u:tgt->src *) +let grow tgt = + uniq ((tgt,None)::(get_coercions_to tgt)) ;; -let lb c = +let lb (c,_,_) = let l = get_coercions_from c in - function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l + fun (x,_,_) -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l ;; +(* given the set { (s,u1,u2) | u1:s->t1 /\ u2:s->t2 } removes the elements + * (s,_,_) such that (s',_,_) is in the set and there exists a coercion s->s' *) let rec min acc = function | c::tl -> if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl | [] -> acc ;; -let meets left right = - let u = UriManager.uri_of_string "cic:/foo.con" in - min [] (List.map fst (intersect (grow [left,u]) (grow [right,u]))) +let meets metasenv subst context left right = + let saturate metasenv uo = + match uo with + | None -> metasenv, None + | Some u -> + match saturate_coercion [u] metasenv subst context with + | [metasenv, sat, last] -> metasenv, Some (sat, last) + | _ -> assert false + in + List.map + (fun (c,uo1,uo2) -> + let metasenv, uo1 = saturate metasenv uo1 in + let metasenv, uo2 = saturate metasenv uo2 in + c,metasenv, uo1, uo2) + (min [] (intersect (grow left) (grow right))) ;; (* EOF *) diff --git a/components/cic_unification/coercGraph.mli b/components/cic_unification/coercGraph.mli index 62e484499..ae2bd9233 100644 --- a/components/cic_unification/coercGraph.mli +++ b/components/cic_unification/coercGraph.mli @@ -52,7 +52,13 @@ val source_of: Cic.term -> Cic.term val generate_dot_file: unit -> string +(* given the Appl contents returns the argument of the head coercion *) +val coerced_arg: Cic.term list -> Cic.term option + +(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *) val meets : + Cic.metasenv -> Cic.substitution -> Cic.context -> CoercDb.coerc_carr -> CoercDb.coerc_carr -> - CoercDb.coerc_carr list + (CoercDb.coerc_carr * Cic.metasenv * + (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 4e64e6bad..a4908ce7c 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -254,14 +254,27 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = CoercDb.Fun arity | _ -> assert false in - let already_in = + let already_in_obj src_carr tgt_carr uri obj = List.exists (fun (s,t,ul) -> List.exists (fun u -> - UriManager.eq u uri && + let bo = + match obj with + | Cic.Constant (_, Some bo, _, _, _) -> bo + | _ -> assert false + in CoercDb.eq_carr s src_carr && - CoercDb.eq_carr t tgt_carr) + CoercDb.eq_carr t tgt_carr && + if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo + CicUniv.oblivion_ugraph) + then true else + (HLog.warn + ("Coercions " ^ + UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri + uri^" are not convertible, but are between the same nodes.\n"^ + "From now on nification can fail randomly."); + false)) ul) (CoercDb.to_list ()) in @@ -272,52 +285,44 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri baseuri in + let new_coercions = + List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj)) + new_coercions + in let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in - if already_in then - (* this if starts here just to be sure the closure function works fine *) - begin - assert (new_coercions = []); - HLog.warn - (UriManager.string_of_uri uri ^ - " is already declared as a coercion! skipping..."); - [] - end - else - begin - (* update the DB *) - List.iter - (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) - new_coercions; - CoercDb.add_coercion (src_carr, tgt_carr, uri); - (* add the composites obj and they eventual lemmas *) - let lemmas = - if add_composites then - List.fold_left - (fun acc (_,tgt,uri,obj) -> - add_single_obj uri obj refinement_toolkit; - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in - (uri,arity)::acc) - [] new_coercions - else - [] - in - (* store that composite_uris are related to uri. the first component is - * the stuff in the DB while the second is stuff for remove_obj *) - (* - prerr_endline ("adding: " ^ - string_of_bool add_composites ^ UriManager.string_of_uri uri); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composite_uris; - *) - UriManager.UriHashtbl.add coercion_hashtbl uri - (composite_uris,if add_composites then composite_uris else []); - (* - prerr_endline ("lemmas:"); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - lemmas; - prerr_endline ("lemmas END");*) - lemmas - end + (* update the DB *) + List.iter + (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) + new_coercions; + CoercDb.add_coercion (src_carr, tgt_carr, uri); + (* add the composites obj and they eventual lemmas *) + let lemmas = + if add_composites then + List.fold_left + (fun acc (_,tgt,uri,obj) -> + add_single_obj uri obj refinement_toolkit; + let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in + (uri,arity)::acc) + [] new_coercions + else + [] + in + (* store that composite_uris are related to uri. the first component is + * the stuff in the DB while the second is stuff for remove_obj *) + (* + prerr_endline ("adding: " ^ + string_of_bool add_composites ^ UriManager.string_of_uri uri); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + composite_uris; + *) + UriManager.UriHashtbl.add coercion_hashtbl uri + (composite_uris,if add_composites then composite_uris else []); + (* + prerr_endline ("lemmas:"); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + lemmas; + prerr_endline ("lemmas END");*) + lemmas ;; let remove_coercion uri =