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 =
41 let tbln n = "table" ^ string_of_int n
44 let add_depth_constr depth_opt cur_tbl where =
47 | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
50 let mk_positions positions cur_tbl =
55 let pos_str = MetadataPp.pp_position_tag pos in
60 | `MainConclusion None
61 | `MainHypothesis None ->
62 sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
63 | `MainConclusion (Some d)
64 | `MainHypothesis (Some d) ->
65 sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
66 cur_tbl pos_str cur_tbl d)
67 (positions :> MetadataTypes.position list)) ^
70 let explode_card_constr = function
71 | Eq card -> "=", card
72 | Gt card -> ">", card
73 | Lt card -> "<", card
75 let add_card_constr tbl (n,from,where) = function
76 | None -> (n,from,where)
78 let cur_tbl = tbln n in
79 let op, card = explode_card_constr constr in
81 (sprintf "%s as %s" tbl cur_tbl :: from),
82 (sprintf "%s.no %s %d" cur_tbl op card ::
84 else [sprintf "table0.source = %s.source" cur_tbl]) @
87 let add_diff_constr conclno_tbl hypno_tbl (n,from,where) = function
88 | None -> (n,from,where)
90 let cur_tbl1, cur_tbl2 = tbln n, tbln (n+1) in
91 let op, card = explode_card_constr constr in
93 (sprintf "%s as %s" conclno_tbl cur_tbl1 ::
94 sprintf "%s as %s" hypno_tbl cur_tbl2 :: from),
95 (sprintf "%s.no - %s.no %s %d" cur_tbl2 cur_tbl1 op card ::
96 (if n=0 then assert false
97 else [sprintf "table0.source = %s.source" cur_tbl1;
98 sprintf "table0.source = %s.source" cur_tbl2]) @
101 let add_constraint tables (n,from,where) metadata =
102 let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in
103 let cur_tbl = tbln n in
105 | `Obj (uri, positions) ->
106 let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
108 (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
109 mk_positions positions cur_tbl ::
111 else [sprintf "table0.source = %s.source" cur_tbl]) @
116 let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
118 mk_positions positions cur_tbl ::
120 else [sprintf "table0.source = %s.source" cur_tbl]) @
124 | `Sort (sort, positions) ->
125 let sort_str = CicPp.ppsort sort in
126 let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
128 (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
129 mk_positions positions cur_tbl ::
133 [sprintf "table0.source = %s.source" cur_tbl ]) @ where
137 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables
138 (metadata: MetadataTypes.constr list)
140 let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in
141 if (metadata = []) && concl_card = None && full_card = None then
142 failwith "MetadataQuery.at_least: no constraints given";
144 List.fold_left (add_constraint tables) (0,[],[]) metadata
147 add_card_constr conclno_tbl (n,from,where) concl_card
150 add_card_constr fullno_tbl (n,from,where) full_card
153 add_diff_constr conclno_tbl hypno_tbl (n,from,where) diff
155 let from = String.concat ", " from in
156 let where = String.concat " and " where in
160 ("select table0.source from %s, %s where %s and %s.source = table0.source"
161 ^^ " order by %s.no")
162 from fullno_tbl where fullno_tbl fullno_tbl
164 sprintf "select table0.source from %s where %s" from where
166 (* prerr_endline query; *)
167 let result = Mysql.exec dbd query in
169 (fun row -> match row.(0) with Some s -> s | _ -> assert false)
172 ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff
173 (metadata: MetadataTypes.constr list)
175 let module MT = MetadataTypes in
176 if MT.are_tables_ownerized () then
177 (at_least ~dbd ?concl_card ?full_card ?diff
178 (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (),
179 MT.conclno_tbl (),MT.fullno_tbl (),MT.hypno_tbl ())
182 (at_least ~dbd ?concl_card ?full_card ?diff
183 (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
184 MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl)
187 at_least ~dbd ?concl_card ?full_card ?diff
188 (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
189 MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl)
193 (** Prefix handling *)
195 let filter_by_card n =
196 SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
199 let init = SetSet.union a b in
200 let merge_single_set s1 b =
202 (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
205 SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
209 let rec inspect_children n childs =
211 (fun res term -> merge n (inspect_conclusion n term) res)
214 and add_root n root childs =
215 let childunion = inspect_children n childs in
216 let addroot = StringSet.add root in
218 (fun child newsets -> SetSet.add (addroot child) newsets)
220 (SetSet.singleton (StringSet.singleton root))
222 and inspect_conclusion n t =
223 if n = 0 then SetSet.empty
228 | Cic.Implicit _ -> SetSet.empty
229 | Cic.Var (u,exp_named_subst) -> SetSet.empty
230 | Cic.Const (u,exp_named_subst) ->
231 SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
232 | Cic.MutInd (u, t, exp_named_subst) ->
233 SetSet.singleton (StringSet.singleton
234 (UriManager.string_of_uriref (u, [t])))
235 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
236 SetSet.singleton (StringSet.singleton
237 (UriManager.string_of_uriref (u, [t; c])))
238 | Cic.Cast (t, _) -> inspect_conclusion n t
239 | Cic.Prod (_, s, t) ->
240 merge n (inspect_conclusion n s) (inspect_conclusion n t)
241 | Cic.Lambda (_, s, t) ->
242 merge n (inspect_conclusion n s) (inspect_conclusion n t)
243 | Cic.LetIn (_, s, t) ->
244 merge n (inspect_conclusion n s) (inspect_conclusion n t)
245 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
246 let suri = UriManager.string_of_uri u in
247 add_root (n-1) suri l
248 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
249 let suri = UriManager.string_of_uriref (u, [t]) in
250 add_root (n-1) suri l
251 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
252 let suri = UriManager.string_of_uriref (u, [t; c]) in
253 add_root (n-1) suri l
256 | Cic.MutCase (u, t, tt, uu, m) ->
260 | Cic.CoFix (_, m) ->
263 let rec inspect_term n t =
271 | Cic.Implicit _ -> None, SetSet.empty
272 | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
273 | Cic.Const (u,exp_named_subst) ->
274 Some (UriManager.string_of_uri u), SetSet.empty
275 | Cic.MutInd (u, t, exp_named_subst) ->
276 let uri = UriManager.string_of_uriref (u, [t]) in
277 Some uri, SetSet.empty
278 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
279 let uri = UriManager.string_of_uriref (u, [t; c]) in
280 Some uri, SetSet.empty
281 | Cic.Cast (t, _) -> inspect_term n t
282 | Cic.Prod (_, _, t) -> inspect_term n t
283 | Cic.LetIn (_, _, t) -> inspect_term n t
284 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
285 let suri = UriManager.string_of_uri u in
286 let childunion = inspect_children (n-1) l in
287 Some suri, childunion
288 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
289 let suri = UriManager.string_of_uriref (u, [t]) in
290 if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
291 (* equality is handled in a special way: in particular,
292 the type, if defined, is always added to the prefix,
293 and n is not decremented - it should have been n-2 *)
295 Cic.Const (u1,exp_named_subst1)::l1 ->
296 let suri1 = UriManager.string_of_uri u1 in
297 let inconcl = add_root (n-1) suri1 l1 in
299 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
300 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
301 let inconcl = add_root (n-1) suri1 l1 in
303 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
304 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
305 let inconcl = add_root (n-1) suri1 l1 in
307 | _ :: _ -> Some suri, SetSet.empty
308 | _ -> assert false (* args number must be > 0 *)
310 let childunion = inspect_children (n-1) l in
311 Some suri, childunion
312 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
313 let suri = UriManager.string_of_uriref (u, [t; c]) in
314 let childunion = inspect_children (n-1) l in
315 Some suri, childunion
316 | _ -> None, SetSet.empty
318 let add_cardinality s =
319 let l = SetSet.elements s in
323 let el = StringSet.elements set in
324 (List.length el, el)) l in
325 (* ordered by descending cardinality *)
326 List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
329 match inspect_term n t with
330 Some a, set -> Some a, add_cardinality set
331 | None, set when (SetSet.is_empty set) -> None, []
332 | _, _ -> assert false
335 let rec add children =
337 (fun acc t -> StringSet.union (signature_concl t) acc)
338 (StringSet.empty) children
340 (* this function creates the set of all different constants appearing in
341 the conclusion of the term *)
342 and signature_concl =
347 | Cic.Implicit _ -> StringSet.empty
348 | Cic.Var (u,exp_named_subst) -> StringSet.empty
349 | Cic.Const (u,exp_named_subst) ->
350 StringSet.singleton (UriManager.string_of_uri u)
351 | Cic.MutInd (u, t, exp_named_subst) ->
352 let uri = UriManager.string_of_uriref (u, [t]) in
353 StringSet.singleton uri
354 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
355 let uri = UriManager.string_of_uriref (u, [t;c]) in
356 StringSet.singleton uri
357 | Cic.Cast (t, _) -> signature_concl t
358 | Cic.Prod (_, s, t) ->
359 StringSet.union (signature_concl s) (signature_concl t)
360 | Cic.Lambda (_, s, t) ->
361 StringSet.union (signature_concl s) (signature_concl t)
362 | Cic.LetIn (_, s, t) ->
363 StringSet.union (signature_concl s) (signature_concl t)
364 | Cic.Appl l -> add l
370 let rec signature_of = function
371 | Cic.Cast (t, _) -> signature_of t
372 | Cic.Prod (_, _, t) -> signature_of t
373 | Cic.LetIn (_, _, t) -> signature_of t
374 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
375 let suri = UriManager.string_of_uri u in
376 Some (suri, []), add l
377 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
378 let suri = UriManager.string_of_uriref (u, [t]) in
379 if u = HelmLibraryObjects.Logic.eq_URI then
380 (* equality is handled in a special way: in particular,
381 the type, if defined, is always added to the prefix,
382 and n is not decremented - it should have been n-2 *)
384 Cic.Const (u1,exp_named_subst1)::l1 ->
385 let suri1 = UriManager.string_of_uri u1 in
386 let inconcl = StringSet.remove suri1 (add l1) in
387 Some (suri, [suri1]), inconcl
388 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
389 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
390 let inconcl = StringSet.remove suri1 (add l1) in
391 Some (suri, [suri1]), inconcl
392 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
393 let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
394 let inconcl = StringSet.remove suri1 (add l1) in
395 Some (suri, [suri1]), inconcl
396 | _ :: _ -> Some (suri, []), StringSet.empty
397 | _ -> assert false (* args number must be > 0 *)
399 Some (suri, []), add l
400 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
401 let suri = UriManager.string_of_uriref (u, [t;c]) in
402 Some (suri, []), add l
403 | t -> None, signature_concl t
405 (* takes a list of lists and returns the list of all elements
406 without repetitions *)
408 let rec drop_repetitions = function
411 | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
412 | u::l -> u::(drop_repetitions l) in
413 drop_repetitions (List.sort Pervasives.compare (List.concat l))
415 let must_of_prefix ?(where = `Conclusion) m s =
418 | `Conclusion -> [`InConclusion]
419 | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
421 let s' = List.map (fun u -> `Obj (u, positions)) s in
422 `Obj (m, [`MainConclusion None]) :: s'
424 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
426 let get_constants (dbd:Mysql.dbd) ~where uri =
427 let uri = escape uri in
430 | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
432 [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
433 MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
438 (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
440 sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
441 "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
442 (MetadataTypes.obj_tbl ()) uri pos_predicate
443 MetadataTypes.library_obj_tbl uri pos_predicate
446 let result = Mysql.exec dbd query in
447 let set = ref StringSet.empty in
451 | Some uri -> set := StringSet.add uri !set
452 | _ -> assert false);
455 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
456 let inconcl = get_constants dbd ~where u in
457 StringSet.subset inconcl only
459 (* Special handling of equality. The problem is filtering out theorems just
460 * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
461 * ad-hoc, no better solution found at the moment *)
462 let myspeciallist_of_facts =
463 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
465 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
466 (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
467 0,"cic:/Coq/Init/Logic/trans_eq.con";
468 0,"cic:/Coq/Init/Logic/f_equal.con";
469 0,"cic:/Coq/Init/Logic/f_equal2.con";
470 0,"cic:/Coq/Init/Logic/f_equal3.con"]
473 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
477 if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
478 (if facts then myspeciallist_of_facts
482 let must = must_of_prefix ~where main s in
484 | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
485 | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
487 List.map (fun uri -> (m, uri)) res)
490 (* critical value reached, fallback to "only" constraints *)
492 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
493 main prefixes constants
495 let max_prefix_length =
498 | (max,_)::_ -> max in
499 let maximal_prefixes =
500 let rec filter res = function
502 | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
504 filter [] prefixes in
510 let must = must_of_prefix ~where main s in
513 | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
514 | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
516 (* we tag the uri with m+1, for sorting purposes *)
517 List.map (fun uri -> (m+1, uri)) res))
520 List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
521 let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
522 greater_than @ equal_to
524 (* real match query implementation *)
526 let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t =
527 let (main, constants) = signature_of t in
530 | Some (main, types) ->
531 (* the type of eq is not counted in constants_no *)
532 let types_no = List.length types in
533 let constants_no = StringSet.cardinal constants in
534 if (constants_no > critical_value) then
535 let prefixes = prefixes just_factor t in
537 | Some main, all_concl ->
539 List.fold_right StringSet.add types (StringSet.add main constants)
541 compute_with_only ~dbd ~facts main all_concl all_constants
544 (* in this case we compute all prefixes, and we do not need
545 to apply the only constraints *)
547 if constants_no = 0 then
548 (if types_no = 0 then
551 Some main, [0, []; types_no, types])
553 prefixes (constants_no+types_no+1) t
556 Some main, all_concl ->
557 compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
562 let must = must_of_prefix ~where:`Conclusion main s in
563 let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
564 List.map (fun uri -> (m, uri)) res)
568 let power_upto upto consts =
569 let l = StringSet.elements consts in
570 List.sort (fun (n,_) (m,_) -> m - n)
573 List.filter (function (n,l) -> n <= upto)
574 res@(List.map (function (n,l) -> (n+1,a::l)) res))
578 let l = StringSet.elements consts in
579 List.sort (fun (n,_) (m,_) -> m - n)
581 (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
584 type where = [ `Conclusion | `Statement ]
586 let sigmatch ~(dbd:Mysql.dbd)
587 ?(facts=false) ?(where = `Conclusion) (main, constants) =
590 | Some (main, types) ->
591 let constants_no = StringSet.cardinal constants in
592 if (constants_no > critical_value) then
594 let subsets = power_upto just_factor constants in
595 let types_no = List.length types in
596 List.map (function (n,l) -> (n+types_no,types@l)) subsets
599 List.fold_right StringSet.add types (StringSet.add main constants)
601 compute_with_only ~dbd ~where main subsets all_constants
604 let subsets = power constants in
605 let types_no = List.length types in
607 (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
610 compute_exactly ~dbd ~facts ~where main subsets
612 (* match query wrappers *)
616 let cmatch ~dbd ?(facts=false) term =
619 (fun x y -> Pervasives.compare (fst y) (fst x))
620 (cmatch' ~dbd ~facts term))
622 let constants_of = signature_concl