X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=83f861b4ef6b790e6d92a48ac9f040ff562bf80c;hb=efdf796669355e4e326da2069f7aa57c4778beb8;hp=a3429840b7b2e169c835c753529de9e4cabed0e3;hpb=4b98f68b964c9f87868c445e794bc745a99d5b17;p=helm.git diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index a3429840b..83f861b4e 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -111,7 +111,7 @@ let add_single_obj uri obj refinement_toolkit = let module RT = RefinementTool in let obj = if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) - not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) + not (CoercDb.is_a_coercion' (Cic.Const (uri, []))) then refinement_toolkit.RT.pack_coercion_obj obj else @@ -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 = @@ -173,8 +173,8 @@ let remove_single_obj uri = (fun uri -> ignore (LibraryDb.remove_uri uri); (*CoercGraph.remove_coercion uri;*) - CicEnvironment.remove_obj uri - ) uris_to_remove + ) uris_to_remove ; + CicEnvironment.remove_obj uri (*** GENERATION OF AUXILIARY LEMMAS ***) @@ -211,7 +211,7 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,u1) -> true) -let add_coercion ~add_composites refinement_toolkit uri arity = +let add_coercion ~add_composites refinement_toolkit uri arity baseuri = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -254,14 +254,27 @@ let add_coercion ~add_composites refinement_toolkit uri arity = 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 @@ -270,52 +283,46 @@ let add_coercion ~add_composites refinement_toolkit uri arity = else let new_coercions = 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 (_,_,uri,obj) -> - add_single_obj uri obj refinement_toolkit; - uri::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 = @@ -357,14 +364,19 @@ let generate_projections refinement_toolkit uri fields = if coercion then begin (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*) + (*CSC: I think there is a bug here. The composite coercions + are not remembered in the .moo file. Thus they are re-generated + every time. Right? *) let x = add_coercion ~add_composites:true refinement_toolkit uri arity + (UriManager.buri_of_uri uri) in (*prerr_endline ("are: "); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; prerr_endline "---"; *) - x + (*CSC: I throw the arity away. See comment above *) + List.map fst x end else [] @@ -393,12 +405,54 @@ 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 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 @