From: Enrico Tassi Date: Tue, 8 Feb 2005 15:47:49 +0000 (+0000) Subject: at_least now supports the ownerized tables X-Git-Tag: before_svn_merge~22 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=353d488657a8c919140bcc4b6951296cc058e964;p=helm.git at_least now supports the ownerized tables --- diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 6a30e75d0..73e6f288d 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -85,71 +85,53 @@ let add_card_constr tbl (n,from,where) = function else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) -let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card +let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card tables (metadata: MetadataTypes.constr list) = if (metadata = []) && concl_card = None && full_card = None then failwith "MetadataQuery.at_least: no constraints given"; + let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,conclno_hyp_tbl = tables in let add_constraint (n,from,where) metadata = let cur_tbl = tbln n in - let cur_ltbl = tbln (n+1) in match metadata with | `Obj (uri, positions) -> - let tbl = MetadataTypes.obj_tbl () in - let ltbl = MetadataTypes.library_obj_tbl in - let from = - (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from - in - let where = - (sprintf "(%s.h_occurrence = \"%s\" OR %s.h_occurrence = \"%s\")" - cur_tbl uri cur_ltbl uri) :: + let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in + let where = + (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) :: mk_positions positions cur_tbl :: (if n=0 then [] - else [sprintf - "(table0.source = %s.source OR table0.source = %s.source)" - cur_tbl cur_ltbl]) @ where + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where in ((n+2), from, where) | `Rel positions -> - let tbl = MetadataTypes.rel_tbl () in - let ltbl = MetadataTypes.library_rel_tbl in - let from = - (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from - in + let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in let where = mk_positions positions cur_tbl :: (if n=0 then [] - else [sprintf - "(table0.source = %s.source OR table0.source = %s.source)" - cur_tbl cur_ltbl]) @ where + else [sprintf "table0.source = %s.source" cur_tbl]) @ + where in ((n+2), from, where) | `Sort (sort, positions) -> - let tbl = MetadataTypes.sort_tbl () in - let ltbl = MetadataTypes.library_sort_tbl in let sort_str = CicPp.ppsort sort in - let from = - (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from - in + let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in let where = - (sprintf "(%s.h_sort = \"%s\" OR %s.h_sort = \"%s\")" - cur_tbl sort_str cur_ltbl sort_str) :: + (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: mk_positions positions cur_tbl :: (if n=0 then [] else - [sprintf - "(table0.source = %s.source OR table0.source = %s.source)" - cur_tbl cur_ltbl]) @ where + [sprintf "table0.source = %s.source" cur_tbl ]) @ where in ((n+2), 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 + add_card_constr conclno_tbl (n,from,where) concl_card in let (n,from,where) = - add_card_constr (MetadataTypes.conclno_hyp_tbl ()) (n,from,where) full_card + add_card_constr conclno_hyp_tbl (n,from,where) full_card in let from = String.concat ", " from in let where = String.concat " and " where in @@ -158,6 +140,27 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card Mysql.map result (fun row -> match row.(0) with Some s -> s | _ -> assert false) +let at_least + ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list) += + let module MT = MetadataTypes in + if MT.are_tables_ownerized () then + (at_least ~dbd ?concl_card ?full_card + (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), + MT.conclno_tbl (),MT.conclno_hyp_tbl ()) + metadata) + @ + (at_least ~dbd ?concl_card ?full_card + (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, + MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) + metadata) + else + at_least ~dbd ?concl_card ?full_card + (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, + MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) + metadata + + (** Prefix handling *) let filter_by_card n = @@ -401,7 +404,7 @@ let get_constants (dbd:Mysql.dbd) ~where uri = "\"MainHypothesis\""] in let query = - sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION"^^ + sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^ "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)") (MetadataTypes.obj_tbl ()) uri (String.concat " OR " positions) MetadataTypes.library_obj_tbl uri (String.concat " OR " positions) diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 9e0d7c0b8..3f55b886f 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -104,3 +104,6 @@ let library_conclno_tbl = conclno_tbl_original let library_conclno_hyp_tbl = conclno_hyp_tbl_original let library_name_tbl = name_tbl_original +let are_tables_ownerized () = + sort_tbl () <> library_sort_tbl + diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli index c471d167a..b20c8ce14 100644 --- a/helm/ocaml/metadata/metadataTypes.mli +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -60,6 +60,7 @@ val constr_of_metadata: metadata -> constr (** invoke this function to set the current owner. Afterwards the functions * below will return the name of the table of the set owner *) val ownerize_tables : string -> unit +val are_tables_ownerized : unit -> bool val sort_tbl: unit -> string val rel_tbl: unit -> string