let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;;
+let in_body = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InBody'";;
+
let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
let hyp_const (conn:Mysql.dbd) uri =
(*query to obtain all the constants in the hypothesis and conclusion of the theorem*)
let query =
"select h_occurrence from refObj where source='"^uri^
- "' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^
- "or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
-(* prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
+ "' and (not (h_position ="^in_body^"))" in
+ (*prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
let result = Mysql.exec conn query in
(* now we transform the result in a set *)
let f a =
-let rec exec_query (conn:Mysql.dbd) uris k =
+let rec exec_query (conn:Mysql.dbd) (uris,main) k =
let add_must (n,from,where) uri =
let refObjn = "refObj" ^ (string_of_int n) in
let new_must =
[ refObjn^".h_occurrence = '" ^ uri ^ "'";
- "("^refObjn^".h_position = " ^ main_conclusion^ " or "
- ^refObjn^".h_position = " ^ in_conclusion^ " or "
- ^refObjn^".h_position = " ^ main_hypothesis^ " or "
- ^refObjn^".h_position = " ^ in_hypothesis^ ")"] in
+ "(not ("^refObjn^".h_position ="^in_body^"))"] in
let where' =
if n = 0 then new_must@where
else
let (_,from,where) =
List.fold_left add_must (0,[],[]) uris in
let from,where =
- "no_concl_hyp"::from,
- ("no=" ^ (string_of_int k))::
- ("no_concl_hyp.source = refObj0.source")::where
+ ["no_concl_hyp";"refObj as main"]@from,
+ ["no=" ^ (string_of_int k);
+ "no_concl_hyp.source = refObj0.source";
+ "main.source = refObj0.source";
+ "main.h_occurrence = '" ^ main ^ "'";
+ "main.h_position = " ^ main_conclusion]@where
in
let from = String.concat "," from in
let where = String.concat " and " where in
- let query = "select refObj0.source from " ^ from ^ " where " ^ where in
- (* prerr_endline query;*)
+ let query = "select distinct(refObj0.source) from " ^ from ^ " where " ^ where in
+ (*prerr_endline query;*)
Mysql.exec conn query
;;
;;
-let filter_uris (conn:Mysql.dbd) const uris =
+let filter_uris (conn:Mysql.dbd) const uris main =
let subsets_of_consts =
setset_to_listlist (powerset const) in
+ let ex u =
+ if u = main then true
+ else false
+ in
+ let subsets_of_consts =
+ List.filter
+ (fun (_,b) -> (List.exists ex b))
+ subsets_of_consts in
let uris_of_const =
List.concat
(List.map
(fun (m,s) ->
(let res =
- exec_query conn s m in
+ exec_query conn (s,main) m in
let f a =
match (Array.to_list a) with
[Some uri] -> uri