From: Enrico Tassi 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