From 5b32b7905bc78c11e353efd68137b8eb7b6ac73b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Sep 2005 12:54:24 +0000 Subject: [PATCH] universes are saved to disk --- helm/matita/matitaEngine.ml | 2 +- helm/matita/matitaMisc.ml | 5 ++++- helm/matita/matitaSync.ml | 27 +++++++++++++++++++-------- helm/matita/matitaSync.mli | 3 ++- 4 files changed, 26 insertions(+), 11 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 365f947c0..707e31d98 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -580,7 +580,7 @@ let eval_coercion status coercion = (* also adds them to the Db *) CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in let status = - List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status) + List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status) status new_coercions in let statement_of name = GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index c67602dba..56cb4a295 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -126,7 +126,10 @@ let mkdir path = Unix.mkdir path 0o755 with | Unix.Unix_error (Unix.EEXIST,_,_) -> () - | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e))); + | Unix.Unix_error (e,_,_) -> + raise + (Failure + ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e)))); aux path tl in aux "" components diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 3d9d74dcc..fe2726a0a 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -106,6 +106,7 @@ let paths_and_uris_of_obj uri status = 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 univgraphuri = UriManager.univgraphuri_of_uri uri in let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in let innertypespath = basedir ^ "/" ^ innertypesfilename in @@ -115,9 +116,13 @@ let paths_and_uris_of_obj uri status = let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" (UriManager.string_of_uri uri) ^ ".body.xml.gz" in let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in - xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri + let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in + let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in + xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri -let save_object_to_disk status uri obj = +let save_object_to_disk status uri obj ugraph univlist = let ensure_path_exists path = let dir = Filename.dirname path in MatitaMisc.mkdir dir @@ -129,7 +134,8 @@ let save_object_to_disk status uri obj = Cic2Xml.print_object uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj in - let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = + let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, + xmlunivgraphpath, univgraphuri = paths_and_uris_of_obj uri status in let path_scheme_of path = "file://" ^ path in @@ -137,9 +143,11 @@ let save_object_to_disk status uri obj = (List.map Filename.dirname [innertypespath; xmlpath]); (* now write to disk *) ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath) ; + Xml.pp ~gzip:true xml (Some xmlpath); + CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; (* we return a list of uri,path we registered/created *) - (uri,xmlpath) :: + (uri,xmlpath) :: (innertypesuri,innertypespath) :: + (univgraphuri,xmlunivgraphpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with None,None -> [] @@ -170,10 +178,12 @@ let add_obj uri obj status = command_error (sprintf "%s already defined" suri) else begin typecheck_obj uri obj; (* 1 *) + let _, ugraph, univlist = + CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in try index_obj ~dbd ~uri; (* 2 must be in the env *) try - let new_stuff = save_object_to_disk status uri obj in (* 3 *) + let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*) try MatitaLog.message (sprintf "%s defined" suri); let status = add_aliases_for_object status suri obj in @@ -187,7 +197,7 @@ let add_obj uri obj status = raise exc with exc -> CicEnvironment.remove_obj uri; (* -1 *) - raise exc + raise exc end let add_obj = @@ -279,9 +289,10 @@ let time_travel ~present ~past = let remove ~verbose uri = let derived_uris_of_uri uri = UriManager.innertypesuri_of_uri uri :: + UriManager.univgraphuri_of_uri uri :: (match UriManager.bodyuri_of_uri uri with | None -> [] - | Some u -> [u]) + | Some u -> [u]) in let to_remove = uri :: diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index df5eb84b5..9dd13529c 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -24,7 +24,8 @@ *) val add_obj: - UriManager.uri -> Cic.obj -> MatitaTypes.status -> MatitaTypes.status + UriManager.uri -> Cic.obj -> + MatitaTypes.status -> MatitaTypes.status val time_travel: present:MatitaTypes.status -> past:MatitaTypes.status -> unit -- 2.39.2