From: Stefano Zacchiroli Date: Mon, 18 Oct 2004 13:49:01 +0000 (+0000) Subject: implemented here at_least constraints matching engine X-Git-Tag: V_0_0_10~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=43f7741d0d6e714f0e1fd183d2fc43af267a445c;p=helm.git implemented here at_least constraints matching engine --- diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend index f25f462cb..caa9708d6 100644 --- a/helm/ocaml/metadata/.depend +++ b/helm/ocaml/metadata/.depend @@ -1,8 +1,13 @@ metadataExtractor.cmi: metadataTypes.cmo metadataPp.cmi: metadataTypes.cmo +metadataQuery.cmi: metadataTypes.cmo metadataExtractor.cmo: metadataTypes.cmo metadataExtractor.cmi metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi metadataPp.cmo: metadataPp.cmi metadataPp.cmx: metadataPp.cmi -metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataDb.cmi -metadataDb.cmx: metadataExtractor.cmx metadataPp.cmx metadataDb.cmi +metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataTypes.cmo \ + metadataDb.cmi +metadataDb.cmx: metadataExtractor.cmx metadataPp.cmx metadataTypes.cmx \ + metadataDb.cmi +metadataQuery.cmo: metadataPp.cmi metadataTypes.cmo metadataQuery.cmi +metadataQuery.cmx: metadataPp.cmx metadataTypes.cmx metadataQuery.cmi diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 5acf3b87a..e685915a3 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -2,14 +2,20 @@ PACKAGE = metadata REQUIRES = dbi helm-cic_proof_checking PREDICATES = -INTERFACE_FILES = metadataExtractor.mli metadataPp.mli metadataDb.mli +INTERFACE_FILES = \ + metadataExtractor.mli \ + metadataPp.mli \ + metadataDb.mli \ + metadataQuery.mli IMPLEMENTATION_FILES = metadataTypes.ml $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = all: -test: test.ml metadata.cma +test: test.ml $(PACKAGE).cma + $(OCAMLFIND) ocamlc -thread -package dbi.mysql,helm-metadata -linkpkg -o $@ $< +test_query: test_query.ml $(PACKAGE).cma $(OCAMLFIND) ocamlc -thread -package dbi.mysql,helm-metadata -linkpkg -o $@ $< include ../Makefile.common diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index 3d618a52c..e7e60faff 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -23,18 +23,12 @@ * http://helm.cs.unibo.it/ *) +open MetadataTypes + open Printf module DB = Dbi_mysql -let sort_tbl = "refSort" -let rel_tbl = "refRel" -let obj_tbl = "refObj" -let owners_tbl = "owners" -let conclno_tbl = "no_inconcl_aux" -let conclno_hyp_tbl = "no_concl_hyp" -let name_tbl = "objectName" - (* let baseuri = "http://www.cs.unibo.it/helm/schemas/schema-helm#" *) let baseuri = "" let inconcl_uri = baseuri ^ "InConclusion" @@ -122,14 +116,14 @@ let clean ~(dbh: Dbi.connection) ~owner = in query#execute []; List.map - (function [source_col] -> source_col | _ -> assert false) + (function [`String source_col] -> source_col | _ -> assert false) (query#fetchall ()) in let del_from tbl = let query = dbh#prepare (sprintf "DELETE FROM %s WHERE source LIKE \"?%%\"" tbl) in - query#execute owned_uris + List.iter (fun source_col -> query#execute [`String source_col]) owned_uris in List.iter del_from [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl; diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli index bd044c713..ba987dca3 100644 --- a/helm/ocaml/metadata/metadataPp.mli +++ b/helm/ocaml/metadata/metadataPp.mli @@ -23,6 +23,11 @@ * http://helm.cs.unibo.it/ *) +(** metadata -> string *) + +val pp_position: MetadataTypes.position -> string +val pp_sort: Cic.sort -> string + (** Pretty printer and OCamlDBI friendly interface *) type t = diff --git a/helm/ocaml/metadata/metadataQuery.ml b/helm/ocaml/metadata/metadataQuery.ml new file mode 100644 index 000000000..a5cd99654 --- /dev/null +++ b/helm/ocaml/metadata/metadataQuery.ml @@ -0,0 +1,118 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +type cardinality_condition = + | Eq of int + | Gt of int + +let tbln n = "table" ^ string_of_int n + +let add_depth_constr depth_opt cur_tbl where = + match depth_opt with + | None -> where + | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where + +let add_card_constr tbl (n,from,where) = function + | None -> (n,from,where) + | Some (Eq card) -> + (n+1, + (sprintf "%s as %s" tbl (tbln n) :: from), + (sprintf "no=%d" card :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" (tbln n)]) @ + where)) + | Some (Gt card) -> + (n+1, + (sprintf "%s as %s" tbl (tbln n) :: from), + (sprintf "no>%d" card :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" (tbln n)]) @ + where)) + +let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card + (metadata: MetadataTypes.metadata list) += + if (metadata = []) && concl_card = None && full_card = None then + failwith "MetadataQuery.at_least: no constraints given"; + let add_constraint (n,from,where) metadata = + let cur_tbl = tbln n in + match metadata with + | `Obj (uri, pos, depth_opt) -> + let tbl = MetadataTypes.obj_tbl in + let pos_str = MetadataPp.pp_position pos in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + let where = add_depth_constr depth_opt cur_tbl where in + ((n+1), from, where) + | `Rel (pos, depth) -> + let tbl = MetadataTypes.rel_tbl in + let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + let where = add_depth_constr (Some depth) cur_tbl where in + ((n+1), from, where) + | `Sort (sort, pos, depth) -> + let tbl = MetadataTypes.sort_tbl in + let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in + let sort_str = MetadataPp.pp_sort sort in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) :: + (if n=0 then [] + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where + in + let where = add_depth_constr (Some depth) cur_tbl where in + ((n+1), from, where) + in + let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in + let (n,from,where) = + add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card + in + let (n,from,where) = + add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card + in + let from = String.concat ", " from in + let where = String.concat " and " where in + let query = sprintf "select table0.source from %s where %s" from where in +prerr_endline query; + let query = dbh#prepare query in + query#execute []; + List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ()) + diff --git a/helm/ocaml/metadata/metadataQuery.mli b/helm/ocaml/metadata/metadataQuery.mli new file mode 100644 index 000000000..38da9e956 --- /dev/null +++ b/helm/ocaml/metadata/metadataQuery.mli @@ -0,0 +1,40 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + + (** constraing on the number of distinct constants *) +type cardinality_condition = + | Eq of int + | Gt of int + + (** @param concl_card cardinality condition on conclusion only + * @param full_card cardinality condition on the whole statement + * @return list of URI satisfying given constraints *) +val at_least: + dbh:Dbi.connection -> + ?concl_card:cardinality_condition -> + ?full_card:cardinality_condition -> + MetadataTypes.metadata list -> + string list + diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index dbe94695e..0db48f299 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -40,3 +40,11 @@ type metadata = | `Obj of string * position * pi_depth option ] +let sort_tbl = "refSort" +let rel_tbl = "refRel" +let obj_tbl = "refObj" +let owners_tbl = "owners" +let conclno_tbl = "no_inconcl_aux" +let conclno_hyp_tbl = "no_concl_hyp" +let name_tbl = "objectName" +