]> matita.cs.unibo.it Git - helm.git/blob - helm/metadata/create2/mk_forward/mk_forward.ml
Modified Files:
[helm.git] / helm / metadata / create2 / mk_forward / mk_forward.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 03/04/2001                                 *)
32 (*                                                                            *)
33 (*                            Missing description                             *)
34 (*                                                                            *)
35 (******************************************************************************)
36
37 let iteri foo =
38  let counter = ref 0 in
39   List.iter (function e -> incr counter ; foo e !counter)
40 ;;
41
42 let pathname_of_uri uristring =
43  "forward" ^
44   Str.replace_first (Str.regexp "^cic:") "" uristring
45 ;;
46
47 let make_dirs dirpath =
48  ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\""))
49 ;;
50
51 module UriHash =
52  struct
53   type classification =
54      Backbone
55    | Branch
56    | InConclusion
57    | InHypothesis
58    | InBody
59   ;;
60
61 let soften_classification =
62  function
63     Backbone -> InConclusion
64   | Branch -> InHypothesis
65   | InBody -> assert false
66   | k -> k
67 ;;
68
69   let hash = Hashtbl.create 117 ;;
70
71   let add_uri uri kind =
72    let old_kinds =
73     try
74      Hashtbl.find hash uri
75     with
76      Not_found -> []
77    in
78     let new_kinds = 
79      match kind,old_kinds with
80         InBody,[] -> [InBody]
81       | InBody,_  -> old_kinds
82       | k,_ when List.mem k old_kinds -> old_kinds
83       | k,_ -> k::old_kinds
84     in
85      Hashtbl.replace hash uri new_kinds
86   ;;
87
88   (* It also removes every element in the hash *)
89   let uris_fold foo init =
90    let xml_element_name_of_kind =
91     function
92        Backbone     -> "MainConclusion"
93      | Branch       -> "MainHypothesis"
94      | InConclusion -> "InConclusion"
95      | InHypothesis -> "InHypothesis"
96      | InBody       -> "InBody"
97    in
98     let res =
99      Hashtbl.fold
100       (fun uri kinds i ->
101         List.fold_left
102          (fun j kind ->
103            foo j uri (xml_element_name_of_kind kind)
104          ) i kinds
105       ) hash init
106     in
107      Hashtbl.clear hash ;
108      res
109   ;;
110  end
111 ;;
112
113 let output_content () =
114  UriHash.uris_fold
115   (fun i uri kind ->
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 ;
119            "rdf:value",uri]
120         ) ;
121        i
122     >]
123   ) [<>]
124 ;;
125
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)) ;
132    X.pp
133     [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
134        X.xml_nempty "rdf:RDF"
135         ["xml:lang","en" ;
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#"]
138
139         (try
140           Stream.empty content ; (* raise Stream.failure if not empty *)
141           X.xml_empty "h:Object" ["rdf:about",cic_string_uri]
142          with
143           Stream.Failure ->
144            X.xml_nempty "h:Object" ["rdf:about",cic_string_uri] content
145         )
146     >]
147     (Some (pathname_of_uri rdf_string_uri ^ ".xml"))
148 ;;
149
150 let get_obj uri =
151  let cicfilename = Getter.getxml uri in
152   let res = CicParser.obj_of_xml cicfilename uri in
153    Unix.unlink cicfilename ;
154    res
155 ;;
156
157 let add_every_constructor uri typeno kind =
158  let module C = Cic in
159   match (get_obj uri) with
160       (C.InductiveDefinition (itys,_,_)) ->
161         let string_uri = UriManager.string_of_uri uri in
162         let sn = string_of_int (typeno + 1) in
163         let (_,_,_,cons) = List.nth itys typeno in
164          iteri
165           (fun (_,cty,_) m ->
166             let sm = string_of_int m in
167              UriHash.add_uri
168               (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
169               kind
170           ) cons
171    | _ -> assert false
172 ;;
173
174 let process_type term =
175  let module U = UriManager in
176  let module H = UriHash in
177  let module C = Cic in
178   let rec process_type_aux kind =
179    function
180     | C.Var uri ->
181        H.add_uri (U.string_of_uri uri) kind
182     | C.Cast (te,_) ->
183        (* type ignored *)
184        process_type_aux kind te
185     | C.Prod (_,sou,ta) ->
186        let (source_kind,target_kind) =
187         match kind with
188            H.Backbone -> (H.Branch,H.Backbone)
189          | H.Branch -> (H.InHypothesis,H.InHypothesis)
190          | H.InBody -> assert false
191          | k -> (k,k)
192        in
193         process_type_aux source_kind sou ;
194         process_type_aux target_kind ta
195     | C.Lambda (_,sou,ta) ->
196         let kind' = H.soften_classification kind in
197          process_type_aux kind' sou ;
198          process_type_aux kind' ta
199     | C.LetIn (_,te,ta)->
200        let kind' = H.soften_classification kind in
201         process_type_aux kind' te ;
202         process_type_aux kind ta
203     | C.Appl (he::tl) ->
204        let kind' = H.soften_classification kind in
205         process_type_aux kind he ;
206         List.iter (process_type_aux kind') tl
207     | C.Appl _ -> assert false
208     | C.Const (uri,_) ->
209        UriHash.add_uri (U.string_of_uri uri) kind
210     | C.Abst _ -> assert false
211     | C.MutInd (uri,_,typeno) ->
212        H.add_uri
213         (U.string_of_uri uri ^ "#xpointer(1/" ^
214           string_of_int (typeno + 1) ^ ")")
215         kind
216     | C.MutConstruct (uri,_,typeno,consno) ->
217        H.add_uri
218         (U.string_of_uri uri ^ "#xpointer(1/" ^
219           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
220         kind
221     | C.MutCase (uri,_,typeno,_,term,patterns) ->
222        (* outtype ignored *)
223        let kind' = H.soften_classification kind in
224         add_every_constructor uri typeno kind' ;
225         process_type_aux kind' term ;
226         List.iter (process_type_aux kind') patterns
227     | C.Fix (_,funs) ->
228        let kind' = H.soften_classification kind in
229         List.iter
230          (function (_,_,bo,ty) ->
231            process_type_aux kind' bo ;
232            process_type_aux kind' ty ;
233          ) funs
234     | C.CoFix (_,funs) ->
235        let kind' = H.soften_classification kind in
236         List.iter
237          (function (_,bo,ty) ->
238            process_type_aux kind' bo ;
239            process_type_aux kind' ty ;
240          ) funs
241     | _ -> ()
242 in
243  process_type_aux H.Backbone (CicMiniReduction.letin_nf term)
244 ;;
245
246 let process_body =
247  let module U = UriManager in
248  let module H = UriHash in
249  let module C = Cic in
250   let rec process_body_aux =
251    function
252       C.Var uri ->
253        H.add_uri (U.string_of_uri uri) H.InBody
254     | C.Cast (te,ty) ->
255        process_body_aux te ;
256        process_body_aux ty
257     | C.Prod (_,sou,ta) ->
258        process_body_aux sou ;
259        process_body_aux ta
260     | C.Lambda (_,sou,ta) ->
261        process_body_aux sou ;
262        process_body_aux ta
263     | C.LetIn (_,te,ta)->
264        process_body_aux te ;
265        process_body_aux ta
266     | C.Appl l ->
267        List.iter process_body_aux l
268     | C.Const (uri,_) ->
269        UriHash.add_uri (U.string_of_uri uri) H.InBody
270     | C.Abst _ -> assert false
271     | C.MutInd (uri,_,typeno) ->
272        H.add_uri
273         (U.string_of_uri uri ^ "#xpointer(1/" ^
274           string_of_int (typeno + 1) ^ ")")
275         H.InBody
276     | C.MutConstruct (uri,_,typeno,consno) ->
277        H.add_uri
278         (U.string_of_uri uri ^ "#xpointer(1/" ^
279           string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
280         H.InBody
281     | C.MutCase (uri,_,typeno,outtype,term,patterns) ->
282        add_every_constructor uri typeno H.InBody ;
283        process_body_aux outtype ;
284        process_body_aux term ;
285        List.iter process_body_aux patterns
286     | C.Fix (_,funs) ->
287        List.iter
288         (function (_,_,bo,ty) ->
289           process_body_aux bo ;
290           process_body_aux ty ;
291         ) funs
292     | C.CoFix (_,funs) ->
293        List.iter
294         (function (_,bo,ty) ->
295           process_body_aux bo ;
296           process_body_aux ty ;
297         ) funs
298     | _ -> ()
299 in
300  process_body_aux
301 ;;
302
303 let process_obj string_uri =
304  let module U = UriManager in
305  let module C = Cic in
306   function
307      (C.Definition (_,bo,ty,_)) ->
308        process_type ty ;
309        process_body bo ;
310        output_file string_uri string_uri
311    | (C.Axiom (_,ty,_)) ->
312        process_type ty ;
313        output_file string_uri string_uri
314    | (C.Variable (_,bo,ty)) ->
315        process_type ty ;
316        begin
317         match bo with
318            (Some bo') -> process_body bo'
319          | _ -> ()
320        end ;
321        output_file string_uri string_uri
322    | (C.InductiveDefinition _) as id ->
323        begin
324         let id' =
325          CicSubstitution.undebrujin_inductive_def
326           (U.uri_of_string string_uri) id
327         in
328          match id' with
329             (C.InductiveDefinition (itys,_,_)) -> 
330               iteri
331                (fun (_,_,ty,cons) n ->
332                  let sn = string_of_int n in
333                   process_type ty ;
334                   output_file
335                    (string_uri ^ "#xpointer(1/" ^ sn ^ ")")
336                    (string_uri ^ "," ^ sn) ;
337                   iteri
338                    (fun (_,cty,_) m ->
339                      let sm = string_of_int m in
340                       process_type cty ;
341                       output_file
342                        (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
343                        (string_uri ^ "," ^ sn ^ "," ^ sm)
344                    ) cons
345                ) itys
346           | _ -> assert false
347        end
348    | (C.CurrentProof _) -> assert false
349 ;;
350
351 let mk_forward string_uri =
352  let module U = UriManager in
353   print_endline ("Now computing metadata of " ^ string_uri) ;
354   flush stdout ;
355   let uri = U.uri_of_string string_uri in
356   let obj = get_obj uri in
357    process_obj string_uri obj
358 ;;
359
360 let _ =
361  let usage_msg = "usage: mk_forward[.opt] URI" in
362  let uri = ref "" in
363   Arg.parse []
364    (fun x ->
365      if x = "" then
366       begin
367        prerr_string "No URI provided.\n" ;
368        Arg.usage [] usage_msg ;
369        exit (-1)
370       end
371      else if !uri = "" then
372       uri := x
373      else
374       begin
375        prerr_string "More than two arguments provided.\n" ;
376        Arg.usage [] usage_msg ;
377        exit (-1)
378       end
379    ) usage_msg ;
380    if !uri = "" then
381     begin
382      prerr_string "No URI provided.\n" ;
383      Arg.usage [] usage_msg ;
384      exit (-1)
385     end ;
386    mk_forward !uri
387 ;;