From: Enrico Tassi Date: Mon, 2 May 2005 12:52:30 +0000 (+0000) Subject: removed no_inconcl_aux, no_concl_hyp, no_hyp and added count X-Git-Tag: single_binding~126 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6fa3218efdfca5dd28fee2ef7a8c5e8de67ce829;p=helm.git removed no_inconcl_aux, no_concl_hyp, no_hyp and added count --- diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile index 3535d485d..9d16a2c8d 100644 --- a/helm/ocaml/metadata/Makefile +++ b/helm/ocaml/metadata/Makefile @@ -6,8 +6,8 @@ INTERFACE_FILES = \ metadataTypes.mli \ metadataExtractor.mli \ metadataPp.mli \ - metadataDb.mli \ - metadataConstraints.mli + metadataConstraints.mli \ + metadataDb.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 3e9cd9c5a..cbeaad49d 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -76,34 +76,36 @@ let explode_card_constr = function | Gt card -> ">", card | Lt card -> "<", card -let add_card_constr tbl (n,from,where) = function - | None -> (n,from,where) +let add_card_constr tbl col where = function + | None -> where | 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 %s %d" cur_tbl op card :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where)) + (* count(_utente).hypothesis = 3 *) + (sprintf "%s.%s %s %d" tbl col op card :: where) -let add_diff_constr conclno_tbl hypno_tbl (n,from,where) = function - | None -> (n,from,where) +let add_diff_constr tbl where = function + | None -> 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)) + (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where) + +let add_all_constr tbl (n,from,where) concl full diff = + match (concl, full, diff) with + | None, None, None -> (n,from,where) + | _ -> + let where = add_card_constr tbl "conclusion" where concl in + let where = add_card_constr tbl "statement" where full in + let where = add_diff_constr tbl where diff in + (n,tbl :: from, + (if n > 0 then + sprintf "table0.source = %s.source" tbl :: where + else + where)) + let add_constraint tables (n,from,where) metadata = - let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in + let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables + in let cur_tbl = tbln n in match metadata with | `Obj (uri, positions) -> @@ -138,34 +140,24 @@ let add_constraint tables (n,from,where) metadata = in ((n+2), from, where) + let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables (metadata: MetadataTypes.constr list) = - let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in + let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables + in if (metadata = []) && concl_card = None && full_card = None then failwith "MetadataQuery.at_least: no constraints given"; let (n,from,where) = List.fold_left (add_constraint tables) (0,[],[]) metadata in let (n,from,where) = - add_card_constr conclno_tbl (n,from,where) concl_card - in - let (n,from,where) = - 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 + add_all_constr count_tbl (n,from,where) concl_card full_card diff in let from = String.concat ", " from in let where = String.concat " and " where in let query = match rating with -(* - 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 - *) | None -> sprintf "select table0.source from %s where %s" from where | Some `Hits -> sprintf @@ -173,11 +165,12 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables ^^ " and hits.source = table0.source order by hits.no desc") from where in -(* prerr_endline query; *) + 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 ?rating (metadata: MetadataTypes.constr list) @@ -185,18 +178,17 @@ let at_least let module MT = MetadataTypes in if MT.are_tables_ownerized () then (at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), - MT.conclno_tbl (),MT.fullno_tbl (),MT.hypno_tbl ()) + (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), MT.count_tbl ()) metadata) @ (at_least ~dbd ?concl_card ?full_card ?diff ?rating (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) + MT.library_count_tbl) metadata) else at_least ~dbd ?concl_card ?full_card ?diff ?rating (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) + MT.library_count_tbl) metadata diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index a4e6008a8..e20e00002 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -72,7 +72,33 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) = ignore (Mysql.exec dbd query_obj) end + +let count_distinct position l = + MetadataConstraints.StringSet.cardinal + (List.fold_left (fun acc d -> + match position with + | `Conclusion -> + (match d with + | `Obj (name,`InConclusion) + | `Obj (name,`MainConclusion _ ) -> + MetadataConstraints.StringSet.add name acc + | _ -> acc) + | `Hypothesis -> + (match d with + | `Obj (name,`InHypothesis) + | `Obj (name,`MainHypothesis _) -> + MetadataConstraints.StringSet.add name acc + | _ -> acc) + | `Statement -> + (match d with + | `Obj (name,`InBody) -> acc + | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc + | _ -> acc) + ) MetadataConstraints.StringSet.empty l) +(* let insert_const_no dbd uri = + let term = CicUtil.term_of_uri uri in + let ty = CicTypeChecker.type_of_aux' let inconcl_no = sprintf "INSERT %s SELECT \"%s\", COUNT(DISTINCT h_occurrence) FROM %s WHERE (h_position=\"%s\" OR h_position=\"%s\") AND source LIKE \"%s%%\"" (conclno_tbl ()) uri (obj_tbl ()) inconcl_pos mainconcl_pos uri @@ -86,7 +112,17 @@ let insert_const_no dbd uri = in ignore (Mysql.exec dbd inconcl_no); ignore (Mysql.exec dbd concl_hyp) - +*) +let insert_const_no dbd (uri,metadata) = + let no_concl = count_distinct `Conclusion metadata in + let no_hyp = count_distinct `Hypothesis metadata in + let no_full = count_distinct `Statement metadata in + let insert = + sprintf "INSERT INTO %s VALUES (\"%s\", %d, %d, %d)" + (count_tbl ()) uri no_concl no_hyp no_full + in + ignore (Mysql.exec dbd insert) + let insert_name ~dbd ~uri ~name = let query = sprintf "INSERT %s VALUES (\"%s\", \"%s\")" (name_tbl ()) uri name @@ -129,18 +165,18 @@ let index_inductive_def ~dbd = let index_obj ~dbd ~uri = if not (already_indexed uri) then begin let metadata = MetadataExtractor.compute_obj uri in - let uri_of (a,b,c) = a in - let uris = UriManager.string_of_uri uri :: List.map uri_of metadata in + let uri_of (a,b,c) = (a,c) in let uri = UriManager.string_of_uri uri in let columns = MetadataPp.columns_of_metadata metadata in execute_insert dbd uri (columns :> columns); - List.iter (insert_const_no dbd) uris; + List.iter (insert_const_no dbd) (List.map uri_of metadata); List.iter (fun (uri, name, _) -> insert_name ~dbd ~uri ~name) metadata end let tables_to_clean = - [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl; hypno_tbl] + [sort_tbl; rel_tbl; obj_tbl; (*conclno_tbl; fullno_tbl; hypno_tbl;*) name_tbl; + count_tbl] let clean ~(dbd:Mysql.dbd) = let owned_uris = (* list of uris in list-of-columns format *) diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 948d08678..51f79c828 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -67,47 +67,37 @@ let constr_of_metadata: metadata -> constr = function let sort_tbl_original = "refSort" let rel_tbl_original = "refRel" let obj_tbl_original = "refObj" -let conclno_tbl_original = "no_inconcl_aux" -let fullno_tbl_original = "no_concl_hyp" -let hypno_tbl_original = "no_hyp" let name_tbl_original = "objectName" +let count_tbl_original = "count" (** the names currently used *) let sort_tbl_real = ref sort_tbl_original let rel_tbl_real = ref rel_tbl_original let obj_tbl_real = ref obj_tbl_original -let conclno_tbl_real = ref conclno_tbl_original -let fullno_tbl_real = ref fullno_tbl_original -let hypno_tbl_real = ref hypno_tbl_original let name_tbl_real = ref name_tbl_original +let count_tbl_real = ref count_tbl_original (** the exported symbols *) let sort_tbl () = ! sort_tbl_real ;; let rel_tbl () = ! rel_tbl_real ;; let obj_tbl () = ! obj_tbl_real ;; -let conclno_tbl () = ! conclno_tbl_real ;; -let fullno_tbl () = ! fullno_tbl_real ;; -let hypno_tbl () = ! hypno_tbl_real ;; let name_tbl () = ! name_tbl_real ;; +let count_tbl () = ! count_tbl_real ;; (** to use the owned tables *) let ownerize_tables owner = sort_tbl_real := ( sort_tbl_original ^ "_" ^ owner) ; rel_tbl_real := ( rel_tbl_original ^ "_" ^ owner) ; obj_tbl_real := ( obj_tbl_original ^ "_" ^ owner) ; - conclno_tbl_real := ( conclno_tbl_original ^ "_" ^ owner) ; - fullno_tbl_real := ( fullno_tbl_original ^ "_" ^ owner) ; - hypno_tbl_real := ( hypno_tbl_original ^ "_" ^ owner) ; - name_tbl_real := ( name_tbl_original ^ "_" ^ owner) + name_tbl_real := ( name_tbl_original ^ "_" ^ owner); + count_tbl_real := ( count_tbl_original ^ "_" ^ owner) ;; let library_sort_tbl = sort_tbl_original let library_rel_tbl = rel_tbl_original let library_obj_tbl = obj_tbl_original -let library_conclno_tbl = conclno_tbl_original -let library_fullno_tbl = fullno_tbl_original -let library_hypno_tbl = hypno_tbl_original let library_name_tbl = name_tbl_original +let library_count_tbl = count_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 206967678..d775fc587 100644 --- a/helm/ocaml/metadata/metadataTypes.mli +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -65,16 +65,12 @@ val are_tables_ownerized : unit -> bool val sort_tbl: unit -> string val rel_tbl: unit -> string val obj_tbl: unit -> string -val conclno_tbl: unit -> string -val fullno_tbl: unit -> string -val hypno_tbl: unit -> string val name_tbl: unit -> string +val count_tbl: unit -> string val library_sort_tbl: string val library_rel_tbl: string val library_obj_tbl: string -val library_conclno_tbl: string -val library_fullno_tbl: string -val library_hypno_tbl: string val library_name_tbl: string +val library_count_tbl: string diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml index 43b29e4b6..a7040e659 100644 --- a/helm/ocaml/metadata/test.ml +++ b/helm/ocaml/metadata/test.ml @@ -40,6 +40,6 @@ end else | _ -> prerr_endline ("total persing time " ^ - (string_of_float !CicEnvironment.total_prasing_time)); + (string_of_float !CicEnvironment.total_parsing_time)); close_in ic