1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let paths_and_uris_of_obj uri status =
31 let basedir = get_string_option status "basedir" in
32 let innertypesuri = UriManager.innertypesuri_of_uri uri in
33 let bodyuri = UriManager.bodyuri_of_uri uri in
34 let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
35 (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
36 let innertypespath = basedir ^ "/" ^ innertypesfilename in
37 let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
38 (UriManager.string_of_uri uri) ^ ".xml.gz" in
39 let xmlpath = basedir ^ "/" ^ xmlfilename in
40 let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
41 (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
42 let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
43 xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri
45 let save_object_to_disk status uri obj =
46 let ensure_path_exists path =
47 let dir = Filename.dirname path in
50 (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
51 let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
52 Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
56 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
60 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
61 ~ask_dtd_to_the_getter:false
63 let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri =
64 paths_and_uris_of_obj uri status
66 let path_scheme_of path = "file://" ^ path in
67 List.iter MatitaMisc.mkdir
68 (List.map Filename.dirname [innertypespath; xmlpath]);
69 (* now write to disk *)
70 ensure_path_exists innertypespath;
71 Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
72 ensure_path_exists xmlpath;
73 Xml.pp ~gzip:true xml (Some xmlpath) ;
74 (* now register to the getter *)
75 Http_getter.register' innertypesuri (path_scheme_of innertypespath);
76 Http_getter.register' uri (path_scheme_of xmlpath);
77 (* we return a list of uri,path we registered/created *)
78 (uri,xmlpath) :: (innertypesuri,innertypespath) ::
79 (* now the optional body, both write and register *)
80 (match bodyxml,bodyuri with
82 | Some bodyxml,Some bodyuri->
83 ensure_path_exists xmlbodypath;
84 Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
85 Http_getter.register' bodyuri (path_scheme_of xmlbodypath);
89 let unregister_if_some = function
90 | Some u -> Http_getter.unregister' u | None -> ()
92 let remove_object_from_disk uri path =
94 Http_getter.unregister' uri
96 let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
97 let dbd = MatitaDb.instance () in
98 let suri = UriManager.string_of_uri uri in
99 if CicEnvironment.in_library uri then
100 command_error (sprintf "%s constant already defined" suri)
102 let name = UriManager.name_of_uri uri in
103 let obj = Cic.Constant (name, body, ty, params, attrs) in
104 let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
105 CicEnvironment.add_type_checked_term uri (obj, ugraph);
106 MetadataDb.index_constant ~dbd ~uri ~body ~ty;
107 let new_stuff = save_object_to_disk status uri obj in
108 MatitaLog.message (sprintf "%s constant defined" suri);
109 { status with objects = new_stuff @ status.objects }
112 let split_obj = function
113 | Cic.Constant (name, body, ty, _, attrs)
114 | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
117 let add_inductive_def
118 ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status
120 let dbd = MatitaDb.instance () in
121 let suri = UriManager.string_of_uri uri in
122 if CicEnvironment.in_library uri then
123 command_error (sprintf "%s inductive type already defined" suri)
125 let name = UriManager.name_of_uri uri in
126 let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
127 let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
128 CicEnvironment.put_inductive_definition uri (obj, ugraph);
129 MetadataDb.index_inductive_def ~dbd ~uri ~types:types;
130 let new_stuff = save_object_to_disk status uri obj in
131 MatitaLog.message (sprintf "%s inductive type defined" suri);
132 let status = { status with objects = new_stuff @ status.objects } in
133 let elim sort status =
135 let obj = CicElim.elim_of ~sort uri 0 in
136 let (name, body, ty, attrs) = split_obj obj in
137 let suri = MatitaMisc.qualify status name ^ ".con" in
138 let uri = UriManager.uri_of_string suri in
139 (* TODO Zack: make CicElim returns a universe *)
140 let ugraph = CicUniv.empty_ugraph in
141 add_constant ~uri ?body ~ty ~attrs ~ugraph status;
142 with CicElim.Can_t_eliminate -> status
145 (fun status sort -> elim sort status)
147 [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
152 type t = UriManager.uri * string
153 let compare (u1, _) (u2, _) = UriManager.compare u1 u2
156 module UriSet = Set.Make (OrderedUri)
158 (* returns the uri of objects that were added in the meanwhile...
159 * status1 ----> status2
160 * assumption: objects defined in status2 are a superset of those defined in
163 let delta_status status1 status2 =
164 let module S = UriSet in
166 let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
167 let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
168 let diff = S.diff s2 s1 in
169 S.fold (fun uri uris -> uri :: uris) diff []
171 diff status1.objects status2.objects
173 let time_travel ~present ~past =
174 let list_of_objs_to_remove = List.rev (delta_status past present) in
175 (* List.rev is just for the debugging code, which otherwise may list both
176 * something.ind and something.ind#xpointer ... (ask Enrico :-) *)
177 let debug_list = ref [] in
178 List.iter (fun (x,p) ->
179 remove_object_from_disk x p;
181 CicEnvironment.remove_obj x
182 with CicEnvironment.Object_not_found _ ->
184 (sprintf "time_travel removes from cache %s that is not in"
185 (UriManager.string_of_uri x)));
186 let l = MatitaDb.remove_uri x in
187 debug_list := UriManager.string_of_uri x :: !debug_list @ l)
188 list_of_objs_to_remove;
190 (* this is debug code
191 * idea: debug_list is the list of objects to be removed as computed from the
192 * db, while list_of_objs_to_remove is the same list but computer from the
193 * differences between statuses *)
194 let l1 = List.sort Pervasives.compare !debug_list in
195 let l2 = List.sort Pervasives.compare
196 (List.map (fun (x,_) -> UriManager.string_of_uri x) list_of_objs_to_remove)
198 let rec uniq = function
201 | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl)
202 | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
207 List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2
209 | Invalid_argument _ | Exit ->
210 MatitaLog.debug "It seems you garbaged something...";
211 MatitaLog.debug "l1:";
212 List.iter MatitaLog.debug l1;
213 MatitaLog.debug "l2:";
214 List.iter MatitaLog.debug l2
216 let alias_diff ~from status =
217 let module Map = DisambiguateTypes.Environment in
219 (fun domain_item codomain_item acc ->
220 if not (Map.mem domain_item from.aliases) then
221 Map.add domain_item codomain_item acc
224 status.aliases Map.empty