]> matita.cs.unibo.it Git - helm.git/commitdiff
We add a binary for computing the "heights" of helm objects
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 26 Jul 2007 14:35:05 +0000 (14:35 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 26 Jul 2007 14:35:05 +0000 (14:35 +0000)
[this is related to the height of the dependece tree]

components/binaries/Makefile
components/binaries/heights/.depend [new file with mode: 0644]
components/binaries/heights/.depend.opt [new file with mode: 0644]
components/binaries/heights/Makefile [new file with mode: 0644]
components/binaries/heights/heights.conf.xml [new file with mode: 0644]
components/binaries/heights/heights.ml [new file with mode: 0644]
components/hmysql/hSql.mli
components/library/libraryDb.ml
components/library/libraryDb.mli

index db074309d2e221c6edbc50380af1374b3124c8bc..cd732517c066706a5f7ab7540acc288905d1b104 100644 (file)
@@ -3,7 +3,7 @@ H=@
 #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@%)
diff --git a/components/binaries/heights/.depend b/components/binaries/heights/.depend
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/components/binaries/heights/.depend.opt b/components/binaries/heights/.depend.opt
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/components/binaries/heights/Makefile b/components/binaries/heights/Makefile
new file mode 100644 (file)
index 0000000..d989d9c
--- /dev/null
@@ -0,0 +1,104 @@
+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
diff --git a/components/binaries/heights/heights.conf.xml b/components/binaries/heights/heights.conf.xml
new file mode 100644 (file)
index 0000000..9ecb8b6
--- /dev/null
@@ -0,0 +1,7 @@
+<?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>
diff --git a/components/binaries/heights/heights.ml b/components/binaries/heights/heights.ml
new file mode 100644 (file)
index 0000000..f77c6cb
--- /dev/null
@@ -0,0 +1,48 @@
+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   
index 6cfc8865542da846ed8acd777b48ce68df62b811..3c7de40ccb9950a211015ac7e9f099d72dde47e4 100644 (file)
@@ -65,6 +65,6 @@ val escape_string_for_like: dbtype -> dbd -> ('a,'b,'c,'a) format4
 
 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
 
index 9e5a13bdb1623241975169b24168ace7bbb8b783..7ee8427f74086da808c463fac9391a324897efa8 100644 (file)
 
 (* $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
@@ -33,12 +37,7 @@ let parse_dbd_conf _ =
     (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
@@ -176,10 +175,10 @@ let remove_uri uri =
   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 -> 
@@ -201,7 +200,7 @@ let xpointers_of_ind uri =
     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))
index d279f15eee46ae0bc3994c89ddaba6a86e9ffea8..e608a9c24a5ce9055c62e11ebcbd9f61e705a224 100644 (file)
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+val dbtype_of_string: string -> HSql.dbtype
+
 val instance: unit -> HSql.dbd
 val parse_dbd_conf: unit -> HSql.dbspec