X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=32e34a40a1592e8b278aedd0c75093d3d5c9fea1;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=6a30e75d074402edddeac7f78d131bc70a519604;hpb=50e4370320ba30b3ec6e3542bdd1be1f9d3ea018;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 6a30e75d0..32e34a40a 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -36,6 +36,7 @@ type term_signature = (string * string list) option * StringSet.t type cardinality_condition = | Eq of int | Gt of int + | Lt of int let tbln n = "table" ^ string_of_int n @@ -66,98 +67,129 @@ let mk_positions positions cur_tbl = (positions :> MetadataTypes.position list)) ^ ")" +let explode_card_constr = function + | Eq card -> "=", card + | Gt card -> ">", card + | Lt card -> "<", card + let add_card_constr tbl (n,from,where) = function | None -> (n,from,where) - | Some (Eq card) -> + | Some constr -> let cur_tbl = tbln n in + let op, card = explode_card_constr constr in (n+1, (sprintf "%s as %s" tbl cur_tbl :: from), - (sprintf "%s.no=%d" cur_tbl card :: + (sprintf "%s.no %s %d" cur_tbl op card :: (if n=0 then [] else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) - | Some (Gt card) -> - let cur_tbl = tbln n in - (n+1, - (sprintf "%s as %s" tbl cur_tbl :: from), - (sprintf "%s.no>%d" cur_tbl card :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ + +let add_diff_constr conclno_tbl hypno_tbl (n,from,where) = function + | None -> (n,from,where) + | Some constr -> + let cur_tbl1, cur_tbl2 = tbln n, tbln (n+1) in + let op, card = explode_card_constr constr in + (n+2, + (sprintf "%s as %s" conclno_tbl cur_tbl1 :: + sprintf "%s as %s" hypno_tbl cur_tbl2 :: from), + (sprintf "%s.no - %s.no %s %d" cur_tbl2 cur_tbl1 op card :: + (if n=0 then assert false + else [sprintf "table0.source = %s.source" cur_tbl1; + sprintf "table0.source = %s.source" cur_tbl2]) @ where)) -let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card +let add_constraint tables (n,from,where) metadata = + let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in + let cur_tbl = tbln n in + match metadata with + | `Obj (uri, positions) -> + 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" cur_tbl]) @ + where + in + ((n+2), from, where) + | `Rel positions -> + 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" cur_tbl]) @ + where + in + ((n+2), from, where) + | `Sort (sort, positions) -> + let sort_str = CicPp.ppsort sort in + let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in + let where = + (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: + mk_positions positions cur_tbl :: + (if n=0 then + [] + else + [sprintf "table0.source = %s.source" cur_tbl ]) @ where + in + ((n+2), from, where) + +let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables (metadata: MetadataTypes.constr list) = + let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in 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 - 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) :: - 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 - 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 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 - 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 where = - (sprintf "(%s.h_sort = \"%s\" OR %s.h_sort = \"%s\")" - cur_tbl sort_str cur_ltbl 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 - in - ((n+2), from, where) + let (n,from,where) = + List.fold_left (add_constraint tables) (0,[],[]) metadata 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 fullno_tbl (n,from,where) full_card + in + let (n,from,where) = + add_diff_constr conclno_tbl hypno_tbl (n,from,where) diff 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 + let query = +(* + sprintf + ("select table0.source from %s, %s where %s and %s.source = table0.source" + ^^ " order by %s.no") + from fullno_tbl where fullno_tbl fullno_tbl + *) + sprintf "select table0.source from %s where %s" from where + in +(* prerr_endline query; *) let result = Mysql.exec dbd query in Mysql.map result (fun row -> match row.(0) with Some s -> s | _ -> assert false) +let at_least + ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff + (metadata: MetadataTypes.constr list) += + let module MT = MetadataTypes in + if MT.are_tables_ownerized () then + (at_least ~dbd ?concl_card ?full_card ?diff + (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), + MT.conclno_tbl (),MT.fullno_tbl (),MT.hypno_tbl ()) + metadata) + @ + (at_least ~dbd ?concl_card ?full_card ?diff + (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, + MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) + metadata) + else + at_least ~dbd ?concl_card ?full_card ?diff + (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, + MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) + metadata + + (** Prefix handling *) let filter_by_card n = @@ -395,16 +427,20 @@ let get_constants (dbd:Mysql.dbd) ~where uri = let uri = escape uri in let positions = match where with - | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""] + | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ] | `Statement -> - ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\""; - "\"MainHypothesis\""] + [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos; + MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ] in let query = - sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION"^^ + let pos_predicate = + String.concat " OR " + (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions) + in + 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) + (MetadataTypes.obj_tbl ()) uri pos_predicate + MetadataTypes.library_obj_tbl uri pos_predicate in let result = Mysql.exec dbd query in