let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;;
+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*)
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);
+(* 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
;;