X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=fd89f77c8f7e89744e7a745bd8ff16f5df094b79;hb=2e2648a9ed26d9b813de8e6a10e2776162565f09;hp=4dc20f77fa968ed961361a7449c69646d06b8037;hpb=b4670008138505f7462252c29eb755ab127862ba;p=helm.git diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 4dc20f77f..fd89f77c8 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 @@ -44,7 +48,7 @@ let uris_of_obj uri = innertypesuri,bodyuri,univgraphuri let paths_and_uris_of_obj uri = - let resolved = Http_getter.filename' ~writable:true uri in + let resolved = Http_getter.filename' ~local:true ~writable:true uri in let basepath = Filename.dirname resolved in let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in @@ -70,12 +74,28 @@ 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 = Cic2acic.plain_acic_object_of_cic_object obj in + 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, Some ids_to_inner_sorts, false + else + let annobj = Cic2acic.plain_acic_object_of_cic_object obj in + 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 - in + uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false + ~generate_attributes annobj + in let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri = paths_and_uris_of_obj uri @@ -88,6 +108,14 @@ let save_object_to_disk uri obj ugraph univlist = (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: (univgraphuri,xmlunivgraphpath) :: + (* now the optional inner types, both write and register *) + (match innertypes with + | None -> [] + | Some innertypesxml -> + write ensure_path_exists innertypespath; + write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath); + [innertypesuri, innertypespath] + ) @ (* now the optional body, both write and register *) (match bodyxml,bodyuri with None,_ -> [] @@ -100,7 +128,8 @@ let save_object_to_disk uri obj ugraph univlist = let typecheck_obj = let profiler = HExtlib.profile "add_obj.typecheck_obj" in - fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj + fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) + (Unshare.fresh_types obj) let index_obj = let profiler = HExtlib.profile "add_obj.index_obj" in @@ -111,7 +140,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 @@ -138,6 +167,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)) @@ -149,7 +183,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 = @@ -164,7 +198,7 @@ let remove_single_obj uri = List.iter (fun uri -> (try - let file = Http_getter.resolve' ~writable:true uri in + 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 _ -> ()); @@ -195,7 +229,7 @@ let generate_elimination_principles uri refinement_toolkit = List.iter remove_single_obj !uris; raise exn in - let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in + let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in match obj with | Cic.InductiveDefinition (indTypes, _, _, _) -> let counter = ref 0 in @@ -209,12 +243,37 @@ let generate_elimination_principles uri refinement_toolkit = let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; - CoercDb.remove_coercion (fun (_,_,u1) -> true) + 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 baseuri = +let add_coercion ~add_composites refinement_toolkit 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 @@ -227,7 +286,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = * should we saturate it with metas in case we insert it? * *) - let spline2list ty = + let spine2list ty = let rec aux = function | Cic.Prod( _, src, tgt) -> src::aux tgt | t -> [t] @@ -235,88 +294,98 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = aux ty in let src_carr, tgt_carr = - let list_remove_from_tail n l = - let rec aux n = function - | hd::tl when n > 0 -> aux (n-1) tl - | l when n = 0 -> l - | _ -> assert false + let get_classes arity saturations l = + (* this is the ackerman's function revisited *) + let rec aux = function + 0,0,None,tgt::src::_ -> src,Some (`Class tgt) + | 0,0,target,src::_ -> src,target + | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl) + | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl) + | arity,saturations,None,_::tl -> + aux (arity, saturations, Some `Funclass, tl) + | arity,saturations,target,_::tl -> + aux (arity - 1, saturations, target, tl) + | _ -> assert false in - aux n (List.rev l) + aux (arity,saturations,None,List.rev l) in - let types = spline2list coer_ty in - match arity, list_remove_from_tail arity types with - | 0,tgt::src::_ -> - (* if ~delta is true, it is impossible to define an identity coercion *) - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) - | n,_::src::_ -> - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), - CoercDb.Fun arity - | _ -> assert false + 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) 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 && + (fun u,_ -> + 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 unification can fail randomly."); + false)) ul) (CoercDb.to_list ()) in if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri);[]) + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); + UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]); + []) else let new_coercions = - CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri + CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations baseuri 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 + 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 + (* 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 = + List.fold_left + (fun acc (_,tgt,uri,saturations,obj,arity) -> + add_single_obj uri obj refinement_toolkit; + (uri,arity,saturations)::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,composite_uris); + (* + prerr_endline ("lemmas:"); + List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) + lemmas; + prerr_endline ("lemmas END");*) + lemmas ;; let remove_coercion uri = @@ -328,15 +397,16 @@ 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)) + (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..... *) + Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *) let generate_projections refinement_toolkit uri fields = @@ -348,9 +418,10 @@ let generate_projections refinement_toolkit uri fields = 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 ty, _ = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_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; @@ -358,15 +429,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) + saturations (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 (fun u,_,_ -> u) x end else [] @@ -395,36 +470,84 @@ 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 @ - 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; 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 =