1 (* Copyright (C) 2004, 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 prepare_insert () =
32 let insert_owner a b =
33 sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (owners_tbl ())a b
36 let insert_sort a b c d =
37 sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d, \"%s\")" (sort_tbl ())a b c d
39 let insert_rel a b c =
40 sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d)" (rel_tbl ()) a b c
42 let insert_obj a b c d =
43 sprintf "INSERT %s VALUES (\"%s\", \"%s\", \"%s\", %s)" (obj_tbl ()) a b c d
45 ((*insert_owner, *)insert_sort, insert_rel, insert_obj)
47 let execute_insert dbd ((*insert_owner, *)insert_sort, insert_rel, insert_obj)
48 uri (sort_cols, rel_cols, obj_cols)
50 (* ignore (Mysql.exec dbd (insert_owner uri owner)); *)
52 | [`String a; `String b; `Int c; `String d] ->
53 ignore (Mysql.exec dbd (insert_sort a b c d))
57 | [`String a; `String b; `Int c] ->
58 ignore (Mysql.exec dbd (insert_rel a b c))
62 | [`String a; `String b; `String c; `Int d] ->
63 ignore (Mysql.exec dbd (insert_obj a b c (string_of_int d)))
64 | [`String a; `String b; `String c; `Null] ->
65 ignore (Mysql.exec dbd (insert_obj a b c "NULL"))
69 let insert_const_no dbd uri =
71 sprintf "INSERT %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\""
72 (conclno_tbl ()) uri (obj_tbl ()) inconcl_pos mainconcl_pos uri
76 SELECT \"%s\",COUNT(DISTINCT h_occurrence)
78 WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
79 (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri
81 ignore (Mysql.exec dbd inconcl_no);
82 ignore (Mysql.exec dbd concl_hyp)
84 let insert_name ~dbd ~uri ~name =
86 sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name
88 ignore (Mysql.exec dbd query)
91 MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
93 (* TODO ZACK: verify if an object has already been indexed *)
94 let already_indexed _ = false
96 let index_constant ~dbd =
97 let query = prepare_insert () in
99 if not (already_indexed uri) then begin
100 let name = UriManager.name_of_uri uri in
101 let uri = UriManager.string_of_uri uri in
102 let metadata = MetadataExtractor.compute ~body ~ty in
103 let columns = MetadataPp.columns_of_metadata ~about:uri metadata in
104 execute_insert dbd query uri (columns :> columns);
105 insert_const_no dbd uri;
106 insert_name ~dbd ~uri ~name
109 let index_inductive_def ~dbd =
110 let query = prepare_insert () in
112 if not (already_indexed uri) then begin
113 let metadata = MetadataExtractor.compute_ind ~uri ~types in
114 let uri_of (a,b,c) = a in
115 let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in
116 let uri = UriManager.string_of_uri uri in
117 let columns = MetadataPp.columns_of_ind_metadata metadata in
118 execute_insert dbd query uri (columns :> columns);
119 List.iter (insert_const_no dbd) uris;
120 List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata
123 let tables_to_clean =
124 [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl; hypno_tbl]
126 let clean ~(dbd:Mysql.dbd) =
127 let owned_uris = (* list of uris in list-of-columns format *)
128 let query = sprintf "SELECT source FROM %s" (obj_tbl ()) in
129 let result = Mysql.exec dbd query in
130 let uris = Mysql.map result (fun cols ->
133 | None -> assert false) in
134 (* and now some stuff to remove #xpointers and duplicates *)
139 sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) s
142 (fun source_col -> ignore (Mysql.exec dbd (query source_col)))
145 List.iter del_from tables_to_clean;
148 let unindex ~dbd ~uri =
149 let uri = UriManager.string_of_uri uri in
152 sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" (tbl ()) uri
154 ignore (Mysql.exec dbd (query tbl))
156 List.iter del_from tables_to_clean