]> matita.cs.unibo.it Git - helm.git/blob - helm/metadata/create2/touch/touch.ml
Modified Files:
[helm.git] / helm / metadata / create2 / touch / touch.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  "backward" ^
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 let touch_file rdf_string_uri =
52  let module U = UriManager in
53   let rdf_uri = U.uri_of_string rdf_string_uri in
54    make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ;
55    ignore (
56     Unix.system
57      ("touch \"" ^ (pathname_of_uri rdf_string_uri) ^ "\"")
58    )
59 ;;
60
61 let get_obj uri =
62  let cicfilename = Getter.getxml uri in
63   let res = CicParser.obj_of_xml cicfilename uri in
64    Unix.unlink cicfilename ;
65    res
66 ;;
67
68 let touch_obj string_uri =
69  let module U = UriManager in
70  let module C = Cic in
71   function
72      Some (C.InductiveDefinition (itys,_,_)) ->
73       iteri
74        (fun (_,_,_,cons) n ->
75          let sn = string_of_int n in
76           touch_file
77            (string_uri ^ "," ^ sn) ;
78           iteri
79            (fun (_,_,_) m ->
80              let sm = string_of_int m in
81               touch_file
82                (string_uri ^ "," ^ sn ^ "," ^ sm)
83            ) cons
84        ) itys
85    | Some _ -> assert false
86    | None ->
87       touch_file string_uri
88 ;;
89
90 let touch string_uri =
91  let module S = String in
92  let module U = UriManager in
93   print_endline ("Now touching metadata file for " ^ string_uri) ;
94   flush stdout ;
95   let uri = U.uri_of_string string_uri in
96   let obj =
97    if S.sub string_uri (S.length string_uri - 3) 3 = "ind" then
98     Some (get_obj uri)
99    else
100     None
101   in
102    touch_obj string_uri obj
103 ;;
104
105 let _ =
106  let usage_msg = "usage: touch[.opt] URI" in
107  let uri = ref "" in
108   Arg.parse []
109    (fun x ->
110      if x = "" then
111       begin
112        prerr_string "No URI provided.\n" ;
113        Arg.usage [] usage_msg ;
114        exit (-1)
115       end
116      else if !uri = "" then
117       uri := x
118      else
119       begin
120        prerr_string "More than two arguments provided.\n" ;
121        Arg.usage [] usage_msg ;
122        exit (-1)
123       end
124    ) usage_msg ;
125    if !uri = "" then
126     begin
127      prerr_string "No URI provided.\n" ;
128      Arg.usage [] usage_msg ;
129      exit (-1)
130     end ;
131    touch !uri
132 ;;