added Match (partially) and sync with the count table

[helm.git] / helm / matita / matitaDb.ml

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index 93a1abaa5a731d34c81f044fbb8cc76787d0b3fc..a4f0f4f96f4f76834182df484c3fcf9e76043eb4 100644 (file)
--- a/helm/matita/matitaDb.ml
+++ b/helm/matita/matitaDb.ml
@@ -45,15 +45,17 @@ let clean_owner_environment () =
   let sort_tbl = MetadataTypes.sort_tbl () in
   let rel_tbl = MetadataTypes.rel_tbl () in
   let name_tbl =  MetadataTypes.name_tbl () in
-  let conclno_tbl = MetadataTypes.conclno_tbl () in
-  let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
+  (*let conclno_tbl = MetadataTypes.conclno_tbl () in
+  let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in*)
+  let count_tbl = MetadataTypes.count_tbl () in
   let statements = [
     sprintf "DROP TABLE %s ;" obj_tbl;
     sprintf "DROP TABLE %s ;" sort_tbl;
     sprintf "DROP TABLE %s ;" rel_tbl;
     sprintf "DROP TABLE %s ;" name_tbl;
-    sprintf "DROP TABLE %s ;" conclno_tbl;
-    sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in
+    sprintf "DROP TABLE %s ;" count_tbl
+    (*sprintf "DROP TABLE %s ;" conclno_tbl;
+    sprintf "DROP TABLE %s ;" conclno_hyp_tbl*) ] in
 (*
 DROP INDEX refObj_source ON refObj (source);
 DROP INDEX refObj_target ON refObj (h_occurrence);
@@ -97,8 +99,9 @@ let create_owner_environment () =
   let sort_tbl = MetadataTypes.sort_tbl () in
   let rel_tbl = MetadataTypes.rel_tbl () in
   let name_tbl =  MetadataTypes.name_tbl () in
-  let conclno_tbl = MetadataTypes.conclno_tbl () in
-  let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
+  (*let conclno_tbl = MetadataTypes.conclno_tbl () in
+  let conclno_hyp_tbl = MetadataTypes.fullno_tbl ()*) 
+  let count_tbl = MetadataTypes.count_tbl () in
   let statements = [
     sprintf "CREATE TABLE %s (
                   source varchar(255) binary not null,
@@ -121,14 +124,21 @@ let create_owner_environment () =
                   source varchar(255) binary not null,
                   value varchar(255) binary not null
               );" name_tbl;
-    sprintf "CREATE TABLE %s (
+   sprintf "CREATE TABLE %s (
+    source varchar(255) binary unique not null,
+    conclusion smallint(6) not null,
+    hypothesis smallint(6) not null,
+    statement smallint(6) not null
+);" count_tbl
+           
+   (* sprintf "CREATE TABLE %s (
                   source varchar(255) binary not null,
                   no tinyint(4) not null
               );" conclno_tbl;
     sprintf "CREATE TABLE %s (
                   source varchar(255) binary not null,
                   no tinyint(4) not null
-              );" conclno_hyp_tbl ] in
+              );" conclno_hyp_tbl *)] in
 (*
 CREATE INDEX refObj_source ON refObj (source);
 CREATE INDEX refObj_target ON refObj (h_occurrence);
@@ -164,8 +174,10 @@ let remove_uri uri =
   let sort_tbl = MetadataTypes.sort_tbl () in
   let rel_tbl = MetadataTypes.rel_tbl () in
   let name_tbl =  MetadataTypes.name_tbl () in
-  let conclno_tbl = MetadataTypes.conclno_tbl () in
-  let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in
+  (*let conclno_tbl = MetadataTypes.conclno_tbl () in
+  let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in*)
+  let count_tbl = MetadataTypes.count_tbl () in
+  
   let dbd = instance () in
   let suri = UriManager.string_of_uri uri in 
   let query table suri = sprintf 
@@ -176,7 +188,8 @@ let remove_uri uri =
       ignore (Mysql.exec dbd (query t suri))
     with
       exn -> raise exn (* no errors should be accepted *)
-    ) [obj_tbl;sort_tbl;rel_tbl;name_tbl;conclno_tbl;conclno_hyp_tbl];
+    )
+  [obj_tbl;sort_tbl;rel_tbl;name_tbl;(*conclno_tbl;conclno_hyp_tbl*)count_tbl];
   (* and now the debug job *)  
   let dbg_q = 
     sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri