1 (* Copyright (C) 2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 let nonvar uri = not (UriManager.uri_is_var uri)
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 "_"
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:"\\_"
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
50 ("SELECT source FROM %s WHERE value LIKE \"%s\" "
51 ^^ HSql.escape_string_for_like
53 "SELECT source FROM %s WHERE value LIKE \"%s\" "
54 ^^ HSql.escape_string_for_like)
55 (MetadataTypes.name_tbl ()) (escape sql_pat)
56 MetadataTypes.library_name_tbl (escape sql_pat)
58 let result = HSql.exec dbd query in
61 (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
63 let match_term ~(dbd:HSql.dbd) ty =
64 (* debug_print (lazy (CicPp.ppterm ty)); *)
65 let metadata = MetadataExtractor.compute ~body:None ~ty in
67 MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
70 if CicUtil.is_meta_closed ty then
71 Some (MetadataConstraints.Eq constants_no), None
74 let (hyp_constants, concl_constants) =
75 (* collect different constants in hypotheses and conclusions *)
77 (fun ((hyp, concl) as acc) metadata ->
78 match (metadata: MetadataTypes.metadata) with
79 | `Sort _ | `Rel _ -> acc
80 | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
81 when not (List.mem uri concl) -> (hyp, uri :: concl)
82 | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
83 when not (List.mem uri hyp) -> (uri :: hyp, concl)
88 List.length hyp_constants - List.length concl_constants
90 let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
92 if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
93 Some (MetadataConstraints.Eq diff_no)
94 else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
95 Some (MetadataConstraints.Gt (diff_no - 1))
96 else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
97 Some (MetadataConstraints.Lt (diff_no + 1))
103 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
104 MetadataConstraints.at_least ~dbd ?full_card ?diff constraints
106 let fill_with_dummy_constants t =
107 let rec aux i types =
109 Cic.Lambda (n,s,t) ->
111 UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
112 (aux (i+1) (s::types)
113 (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
116 let t,types = aux 0 [] t in
119 let instance ~dbd t =
120 let t',types = fill_with_dummy_constants t in
121 let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
125 (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))))
127 let no_concl = MetadataDb.count_distinct `Conclusion metadata in
128 let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
129 let no_full = MetadataDb.count_distinct `Statement metadata in
130 let is_dummy = function
131 | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy"
134 let rec look_for_dummy_main = function
136 | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
137 when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
138 let s = UriManager.string_of_uri s in
139 let len = String.length s in
140 let dummy_index = int_of_string (String.sub s 11 (len-15)) in
141 let dummy_type = List.nth types dummy_index in
143 | _::l -> look_for_dummy_main l
145 match (look_for_dummy_main metadata) with
147 (* debug_print (lazy "Caso None"); *)
148 (* no dummy in main position *)
149 let metadata = List.filter is_dummy metadata in
150 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
151 let concl_card = Some (MetadataConstraints.Eq no_concl) in
152 let full_card = Some (MetadataConstraints.Eq no_full) in
153 let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
154 MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff
156 | Some (depth, dummy_type) ->
158 (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *)
159 (* a dummy in main position *)
160 let metadata_for_dummy_type =
161 MetadataExtractor.compute ~body:None ~ty:dummy_type in
162 (* Let us skip this for the moment
163 let main_of_dummy_type =
164 look_for_dummy_main metadata_for_dummy_type in *)
165 let metadata = List.filter is_dummy metadata in
166 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
167 let metadata_for_dummy_type =
168 List.filter is_dummy metadata_for_dummy_type in
169 let metadata_for_dummy_type, depth' =
170 (* depth' = the depth of the A -> A -> Prop *)
171 List.fold_left (fun (acc,dep) c ->
173 | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
174 (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
175 | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
176 (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
177 | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) ->
178 (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
179 | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
181 let constraints_for_dummy_type =
182 List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
183 (* start with the dummy constant in main conlusion *)
184 let from = ["refObj as table0"] in
186 [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
187 sprintf "table0.h_depth >= %d" depth] in
190 (MetadataConstraints.add_constraint ~start:2)
191 (2,from,where) constraints in
192 let concl_card = Some (MetadataConstraints.Eq no_concl) in
193 let full_card = Some (MetadataConstraints.Eq no_full) in
194 let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
196 MetadataConstraints.add_all_constr
197 (n,from,where) concl_card full_card diff in
198 (* join with the constraints over the type of the constant *)
200 (sprintf "table0.h_occurrence = table%d.source" n)::where in
202 sprintf "table0.h_depth - table%d.h_depth = %d"
203 n (depth - depth')::where
207 (MetadataConstraints.add_constraint ~start:n)
208 (n,from,where) constraints_for_dummy_type in
209 MetadataConstraints.exec ~dbd (m,from,where)
213 [`Rel [`MainConclusion None];
214 `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
215 `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
216 `Obj (uri,[`InHypothesis]);
219 MetadataConstraints.at_least ~rating:`Hits ~dbd constraints