helm/ocaml/tactics/match_concl.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*********************************************************************)
  27 (*                                                                   *)
  28 (*                           PROJECT HELM                            *)
  29 (*                                                                   *)
  30 (*                  Andrea Asperti, Matteo Selmi                     *)
  31 (*                           1/04/2004                               *)
  32 (*                                                                   *)
  33 (*                                                                   *)
  34 (*********************************************************************)
  35
  36
  37 (* the file contains:
  38    - functions executing must, just and only constraints on the mysql
  39      data base;
  40    - the general function cmatch for retrieving all statements matching
  41      a given conclusion
  42 *)
  43
  44 type count_condition =
  45     NIL | EQ of int | GT of int
  46 ;;
  47
  48 let main_conclusion =
  49   "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'"
  50 ;;
  51
  52 let in_conclusion =
  53   "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'"
  54 ;;
  55
  56 let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
  57
  58
  59 let get_inconcl (conn:Mysql.dbd) uri =
  60   let uri = escape uri in
  61   let query =
  62     "select h_occurrence from refObj where source='"^uri^
  63     "' and (h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
  64   prerr_endline query;
  65   let result = Mysql.exec conn query in
  66   (* now we transform the result in a set *)
  67   let f a =
  68     match (Array.to_list a) with
  69         [Some uri] -> uri
  70       | _ -> assert false in
  71   let result = Mysql.map ~f:f result in
  72   List.fold_left
  73     (fun set uri ->
  74        NewConstraints.StringSet.add uri set)
  75     NewConstraints.StringSet.empty result
  76 ;;
  77
  78 let test_only (conn:Mysql.dbd) only u =
  79   let inconcl = get_inconcl conn u in
  80     NewConstraints.StringSet.subset inconcl only
  81 ;;
  82
  83 let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition) =
  84   let add_must (n,from,where) (pos,uri) =
  85     match pos with
  86         `MainHypothesis _ -> assert false
  87       | `MainConclusion None ->
  88           let refObjn = "refObj" ^ (string_of_int n) in
  89           let new_must =
  90             [ refObjn^".h_occurrence = '" ^ uri ^ "'";
  91               refObjn^".h_position = " ^ main_conclusion] in
  92           let where' =
  93             if n = 0 then new_must@where
  94             else
  95               (refObjn^".source = refObj" ^ (string_of_int (n-1))
  96                ^ ".source")::new_must@where in
  97           (n+1,("refObj as "^refObjn)::from,where')
  98       | `MainConclusion(Some(d)) ->
  99           let refObjn = "refObj" ^ (string_of_int n) in
 100           let new_must =
 101             [ refObjn^".h_occurrence = '" ^ uri ^ "'";
 102               refObjn^".h_position = " ^ main_conclusion;
 103               refObjn^".h_depth = " ^ (string_of_int d)] in
 104           let where' =
 105             if n = 0 then new_must@where
 106             else
 107               (refObjn^".source = refObj" ^ (string_of_int (n-1))
 108                ^ ".source")::new_must@where in
 109           (n+1,("refObj as "^refObjn)::from,where')
 110       | `InHypothesis -> assert false
 111       | `InConclusion ->
 112           let refObjn = "refObj" ^ (string_of_int n) in
 113           let new_must =
 114             [ refObjn^".h_occurrence = '" ^ uri ^ "'";
 115               refObjn^".h_position = " ^ in_conclusion] in
 116           let where' =
 117             if n = 0 then new_must@where
 118             else
 119               (refObjn^".source = refObj" ^ (string_of_int (n-1))
 120                ^ ".source")::new_must@where in
 121           (n+1,("refObj as "^refObjn)::from,where')
 122       | `InBody -> assert false
 123   in
 124   let (_,from,where) =
 125     List.fold_left add_must (0,[],[]) l in
 126   let from,where =
 127     (match cc with
 128          NIL -> from, where
 129        | EQ n ->
 130            "no_inconcl_aux"::from,
 131            ("no=" ^ (string_of_int n))::
 132              ("no_inconcl_aux.source = refObj0.source")::where
 133        | GT n ->
 134            "no_inconcl_aux"::from,
 135            ("no>" ^ (string_of_int n))::
 136              ("no_inconcl_aux.source = refObj0.source")::where) in
 137   let from = String.concat "," from in
 138   let where = String.concat " and " where in
 139   let query = "select refObj0.source from " ^ from ^ " where " ^ where in
 140     prerr_endline query;
 141     Mysql.exec conn query
 142 ;;
 143
 144
 145 let (must_of_prefix m s):MQGTypes.r_obj list =
 146   let s' = List.map (fun u -> (`InConclusion, u)) s in
 147   (`MainConclusion None,m)::s'
 148 ;;
 149
 150 (* takes a list of lists and returns the list of all elements
 151    without repetitions *)
 152 let union l =
 153   let rec drop_repetitions = function
 154       [] -> []
 155     | [a] -> [a]
 156     | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
 157     | u::l -> u::(drop_repetitions l) in
 158   drop_repetitions (List.sort Pervasives.compare (List.concat l))
 159 ;;
 160
 161 let critical_value = 6;;
 162 let just_factor = 3;;
 163
 164 let cmatch (conn:Mysql.dbd) t =
 165   let eq,constants = NewConstraints.constants_of t in
 166   (* the type of eq is not counted in constants_no *)
 167   let constants_no =
 168     if eq then (NewConstraints.StringSet.cardinal constants)
 169     else (NewConstraints.StringSet.cardinal constants) in
 170   if (constants_no > critical_value) then
 171     let prefixes = NewConstraints.prefixes just_factor t in
 172     (match prefixes with
 173          Some main, all_concl ->
 174 (*
 175            NewConstraints.pp_prefixes all_concl;
 176 *)
 177            (* in some cases, max_prefix_length could be less than n *)
 178            let max_prefix_length =
 179              match all_concl with
 180                  [] -> assert false
 181                | (max,_)::_ -> max in
 182            let maximal_prefixes =
 183              let rec filter res = function
 184                  [] -> res
 185                | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
 186                | _::_-> res in
 187                filter [] all_concl in
 188            let greater_than :(int*string) list=
 189              let all =
 190                union
 191                  (List.map
 192                     (fun (m,s) ->
 193                        (let res =
 194                           exec_must conn (must_of_prefix main s) (GT (m+1)) in
 195                         let f a =
 196                           match (Array.to_list a) with
 197                               (* we tag the uri with m+1, for sorting purposes *)
 198                               [Some uri] -> (m+1,uri)
 199                             | _ -> assert false in
 200                           Mysql.map ~f:f res))
 201                     maximal_prefixes) in
 202                List.filter
 203                  (function (_,uri) -> test_only conn constants uri) all in
 204            let equal_to =
 205              List.concat
 206                (List.map
 207                   (fun (m,s) ->
 208                      (let res =
 209                         exec_must conn (must_of_prefix main s) (EQ (m+1)) in
 210                       let f a =
 211                         match (Array.to_list a) with
 212                             (* we tag the uri with m, for sorting purposes *)
 213                             [Some uri] -> (m,uri)
 214                           | _ -> assert false in
 215                         Mysql.map ~f:f res))
 216                   all_concl) in
 217              greater_than @ equal_to
 218        | _, _ -> [])
 219   else if constants_no = 0 then []
 220   else
 221     (* in this case we compute all prefixes, and we do not need
 222        to apply the only constraints *)
 223     let prefixes = NewConstraints.prefixes constants_no t in
 224     (match prefixes with
 225          Some main, all_concl ->
 226            List.concat
 227            (List.map
 228               (fun (m,s) ->
 229                  (let res =
 230                     exec_must conn (must_of_prefix main s) (EQ (m+1)) in
 231                   let f a =
 232                     match (Array.to_list a) with
 233                         (* we tag the uri with m, for sorting purposes *)
 234                         [Some uri] -> (m,uri)
 235                       | _ -> assert false in
 236                     Mysql.map ~f:f res))
 237               all_concl)
 238        | _, _ -> [])
 239 ;;
 240
 241