X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=a3429840b7b2e169c835c753529de9e4cabed0e3;hb=4f9820060bce92cfdb862b3c699e96c20c64a051;hp=e1b73821bc6176014ca5c55bb30474858b126f30;hpb=e09745b16df1d7a897cddfb6a79b8f8572de1380;p=helm.git diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index e1b73821b..a3429840b 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -157,40 +157,53 @@ let remove_single_obj uri = let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u]) in - let to_remove = - uri :: - (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @ - derived_uris_of_uri uri - 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' ~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 -> - (try - let file = Http_getter.resolve' ~writable:true uri in - HExtlib.safe_remove file; - HExtlib.rmdir_descend (Filename.dirname file) - with Http_getter_types.Key_not_found _ -> ()); - ignore (LibraryDb.remove_uri uri); - (*CoercGraph.remove_coercion uri;*) - CicEnvironment.remove_obj uri) - to_remove + (fun uri -> + ignore (LibraryDb.remove_uri uri); + (*CoercGraph.remove_coercion uri;*) + CicEnvironment.remove_obj uri + ) uris_to_remove (*** GENERATION OF AUXILIARY LEMMAS ***) let generate_elimination_principles uri refinement_toolkit = let uris = ref [] in - let elim sort = - try - let uri,obj = CicElim.elim_of ~sort uri 0 in - add_single_obj uri obj refinement_toolkit; - uris := uri :: !uris - with CicElim.Can_t_eliminate -> () + 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 - try - List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - !uris - with exn -> - List.iter remove_single_obj !uris; - raise exn + 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 ***********************************************************) @@ -198,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 = +let add_coercion ~add_composites refinement_toolkit uri arity = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -214,23 +227,44 @@ let add_coercion ~add_composites refinement_toolkit uri = * should we saturate it with metas in case we insert it? * *) - let extract_last_two_p ty = + let spline2list ty = let rec aux = function - | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> - aux t - | Cic.Prod( _, src, tgt) -> src, tgt - | _ -> assert false + | Cic.Prod( _, src, tgt) -> src::aux tgt + | t -> [t] in 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 + in + aux n (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 + in let already_in = List.exists - (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul) + (fun (s,t,ul) -> + List.exists + (fun u -> + UriManager.eq u uri && + CoercDb.eq_carr s src_carr && + CoercDb.eq_carr t tgt_carr) + ul) (CoercDb.to_list ()) in - let ty_src, ty_tgt = extract_last_two_p coer_ty in - let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in - let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in if not add_composites then (CoercDb.add_coercion (src_carr, tgt_carr, uri);[]) else @@ -306,10 +340,13 @@ let remove_coercion uri = let generate_projections refinement_toolkit uri fields = let uris = ref [] in - let projections = CicRecord.projections_of uri (List.map fst fields) in + let projections = + CicRecord.projections_of uri + (List.map (fun (x,_,_) -> x) fields) + in try List.iter2 - (fun (uri, name, bo) (_name, coercion) -> + (fun (uri, name, bo) (_name, coercion, arity) -> try let ty, ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in @@ -320,7 +357,8 @@ let generate_projections refinement_toolkit uri fields = if coercion then begin (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*) - let x = add_coercion ~add_composites:true refinement_toolkit uri + let x = + add_coercion ~add_composites:true refinement_toolkit uri arity in (*prerr_endline ("are: "); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; @@ -350,11 +388,10 @@ let generate_projections refinement_toolkit uri fields = let build_inversion_principle = ref (fun a b -> assert false);; let generate_inversion refinement_toolkit uri obj = - match !build_inversion_principle uri obj with - None -> [] - | Some (ind_uri,ind_obj) -> - add_single_obj ind_uri ind_obj refinement_toolkit; - [ind_uri] + List.map + (fun (ind_uri,ind_obj) -> + add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri) + (!build_inversion_principle uri obj) let add_obj refinement_toolkit uri obj = add_single_obj uri obj refinement_toolkit;