#CSC: saturate is broken after the huge refactoring of auto/paramodulation
#CSC: by Andrea
#BINARIES=extractor table_creator utilities saturate
-BINARIES=extractor table_creator utilities transcript
+BINARIES=extractor table_creator utilities transcript heights
all: $(BINARIES:%=rec@all@%)
opt: $(BINARIES:%=rec@opt@%)
--- /dev/null
+include ../../../Makefile.defs
+
+H=@
+
+REQUIRES = helm-library
+
+MLS = heights.ml
+MLIS =
+CLEAN =
+
+LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+
+CMOS = $(MLS:%.ml=%.cmo)
+CMXS = $(MLS:%.ml=%.cmx)
+CMIS = $(MLIS:%.mli=%.cmi)
+EXTRAS =
+
+OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg
+OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg
+OCAMLDEP = $(OCAMLFIND) ocamldep
+OCAMLYACC = ocamlyacc
+OCAMLLEX = ocamllex
+
+all: heights .depend
+ @echo -n
+
+opt: heights.opt $(EXTRAS) .depend.opt
+ @echo -n
+
+heights: $(CMIS) $(CMOS) $(EXTRAS)
+ @echo " OCAMLC $(CMOS)"
+ $(H)$(OCAMLC) -o $@ $(CMOS)
+
+heights.opt: $(CMIS) $(CMXS) $(EXTRAS)
+ @echo " OCAMLOPT $(CMXS)"
+ $(H)$(OCAMLOPT) -o $@ $(CMXS)
+
+clean:
+ $(H)rm -f *.cm[iox] *.a *.o *.output
+ $(H)rm -f heights heights.opt $(CLEAN)
+
+.depend: $(MLIS) $(MLS) $(EXTRAS)
+ @echo " OCAMLDEP $(MLIS) $(MLS)"
+ $(H)$(OCAMLDEP) $(MLIS) $(MLS) > .depend
+
+.depend.opt: $(MLIS) $(MLS) $(EXTRAS)
+ @echo " OCAMLDEP -native $(MLIS) $(MLS)"
+ $(H)$(OCAMLDEP) -native $(MLIS) $(MLS) > .depend.opt
+
+test: heights heights.conf.xml
+ @echo " HEIGHTS"
+ $(H)$< 1> heights.txt 2> errors.txt
+
+test.opt: heights.opt heights.conf.xml $(PACKAGES:%=%.conf.xml)
+ @echo " HEIGHTS.OPT"
+ $(H)$< 1> heights.txt 2> errors.txt
+
+export: clean
+ $(H)rm -f *~
+ @echo " TAR heights"
+ $(H)cd .. && tar --exclude=heights/.svn -czf heights.tgz heights
+
+depend: .depend
+
+depend.opt: .depend.opt
+
+%.cmi: %.mli $(EXTRAS)
+ @echo " OCAMLC $<"
+ $(H)$(OCAMLC) -c $<
+%.cmo %.cmi: %.ml $(EXTRAS) $(LIBRARIES)
+ @echo " OCAMLC $<"
+ $(H)$(OCAMLC) -c $<
+%.cmx: %.ml $(EXTRAS) $(LIBRARIES_OPT)
+ @echo " OCAMLOPT $<"
+ $(H)$(OCAMLOPT) -c $<
+%.ml %.mli: %.mly $(EXTRAS)
+ @echo " OCAMLYACC $<"
+ $(H)$(OCAMLYACC) -v $<
+%.ml: %.mll $(EXTRAS)
+ @echo " OCAMLLEX $<"
+ $(H)$(OCAMLLEX) $<
+
+include ../../../Makefile.defs
+
+ifeq ($(MAKECMDGOALS),)
+ include .depend
+endif
+
+ifeq ($(MAKECMDGOALS), all)
+ include .depend
+endif
+
+ifeq ($(MAKECMDGOALS), opt)
+ include .depend.opt
+endif
+
+ifeq ($(MAKECMDGOALS), test)
+ include .depend
+endif
+
+ifeq ($(MAKECMDGOALS), test.opt)
+ include .depend.opt
+endif
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="db">
+ <key name="metadata">mysql://mowgli.cs.unibo.it mowgli helm none legacy</key>
+ <key name="type">legacy</key>
+ </section>
+</helm_registry>
--- /dev/null
+module Registry = Helm_registry
+module SQL = HSql
+module DB = LibraryDb
+
+let tbl = Hashtbl.create 50147
+let ord = ref 1
+let conf_file = ref "heights.conf.xml"
+
+let rec mesure db_type dbd prim str =
+ try
+ let h, p = Hashtbl.find tbl str in
+ if prim then begin
+ if p > 0 then Printf.eprintf "Hit %2u: %s\n" (succ p) str;
+ Hashtbl.replace tbl str (h, succ p)
+ end;
+ h
+ with Not_found ->
+ let query =
+ Printf.sprintf "SELECT h_occurrence FROM refObj WHERE source = '%s'"
+ (SQL.escape db_type dbd str)
+ in
+ let result = SQL.exec db_type dbd query in
+ let f res = match res.(0) with
+ | Some str -> mesure db_type dbd false str
+ | None -> assert false
+ in
+ let hs = SQL.map result ~f in
+ let h = succ (List.fold_left max 0 hs) in
+ Printf.printf "%3u %5u %s\n" h !ord str; flush stdout;
+ ord := succ !ord;
+ let p = if prim then 1 else 0 in
+ Hashtbl.add tbl str (h, p); h
+
+let scan_objs db_type dbd =
+ let query = "SELECT source FROM objectName" in
+ let result = SQL.exec db_type dbd query in
+ let f res = match res.(0) with
+ | Some str -> ignore (mesure db_type dbd true str)
+ | None -> assert false
+ in
+ SQL.iter result ~f
+
+let _ =
+ Registry.load_from !conf_file;
+ let db_type = DB.dbtype_of_string (Registry.get_string "db.type") in
+ let db_spec = DB.parse_dbd_conf () in
+ let dbd = SQL.quick_connect db_spec in
+ scan_objs db_type dbd
val isMysql : dbtype -> dbd -> bool
-(* this dbd can't du queries, used only in table_creator *)
+(* this dbd can't do queries, used only in table_creator *)
val fake_db_for_mysql: dbtype -> dbd
(* $Id$ *)
-open Printf ;;
+let dbtype_of_string dbtype =
+ if dbtype = "library" then HSql.Library
+ else if dbtype = "user" then HSql.User
+ else if dbtype = "legacy" then HSql.Legacy
+ else raise (HSql.Error "HSql: wrong config file format")
let parse_dbd_conf _ =
let metadata = Helm_registry.get_list Helm_registry.string "db.metadata" in
(fun s ->
match Pcre.split ~pat:"\\s+" s with
| [path;db;user;pwd;dbtype] ->
- let dbtype =
- if dbtype = "library" then HSql.Library
- else if dbtype = "user" then HSql.User
- else if dbtype = "legacy" then HSql.Legacy
- else raise (HSql.Error "HSql: wrong config file format")
- in
+ let dbtype = dbtype_of_string dbtype in
let pwd = if pwd = "none" then None else Some pwd in
(* TODO parse port *)
path, None, db, user, pwd, dbtype
in
let query table suri =
if HSql.isMysql dbtype dbd then
- sprintf "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table
+ Printf.sprintf "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table
(HSql.escape dbtype dbd suri)
else
- sprintf "DELETE FROM %s WHERE source='%s'" table
+ Printf.sprintf "DELETE FROM %s WHERE source='%s'" table
(HSql.escape dbtype dbd suri)
in
List.iter (fun t ->
Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_"
(HSql.escape dbtype dbd s)
in
- let query = sprintf
+ let query = Printf.sprintf
("SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' "
^^ HSql.escape_string_for_like dbtype dbd)
name_tbl (escape (UriManager.string_of_uri uri))
* http://helm.cs.unibo.it/
*)
+val dbtype_of_string: string -> HSql.dbtype
+
val instance: unit -> HSql.dbd
val parse_dbd_conf: unit -> HSql.dbspec