X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataDb.ml;h=7eaf4d88167b875957853bbe0f1b1fd875520ed9;hb=275727242ccdce9df01af65f3bfb2d65283fa197;hp=f4ce2dd395d9137eb1ab239b499f186af0ec6c6b;hpb=4bc5e3edbedb79e13f16a09abe18ee38e9c78a20;p=helm.git diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index f4ce2dd39..7eaf4d881 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -27,93 +27,106 @@ open MetadataTypes open Printf -let prepare_insert (dbh: Dbi.connection) = - let insert_owner = - dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\")" owners_tbl) +let prepare_insert () = + let insert_owner a b = + sprintf "INSERT %s VALUES (\"%s\", \"%s\")" owners_tbl a b in - let insert_sort = - dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?,\"?\")" sort_tbl) + let insert_sort a b c d = + sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d, \"%s\")" sort_tbl a b c d in - let insert_rel = - dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",?)" rel_tbl) + let insert_rel a b c = + sprintf "INSERT %s VALUES (\"%s\", \"%s\", %d)" rel_tbl a b c in - let insert_obj = - dbh#prepare (sprintf "INSERT INTO %s VALUES (\"?\",\"?\",\"?\",?)" obj_tbl) + let insert_obj a b c d = + sprintf "INSERT %s VALUES (\"%s\", \"%s\", \"%s\", %s)" obj_tbl a b c d in (insert_owner, insert_sort, insert_rel, insert_obj) -let execute_insert dbh (insert_owner, insert_sort, insert_rel, insert_obj) +let execute_insert dbd (insert_owner, insert_sort, insert_rel, insert_obj) uri owner (sort_cols, rel_cols, obj_cols) = - insert_owner#execute [`String uri; `String owner]; - List.iter insert_sort#execute sort_cols; - List.iter insert_rel#execute rel_cols; - List.iter insert_obj#execute obj_cols + ignore (Mysql.exec dbd (insert_owner uri owner)); + List.iter (function + | [`String a; `String b; `Int c; `String d] -> + ignore (Mysql.exec dbd (insert_sort a b c d)) + | _ -> assert false) + sort_cols; + List.iter (function + | [`String a; `String b; `Int c] -> + ignore (Mysql.exec dbd (insert_rel a b c)) + | _ -> assert false) + rel_cols; + List.iter (function + | [`String a; `String b; `String c; `Int d] -> + ignore (Mysql.exec dbd (insert_obj a b c (string_of_int d))) + | [`String a; `String b; `String c; `Null] -> + ignore (Mysql.exec dbd (insert_obj a b c "NULL")) + | _ -> assert false) + obj_cols -let insert_const_no dbh uri = +let insert_const_no dbd uri = let inconcl_no = - sprintf "INSERT INTO %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\"" + sprintf "INSERT %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\"" conclno_tbl uri obj_tbl inconcl_pos mainconcl_pos uri in let concl_hyp = - sprintf "INSERT INTO %s + sprintf "INSERT %s SELECT \"%s\",COUNT(DISTINCT h_occurrence) FROM %s WHERE NOT (h_position=\"%s\") AND (source = \"%s\")" conclno_hyp_tbl uri obj_tbl inbody_pos uri in - (dbh#prepare inconcl_no)#execute []; - (dbh#prepare concl_hyp)#execute [] + ignore (Mysql.exec dbd inconcl_no); + ignore (Mysql.exec dbd concl_hyp) -let insert_name ~dbh ~uri ~name = +let insert_name ~dbd ~uri ~name = let query = - dbh#prepare - (sprintf "INSERT INTO %s VALUES (\"%s\", \"%s\")" name_tbl uri name) + sprintf "INSERT %s VALUES (\"%s\", \"%s\")" name_tbl uri name in - query#execute [] + ignore (Mysql.exec dbd query) -type dbi_columns = - Dbi.sql_t list list * Dbi.sql_t list list * Dbi.sql_t list list +type columns = + MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list -let index_constant ~dbh = - let query = prepare_insert dbh in +let index_constant ~dbd = + let query = prepare_insert () in fun ~owner ~uri ~body ~ty -> let name = UriManager.name_of_uri uri in let uri = UriManager.string_of_uri uri in let metadata = MetadataExtractor.compute ~body ~ty in let columns = MetadataPp.columns_of_metadata ~about:uri metadata in - execute_insert dbh query uri owner (columns :> dbi_columns); - insert_const_no dbh uri; - insert_name ~dbh ~uri ~name + execute_insert dbd query uri owner (columns :> columns); + insert_const_no dbd uri; + insert_name ~dbd ~uri ~name -let index_inductive_def ~dbh = - let query = prepare_insert dbh in +let index_inductive_def ~dbd = + let query = prepare_insert () in fun ~owner ~uri ~types -> let metadata = MetadataExtractor.compute_ind ~uri ~types in let uri_of (a,b,c) = a in let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in let uri = UriManager.string_of_uri uri in let columns = MetadataPp.columns_of_ind_metadata metadata in - execute_insert dbh query uri owner (columns :> dbi_columns); - List.iter (insert_const_no dbh) uris; - List.iter (fun (uri, name, _) -> insert_name ~dbh ~uri ~name) metadata + execute_insert dbd query uri owner (columns :> columns); + List.iter (insert_const_no dbd) uris; + List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata -let clean ~(dbh: Dbi.connection) ~owner = +let clean ~(dbd:Mysql.dbd) ~owner = let owned_uris = (* list of uris in list-of-columns format *) let query = - dbh#prepare (sprintf - "SELECT source FROM %s WHERE owner = \"%s\"" owners_tbl owner) + sprintf "SELECT source FROM %s WHERE owner = \"%s\"" owners_tbl owner in - query#execute []; - List.map - (function [`String source_col] -> source_col | _ -> assert false) - (query#fetchall ()) + let result = Mysql.exec dbd query in + Mysql.map result (fun cols -> + match cols.(0) with + | Some src -> src + | None -> assert false) in let del_from tbl = - let query = - dbh#prepare (sprintf "DELETE FROM %s WHERE source LIKE \"?%%\"" tbl) - in - List.iter (fun source_col -> query#execute [`String source_col]) owned_uris + let query s = sprintf "DELETE FROM %s WHERE source LIKE \"%s%%\"" tbl s in + List.iter + (fun source_col -> ignore (Mysql.exec dbd (query source_col))) + owned_uris in List.iter del_from [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl;