From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Apr 2005 08:30:30 +0000 (+0000)
Subject: - added no_hyp table
X-Git-Tag: after_svn_merge~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3feb47fdb6a5060b3b68f9fe435a17a2b9920f52;p=helm.git

- added no_hyp table
- changed constants number integer type to small int
- added comments describing tables
---

diff --git a/helm/metadata/sql/create_mowgli_tables.mysql.sql b/helm/metadata/sql/create_mowgli_tables.mysql.sql
index e2195891a..bc2e28460 100644
--- a/helm/metadata/sql/create_mowgli_tables.mysql.sql
+++ b/helm/metadata/sql/create_mowgli_tables.mysql.sql
@@ -22,11 +22,19 @@ CREATE TABLE objectName (
 );
 CREATE TABLE no_inconcl_aux (
     source varchar(255) binary not null,
-    no tinyint(4) not null
+    no smallint(6) not null
 );
 CREATE TABLE no_concl_hyp (
     source varchar(255) binary not null,
-    no tinyint(4) not null
+    no smallint(6) not null
+);
+CREATE TABLE no_hyp (
+    source varchar(255) binary unique not null,
+    no smallint(6) not null
+);
+CREATE TABLE owners (
+    source varchar(255) binary not null,
+    owner varchar(255) binary not null
 );
 
 CREATE INDEX refObj_source ON refObj (source);
@@ -38,4 +46,8 @@ CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source);
 CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no);
 CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source);
 CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no);
+CREATE INDEX no_hyp_no ON no_hyp (no);
+CREATE INDEX no_hyp_source ON no_hyp (source);
+CREATE INDEX owners_owner ON owners (owner);
+CREATE INDEX owners_source ON owners (source);
 
diff --git a/helm/metadata/sql/fill_inconcl_aux.sql b/helm/metadata/sql/fill_inconcl_aux.sql
index 2e7140e18..50146e0fd 100644
--- a/helm/metadata/sql/fill_inconcl_aux.sql
+++ b/helm/metadata/sql/fill_inconcl_aux.sql
@@ -1,4 +1,5 @@
 
+-- table mapping sources to number of distinct constants occurring in conclusion
 INSERT INTO no_inconcl_aux
 SELECT source, COUNT(h_occurrence)
 FROM refObj
diff --git a/helm/metadata/sql/fill_no_concl_hyp.sql b/helm/metadata/sql/fill_no_concl_hyp.sql
index 3294fe121..3c82358a2 100644
--- a/helm/metadata/sql/fill_no_concl_hyp.sql
+++ b/helm/metadata/sql/fill_no_concl_hyp.sql
@@ -1,4 +1,6 @@
 
+-- table mapping sources to number of distinct constants occurring everywhere
+-- except body
 INSERT INTO no_concl_hyp
 SELECT source, COUNT(DISTINCT h_occurrence)
 FROM refObj
diff --git a/helm/metadata/sql/fill_no_hyp.sql b/helm/metadata/sql/fill_no_hyp.sql
new file mode 100644
index 000000000..b920e1ca8
--- /dev/null
+++ b/helm/metadata/sql/fill_no_hyp.sql
@@ -0,0 +1,15 @@
+
+-- table mapping sources to number of distinct constants occurring in hypothesis
+INSERT INTO no_hyp
+SELECT source, COUNT(DISTINCT h_occurrence)
+FROM refObj
+WHERE (h_position="http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis"
+    OR h_position="http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis")
+GROUP BY source;
+
+INSERT IGNORE INTO no_hyp
+SELECT source, 0
+FROM refObj
+WHERE NOT (h_position="http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis"
+    OR h_position="http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis")
+GROUP BY source;