1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
33 (* Missing description *)
35 (******************************************************************************)
38 let counter = ref 0 in
39 List.iter (function e -> incr counter ; foo e !counter)
42 let pathname_of_uri uristring =
44 Str.replace_first (Str.regexp "^cic:") "" uristring
47 let make_dirs dirpath =
48 ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\""))
61 let soften_classification =
63 Backbone -> InConclusion
64 | Branch -> InHypothesis
65 | InBody -> assert false
69 let hash = Hashtbl.create 117 ;;
71 let add_uri uri kind =
79 match kind,old_kinds with
81 | InBody,_ -> old_kinds
82 | k,_ when List.mem k old_kinds -> old_kinds
85 Hashtbl.replace hash uri new_kinds
88 (* It also removes every element in the hash *)
89 let uris_fold foo init =
90 let xml_element_name_of_kind =
92 Backbone -> "MainConclusion"
93 | Branch -> "MainHypothesis"
94 | InConclusion -> "InConclusion"
95 | InHypothesis -> "InHypothesis"
103 foo j uri (xml_element_name_of_kind kind)
113 let output_content () =
116 [< Xml.xml_nempty "h:refObj" []
117 (Xml.xml_empty "h:Occurrence"
118 ["rdf:about","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#" ^ kind ;
126 let output_file cic_string_uri rdf_string_uri =
127 let module U = UriManager in
128 let module X = Xml in
129 let content = output_content () in
130 let rdf_uri = U.uri_of_string rdf_string_uri in
131 make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ;
133 [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
134 X.xml_nempty "rdf:RDF"
136 "xmlns:rdf","http://www.w3.org/1999/02/22-rdf-syntax-ns#";
137 "xmlns:h","http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#"]
140 Stream.empty content ; (* raise Stream.failure if not empty *)
141 X.xml_empty "h:Object" ["rdf:about",cic_string_uri]
144 X.xml_nempty "h:Object" ["rdf:about",cic_string_uri] content
147 (Some (pathname_of_uri rdf_string_uri ^ ".xml"))
151 let cicfilename = Getter.getxml uri in
153 match CicParser.term_of_xml cicfilename uri false with
155 Deannotate.deannotate_obj annobj
158 Unix.unlink cicfilename ;
162 let add_every_constructor uri typeno kind =
163 let module C = Cic in
164 match (get_obj uri) with
165 (C.InductiveDefinition (itys,_,_)) ->
166 let string_uri = UriManager.string_of_uri uri in
167 let sn = string_of_int (typeno + 1) in
168 let (_,_,_,cons) = List.nth itys typeno in
171 let sm = string_of_int m in
173 (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
179 let process_type term =
180 let module U = UriManager in
181 let module H = UriHash in
182 let module C = Cic in
183 let rec process_type_aux kind =
186 H.add_uri (U.string_of_uri uri) kind
189 process_type_aux kind te
190 | C.Prod (_,sou,ta) ->
191 let (source_kind,target_kind) =
193 H.Backbone -> (H.Branch,H.Backbone)
194 | H.Branch -> (H.InHypothesis,H.InHypothesis)
195 | H.InBody -> assert false
198 process_type_aux source_kind sou ;
199 process_type_aux target_kind ta
200 | C.Lambda (_,sou,ta) ->
201 let kind' = H.soften_classification kind in
202 process_type_aux kind' sou ;
203 process_type_aux kind' ta
204 | C.LetIn (_,te,ta)->
205 let kind' = H.soften_classification kind in
206 process_type_aux kind' te ;
207 process_type_aux kind ta
209 let kind' = H.soften_classification kind in
210 process_type_aux kind he ;
211 List.iter (process_type_aux kind') tl
212 | C.Appl _ -> assert false
214 UriHash.add_uri (U.string_of_uri uri) kind
215 | C.Abst _ -> assert false
216 | C.MutInd (uri,_,typeno) ->
218 (U.string_of_uri uri ^ "#xpointer(1/" ^
219 string_of_int (typeno + 1) ^ ")")
221 | C.MutConstruct (uri,_,typeno,consno) ->
223 (U.string_of_uri uri ^ "#xpointer(1/" ^
224 string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
226 | C.MutCase (uri,_,typeno,_,term,patterns) ->
227 (* outtype ignored *)
228 let kind' = H.soften_classification kind in
229 add_every_constructor uri typeno kind' ;
230 process_type_aux kind' term ;
231 List.iter (process_type_aux kind') patterns
233 let kind' = H.soften_classification kind in
235 (function (_,_,bo,ty) ->
236 process_type_aux kind' bo ;
237 process_type_aux kind' ty ;
239 | C.CoFix (_,funs) ->
240 let kind' = H.soften_classification kind in
242 (function (_,bo,ty) ->
243 process_type_aux kind' bo ;
244 process_type_aux kind' ty ;
248 process_type_aux H.Backbone (CicMiniReduction.letin_nf term)
252 let module U = UriManager in
253 let module H = UriHash in
254 let module C = Cic in
255 let rec process_body_aux =
258 H.add_uri (U.string_of_uri uri) H.InBody
260 process_body_aux te ;
262 | C.Prod (_,sou,ta) ->
263 process_body_aux sou ;
265 | C.Lambda (_,sou,ta) ->
266 process_body_aux sou ;
268 | C.LetIn (_,te,ta)->
269 process_body_aux te ;
272 List.iter process_body_aux l
274 UriHash.add_uri (U.string_of_uri uri) H.InBody
275 | C.Abst _ -> assert false
276 | C.MutInd (uri,_,typeno) ->
278 (U.string_of_uri uri ^ "#xpointer(1/" ^
279 string_of_int (typeno + 1) ^ ")")
281 | C.MutConstruct (uri,_,typeno,consno) ->
283 (U.string_of_uri uri ^ "#xpointer(1/" ^
284 string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
286 | C.MutCase (uri,_,typeno,outtype,term,patterns) ->
287 add_every_constructor uri typeno H.InBody ;
288 process_body_aux outtype ;
289 process_body_aux term ;
290 List.iter process_body_aux patterns
293 (function (_,_,bo,ty) ->
294 process_body_aux bo ;
295 process_body_aux ty ;
297 | C.CoFix (_,funs) ->
299 (function (_,bo,ty) ->
300 process_body_aux bo ;
301 process_body_aux ty ;
308 let process_obj string_uri =
309 let module U = UriManager in
310 let module C = Cic in
312 (C.Definition (_,bo,ty,_)) ->
315 output_file string_uri string_uri
316 | (C.Axiom (_,ty,_)) ->
318 output_file string_uri string_uri
319 | (C.Variable (_,bo,ty)) ->
323 (Some bo') -> process_body bo'
326 output_file string_uri string_uri
327 | (C.InductiveDefinition _) as id ->
330 CicSubstitution.undebrujin_inductive_def
331 (U.uri_of_string string_uri) id
334 (C.InductiveDefinition (itys,_,_)) ->
336 (fun (_,_,ty,cons) n ->
337 let sn = string_of_int n in
340 (string_uri ^ "#xpointer(1/" ^ sn ^ ")")
341 (string_uri ^ "," ^ sn) ;
344 let sm = string_of_int m in
347 (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
348 (string_uri ^ "," ^ sn ^ "," ^ sm)
353 | (C.CurrentProof _) -> assert false
356 let mk_forward string_uri =
357 let module U = UriManager in
358 print_endline ("Now computing metadata of " ^ string_uri) ;
360 let uri = U.uri_of_string string_uri in
361 let obj = get_obj uri in
362 process_obj string_uri obj
366 let usage_msg = "usage: mk_forward[.opt] URI" in
372 prerr_string "No URI provided.\n" ;
373 Arg.usage [] usage_msg ;
376 else if !uri = "" then
380 prerr_string "More than two arguments provided.\n" ;
381 Arg.usage [] usage_msg ;
387 prerr_string "No URI provided.\n" ;
388 Arg.usage [] usage_msg ;