X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fmatch_concl.ml;fp=helm%2Focaml%2Ftactics%2Fmatch_concl.ml;h=4f36f3ee55695705a025ee6927f2a49219834d73;hp=0000000000000000000000000000000000000000;hb=5930f13b2d863abbff240ffa985bcc064c7a5ab8;hpb=4cf419a2e770f4971be7b03b1d73e585d973dc1b diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml new file mode 100644 index 000000000..4f36f3ee5 --- /dev/null +++ b/helm/ocaml/tactics/match_concl.ml @@ -0,0 +1,239 @@ +(* 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) + | _, _ -> []) +;; + +