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 =
| 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) ->
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
^^ " 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)
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
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
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
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 *)
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
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
| _ ->
prerr_endline
("total persing time " ^
- (string_of_float !CicEnvironment.total_prasing_time));
+ (string_of_float !CicEnvironment.total_parsing_time));
close_in ic
projects / helm.git / commitdiff