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 =
let uri = escape uri in
- (*query to obtain all the constants in the hypothesis of the theorem*)
+ (*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 =
const, the set of the costants of the proof *)
let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
let hyp = hyp_const conn uri in
- prerr_endline (NewConstraints.pp_StringSet hyp);
+ (* prerr_endline (NewConstraints.pp_StringSet hyp);*)
NewConstraints.StringSet.subset hyp const
;;
+
+
+
+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 ^ "'";
+ "(not ("^refObjn^".h_position ="^in_body^"))"] in
+ let where' =
+ if n = 0 then new_must@where
+ else
+ (refObjn^".source = refObj" ^ (string_of_int (n-1))
+ ^ ".source")::new_must@where in
+ (n+1,("refObj as "^refObjn)::from,where')
+ in
+ let (_,from,where) =
+ List.fold_left add_must (0,[],[]) uris in
+ let from,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 distinct(refObj0.source) from " ^ from ^ " where " ^ where in
+ (*prerr_endline query;*)
+ Mysql.exec conn query
+;;
+
+let powerset set =
+ let rec powerset_r set sub =
+ if (NewConstraints.StringSet.is_empty set) then sub
+ else
+ let a = NewConstraints.StringSet.min_elt set in
+ let newset = NewConstraints.StringSet.remove a set in
+ let newsub = NewConstraints.SetSet.union (NewConstraints.SetSet.add (NewConstraints.StringSet.singleton a)
+ (NewConstraints.SetSet.fold
+ (fun s t -> (NewConstraints.SetSet.add (NewConstraints.StringSet.add a s) t))
+ sub NewConstraints.SetSet.empty)) sub in
+ powerset_r newset newsub in
+powerset_r set NewConstraints.SetSet.empty
+;;
+
+let setset_to_listlist setset =
+ let listset = NewConstraints.SetSet.elements setset in
+ let res =
+ List.map
+ (fun set ->
+ let el = NewConstraints.StringSet.elements set in
+ (List.length el, el)) listset in
+ (* ordered by descending cardinality *)
+List.sort (fun (n,_) (m,_) -> m - n) res
+
+let exist_element list_of_uris (_,uri) =
+ let ex u =
+ if u = uri then true
+ else false
+ in
+List.exists ex list_of_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,main) m in
+ let f a =
+ match (Array.to_list a) with
+ [Some uri] -> uri
+ | _ -> assert false in
+ Mysql.map ~f:f res))
+ subsets_of_consts)
+ in
+List.filter (exist_element uris_of_const) uris
+;;
+
+let rec power n m =
+ if (m = 1) then n
+ else n*(power n (m-1))
+;;