added Match (partially) and sync with the count table

diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml
index 93ec8c4b9afdca1b8490af2732e337e3957caa6a..54f608692f9c983be6673000fd285917e8a1e343 100644 (file)
--- a/helm/matita/matita.conf.xml
+++ b/helm/matita/matita.conf.xml
@@ -8,10 +8,10 @@
     <key name="owner">gares</key>
   </section>
   <section name="db">
-<!--     <key name="host">localhost</key> -->
-    <key name="host">mowgli.cs.unibo.it</key>
+    <key name="host">localhost</key>
+    <!--    <key name="host">mowgli.cs.unibo.it</key> --> 
     <key name="user">helm</key>
-    <key name="database">matita</key>
+    <key name="database">mowgli</key>
   </section>
   <section name="getter">
     <key name="prefetch">true</key>

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 362c6723a2ba25df9541418432ad05b6d891a797..47c9d9e9ebd11f59927d45d94fe2c5f9648ea427 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1072,7 +1072,7 @@ Copyright (C) 2005,
 
                                  <child>
                                    <widget class="GtkButton" id="introsButton">
-                                     <property name="width_request">50</property>
+                                     <property name="width_request">55</property>
                                      <property name="visible">True</property>
                                      <property name="tooltip" translatable="yes">Intros</property>
                                      <property name="can_focus">True</property>
@@ -1139,7 +1139,7 @@ Copyright (C) 2005,
 
                                  <child>
                                    <widget class="GtkButton" id="exactButton">
-                                     <property name="width_request">50</property>
+                                     <property name="width_request">55</property>
                                      <property name="visible">True</property>
                                      <property name="tooltip" translatable="yes">Exact</property>
                                      <property name="can_focus">True</property>
@@ -1187,7 +1187,7 @@ Copyright (C) 2005,
 
                              <child>
                                <widget class="GtkButton" id="elimButton">
-                                 <property name="width_request">50</property>
+                                 <property name="width_request">55</property>
                                  <property name="visible">True</property>
                                  <property name="tooltip" translatable="yes">Elim</property>
                                  <property name="can_focus">True</property>
@@ -1379,7 +1379,7 @@ Copyright (C) 2005,
 
                                  <child>
                                    <widget class="GtkButton" id="reflexivityButton">
-                                     <property name="width_request">50</property>
+                                     <property name="width_request">55</property>
                                      <property name="visible">True</property>
                                      <property name="tooltip" translatable="yes">Reflexivity</property>
                                      <property name="can_focus">True</property>
@@ -1446,7 +1446,7 @@ Copyright (C) 2005,
 
                                  <child>
                                    <widget class="GtkButton" id="transitivityButton">
-                                     <property name="width_request">50</property>
+                                     <property name="width_request">55</property>
                                      <property name="visible">True</property>
                                      <property name="tooltip" translatable="yes">Transitivity</property>
                                      <property name="can_focus">True</property>
@@ -1500,7 +1500,7 @@ Copyright (C) 2005,
 
                                  <child>
                                    <widget class="GtkButton" id="simplifyButton">
-                                     <property name="width_request">50</property>
+                                     <property name="width_request">55</property>
                                      <property name="visible">True</property>
                                      <property name="tooltip" translatable="yes">Simplify</property>
                                      <property name="can_focus">True</property>
@@ -1567,7 +1567,7 @@ Copyright (C) 2005,
 
                                  <child>
                                    <widget class="GtkButton" id="whdButton">
-                                     <property name="width_request">50</property>
+                                     <property name="width_request">55</property>
                                      <property name="visible">True</property>
                                      <property name="tooltip" translatable="yes">Whd</property>
                                      <property name="can_focus">True</property>
@@ -1615,11 +1615,11 @@ Copyright (C) 2005,
 
                              <child>
                                <widget class="GtkButton" id="assumptionButton">
-                                 <property name="width_request">50</property>
+                                 <property name="width_request">55</property>
                                  <property name="visible">True</property>
                                  <property name="tooltip" translatable="yes">Assumption</property>
                                  <property name="can_focus">True</property>
-                                 <property name="label" translatable="yes">asum</property>
+                                 <property name="label" translatable="yes">assum</property>
                                  <property name="use_underline">True</property>
                                  <property name="relief">GTK_RELIEF_NORMAL</property>
                                  <property name="focus_on_click">True</property>
@@ -1682,7 +1682,7 @@ Copyright (C) 2005,
 
                              <child>
                                <widget class="GtkButton" id="cutButton">
-                                 <property name="width_request">50</property>
+                                 <property name="width_request">55</property>
                                  <property name="visible">True</property>
                                  <property name="tooltip" translatable="yes">Cut</property>
                                  <property name="can_focus">True</property>

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 2d1c4d702f023c59b83439e69a62126d4cc83667..5abba5207e05e0a90febf538dc95a0dd551237e8 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -102,6 +102,22 @@ let eval_statement status mathviewer user_goal s =
           in
           List.iter prerr_endline l;
           prerr_endline "FINITA LA HINT"; assert false
+    | TacticAst.Match (_,term) -> 
+        let dbd = MatitaDb.instance () in
+        let metasenv = MatitaMisc.get_proof_metasenv status in
+        let context = MatitaMisc.get_proof_context status in
+        let aliases = MatitaMisc.get_proof_aliases status in
+        let (_env,_metasenv,term,_graph) = 
+          let interps =
+            MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term 
+          in
+          match interps with 
+          | [x] -> x
+          | _ -> assert false
+        in
+        List.iter prerr_endline (MetadataQuery.match_term ~dbd:dbd term);
+        assert false;
+
         | TacticAst.Check (_,t) ->
             let metasenv = MatitaMisc.get_proof_metasenv status in
             let context = MatitaMisc.get_proof_context status in
@@ -109,8 +125,7 @@ let eval_statement status mathviewer user_goal s =
             let db = MatitaDb.instance () in
             let (_env,_metasenv,term,_graph) = 
               let interps = 
-                MatitaDisambiguator.disambiguate_term db context metasenv 
-                  aliases t 
+                MatitaDisambiguator.disambiguate_term db context metasenv aliases t 
               in
               match interps with 
               | [x] -> x