X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=203f78869b33aac4e75c65bb8355e9d9ea485c5d;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=9b08ba6dc5a662dcc0f6dd2865f686ad7374a4f9;hpb=81cb773cbc402fc74752fb69a436b25be49489ee;p=helm.git diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 9b08ba6dc..203f78869 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -25,6 +25,10 @@ (* $Id$ *) +let object_declaration_hook = ref (fun _ _ -> ());; +let set_object_declaration_hook f = + object_declaration_hook := f + exception AlreadyDefined of UriManager.uri let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 @@ -71,7 +75,9 @@ let save_object_to_disk uri obj ugraph univlist = in (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) let annobj, innertypes, ids_to_inner_sorts, generate_attributes = - if Helm_registry.get_bool "matita.system" then + 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 @@ -160,6 +166,11 @@ let add_single_obj uri obj refinement_toolkit = try (*3*) let new_stuff = save_object_to_disk uri obj ugraph univlist in + (* EXPERIMENTAL: pretty print the object in natural language *) + (try !object_declaration_hook uri obj + with exc -> + prerr_endline ("Error: object_declaration_hook failed"^ + Printexc.to_string exc)); try HLog.message (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) @@ -233,6 +244,29 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,_,_) -> true) +let stack = ref [];; + +let h2l h = + UriManager.UriHashtbl.fold + (fun k v acc -> (k,v) :: acc) h [] +;; + +let push () = + stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack; + remove_all_coercions () +;; + +let pop () = + match !stack with + | [] -> raise (Failure "Unable to POP from librarySync.ml") + | (db,h) :: tl -> + stack := tl; + remove_all_coercions (); + CoercDb.restore db; + List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v) + h +;; + let add_coercion ~add_composites refinement_toolkit uri arity saturations baseuri = @@ -308,7 +342,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations (CoercDb.to_list ()) in if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[]) + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]); + []) else let new_coercions = CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations @@ -327,14 +363,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations 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 - [] 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 *) @@ -344,8 +377,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations 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 []); + UriManager.UriHashtbl.add + coercion_hashtbl uri (composite_uris,composite_uris); (* prerr_endline ("lemmas:"); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) @@ -363,7 +396,8 @@ let remove_coercion 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); + 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)) @@ -371,7 +405,7 @@ let remove_coercion uri = (* remove composites from the lib *) List.iter remove_single_obj composites_in_lib with - Not_found -> () (* mhh..... *) + Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *) let generate_projections refinement_toolkit uri fields = @@ -485,21 +519,25 @@ let add_obj refinement_toolkit uri obj = 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.InductiveDefinition (inductivefuns,_,_,attrs) -> + let _,inductive,_,_ = List.hd inductivefuns in + if inductive then + begin + uris := !uris @ + generate_elimination_principles uri refinement_toolkit; + uris := !uris @ generate_inversion refinement_toolkit uri obj; + end ; + 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;