From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 3 May 2005 12:50:12 +0000 (+0000)
Subject: fix for instance
X-Git-Tag: single_binding~119
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5edfd170706c91c5d3a9d3522360b748a2dc034f;p=helm.git

fix for instance
---

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 23a8b8e67..e01b7e7ed 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -97,6 +97,7 @@ type 'term macro =
   | Check of loc * 'term 
   | Hint of loc
   | Match of loc * 'term 
+  | Instance of loc * 'term 
   | Quit of loc
   | Redo of loc * int option
   | Undo of loc * int option
diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend
index e2a4669b3..48a53815c 100644
--- a/helm/ocaml/metadata/.depend
+++ b/helm/ocaml/metadata/.depend
@@ -7,11 +7,11 @@ metadataExtractor.cmo: metadataTypes.cmi metadataExtractor.cmi
 metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi 
 metadataPp.cmo: metadataTypes.cmi metadataPp.cmi 
 metadataPp.cmx: metadataTypes.cmx metadataPp.cmi 
-metadataDb.cmo: metadataTypes.cmi metadataPp.cmi metadataExtractor.cmi \
-    metadataDb.cmi 
-metadataDb.cmx: metadataTypes.cmx metadataPp.cmx metadataExtractor.cmx \
-    metadataDb.cmi 
 metadataConstraints.cmo: metadataTypes.cmi metadataPp.cmi \
     metadataConstraints.cmi 
 metadataConstraints.cmx: metadataTypes.cmx metadataPp.cmx \
     metadataConstraints.cmi 
+metadataDb.cmo: metadataTypes.cmi metadataPp.cmi metadataExtractor.cmi \
+    metadataConstraints.cmi metadataDb.cmi 
+metadataDb.cmx: metadataTypes.cmx metadataPp.cmx metadataExtractor.cmx \
+    metadataConstraints.cmx metadataDb.cmi 
diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index cbeaad49d..952aa5a57 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -151,6 +151,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   let (n,from,where) =
     List.fold_left (add_constraint tables) (0,[],[]) metadata
   in
+  let selected = if metadata = [] then count_tbl else "table0" in
   let (n,from,where) =
     add_all_constr count_tbl (n,from,where) concl_card full_card diff
   in
@@ -158,12 +159,12 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   let where = String.concat " and " where in
   let query =
     match rating with
-    | None -> sprintf "select table0.source from %s where %s" from where
+    | None -> sprintf "select %s.source from %s where %s" selected from where
     | Some `Hits ->
         sprintf
-          ("select table0.source from %s, hits where %s"
-           ^^ " and hits.source = table0.source order by hits.no desc")
-          from where
+          ("select %s.source from %s, hits where %s"
+           ^^ " and hits.source = %s.source order by hits.no desc")
+          selected from where selected
   in
   prerr_endline query; 
   let result = Mysql.exec dbd query in
diff --git a/helm/ocaml/metadata/metadataDb.mli b/helm/ocaml/metadata/metadataDb.mli
index 20f618f8d..672c900eb 100644
--- a/helm/ocaml/metadata/metadataDb.mli
+++ b/helm/ocaml/metadata/metadataDb.mli
@@ -35,3 +35,7 @@ val clean: dbd:Mysql.dbd -> string list
 
 val unindex: dbd:Mysql.dbd -> uri:UriManager.uri -> unit
 
+val count_distinct: 
+  [ `Conclusion | `Hypothesis | `Statement] -> 
+  MetadataTypes.metadata list -> 
+    int     
diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 49472ed72..5f83dd608 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -355,7 +355,7 @@ let fill_with_dummy_constants t =
     function
 	Cic.Lambda (n,s,t) -> 
 	  let dummy_uri = 
-	    UriManager.uri_of_string ("dummy_"^(string_of_int i)) in
+	    UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in
 	  (aux (i+1) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
       | t -> t
   in aux 0 t
@@ -368,7 +368,7 @@ let instance ~dbd t =
   let no_full = MetadataDb.count_distinct `Statement metadata in 
   let is_dummy =
       function
-	  `Obj(s, _) -> (String.sub s 0 5) = "dummy" 
+	  `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" 
 	| _ -> false in
   let metadata = List.filter is_dummy metadata in
   let constraints = List.map MetadataTypes.constr_of_metadata metadata in