X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaSync.ml;h=55cb4a45c09d45c887e07c26602934283bc61679;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=f14e3d1269044d63e15eec3e931c8bc7ab9e1c1b;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index f14e3d126..55cb4a45c 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -27,8 +27,76 @@ open Printf open MatitaTypes +let alias_diff ~from status = + let module Map = DisambiguateTypes.Environment in + Map.fold_flatten + (fun domain_item codomain_item acc -> + if not (Map.mem domain_item from.aliases) then + Map.cons domain_item codomain_item acc + else + begin + try + let codomain1 = Map.find domain_item from.aliases in + let codomain2 = Map.find domain_item status.aliases in + List.fold_right + (fun item env -> + let dsc = fst item in + if not (List.exists (fun (dsc', _) -> dsc'=dsc) codomain1) then + Map.cons domain_item codomain_item env + else + env) + codomain2 acc + with Not_found -> acc + end) + status.aliases Map.empty + +let set_proof_aliases status aliases = + let new_status = { status with aliases = aliases } in + let diff = alias_diff ~from:status new_status in + if DisambiguateTypes.Environment.is_empty diff then + new_status + else + add_moo_content (DisambiguatePp.commands_of_environment diff) new_status + +(** given a uri and a type list (the contructors types) builds a list of pairs + * (name,uri) that is used to generate authomatic aliases **) +let extract_alias types uri = + fst(List.fold_left ( + fun (acc,i) (name, _, _, cl) -> + (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None)) + :: + (fst(List.fold_left ( + fun (acc,j) (name,_) -> + (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i + (Some j))) :: acc) , j+1) + ) (acc,1) cl)),i+1 + ) ([],0) types) + +let env_of_list l env = + let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in + DisambiguateTypes.env_of_list l' env + +let add_aliases_for_inductive_def status types suri = + let uri = UriManager.uri_of_string suri in + let aliases = env_of_list (extract_alias types uri) status.aliases in + set_proof_aliases status aliases + +let add_alias_for_constant status suri = + let uri = UriManager.uri_of_string suri in + let name = UriManager.name_of_uri uri in + let new_env = env_of_list [(name,suri)] status.aliases in + set_proof_aliases status new_env + +let add_aliases_for_object status suri = + function + Cic.InductiveDefinition (types,_,_,_) -> + add_aliases_for_inductive_def status types suri + | Cic.Constant _ -> add_alias_for_constant status suri + | Cic.Variable _ + | Cic.CurrentProof _ -> assert false + let paths_and_uris_of_obj uri status = - let basedir = get_string_option status "basedir" in + let basedir = get_string_option status "basedir" ^ "/xml" in let innertypesuri = UriManager.innertypesuri_of_uri uri in let bodyuri = UriManager.bodyuri_of_uri uri in let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" @@ -68,12 +136,9 @@ let save_object_to_disk status uri obj = (List.map Filename.dirname [innertypespath; xmlpath]); (* now write to disk *) ensure_path_exists innertypespath; - Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ; + Xml.pp ~gzip:true xmlinnertypes (Some innertypespath); ensure_path_exists xmlpath; Xml.pp ~gzip:true xml (Some xmlpath) ; - (* now register to the getter *) - Http_getter.register' innertypesuri (path_scheme_of innertypespath); - Http_getter.register' uri (path_scheme_of xmlpath); (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: (innertypesuri,innertypespath) :: (* now the optional body, both write and register *) @@ -81,112 +146,92 @@ let save_object_to_disk status uri obj = None,None -> [] | Some bodyxml,Some bodyuri-> ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ; - Http_getter.register' bodyuri (path_scheme_of xmlbodypath); - [bodyuri,xmlbodypath] + Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + [bodyuri, xmlbodypath] | _-> assert false) -let unregister_if_some = function - | Some u -> Http_getter.unregister' u | None -> () - -let remove_object_from_disk uri path = - Sys.remove path; - Http_getter.unregister' uri - -let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = - let dbd = MatitaDb.instance () in - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - command_error (sprintf "%s constant already defined" suri) - else begin - let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name, body, ty, params, attrs) in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_term uri (obj, ugraph); - MetadataDb.index_constant ~dbd ~uri ~body ~ty; - let new_stuff = save_object_to_disk status uri obj in - MatitaLog.message (sprintf "%s constant defined" suri); - { status with objects = new_stuff @ status.objects } - end - -let split_obj = function - | Cic.Constant (name, body, ty, _, attrs) - | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) - | _ -> assert false - -let add_inductive_def - ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status -= +let add_obj uri obj status = let dbd = MatitaDb.instance () in let suri = UriManager.string_of_uri uri in if CicEnvironment.in_library uri then - command_error (sprintf "%s inductive type already defined" suri) + command_error (sprintf "%s already defined" suri) else begin - let name = UriManager.name_of_uri uri in - let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.put_inductive_definition uri (obj, ugraph); - MetadataDb.index_inductive_def ~dbd ~uri ~types:types; - let new_stuff = save_object_to_disk status uri obj in - MatitaLog.message (sprintf "%s inductive type defined" suri); - let status = { status with objects = new_stuff @ status.objects } in - let elim sort status = + CicTypeChecker.typecheck_obj uri obj; (* 1 *) + try + MetadataDb.index_obj ~dbd ~uri; (* 2 must be in the env *) try - let obj = CicElim.elim_of ~sort uri 0 in - let (name, body, ty, attrs) = split_obj obj in - let suri = MatitaMisc.qualify status name ^ ".con" in - let uri = UriManager.uri_of_string suri in - (* TODO Zack: make CicElim returns a universe *) - let ugraph = CicUniv.empty_ugraph in - add_constant ~uri ?body ~ty ~attrs ~ugraph status; - with CicElim.Can_t_eliminate -> status - in - List.fold_left - (fun status sort -> elim sort status) - status - [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + let new_stuff = save_object_to_disk status uri obj in (* 3 *) + try + MatitaLog.message (sprintf "%s defined" suri); + let status = add_aliases_for_object status suri obj in + { status with objects = new_stuff @ status.objects; + proof_status = No_proof } + with exc -> + List.iter MatitaMisc.safe_remove (List.map snd new_stuff); (* -3 *) + raise exc + with exc -> + ignore(MatitaDb.remove_uri uri); (* -2 *) + raise exc + with exc -> + CicEnvironment.remove_obj uri; (* -1 *) + raise exc end - + module OrderedUri = struct type t = UriManager.uri * string let compare (u1, _) (u2, _) = UriManager.compare u1 u2 end +module OrderedId = +struct + type t = CicNotation.notation_id + let compare = Pervasives.compare +end + module UriSet = Set.Make (OrderedUri) +module IdSet = Set.Make (OrderedId) -(* returns the uri of objects that were added in the meanwhile... - * status1 ----> status2 - * assumption: objects defined in status2 are a superset of those defined in - * status1 - *) -let delta_status status1 status2 = + (** @return l2 \ l1 *) +let uri_list_diff l2 l1 = let module S = UriSet in - let diff l1 l2 = - let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in - let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in - let diff = S.diff s2 s1 in - S.fold (fun uri uris -> uri :: uris) diff [] - in - diff status1.objects status2.objects + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + (** @return l2 \ l1 *) +let id_list_diff l2 l1 = + let module S = IdSet in + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + +let remove_coercion uri = + CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri) + let time_travel ~present ~past = - let list_of_objs_to_remove = List.rev (delta_status past present) in - (* List.rev is just for the debugging code, which otherwise may list both - * something.ind and something.ind#xpointer ... (ask Enrico :-) *) + let objs_to_remove = uri_list_diff present.objects past.objects in + let notation_to_remove = + id_list_diff present.notation_ids past.notation_ids + in let debug_list = ref [] in - List.iter (fun (x,p) -> - remove_object_from_disk x p; - (try - CicEnvironment.remove_obj x - with CicEnvironment.Object_not_found _ -> - MatitaLog.debug - (sprintf "time_travel removes from cache %s that is not in" - (UriManager.string_of_uri x))); - let l = MatitaDb.remove_uri x in - debug_list := UriManager.string_of_uri x :: !debug_list @ l) - list_of_objs_to_remove; - + List.iter + (fun (uri,p) -> + MatitaMisc.safe_remove p; + remove_coercion uri; + (try + CicEnvironment.remove_obj uri + with CicEnvironment.Object_not_found _ -> + MatitaLog.debug + (sprintf "time_travel removes from cache %s that is not in" + (UriManager.string_of_uri uri))); + let l = MatitaDb.remove_uri uri in + debug_list := UriManager.string_of_uri uri :: !debug_list @ l) + objs_to_remove; + List.iter CicNotation.remove_notation notation_to_remove + (* (* this is debug code * idea: debug_list is the list of objects to be removed as computed from the * db, while list_of_objs_to_remove is the same list but computer from the @@ -212,14 +257,28 @@ let time_travel ~present ~past = List.iter MatitaLog.debug l1; MatitaLog.debug "l2:"; List.iter MatitaLog.debug l2 + *) -let alias_diff ~from status = - let module Map = DisambiguateTypes.Environment in - Map.fold - (fun domain_item codomain_item acc -> - if not (Map.mem domain_item from.aliases) then - Map.add domain_item codomain_item acc - else - acc) - status.aliases Map.empty - +let remove ~verbose uri = + let derived_uris_of_uri uri = + UriManager.innertypesuri_of_uri uri :: + (match UriManager.bodyuri_of_uri uri with + | None -> [] + | Some u -> [u]) + in + let to_remove = + uri :: + (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @ + derived_uris_of_uri uri + in + List.iter + (fun uri -> + (try + if verbose then + MatitaLog.debug ("Removing: " ^ UriManager.string_of_uri uri); + MatitaMisc.safe_remove (Http_getter.resolve' uri) + with Http_getter_types.Key_not_found _ -> ()); + remove_coercion uri; + ignore (MatitaDb.remove_uri uri); + CicEnvironment.remove_obj uri) + to_remove