--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*********************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Andrea Asperti, Matteo Selmi *)
+(* 1/04/2004 *)
+(* *)
+(* *)
+(*********************************************************************)
+
+
+(* the file contains:
+ - functions executing must, just and only constraints on the mysql
+ data base;
+ - the general function cmatch for retrieving all statements matching
+ a given conclusion
+*)
+
+type count_condition =
+ NIL | EQ of int | GT of int
+;;
+
+let main_conclusion =
+ "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'"
+;;
+
+let in_conclusion =
+ "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'"
+;;
+
+let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
+
+
+let get_inconcl (conn:Mysql.dbd) uri =
+ let uri = escape uri in
+ let query =
+ "select h_occurrence from refObj where source='"^uri^
+ "' and (h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
+ prerr_endline query;
+ let result = Mysql.exec conn query in
+ (* now we transform the result in a set *)
+ let f a =
+ match (Array.to_list a) with
+ [Some uri] -> uri
+ | _ -> assert false in
+ let result = Mysql.map ~f:f result in
+ List.fold_left
+ (fun set uri ->
+ NewConstraints.StringSet.add uri set)
+ NewConstraints.StringSet.empty result
+;;
+
+let test_only (conn:Mysql.dbd) only u =
+ let inconcl = get_inconcl conn u in
+ NewConstraints.StringSet.subset inconcl only
+;;
+
+let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition) =
+ let add_must (n,from,where) (pos,uri) =
+ match pos with
+ `MainHypothesis _ -> assert false
+ | `MainConclusion None ->
+ let refObjn = "refObj" ^ (string_of_int n) in
+ let new_must =
+ [ refObjn^".h_occurrence = '" ^ uri ^ "'";
+ refObjn^".h_position = " ^ main_conclusion] 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')
+ | `MainConclusion(Some(d)) ->
+ let refObjn = "refObj" ^ (string_of_int n) in
+ let new_must =
+ [ refObjn^".h_occurrence = '" ^ uri ^ "'";
+ refObjn^".h_position = " ^ main_conclusion;
+ refObjn^".h_depth = " ^ (string_of_int d)] 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')
+ | `InHypothesis -> assert false
+ | `InConclusion ->
+ let refObjn = "refObj" ^ (string_of_int n) in
+ let new_must =
+ [ refObjn^".h_occurrence = '" ^ uri ^ "'";
+ refObjn^".h_position = " ^ in_conclusion] 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')
+ | `InBody -> assert false
+ in
+ let (_,from,where) =
+ List.fold_left add_must (0,[],[]) l in
+ let from,where =
+ (match cc with
+ NIL -> from, where
+ | EQ n ->
+ "no_inconcl_aux"::from,
+ ("no=" ^ (string_of_int n))::
+ ("no_inconcl_aux.source = refObj0.source")::where
+ | GT n ->
+ "no_inconcl_aux"::from,
+ ("no>" ^ (string_of_int n))::
+ ("no_inconcl_aux.source = refObj0.source")::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;
+ Mysql.exec conn query
+;;
+
+
+let (must_of_prefix m s):MQGTypes.r_obj list =
+ let s' = List.map (fun u -> (`InConclusion, u)) s in
+ (`MainConclusion None,m)::s'
+;;
+
+(* takes a list of lists and returns the list of all elements
+ without repetitions *)
+let union l =
+ let rec drop_repetitions = function
+ [] -> []
+ | [a] -> [a]
+ | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
+ | u::l -> u::(drop_repetitions l) in
+ drop_repetitions (List.sort Pervasives.compare (List.concat l))
+;;
+
+let critical_value = 6;;
+let just_factor = 3;;
+
+let cmatch (conn:Mysql.dbd) t =
+ let eq,constants = NewConstraints.constants_of t in
+ (* the type of eq is not counted in constants_no *)
+ let constants_no =
+ if eq then (NewConstraints.StringSet.cardinal constants)
+ else (NewConstraints.StringSet.cardinal constants) in
+ if (constants_no > critical_value) then
+ let prefixes = NewConstraints.prefixes just_factor t in
+ (match prefixes with
+ Some main, all_concl ->
+ NewConstraints.pp_prefixes all_concl;
+ (* in some cases, max_prefix_length could be less than n *)
+ let max_prefix_length =
+ match all_concl with
+ [] -> assert false
+ | (max,_)::_ -> max in
+ let maximal_prefixes =
+ let rec filter res = function
+ [] -> res
+ | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
+ | _::_-> res in
+ filter [] all_concl in
+ let greater_than :(int*string) list=
+ let all =
+ union
+ (List.map
+ (fun (m,s) ->
+ (let res =
+ exec_must conn (must_of_prefix main s) (GT (m+1)) in
+ let f a =
+ match (Array.to_list a) with
+ (* we tag the uri with m+1, for sorting purposes *)
+ [Some uri] -> (m+1,uri)
+ | _ -> assert false in
+ Mysql.map ~f:f res))
+ maximal_prefixes) in
+ List.filter
+ (function (_,uri) -> test_only conn constants uri) all in
+ let equal_to =
+ List.concat
+ (List.map
+ (fun (m,s) ->
+ (let res =
+ exec_must conn (must_of_prefix main s) (EQ (m+1)) in
+ let f a =
+ match (Array.to_list a) with
+ (* we tag the uri with m, for sorting purposes *)
+ [Some uri] -> (m,uri)
+ | _ -> assert false in
+ Mysql.map ~f:f res))
+ all_concl) in
+ greater_than @ equal_to
+ | _, _ -> [])
+ else if constants_no = 0 then []
+ else
+ (* in this case we compute all prefixes, and we do not need
+ to apply the only constraints *)
+ let prefixes = NewConstraints.prefixes constants_no t in
+ (match prefixes with
+ Some main, all_concl ->
+ List.concat
+ (List.map
+ (fun (m,s) ->
+ (let res =
+ exec_must conn (must_of_prefix main s) (EQ (m+1)) in
+ let f a =
+ match (Array.to_list a) with
+ (* we tag the uri with m, for sorting purposes *)
+ [Some uri] -> (m,uri)
+ | _ -> assert false in
+ Mysql.map ~f:f res))
+ all_concl)
+ | _, _ -> [])
+;;
+
+
projects / helm.git / blobdiff