From: Enrico Tassi Date: Mon, 2 May 2005 12:53:56 +0000 (+0000) Subject: added Match (partially) and sync with the count table X-Git-Tag: single_binding~124 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e4659bb1bd31c92fa7c82fe502aabb1dc9dbb75;p=helm.git added Match (partially) and sync with the count table --- diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml index 93ec8c4b9..54f608692 100644 --- a/helm/matita/matita.conf.xml +++ b/helm/matita/matita.conf.xml @@ -8,10 +8,10 @@ gares
- - mowgli.cs.unibo.it + localhost + helm - matita + mowgli
true diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 362c6723a..47c9d9e9e 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1072,7 +1072,7 @@ Copyright (C) 2005, - 50 + 55 True Intros True @@ -1139,7 +1139,7 @@ Copyright (C) 2005, - 50 + 55 True Exact True @@ -1187,7 +1187,7 @@ Copyright (C) 2005, - 50 + 55 True Elim True @@ -1379,7 +1379,7 @@ Copyright (C) 2005, - 50 + 55 True Reflexivity True @@ -1446,7 +1446,7 @@ Copyright (C) 2005, - 50 + 55 True Transitivity True @@ -1500,7 +1500,7 @@ Copyright (C) 2005, - 50 + 55 True Simplify True @@ -1567,7 +1567,7 @@ Copyright (C) 2005, - 50 + 55 True Whd True @@ -1615,11 +1615,11 @@ Copyright (C) 2005, - 50 + 55 True Assumption True - asum + assum True GTK_RELIEF_NORMAL True @@ -1682,7 +1682,7 @@ Copyright (C) 2005, - 50 + 55 True Cut True diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index 93a1abaa5..a4f0f4f96 100644 --- 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 2d1c4d702..5abba5207 100644 --- 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