]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/whelp/whelp.ml
* bump standards-version, no changes needed
[helm.git] / 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