X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=e621a7a0cf1311ef26319e7363714db36fce5383;hb=936f80cf031a7b034dd70fef49abb90e69f2e680;hp=4e64e6badc369c21d92e83d96c9719a4d72f1caa;hpb=81911249f5f2a6ca774f98a19cd1a34bf1dde384;p=helm.git diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 4e64e6bad..e621a7a0c 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -149,7 +149,7 @@ let add_single_obj uri obj refinement_toolkit = raise exc with exc -> CicEnvironment.remove_obj uri; (* -1 *) - raise exc + raise exc end let remove_single_obj uri = @@ -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 = @@ -400,12 +405,55 @@ let generate_inversion refinement_toolkit uri obj = add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri) (!build_inversion_principle uri obj) +let + generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid += + function + Cic.Fix (_,funs) -> + snd ( + List.fold_right + (fun (name,idx,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n+1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.Fix (n,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + (n+1,uri::uris) + ) funs (1,[])) + | Cic.CoFix (_,funs) -> + snd ( + List.fold_right + (fun (name,ty,bo) (n,uris) -> + if name = name_to_avoid then + (n+1,uris) + else + let uri = + UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in + let bo = Cic.CoFix (n,funs) in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + add_single_obj uri obj refinement_toolkit; + (n+1,uri::uris) + ) funs (1,[])) + | _ -> assert false + let add_obj refinement_toolkit uri obj = add_single_obj uri obj refinement_toolkit; let uris = ref [] in + let not_debug = not (Helm_registry.get_bool "matita.debug") in try begin match obj with + | Cic.Constant (name,Some bo,_,_,attrs) when + List.mem (`Flavour `MutualDefinition) attrs -> + uris := + !uris @ + generate_sibling_mutual_definitions refinement_toolkit uri attrs + name bo | Cic.Constant _ -> () | Cic.InductiveDefinition (_,_,_,attrs) -> uris := !uris @ @@ -427,9 +475,10 @@ let add_obj refinement_toolkit uri obj = end; UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; !uris - with exn -> - List.iter remove_single_obj !uris; - raise exn + with + | exn when not_debug -> + List.iter remove_single_obj !uris; + raise exn let remove_obj uri = let uris =