fix for instance

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 23a8b8e6755c34071a78bdd1419a9ea5e6118808..e01b7e7edf2985559668d517fedd7be60781b08b 100644 (file)
--- 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 e2a4669b37dda73785be91b3fe5f1725b3945ffb..48a53815c59c73fb99970ab53640e245193d79de 100644 (file)
--- 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 cbeaad49d5112825ce632f122b4c7cdee1417f42..952aa5a575a5ed98d725497fcb41918de92ee787 100644 (file)
--- 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 20f618f8d2bcd783c481cae5c951aedd36d5231a..672c900eb850ea3cb8e04538aeb65624aa929e86 100644 (file)
--- 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 49472ed7204f084cb160ac9fdb46378eae334b48..5f83dd608b28df8760760ffb8e725e46c7e654a0 100644 (file)
--- 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