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