X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FlibrarySync.ml;h=abb50f36351b3ca4c641d1440105d40f5732821b;hb=9262517c80e17d46b9bf9931dc879ac653a633e9;hp=707b355b0995304bbe1da901a0a27daac07a1227;hpb=cf3635c0830661f59d16339cd7fc9c3b948fcbc8;p=helm.git diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index 707b355b0..abb50f363 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -23,10 +23,20 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception AlreadyDefined of UriManager.uri let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 +(* 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 merge_coercions obj = let module C = Cic in let rec aux2 = (fun (u,t) -> u,aux t) @@ -40,7 +50,7 @@ let merge_coercions obj = C.Lambda (name, aux so, aux dest) | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest) - | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when + | 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 @@ -170,7 +180,7 @@ let index_obj = let add_single_obj uri obj ~basedir = let obj = - if List.mem `Generated (CicUtil.attributes_of_obj obj) && + if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) then merge_coercions obj @@ -221,7 +231,7 @@ let remove_single_obj uri = HExtlib.rmdir_descend (Filename.dirname file) with Http_getter_types.Key_not_found _ -> ()); ignore (LibraryDb.remove_uri uri); - CoercGraph.remove_coercion uri; + (*CoercGraph.remove_coercion uri;*) CicEnvironment.remove_obj uri) to_remove @@ -243,6 +253,88 @@ let generate_elimination_principles ~basedir uri = List.iter remove_single_obj !uris; raise exn +(* COERCIONS ***********************************************************) + +let remove_all_coercions () = + UriManager.UriHashtbl.clear coercion_hashtbl; + CoercDb.remove_coercion (fun (_,_,u1) -> true) + +let add_coercion ~basedir ~add_composites uri = + let coer_ty,_ = + let coer = CicUtil.term_of_uri uri in + CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph + in + (* we have to get the source and the tgt type uri + * in Coq syntax we have already their names, but + * since we don't support Funclass and similar I think + * all the coercion should be of the form + * (A:?)(B:?)T1->T2 + * So we should be able to extract them from the coercion type + * + * Currently only (_:T1)T2 is supported. + * should we saturate it with metas in case we insert it? + * + *) + let extract_last_two_p 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 + 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 + [] + 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 + +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 ~basedir uri fields = let uris = ref [] in let projections = CicRecord.projections_of uri (List.map fst fields) in @@ -254,15 +346,10 @@ let generate_projections ~basedir uri fields = 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; let composites = - if coercion then - (* this is _NOT_ the place for THIS!!! *) - (* MOO HANDLING IS MISSING *) - let toadd = CoercGraph.add_coercion uri in - List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd; - List.map fst toadd + if coercion then + add_coercion ~basedir ~add_composites:true uri else [] in @@ -321,3 +408,4 @@ let remove_obj uri = Not_found -> [] (*assert false*) in List.iter remove_single_obj (uri::uris) +