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