helm/software/components/whelp/whelp.ml

   1 (* Copyright (C) 2005, 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://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Printf
  29
  30 let nonvar uri = not (UriManager.uri_is_var uri)
  31
  32   (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
  33   * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
  34 let sqlpat_of_shellglob =
  35   let star_RE, qmark_RE, percent_RE, uscore_RE =
  36     Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
  37   in
  38   fun shellglob ->
  39     Pcre.replace ~rex:star_RE ~templ:"%"
  40       (Pcre.replace ~rex:qmark_RE ~templ:"_"
  41         (Pcre.replace ~rex:percent_RE ~templ:"\\%"
  42           (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
  43             shellglob)))
  44
  45 let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
  46   let escape dbtype dbd s = HSql.escape dbtype dbd s in
  47   let sql_pat = sqlpat_of_shellglob pat in
  48   let query dbtype tbl =
  49         sprintf
  50           ("SELECT source FROM %s WHERE value LIKE \"%s\" "
  51            ^^ HSql.escape_string_for_like dbtype dbd)
  52           tbl (escape dbtype dbd sql_pat)
  53   in
  54   let tbls =
  55     [HSql.User, MetadataTypes.name_tbl ();
  56      HSql.Library, MetadataTypes.library_name_tbl;
  57      HSql.Legacy, MetadataTypes.library_name_tbl]
  58   in
  59   let map cols =
  60     match cols.(0) with
  61     | Some s -> UriManager.uri_of_string s | _ -> assert false
  62   in
  63   let result =
  64     List.fold_left
  65       (fun acc (dbtype,tbl) ->
  66          acc @ HSql.map ~f:map (HSql.exec dbtype dbd (query dbtype tbl)))
  67       [] tbls
  68   in
  69   List.filter nonvar result
  70
  71 let match_term ~(dbd:HSql.dbd) ty =
  72 (*   debug_print (lazy (CicPp.ppterm ty)); *)
  73   let metadata = MetadataExtractor.compute ~body:None ~ty in
  74   let constants_no =
  75     MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
  76   in
  77   let full_card, diff =
  78     if CicUtil.is_meta_closed ty then
  79       Some (MetadataConstraints.Eq constants_no), None
  80     else
  81       let diff_no =
  82         let (hyp_constants, concl_constants) =
  83           (* collect different constants in hypotheses and conclusions *)
  84           List.fold_left
  85             (fun ((hyp, concl) as acc) metadata ->
  86                match (metadata: MetadataTypes.metadata) with
  87                | `Sort _ | `Rel _ -> acc
  88                | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
  89                  when not (List.mem uri concl) -> (hyp, uri :: concl)
  90                | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
  91                  when not (List.mem uri hyp) -> (uri :: hyp, concl)
  92                | `Obj _ -> acc)
  93             ([], [])
  94             metadata
  95         in
  96         List.length hyp_constants - List.length concl_constants
  97       in
  98       let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
  99       let diff =
 100         if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
 101           Some (MetadataConstraints.Eq diff_no)
 102         else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
 103           Some (MetadataConstraints.Gt (diff_no - 1))
 104         else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
 105           Some (MetadataConstraints.Lt (diff_no + 1))
 106         else
 107           None
 108       in
 109       None, diff
 110   in
 111   let constraints = List.map MetadataTypes.constr_of_metadata metadata in
 112     MetadataConstraints.at_least ~dbd ?full_card ?diff constraints
 113
 114 let fill_with_dummy_constants t =
 115   let rec aux i types =
 116     function
 117         Cic.Lambda (n,s,t) ->
 118           let dummy_uri =
 119             UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
 120             (aux (i+1) (s::types)
 121                (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
 122       | t -> t,types
 123   in
 124   let t,types = aux 0 [] t in
 125   t, List.rev types
 126
 127 let instance ~dbd t =
 128   let t',types = fill_with_dummy_constants t in
 129   let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
 130 (*   List.iter
 131     (fun x ->
 132        debug_print
 133          (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))))
 134     metadata; *)
 135   let no_concl = MetadataDb.count_distinct `Conclusion metadata in
 136   let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
 137   let no_full = MetadataDb.count_distinct `Statement metadata in
 138   let is_dummy = function
 139     | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy"
 140           | _ -> true
 141   in
 142   let rec look_for_dummy_main = function
 143           | [] -> None
 144     | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
 145       when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
 146       let s = UriManager.string_of_uri s in
 147       let len = String.length s in
 148             let dummy_index = int_of_string (String.sub s 11 (len-15)) in
 149       let dummy_type = List.nth types dummy_index in
 150       Some (d,dummy_type)
 151     | _::l -> look_for_dummy_main l
 152   in
 153   match (look_for_dummy_main metadata) with
 154     | None->
 155 (*         debug_print (lazy "Caso None"); *)
 156         (* no dummy in main position *)
 157         let metadata = List.filter is_dummy metadata in
 158         let constraints = List.map MetadataTypes.constr_of_metadata metadata in
 159         let concl_card = Some (MetadataConstraints.Eq no_concl) in
 160         let full_card = Some (MetadataConstraints.Eq no_full) in
 161         let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
 162           MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff
 163             constraints
 164     | Some (depth, dummy_type) ->
 165 (*         debug_print
 166           (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *)
 167         (* a dummy in main position *)
 168         let metadata_for_dummy_type =
 169           MetadataExtractor.compute ~body:None ~ty:dummy_type in
 170         (* Let us skip this for the moment
 171            let main_of_dummy_type =
 172            look_for_dummy_main metadata_for_dummy_type in *)
 173         let metadata = List.filter is_dummy metadata in
 174         let constraints = List.map MetadataTypes.constr_of_metadata metadata in
 175         let metadata_for_dummy_type =
 176           List.filter is_dummy metadata_for_dummy_type in
 177         let metadata_for_dummy_type, depth' =
 178           (* depth' = the depth of the A -> A -> Prop *)
 179           List.fold_left (fun (acc,dep) c ->
 180             match c with
 181             | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
 182                 (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
 183             | `Obj  (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
 184                 (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
 185             | `Rel  (`MainConclusion (Some (MetadataTypes.Eq i))) ->
 186                 (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
 187             | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
 188         in
 189         let constraints_for_dummy_type =
 190            List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
 191         (* start with the dummy constant in main conlusion *)
 192         let from = ["refObj as table0"] in (* XXX table hardcoded *)
 193         let where =
 194           [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
 195                  sprintf "table0.h_depth >= %d" depth] in
 196         let (n,from,where) =
 197           List.fold_left
 198             (MetadataConstraints.add_constraint ~start:2)
 199             (2,from,where) constraints in
 200         let concl_card = Some (MetadataConstraints.Eq no_concl) in
 201         let full_card = Some (MetadataConstraints.Eq no_full) in
 202         let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
 203         let (n,from,where) =
 204           MetadataConstraints.add_all_constr
 205             (n,from,where) concl_card full_card diff in
 206               (* join with the constraints over the type of the constant *)
 207         let where =
 208           (sprintf "table0.h_occurrence = table%d.source" n)::where in
 209         let where =
 210           sprintf "table0.h_depth - table%d.h_depth = %d"
 211             n (depth - depth')::where
 212         in
 213         (* XXX performed only in library and legacy not user *)
 214         let (m,from,where) =
 215           List.fold_left
 216             (MetadataConstraints.add_constraint ~start:n)
 217             (n,from,where) constraints_for_dummy_type
 218         in
 219         MetadataConstraints.exec HSql.Library ~dbd (m,from,where)
 220         @
 221         MetadataConstraints.exec HSql.Legacy ~dbd (m,from,where)
 222
 223 let elim ~dbd uri =
 224   let constraints =
 225     [`Rel [`MainConclusion None];
 226      `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
 227      `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
 228      `Obj (uri,[`InHypothesis]);
 229     ]
 230   in
 231   MetadataConstraints.at_least ~rating:`Hits ~dbd constraints
 232