1 (* Copyright (C) 2004, 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/
28 let critical_value = 7
31 module StringSet = Set.Make (String)
32 module SetSet = Set.Make (StringSet)
34 type term_signature = (string * string list) option * StringSet.t
36 type cardinality_condition =
40 let tbln n = "table" ^ string_of_int n
43 let add_depth_constr depth_opt cur_tbl where =
46 | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
49 let mk_positions positions cur_tbl =
54 let pos_str = MetadataPp.pp_position_tag pos in
59 | `MainConclusion None
60 | `MainHypothesis None ->
61 sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
62 | `MainConclusion (Some d)
63 | `MainHypothesis (Some d) ->
64 sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
65 cur_tbl pos_str cur_tbl d)
66 (positions :> MetadataTypes.position list)) ^
69 let add_card_constr tbl (n,from,where) = function
70 | None -> (n,from,where)
72 let cur_tbl = tbln n in
74 (sprintf "%s as %s" tbl cur_tbl :: from),
75 (sprintf "%s.no=%d" cur_tbl card ::
77 else [sprintf "table0.source = %s.source" cur_tbl]) @
80 let cur_tbl = tbln n in
82 (sprintf "%s as %s" tbl cur_tbl :: from),
83 (sprintf "%s.no>%d" cur_tbl card ::
85 else [sprintf "table0.source = %s.source" cur_tbl]) @
88 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card tables
89 (metadata: MetadataTypes.constr list)
91 if (metadata = []) && concl_card = None && full_card = None then
92 failwith "MetadataQuery.at_least: no constraints given";
93 let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,conclno_hyp_tbl = tables in
94 let add_constraint (n,from,where) metadata =
95 let cur_tbl = tbln n in
97 | `Obj (uri, positions) ->
98 let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
100 (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
101 mk_positions positions cur_tbl ::
103 else [sprintf "table0.source = %s.source" cur_tbl]) @
108 let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
110 mk_positions positions cur_tbl ::
112 else [sprintf "table0.source = %s.source" cur_tbl]) @
116 | `Sort (sort, positions) ->
117 let sort_str = CicPp.ppsort sort in
118 let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
120 (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
121 mk_positions positions cur_tbl ::
125 [sprintf "table0.source = %s.source" cur_tbl ]) @ where
129 let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
131 add_card_constr conclno_tbl (n,from,where) concl_card
134 add_card_constr conclno_hyp_tbl (n,from,where) full_card
136 let from = String.concat ", " from in
137 let where = String.concat " and " where in
138 let query = sprintf "select table0.source from %s where %s" from where in
139 let result = Mysql.exec dbd query in
141 (fun row -> match row.(0) with Some s -> s | _ -> assert false)
144 ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list)
146 let module MT = MetadataTypes in
147 if MT.are_tables_ownerized () then
148 (at_least ~dbd ?concl_card ?full_card
149 (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (),
150 MT.conclno_tbl (),MT.conclno_hyp_tbl ())
153 (at_least ~dbd ?concl_card ?full_card
154 (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
155 MT.library_conclno_tbl,MT.library_conclno_hyp_tbl)
158 at_least ~dbd ?concl_card ?full_card
159 (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
160 MT.library_conclno_tbl,MT.library_conclno_hyp_tbl)
164 (** Prefix handling *)
166 let filter_by_card n =
167 SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
170 let init = SetSet.union a b in
171 let merge_single_set s1 b =
173 (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
176 SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
180 let rec inspect_children n childs =
182 (fun res term -> merge n (inspect_conclusion n term) res)
185 and add_root n root childs =
186 let childunion = inspect_children n childs in
187 let addroot = StringSet.add root in
189 (fun child newsets -> SetSet.add (addroot child) newsets)
191 (SetSet.singleton (StringSet.singleton root))
193 and inspect_conclusion n t =
194 if n = 0 then SetSet.empty
199 | Cic.Implicit _ -> SetSet.empty
200 | Cic.Var (u,exp_named_subst) -> SetSet.empty
201 | Cic.Const (u,exp_named_subst) ->
202 SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
203 | Cic.MutInd (u, t, exp_named_subst) ->
204 SetSet.singleton (StringSet.singleton
205 (UriManager.string_of_uriref (u, [t])))
206 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
207 SetSet.singleton (StringSet.singleton
208 (UriManager.string_of_uriref (u, [t; c])))
209 | Cic.Cast (t, _) -> inspect_conclusion n t
210 | Cic.Prod (_, s, t) ->
211 merge n (inspect_conclusion n s) (inspect_conclusion n t)
212 | Cic.Lambda (_, s, t) ->
213 merge n (inspect_conclusion n s) (inspect_conclusion n t)
214 | Cic.LetIn (_, s, t) ->
215 merge n (inspect_conclusion n s) (inspect_conclusion n t)
216 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
217 let suri = UriManager.string_of_uri u in
218 add_root (n-1) suri l
219 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
220 let suri = UriManager.string_of_uriref (u, [t]) in
221 add_root (n-1) suri l
222 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
223 let suri = UriManager.string_of_uriref (u, [t; c]) in
224 add_root (n-1) suri l
227 | Cic.MutCase (u, t, tt, uu, m) ->
231 | Cic.CoFix (_, m) ->
234 let rec inspect_term n t =
242 | Cic.Implicit _ -> None, SetSet.empty
243 | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
244 | Cic.Const (u,exp_named_subst) ->
245 Some (UriManager.string_of_uri u), SetSet.empty
246 | Cic.MutInd (u, t, exp_named_subst) ->
247 let uri = UriManager.string_of_uriref (u, [t]) in
248 Some uri, SetSet.empty
249 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
250 let uri = UriManager.string_of_uriref (u, [t; c]) in
251 Some uri, SetSet.empty
252 | Cic.Cast (t, _) -> inspect_term n t
253 | Cic.Prod (_, _, t) -> inspect_term n t
254 | Cic.LetIn (_, _, t) -> inspect_term n t
255 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
256 let suri = UriManager.string_of_uri u in
257 let childunion = inspect_children (n-1) l in
258 Some suri, childunion
259 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
260 let suri = UriManager.string_of_uriref (u, [t]) in
261 if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
262 (* equality is handled in a special way: in particular,
263 the type, if defined, is always added to the prefix,
264 and n is not decremented - it should have been n-2 *)
266 Cic.Const (u1,exp_named_subst1)::l1 ->
267 let suri1 = UriManager.string_of_uri u1 in
268 let inconcl = add_root (n-1) suri1 l1 in
270 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
271 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
272 let inconcl = add_root (n-1) suri1 l1 in
274 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
275 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
276 let inconcl = add_root (n-1) suri1 l1 in
278 | _ :: _ -> Some suri, SetSet.empty
279 | _ -> assert false (* args number must be > 0 *)
281 let childunion = inspect_children (n-1) l in
282 Some suri, childunion
283 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
284 let suri = UriManager.string_of_uriref (u, [t; c]) in
285 let childunion = inspect_children (n-1) l in
286 Some suri, childunion
287 | _ -> None, SetSet.empty
289 let add_cardinality s =
290 let l = SetSet.elements s in
294 let el = StringSet.elements set in
295 (List.length el, el)) l in
296 (* ordered by descending cardinality *)
297 List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
300 match inspect_term n t with
301 Some a, set -> Some a, add_cardinality set
302 | None, set when (SetSet.is_empty set) -> None, []
303 | _, _ -> assert false
306 let rec add children =
308 (fun acc t -> StringSet.union (signature_concl t) acc)
309 (StringSet.empty) children
311 (* this function creates the set of all different constants appearing in
312 the conclusion of the term *)
313 and signature_concl =
318 | Cic.Implicit _ -> StringSet.empty
319 | Cic.Var (u,exp_named_subst) -> StringSet.empty
320 | Cic.Const (u,exp_named_subst) ->
321 StringSet.singleton (UriManager.string_of_uri u)
322 | Cic.MutInd (u, t, exp_named_subst) ->
323 let uri = UriManager.string_of_uriref (u, [t]) in
324 StringSet.singleton uri
325 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
326 let uri = UriManager.string_of_uriref (u, [t;c]) in
327 StringSet.singleton uri
328 | Cic.Cast (t, _) -> signature_concl t
329 | Cic.Prod (_, s, t) ->
330 StringSet.union (signature_concl s) (signature_concl t)
331 | Cic.Lambda (_, s, t) ->
332 StringSet.union (signature_concl s) (signature_concl t)
333 | Cic.LetIn (_, s, t) ->
334 StringSet.union (signature_concl s) (signature_concl t)
335 | Cic.Appl l -> add l
341 let rec signature_of = function
342 | Cic.Cast (t, _) -> signature_of t
343 | Cic.Prod (_, _, t) -> signature_of t
344 | Cic.LetIn (_, _, t) -> signature_of t
345 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
346 let suri = UriManager.string_of_uri u in
347 Some (suri, []), add l
348 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
349 let suri = UriManager.string_of_uriref (u, [t]) in
350 if u = HelmLibraryObjects.Logic.eq_URI then
351 (* equality is handled in a special way: in particular,
352 the type, if defined, is always added to the prefix,
353 and n is not decremented - it should have been n-2 *)
355 Cic.Const (u1,exp_named_subst1)::l1 ->
356 let suri1 = UriManager.string_of_uri u1 in
357 let inconcl = StringSet.remove suri1 (add l1) in
358 Some (suri, [suri1]), inconcl
359 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
360 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
361 let inconcl = StringSet.remove suri1 (add l1) in
362 Some (suri, [suri1]), inconcl
363 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
364 let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
365 let inconcl = StringSet.remove suri1 (add l1) in
366 Some (suri, [suri1]), inconcl
367 | _ :: _ -> Some (suri, []), StringSet.empty
368 | _ -> assert false (* args number must be > 0 *)
370 Some (suri, []), add l
371 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
372 let suri = UriManager.string_of_uriref (u, [t;c]) in
373 Some (suri, []), add l
374 | t -> None, signature_concl t
376 (* takes a list of lists and returns the list of all elements
377 without repetitions *)
379 let rec drop_repetitions = function
382 | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
383 | u::l -> u::(drop_repetitions l) in
384 drop_repetitions (List.sort Pervasives.compare (List.concat l))
386 let must_of_prefix ?(where = `Conclusion) m s =
389 | `Conclusion -> [`InConclusion]
390 | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
392 let s' = List.map (fun u -> `Obj (u, positions)) s in
393 `Obj (m, [`MainConclusion None]) :: s'
395 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
397 let get_constants (dbd:Mysql.dbd) ~where uri =
398 let uri = escape uri in
401 | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""]
403 ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\"";
404 "\"MainHypothesis\""]
407 sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
408 "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
409 (MetadataTypes.obj_tbl ()) uri (String.concat " OR " positions)
410 MetadataTypes.library_obj_tbl uri (String.concat " OR " positions)
413 let result = Mysql.exec dbd query in
414 let set = ref StringSet.empty in
418 | Some uri -> set := StringSet.add uri !set
419 | _ -> assert false);
422 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
423 let inconcl = get_constants dbd ~where u in
424 StringSet.subset inconcl only
426 (* Special handling of equality. The problem is filtering out theorems just
427 * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
428 * ad-hoc, no better solution found at the moment *)
429 let myspeciallist_of_facts =
430 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
432 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
433 (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
434 0,"cic:/Coq/Init/Logic/trans_eq.con";
435 0,"cic:/Coq/Init/Logic/f_equal.con";
436 0,"cic:/Coq/Init/Logic/f_equal2.con";
437 0,"cic:/Coq/Init/Logic/f_equal3.con"]
440 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
444 if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
445 (if facts then myspeciallist_of_facts
449 let must = must_of_prefix ~where main s in
451 | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
452 | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
454 List.map (fun uri -> (m, uri)) res)
457 (* critical value reached, fallback to "only" constraints *)
459 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
460 main prefixes constants
462 let max_prefix_length =
465 | (max,_)::_ -> max in
466 let maximal_prefixes =
467 let rec filter res = function
469 | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
471 filter [] prefixes in
477 let must = must_of_prefix ~where main s in
480 | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
481 | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
483 (* we tag the uri with m+1, for sorting purposes *)
484 List.map (fun uri -> (m+1, uri)) res))
487 List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
488 let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
489 greater_than @ equal_to
491 (* real match query implementation *)
493 let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t =
494 let (main, constants) = signature_of t in
497 | Some (main, types) ->
498 (* the type of eq is not counted in constants_no *)
499 let types_no = List.length types in
500 let constants_no = StringSet.cardinal constants in
501 if (constants_no > critical_value) then
502 let prefixes = prefixes just_factor t in
504 | Some main, all_concl ->
506 List.fold_right StringSet.add types (StringSet.add main constants)
508 compute_with_only ~dbd ~facts main all_concl all_constants
511 (* in this case we compute all prefixes, and we do not need
512 to apply the only constraints *)
514 if constants_no = 0 then
515 (if types_no = 0 then
518 Some main, [0, []; types_no, types])
520 prefixes (constants_no+types_no+1) t
523 Some main, all_concl ->
524 compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
529 let must = must_of_prefix ~where:`Conclusion main s in
530 let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
531 List.map (fun uri -> (m, uri)) res)
535 let power_upto upto consts =
536 let l = StringSet.elements consts in
537 List.sort (fun (n,_) (m,_) -> m - n)
540 List.filter (function (n,l) -> n <= upto)
541 res@(List.map (function (n,l) -> (n+1,a::l)) res))
545 let l = StringSet.elements consts in
546 List.sort (fun (n,_) (m,_) -> m - n)
548 (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
551 type where = [ `Conclusion | `Statement ]
553 let sigmatch ~(dbd:Mysql.dbd)
554 ?(facts=false) ?(where = `Conclusion) (main, constants) =
557 | Some (main, types) ->
558 let constants_no = StringSet.cardinal constants in
559 if (constants_no > critical_value) then
561 let subsets = power_upto just_factor constants in
562 let types_no = List.length types in
563 List.map (function (n,l) -> (n+types_no,types@l)) subsets
566 List.fold_right StringSet.add types (StringSet.add main constants)
568 compute_with_only ~dbd ~where main subsets all_constants
571 let subsets = power constants in
572 let types_no = List.length types in
574 (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
577 compute_exactly ~dbd ~facts ~where main subsets
579 (* match query wrappers *)
583 let cmatch ~dbd ?(facts=false) term =
586 (fun x y -> Pervasives.compare (fst y) (fst x))
587 (cmatch' ~dbd ~facts term))
589 let constants_of = signature_concl