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