X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=185ae53158f7cff7061382b12fbbc7f89f2974aa;hb=d43b4cfa41256e90fceb0129b7eadb38207190c3;hp=5189547d33135903df0731105a50fa99041b2f91;hpb=aaf1c6a4f2e56d08433e2258da4d4cc51c943e4e;p=helm.git diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 5189547d3..185ae5315 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -25,17 +25,32 @@ (* $Id$ *) +let object_declaration_hook = ref [] +let add_object_declaration_hook f = + object_declaration_hook := f :: !object_declaration_hook + exception AlreadyDefined of UriManager.uri -let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 +type coercion_decl = + UriManager.uri -> int (* arity *) -> + int (* saturations *) -> string (* baseuri *) -> + UriManager.uri list (* lemmas (new objs) *) -(* uri |--> (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib) - * - * in case of remove_coercion uri, the first component is removed from the - * coercion DB, while the second is passed to remove_obj (and is not [] only if - * add_coercion is called with add_composites - * *) -let coercion_hashtbl = UriManager.UriHashtbl.create 3 + +let stack = ref [];; + +let push () = + stack := CoercDb.dump () :: !stack; + CoercDb.restore CoercDb.empty_coerc_db; +;; + +let pop () = + match !stack with + | [] -> raise (Failure "Unable to POP from librarySync.ml") + | db :: tl -> + stack := tl; + CoercDb.restore db; +;; let uris_of_obj uri = let innertypesuri = UriManager.innertypesuri_of_uri uri in @@ -70,24 +85,27 @@ let save_object_to_disk uri obj ugraph univlist = HExtlib.mkdir dir in (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) - let annobj, innertypes = - if Helm_registry.get_bool "matita.system" then - let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ = + let annobj, innertypes, ids_to_inner_sorts, generate_attributes = + if Helm_registry.get_bool "matita.system" && + not (Helm_registry.get_bool "matita.noinnertypes") + then + let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ = Cic2acic.acic_object_of_cic_object obj in let innertypesxml = Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false in - annobj, Some innertypesxml + annobj, Some innertypesxml, Some ids_to_inner_sorts, false else let annobj = Cic2acic.plain_acic_object_of_cic_object obj in - annobj, None + annobj, None, None, true in (* prepare XML *) let xml, bodyxml = Cic2Xml.print_object - uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj + uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false + ~generate_attributes annobj in let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri = @@ -128,32 +146,41 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_single_obj uri obj refinement_toolkit = - let module RT = RefinementTool in +let remove_obj uri = + let derived_uris_of_uri uri = + let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in + innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) + in + let uris_to_remove = + if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri] + in + let files_to_remove = uri :: derived_uris_of_uri uri in + List.iter + (fun uri -> + (try + let file = Http_getter.resolve' ~local:true ~writable:true uri in + HExtlib.safe_remove file; + HExtlib.rmdir_descend (Filename.dirname file) + with Http_getter_types.Key_not_found _ -> ()); + ) files_to_remove ; + List.iter (fun uri -> ignore (LibraryDb.remove_uri uri)) uris_to_remove ; + CicEnvironment.remove_obj uri +;; + +let rec add_obj uri obj ~pack_coercion_obj = let obj = - if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) - not (CoercDb.is_a_coercion' (Cic.Const (uri, []))) - then - refinement_toolkit.RT.pack_coercion_obj obj - else - obj + if CoercDb.is_a_coercion (Cic.Const (uri, [])) = None + then pack_coercion_obj obj + else obj in let dbd = LibraryDb.instance () in - if CicEnvironment.in_library uri then - raise (AlreadyDefined uri) - else begin - (*CicUniv.reset_spent_time (); - let before = Unix.gettimeofday () in*) + if CicEnvironment.in_library uri then raise (AlreadyDefined uri); + begin (* ATOMIC *) typecheck_obj uri obj; (* 1 *) - (*let after = Unix.gettimeofday () in - let univ_time = CicUniv.get_spent_time () in - let total_time = after -. before in - prerr_endline - (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" - (univ_time *. 100. /. total_time) (total_time) (univ_time) - (UriManager.name_of_uri uri));*) - let _, ugraph, univlist = - CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in + let obj, ugraph, univlist = + try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri + with CicEnvironment.Object_not_found _ -> assert false + in try index_obj ~dbd ~uri; (* 2 must be in the env *) try @@ -171,73 +198,32 @@ let add_single_obj uri obj refinement_toolkit = with exc -> CicEnvironment.remove_obj uri; (* -1 *) raise exc - end - -let remove_single_obj uri = - let derived_uris_of_uri uri = - let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in - innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) - in - let uris_to_remove = - if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri] - in - let files_to_remove = uri :: derived_uris_of_uri uri in - List.iter - (fun uri -> - (try - let file = Http_getter.resolve' ~local:true ~writable:true uri in - HExtlib.safe_remove file; - HExtlib.rmdir_descend (Filename.dirname file) - with Http_getter_types.Key_not_found _ -> ()); - ) files_to_remove ; - List.iter - (fun uri -> - ignore (LibraryDb.remove_uri uri); - (*CoercGraph.remove_coercion uri;*) - ) uris_to_remove ; - CicEnvironment.remove_obj uri - -(*** GENERATION OF AUXILIARY LEMMAS ***) - -let generate_elimination_principles uri refinement_toolkit = - let uris = ref [] in - let elim i = - let elim sort = - try - let uri,obj = CicElim.elim_of ~sort uri i in - add_single_obj uri obj refinement_toolkit; - uris := uri :: !uris - with CicElim.Can_t_eliminate -> () - in - try - List.iter - elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - with exn -> - List.iter remove_single_obj !uris; - raise exn - in - let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in - match obj with - | Cic.InductiveDefinition (indTypes, _, _, _) -> - let counter = ref 0 in - List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes; - !uris - | _ -> - failwith (Printf.sprintf "not an inductive definition (%s)" - (UriManager.string_of_uri uri)) - -(* COERCIONS ***********************************************************) - -let remove_all_coercions () = - UriManager.UriHashtbl.clear coercion_hashtbl; - CoercDb.remove_coercion (fun (_,_,_,_) -> true) + end; + let added = ref [] in + let add_obj_with_parachute u o = + added := u :: !added; + add_obj u o ~pack_coercion_obj in + let old_db = CoercDb.dump () in + try + List.fold_left + (fun lemmas f -> + f ~add_obj:add_obj_with_parachute + ~add_coercion:(add_coercion ~add_composites:true ~pack_coercion_obj) + uri obj @ lemmas) + [] !object_declaration_hook + with exn -> + List.iter remove_obj !added; + remove_obj uri; + CoercDb.restore old_db; + raise exn + (* /ATOMIC *) -let add_coercion ~add_composites refinement_toolkit uri arity saturations - baseuri +and + add_coercion ~add_composites ~pack_coercion_obj uri arity saturations baseuri = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in - CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph + CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph in (* we have to get the source and the tgt type uri * in Coq syntax we have already their names, but @@ -257,7 +243,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations in aux ty in - let src_carr, tgt_carr = + let src_carr, tgt_carr, no_args = let get_classes arity saturations l = (* this is the ackerman's function revisited *) let rec aux = function @@ -275,248 +261,114 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations in let types = spine2list coer_ty in let src,tgt = get_classes arity saturations types in - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), - match tgt with - None -> assert false - | Some `Funclass -> CoercDb.Fun arity - | Some (`Class tgt) -> - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src) 0, + (match tgt with + | None -> assert false + | Some `Funclass -> CoercDb.coerc_carr_of_term (Cic.Implicit None) arity + | Some (`Class tgt) -> + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) 0), + List.length types - 1 in let already_in_obj src_carr tgt_carr uri obj = List.exists (fun (s,t,ul) -> + if not (CoercDb.eq_carr s src_carr && + CoercDb.eq_carr t tgt_carr) + then false + else List.exists - (fun u,_ -> - let bo = + (fun u,_,_ -> + let bo, ty = match obj with - | Cic.Constant (_, Some bo, _, _, _) -> bo - | _ -> assert false + | Cic.Constant (_, Some bo, ty, _, _) -> bo, ty + | _ -> + (* this is not a composite coercion, thus the uri is valid *) + let bo = CicUtil.term_of_uri uri in + bo, + fst (CicTypeChecker.type_of_aux' [] [] bo + CicUniv.oblivion_ugraph) + in + let are_body_convertible = + fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo + CicUniv.oblivion_ugraph) in - CoercDb.eq_carr s src_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 + if not are_body_convertible then + (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 unification can fail randomly."); - false)) + UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri + uri^" are not convertible, but are between the same nodes.\n"^ + "From now on unification can fail randomly."); + false) + else + match t, tgt_carr with + | CoercDb.Sort (Cic.Type i), CoercDb.Sort (Cic.Type j) + | CoercDb.Sort (Cic.CProp i), CoercDb.Sort (Cic.CProp j) + when not (CicUniv.eq i j) -> + (HLog.warn + ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ + "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ + "different universe : " ^ + CicUniv.string_of_universe j ^ " <> " ^ + CicUniv.string_of_universe i); false) + | CoercDb.Sort Cic.Prop , CoercDb.Sort Cic.Prop + | CoercDb.Sort (Cic.Type _) , CoercDb.Sort (Cic.Type _) + | CoercDb.Sort (Cic.CProp _), CoercDb.Sort (Cic.CProp _) -> + (HLog.warn + ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^ + "it is a duplicate of " ^ UriManager.string_of_uri u); + true) + | CoercDb.Sort s1, CoercDb.Sort s2 -> + (HLog.warn + ("Coercion " ^ UriManager.string_of_uri uri ^ " has the same " ^ + "body of " ^ UriManager.string_of_uri u ^ " but lives in a " ^ + "different universe : " ^ + CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ + CicPp.ppterm (Cic.Sort s2)); false) + | _ -> + let ty', _ = + CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) + CicUniv.oblivion_ugraph + in + if CicUtil.alpha_equivalence ty ty' then + (HLog.warn + ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^ + "it is a duplicate of " ^ UriManager.string_of_uri u); + true) + else false + + ) ul) - (CoercDb.to_list ()) + (CoercDb.to_list (CoercDb.dump ())) in + let cpos = no_args - arity - saturations - 1 in if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[]) + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); []) else + let _ = + if already_in_obj src_carr tgt_carr uri + (fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri)) then + raise (AlreadyDefined uri); + in let new_coercions = CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations baseuri in let new_coercions = - List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj)) + 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 (* update the DB *) - List.iter - (fun (src,tgt,uri,saturations,_,_) -> - CoercDb.add_coercion (src,tgt,uri,saturations)) - new_coercions; - CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); - (* add the composites obj and they eventual lemmas *) let lemmas = - if add_composites then - List.fold_left - (fun acc (_,tgt,uri,saturations,obj,arity) -> - add_single_obj uri obj refinement_toolkit; - (uri,arity,saturations)::acc) - [] new_coercions - else - [] + List.fold_left + (fun acc (src,tgt,uri,saturations,obj,arity,cpos) -> + CoercDb.add_coercion (src,tgt,uri,saturations,cpos); + let acc = add_obj uri obj pack_coercion_obj @ uri::acc in + acc) + [] new_coercions 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");*) + CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations, cpos); +(* CoercDb.prefer uri; *) lemmas ;; -let remove_coercion uri = - try - let (composites_in_db, composites_in_lib) = - UriManager.UriHashtbl.find coercion_hashtbl uri - in - (*prerr_endline ("removing: " ^UriManager.string_of_uri uri); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composites_in_db;*) - UriManager.UriHashtbl.remove coercion_hashtbl uri; - CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u); - (* remove from the DB *) - List.iter - (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1)) - composites_in_db; - (* remove composites from the lib *) - List.iter remove_single_obj composites_in_lib - with - Not_found -> () (* mhh..... *) - -let generate_projections refinement_toolkit uri fields = - let uris = ref [] in - let projections = - CicRecord.projections_of uri - (List.map (fun (x,_,_) -> x) fields) - in - try - List.iter2 - (fun (uri, name, bo) (_name, coercion, arity) -> - let saturations = 0 in - try - let ty, ugraph = - CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in - let attrs = [`Class `Projection; `Generated] in - let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj uri obj refinement_toolkit; - let composites = - 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 - saturations (UriManager.buri_of_uri uri) - in -(*prerr_endline ("are: "); - List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; - prerr_endline "---"; -*) - (*CSC: I throw the arity away. See comment above *) - List.map (fun u,_,_ -> u) x - end - else - [] - in - uris := uri :: composites @ !uris - with - CicTypeChecker.TypeCheckerFailure s -> - HLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s); - | CicEnvironment.Object_not_found uri -> - let depend = UriManager.name_of_uri uri in - HLog.message - ("Unable to create projection " ^ name ^ " because it requires " ^ - depend) - ) projections fields; - !uris - with exn -> - List.iter remove_single_obj !uris; - raise exn - -let build_inversion_principle = ref (fun a b -> assert false);; - -let generate_inversion refinement_toolkit uri obj = - List.map - (fun (ind_uri,ind_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 @ - generate_elimination_principles uri refinement_toolkit; - uris := !uris @ generate_inversion refinement_toolkit uri obj; - let rec get_record_attrs = - function - | [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in - (match get_record_attrs attrs with - | None -> () (* not a record *) - | Some fields -> - uris := !uris @ - (generate_projections refinement_toolkit uri fields)) - | Cic.CurrentProof _ - | Cic.Variable _ -> assert false - end; - UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; - !uris - with - | exn when not_debug -> - List.iter remove_single_obj !uris; - raise exn - -let remove_obj uri = - let uris = - try - let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in - UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri; - res - with - Not_found -> [] (*assert false*) - in - List.iter remove_single_obj (uri::uris) -