]> matita.cs.unibo.it Git - helm.git/blob - components/binaries/heights/heights.ml
tagged 0.5.0-rc1
[helm.git] / components / binaries / heights / heights.ml
1 module Registry = Helm_registry
2 module SQL = HSql
3 module DB = LibraryDb
4
5 let tbl = Hashtbl.create 50147
6 let ord = ref 1
7 let conf_file = ref "heights.conf.xml"
8
9 let rec mesure db_type dbd prim str =
10    try 
11       let h, p = Hashtbl.find tbl str in 
12       if prim then begin
13          if p > 0 then Printf.eprintf "Hit %2u: %s\n" (succ p) str;
14          Hashtbl.replace tbl str (h, succ p)
15       end;
16       h
17    with Not_found -> 
18    let query = 
19       Printf.sprintf "SELECT h_occurrence FROM refObj WHERE source = '%s'"
20       (SQL.escape db_type dbd str)
21    in
22    let result = SQL.exec db_type dbd query in
23    let f res = match res.(0) with
24       | Some str -> mesure db_type dbd false str
25       | None     -> assert false 
26    in
27    let hs = SQL.map result ~f in
28    let h = succ (List.fold_left max 0 hs) in
29    Printf.printf "%3u %5u %s\n" h !ord str; flush stdout;
30    ord := succ !ord;
31    let p = if prim then 1 else 0 in
32    Hashtbl.add tbl str (h, p); h
33
34 let scan_objs db_type dbd =
35    let query = "SELECT source FROM objectName" in
36    let result = SQL.exec db_type dbd query in
37    let f res = match res.(0) with
38       | Some str -> ignore (mesure db_type dbd true str)
39       | None     -> assert false
40    in
41    SQL.iter result ~f
42
43 let _ =
44    Registry.load_from !conf_file;
45    let db_type = DB.dbtype_of_string (Registry.get_string "db.type") in
46    let db_spec = DB.parse_dbd_conf () in
47    let dbd = SQL.quick_connect db_spec in
48    scan_objs db_type dbd