]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/metadata/metadataDb.ml
The getter maps are now dumped also if matitac exits abruptly.
[helm.git] / helm / ocaml / metadata / metadataDb.ml
1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
24  *)
25
26 open MetadataTypes
27
28 open Printf
29
30 let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) =
31   let sort_tuples = 
32     List.fold_left (fun s l -> match l with
33       | [`String a; `String b; `Int c; `String d] -> 
34           sprintf "(\"%s\", \"%s\", %d, \"%s\")" a b c d :: s
35       | _ -> assert false )
36     [] sort_cols
37   in
38   let rel_tuples =
39     List.fold_left (fun s l -> match l with
40       | [`String a; `String b; `Int c] ->
41           sprintf "(\"%s\", \"%s\", %d)" a b c :: s
42       | _ -> assert false)
43     [] rel_cols  
44   in
45   let obj_tuples = List.fold_left (fun s l -> match l with
46       | [`String a; `String b; `String c; `Int d] ->
47           sprintf "(\"%s\", \"%s\", \"%s\", %d)" a b c d :: s
48       | [`String a; `String b; `String c; `Null] ->
49           sprintf "(\"%s\", \"%s\", \"%s\", %s)" a b c "NULL" :: s
50       | _ -> assert false)
51     [] obj_cols
52   in
53   if sort_tuples <> [] then
54     begin
55     let query_sort = 
56       sprintf "INSERT %s VALUES %s;" (sort_tbl ()) (String.concat "," sort_tuples) 
57     in
58     ignore (Mysql.exec dbd query_sort)
59     end;
60   if rel_tuples <> [] then
61     begin
62     let query_rel = 
63       sprintf "INSERT %s VALUES %s;" (rel_tbl ()) (String.concat "," rel_tuples) 
64     in
65     ignore (Mysql.exec dbd query_rel)
66     end;
67   if obj_tuples <> [] then
68     begin
69     let query_obj = 
70       sprintf "INSERT %s VALUES %s;" (obj_tbl ()) (String.concat "," obj_tuples) 
71     in
72     ignore (Mysql.exec dbd query_obj)
73     end
74   
75     
76 let count_distinct position l =
77   MetadataConstraints.StringSet.cardinal
78   (List.fold_left (fun acc d -> 
79     match position with
80     | `Conclusion -> 
81          (match d with
82          | `Obj (name,`InConclusion) 
83          | `Obj (name,`MainConclusion _ ) -> 
84              MetadataConstraints.StringSet.add name acc
85          | _ -> acc)
86     | `Hypothesis ->
87         (match d with
88         | `Obj (name,`InHypothesis) 
89         | `Obj (name,`MainHypothesis _) -> 
90             MetadataConstraints.StringSet.add name acc
91         | _ -> acc)
92     | `Statement ->
93         (match d with
94         | `Obj (name,`InBody) -> acc
95         | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc
96         | _ -> acc)
97     ) MetadataConstraints.StringSet.empty l)
98 (*    
99 let insert_const_no dbd uri =
100   let term = CicUtil.term_of_uri uri in 
101   let ty = CicTypeChecker.type_of_aux' 
102   let inconcl_no =
103     sprintf "INSERT %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\""
104       (conclno_tbl ()) uri (obj_tbl ()) inconcl_pos mainconcl_pos uri
105   in
106   let concl_hyp =
107     sprintf "INSERT %s
108         SELECT \"%s\",COUNT(DISTINCT h_occurrence)
109         FROM %s
110         WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
111       (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri
112   in
113   ignore (Mysql.exec dbd inconcl_no);
114   ignore (Mysql.exec dbd concl_hyp)
115 *)
116 let insert_const_no dbd (uri,metadata) =
117   let no_concl = count_distinct `Conclusion metadata in
118   let no_hyp = count_distinct `Hypothesis metadata in
119   let no_full = count_distinct `Statement metadata in
120   let insert = 
121     sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)" 
122       (count_tbl ()) uri no_concl no_hyp no_full
123   in
124   ignore (Mysql.exec dbd insert)
125   
126 let insert_name ~dbd ~uri ~name =
127   let query =
128     sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name
129   in
130   ignore (Mysql.exec dbd query)
131
132 type columns =
133   MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
134
135   (* TODO ZACK: verify if an object has already been indexed *)
136 let already_indexed _ = false
137 (*
138 let index_constant ~dbd =
139   let query = prepare_insert () in
140   fun ~uri ~body ~ty  ->
141     if not (already_indexed uri) then begin
142       let name = UriManager.name_of_uri uri in
143       let uri = UriManager.string_of_uri uri in
144       let metadata = MetadataExtractor.compute ~body ~ty in
145       let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
146       execute_insert dbd query uri (columns :> columns);
147       insert_const_no dbd uri;
148       insert_name ~dbd ~uri ~name
149     end
150
151 let index_inductive_def ~dbd =
152   let query = prepare_insert () in
153   fun ~uri ~types ->
154     if not (already_indexed uri) then begin
155       let metadata = MetadataExtractor.compute_obj uri in
156       let uri_of (a,b,c) = a in
157       let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
158       let uri = UriManager.string_of_uri uri in
159       let columns = MetadataPp.columns_of_ind_metadata metadata in
160       execute_insert dbd query uri (columns :> columns);
161       List.iter (insert_const_no dbd) uris;
162       List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
163     end
164 *)
165 let index_obj ~dbd ~uri = 
166   if not (already_indexed uri) then begin
167     let metadata = MetadataExtractor.compute_obj uri in
168     let uri_of (a,b,c) = (a,c) in
169     let uri = UriManager.string_of_uri uri in
170     let columns = MetadataPp.columns_of_metadata metadata in
171     execute_insert dbd uri (columns :> columns);
172     List.iter (insert_const_no dbd) (List.map uri_of metadata);
173     List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
174   end
175   
176
177 let tables_to_clean =
178   [sort_tbl; rel_tbl; obj_tbl; name_tbl; count_tbl]
179
180 let clean ~(dbd:Mysql.dbd) =
181   let owned_uris =  (* list of uris in list-of-columns format *)
182     let query = sprintf "SELECT source FROM %s" (name_tbl ()) in
183     let result = Mysql.exec dbd query in
184     let uris = Mysql.map result (fun cols ->
185       match cols.(0) with
186       | Some src -> src
187       | None -> assert false) in
188     (* and now some stuff to remove #xpointers and duplicates *)
189     uris
190   in
191   let del_from tbl =
192     let query s = 
193       sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) s 
194     in
195     List.iter
196       (fun source_col -> ignore (Mysql.exec dbd (query source_col)))
197       owned_uris
198   in
199   List.iter del_from tables_to_clean;
200   owned_uris
201
202 let unindex ~dbd ~uri =
203   let uri = UriManager.string_of_uri uri in
204   let del_from tbl =
205     let query tbl =
206       sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri
207     in
208     ignore (Mysql.exec dbd (query tbl))
209   in
210   List.iter del_from tables_to_clean
211