X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=086893a974985e614026bfaebd29b89e5f4de912;hb=387c6f39b2e55c887e8947039e5d7f56bce7f7a8;hp=7363697d5522a96a8b2551ae1264b14874411bf9;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 7363697d5..086893a97 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -37,112 +37,34 @@ let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 * *) let coercion_hashtbl = UriManager.UriHashtbl.create 3 -let rec merge_coercions = - let module C = Cic in - let aux = (fun (u,t) -> u,merge_coercions t) in - function - C.Rel _ | C.Sort _ | C.Implicit _ as t -> t - | C.Meta (n,subst) -> - let subst' = - List.map - (function None -> None | Some t -> Some (merge_coercions t)) subst - in - C.Meta (n,subst') - | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty) - | C.Prod (name,so,dest) -> - C.Prod (name, merge_coercions so, merge_coercions dest) - | C.Lambda (name,so,dest) -> - C.Lambda (name, merge_coercions so, merge_coercions dest) - | C.LetIn (name,so,dest) -> - C.LetIn (name, merge_coercions so, merge_coercions dest) - | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when - CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> - let source_carr = CoercGraph.source_of c2 in - let tgt_carr = CoercGraph.target_of c1 in - (match CoercGraph.look_for_coercion source_carr tgt_carr - with - | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ] - | _ -> assert false) (* the composite coercion must exist *) - | C.Appl l -> C.Appl (List.map merge_coercions l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.Var (uri, exp_named_subst) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.Const (uri, exp_named_subst) - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.MutInd (uri,tyno,exp_named_subst) - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst = List.map aux exp_named_subst in - C.MutConstruct (uri,tyno,consno,exp_named_subst) - | C.MutCase (uri,tyno,out,te,pl) -> - let pl = List.map merge_coercions pl in - C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl) - | C.Fix (fno, fl) -> - let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in - C.Fix (fno, fl) - | C.CoFix (fno, fl) -> - let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in - C.CoFix (fno, fl) - -let merge_coercions_in_obj obj = - let module C = Cic in - match obj with - | C.Constant (id, body, ty, params, attrs) -> - let body = - match body with - | None -> None - | Some body -> Some (merge_coercions body) - in - let ty = merge_coercions ty in - C.Constant (id, body, ty, params, attrs) - | C.Variable (name, body, ty, params, attrs) -> - let body = - match body with - | None -> None - | Some body -> Some (merge_coercions body) - in - let ty = merge_coercions ty in - C.Variable (name, body, ty, params, attrs) - | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) -> - assert false - | C.InductiveDefinition (indtys, params, leftno, attrs) -> - let indtys = - List.map - (fun (name, ind, arity, cl) -> - let arity = merge_coercions arity in - let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in - (name, ind, arity, cl)) - indtys - in - C.InductiveDefinition (indtys, params, leftno, attrs) - let uris_of_obj uri = let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in let univgraphuri = UriManager.univgraphuri_of_uri uri in innertypesuri,bodyuri,univgraphuri -let paths_and_uris_of_obj uri ~basedir = - let basedir = basedir ^ "/xml" in +let paths_and_uris_of_obj uri = + let resolved = Http_getter.filename' ~writable:true uri in + let basepath = Filename.dirname resolved in let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in - let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" - (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in - let innertypespath = basedir ^ "/" ^ innertypesfilename in - let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".xml.gz" in - let xmlpath = basedir ^ "/" ^ xmlfilename in - let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri uri) ^ ".body.xml.gz" in - let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in - let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" - (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in - let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in + let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in + let innertypespath = basepath ^ "/" ^ innertypesfilename in + let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in + let xmlpath = basepath ^ "/" ^ xmlfilename in + let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in + let xmlbodypath = basepath ^ "/" ^ xmlbodyfilename in + let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in + let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri -let save_object_to_disk ~basedir uri obj ugraph univlist = +let save_object_to_disk uri obj ugraph univlist = + let write f x = + if not (Helm_registry.get_opt_default + Helm_registry.bool "matita.nodisk" ~default:false) + then + f x + in let ensure_path_exists path = let dir = Filename.dirname path in HExtlib.mkdir dir @@ -156,22 +78,22 @@ let save_object_to_disk ~basedir uri obj ugraph univlist = in let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, xmlunivgraphpath, univgraphuri = - paths_and_uris_of_obj uri basedir + paths_and_uris_of_obj uri in - List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); + write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]); (* now write to disk *) - ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath); - CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; + write ensure_path_exists xmlpath; + write (Xml.pp ~gzip:true xml) (Some xmlpath); + write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist; (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: (univgraphuri,xmlunivgraphpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with - None,None -> [] + None,_ -> [] | Some bodyxml,Some bodyuri-> - ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + write ensure_path_exists xmlbodypath; + write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath); [bodyuri, xmlbodypath] | _-> assert false) @@ -185,12 +107,13 @@ let index_obj = fun ~dbd ~uri -> profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri -let add_single_obj uri obj ~basedir = +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 - merge_coercions_in_obj obj + refinement_toolkit.RT.pack_coercion_obj obj else obj in @@ -214,7 +137,7 @@ let add_single_obj uri obj ~basedir = index_obj ~dbd ~uri; (* 2 must be in the env *) try (*3*) - let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in + let new_stuff = save_object_to_disk uri obj ugraph univlist in try HLog.message (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) @@ -234,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' 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 -> + (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 -> + ignore (LibraryDb.remove_uri uri); + (*CoercGraph.remove_coercion uri;*) + ) uris_to_remove ; + CicEnvironment.remove_obj uri (*** GENERATION OF AUXILIARY LEMMAS ***) -let generate_elimination_principles ~basedir uri = +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 ~basedir; - 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 ***********************************************************) @@ -275,7 +211,7 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,u1) -> true) -let add_coercion ~basedir ~add_composites uri = +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 @@ -291,54 +227,112 @@ let add_coercion ~basedir ~add_composites 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( _, src, Cic.Prod (n,t1,t2)) -> - assert false - (* not implemented: aux (Cic.Prod(n,t1,t2)) *) - | Cic.Prod( _, src, tgt) -> src, tgt - | _ -> assert false + | Cic.Prod( _, src, tgt) -> src::aux tgt + | t -> [t] in aux ty in - let ty_src, ty_tgt = extract_last_two_p coer_ty in - let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in - let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in - let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in - let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in - (* update the DB *) - List.iter - (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) - new_coercions; - CoercDb.add_coercion (src_uri, tgt_uri, 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 ~basedir uri obj; - uri::acc) - composite_uris new_coercions - else - [] + 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_obj src_carr tgt_carr uri obj = + List.exists + (fun (s,t,ul) -> + List.exists + (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 && + 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 - (* 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 ("aggiungo: " ^ 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 []); - lemmas + if not add_composites then + (CoercDb.add_coercion (src_carr, tgt_carr, uri);[]) + 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 + (* 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 = try let (composites_in_db, composites_in_lib) = UriManager.UriHashtbl.find coercion_hashtbl uri in - prerr_endline ("removing: " ^UriManager.string_of_uri uri); + (*prerr_endline ("removing: " ^UriManager.string_of_uri uri); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) - composites_in_db; + composites_in_db;*) UriManager.UriHashtbl.remove coercion_hashtbl uri; CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); (* remove from the DB *) @@ -351,21 +345,39 @@ let remove_coercion uri = Not_found -> () (* mhh..... *) -let generate_projections ~basedir uri fields = +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 let attrs = [`Class `Projection; `Generated] in let obj = Cic.Constant (name,Some bo,ty,[],attrs) in - add_single_obj ~basedir uri obj; + add_single_obj uri obj refinement_toolkit; let composites = if coercion then - add_coercion ~basedir ~add_composites:true uri + 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 "---"; +*) + (*CSC: I throw the arity away. See comment above *) + List.map fst x + end else [] in @@ -385,16 +397,67 @@ let generate_projections ~basedir uri fields = 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 uri obj ~basedir = - add_single_obj uri obj ~basedir; +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 @ generate_elimination_principles ~basedir uri; + uris := !uris @ + generate_elimination_principles uri refinement_toolkit; + uris := !uris @ generate_inversion refinement_toolkit uri obj; let rec get_record_attrs = function | [] -> None @@ -404,7 +467,8 @@ let add_obj uri obj ~basedir = (match get_record_attrs attrs with | None -> () (* not a record *) | Some fields -> - uris := !uris @ (generate_projections ~basedir uri fields)) + uris := !uris @ + (generate_projections refinement_toolkit uri fields)) | Cic.CurrentProof _ | Cic.Variable _ -> assert false end;