]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/metadata/metadataConstraints.ml
added mathml_ns
[helm.git] / helm / ocaml / metadata / metadataConstraints.ml
1 (* Copyright (C) 2004, 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 open Printf
27
28 let critical_value = 7
29 let just_factor = 4
30
31 module StringSet = Set.Make (String)
32 module SetSet = Set.Make (StringSet)
33
34 type term_signature = (string * string list) option * StringSet.t
35
36 type cardinality_condition =
37   | Eq of int
38   | Gt of int
39
40 let tbln n = "table" ^ string_of_int n
41
42 (*
43 let add_depth_constr depth_opt cur_tbl where =
44   match depth_opt with
45   | None -> where
46   | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
47 *)
48
49 let mk_positions positions cur_tbl =
50   "(" ^
51   String.concat " or "
52     (List.map
53       (fun pos ->
54         let pos_str = MetadataPp.pp_position_tag pos in
55         match pos with
56         | `InBody
57         | `InConclusion
58         | `InHypothesis
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)) ^
67   ")"
68
69 let add_card_constr tbl (n,from,where) = function
70   | None -> (n,from,where)
71   | Some (Eq card) ->
72       let cur_tbl = tbln n in
73       (n+1,
74        (sprintf "%s as %s" tbl cur_tbl :: from),
75        (sprintf "%s.no=%d" cur_tbl card ::
76         (if n=0 then []
77         else [sprintf "table0.source = %s.source" cur_tbl]) @
78         where))
79   | Some (Gt card) ->
80       let cur_tbl = tbln n in
81       (n+1,
82        (sprintf "%s as %s" tbl cur_tbl :: from),
83        (sprintf "%s.no>%d" cur_tbl card ::
84         (if n=0 then []
85         else [sprintf "table0.source = %s.source" cur_tbl]) @
86         where))
87
88 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
89   (metadata: MetadataTypes.constr list)
90 =
91   if (metadata = []) && concl_card = None && full_card = None then
92     failwith "MetadataQuery.at_least: no constraints given";
93   let add_constraint (n,from,where) metadata =
94     let cur_tbl = tbln n in
95     match metadata with
96     | `Obj (uri, positions) ->
97         let tbl = MetadataTypes.obj_tbl in
98         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
99         let where =
100           (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
101           mk_positions positions cur_tbl ::
102           (if n=0 then []
103           else [sprintf "table0.source = %s.source" cur_tbl]) @
104           where
105         in
106         ((n+1), from, where)
107     | `Rel positions ->
108         let tbl = MetadataTypes.rel_tbl in
109         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
110         let where =
111           mk_positions positions cur_tbl ::
112           (if n=0 then []
113           else [sprintf "table0.source = %s.source" cur_tbl]) @
114           where
115         in
116         ((n+1), from, where)
117     | `Sort (sort, positions) ->
118         let tbl = MetadataTypes.sort_tbl in
119         let sort_str = CicPp.ppsort sort in
120         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
121         let where =
122           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
123           mk_positions positions cur_tbl ::
124           (if n=0 then []
125           else [sprintf "table0.source = %s.source" cur_tbl]) @
126           where
127         in
128         ((n+1), from, where)
129   in
130   let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
131   let (n,from,where) =
132     add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card
133   in
134   let (n,from,where) =
135     add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card
136   in
137   let from = String.concat ", " from in
138   let where = String.concat " and " where in
139   let query = sprintf "select table0.source from %s where %s" from where in
140   let result = Mysql.exec dbd query in
141   Mysql.map result
142     (fun row -> match row.(0) with Some s -> s | _ -> assert false)
143
144   (** Prefix handling *)
145
146 let filter_by_card n =
147   SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
148   
149 let merge n a b = 
150   let init = SetSet.union a b in
151   let merge_single_set s1 b = 
152     SetSet.fold 
153       (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
154       b SetSet.empty in
155   let res = 
156     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
157   in
158   filter_by_card n res 
159
160 let rec inspect_children n childs =
161   List.fold_left 
162     (fun res term -> merge n (inspect_conclusion n term) res)
163     SetSet.empty childs 
164
165 and add_root n root childs =
166   let childunion = inspect_children n childs in
167   let addroot = StringSet.add root in
168     SetSet.fold 
169       (fun child newsets -> SetSet.add (addroot child) newsets)
170       childunion 
171       (SetSet.singleton (StringSet.singleton root))
172
173 and inspect_conclusion n t = 
174   if n = 0 then SetSet.empty
175   else match t with
176       Cic.Rel _                    
177     | Cic.Meta _                     
178     | Cic.Sort _ 
179     | Cic.Implicit _ -> SetSet.empty 
180     | Cic.Var (u,exp_named_subst) -> SetSet.empty
181     | Cic.Const (u,exp_named_subst) -> 
182         SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
183     | Cic.MutInd (u, t, exp_named_subst) -> 
184         SetSet.singleton (StringSet.singleton
185           (UriManager.string_of_uriref (u, [t])))
186     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
187         SetSet.singleton (StringSet.singleton
188           (UriManager.string_of_uriref (u, [t; c])))
189     | Cic.Cast (t, _) -> inspect_conclusion n t
190     | Cic.Prod (_, s, t) -> 
191         merge n (inspect_conclusion n s) (inspect_conclusion n t)
192     | Cic.Lambda (_, s, t) ->
193         merge n (inspect_conclusion n s) (inspect_conclusion n t)
194     | Cic.LetIn (_, s, t) ->
195         merge n (inspect_conclusion n s) (inspect_conclusion n t)
196     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
197         let suri = UriManager.string_of_uri u in
198         add_root (n-1) suri l
199     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
200         let suri = UriManager.string_of_uriref (u, [t]) in
201         add_root (n-1) suri l
202     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
203         let suri = UriManager.string_of_uriref (u, [t; c]) in
204         add_root (n-1) suri l
205     | Cic.Appl l -> 
206         SetSet.empty
207     | Cic.MutCase (u, t, tt, uu, m) ->
208         SetSet.empty
209     | Cic.Fix (_, m) -> 
210         SetSet.empty
211     | Cic.CoFix (_, m) -> 
212         SetSet.empty
213
214 let rec inspect_term n t = 
215   if n = 0 then
216     assert false
217   else
218     match t with
219       Cic.Rel _                    
220     | Cic.Meta _                     
221     | Cic.Sort _ 
222     | Cic.Implicit _ -> None, SetSet.empty 
223     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
224     | Cic.Const (u,exp_named_subst) -> 
225         Some (UriManager.string_of_uri u), SetSet.empty
226     | Cic.MutInd (u, t, exp_named_subst) -> 
227         let uri = UriManager.string_of_uriref (u, [t]) in
228         Some uri, SetSet.empty
229     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
230         let uri = UriManager.string_of_uriref (u, [t; c]) in
231         Some uri, SetSet.empty
232     | Cic.Cast (t, _) -> inspect_term n t
233     | Cic.Prod (_, _, t) -> inspect_term n t
234     | Cic.LetIn (_, _, t) -> inspect_term n t
235     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
236         let suri = UriManager.string_of_uri u in
237         let childunion = inspect_children (n-1) l in
238         Some suri, childunion
239     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
240         let suri = UriManager.string_of_uriref (u, [t]) in
241         if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
242           (* equality is handled in a special way: in particular, 
243              the type, if defined, is always added to the prefix, 
244              and n is not decremented - it should have been n-2 *)
245           match l with
246               Cic.Const (u1,exp_named_subst1)::l1 ->
247                 let suri1 = UriManager.string_of_uri u1 in
248                 let inconcl = add_root (n-1) suri1 l1 in
249                 Some suri, inconcl
250             | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
251                 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
252                 let inconcl = add_root (n-1) suri1 l1 in  
253                 Some suri, inconcl
254             | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
255                 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
256                 let inconcl = add_root (n-1) suri1 l1 in  
257                 Some suri, inconcl
258             | _ :: _ -> Some suri, SetSet.empty
259             | _ -> assert false (* args number must be > 0 *)
260         else
261           let childunion = inspect_children (n-1) l in
262           Some suri, childunion
263     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
264         let suri = UriManager.string_of_uriref (u, [t; c]) in
265         let childunion = inspect_children (n-1) l in
266         Some suri, childunion
267     | _ -> None, SetSet.empty
268
269 let add_cardinality s =
270   let l = SetSet.elements s in
271   let res = 
272     List.map 
273       (fun set -> 
274          let el = StringSet.elements set in
275          (List.length el, el)) l in
276     (* ordered by descending cardinality *)
277     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
278
279 let prefixes n t =
280   match inspect_term n t with
281       Some a, set -> Some a, add_cardinality set
282     | None, set when (SetSet.is_empty set) -> None, []
283     | _, _ -> assert false
284
285
286 let rec add children =
287   List.fold_left
288     (fun acc t -> StringSet.union (signature_concl t) acc)
289     (StringSet.empty) children
290   
291 (* this function creates the set of all different constants appearing in 
292    the conclusion of the term *)
293 and signature_concl = 
294   function
295       Cic.Rel _                    
296     | Cic.Meta _                     
297     | Cic.Sort _ 
298     | Cic.Implicit _ -> StringSet.empty 
299     | Cic.Var (u,exp_named_subst) -> StringSet.empty
300     | Cic.Const (u,exp_named_subst) -> 
301         StringSet.singleton (UriManager.string_of_uri u)
302     | Cic.MutInd (u, t, exp_named_subst) -> 
303         let uri = UriManager.string_of_uriref (u, [t]) in
304         StringSet.singleton uri
305     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
306         let uri = UriManager.string_of_uriref (u, [t;c]) in
307         StringSet.singleton uri
308     | Cic.Cast (t, _) -> signature_concl t
309     | Cic.Prod (_, s, t) -> 
310         StringSet.union (signature_concl s) (signature_concl t)
311     | Cic.Lambda (_, s, t) ->
312         StringSet.union (signature_concl s) (signature_concl t)
313     | Cic.LetIn (_, s, t) ->
314         StringSet.union (signature_concl s) (signature_concl t)
315     | Cic.Appl l  -> add l
316     | Cic.MutCase _
317     | Cic.Fix _
318     | Cic.CoFix _ ->
319         StringSet.empty
320
321 let rec signature_of = function
322   | Cic.Cast (t, _)      -> signature_of t
323   | Cic.Prod (_, _, t)   -> signature_of t               
324   | Cic.LetIn (_, _, t) -> signature_of t
325   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
326       let suri = UriManager.string_of_uri u in
327       Some (suri, []), add l
328   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
329       let suri = UriManager.string_of_uriref (u, [t]) in
330       if u = HelmLibraryObjects.Logic.eq_URI then
331           (* equality is handled in a special way: in particular, 
332              the type, if defined, is always added to the prefix, 
333              and n is not decremented - it should have been n-2 *)
334       match l with
335           Cic.Const (u1,exp_named_subst1)::l1 ->
336             let suri1 = UriManager.string_of_uri u1 in
337             let inconcl = StringSet.remove suri1 (add l1) in
338             Some (suri, [suri1]), inconcl
339         | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
340             let suri1 = UriManager.string_of_uriref (u1, [t1]) in
341             let inconcl =  StringSet.remove suri1 (add l1) in
342               Some (suri, [suri1]), inconcl
343         | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
344             let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
345             let inconcl =  StringSet.remove suri1 (add l1) in
346             Some (suri, [suri1]), inconcl
347         | _ :: _ -> Some (suri, []), StringSet.empty
348         | _ -> assert false (* args number must be > 0 *)
349       else
350         Some (suri, []), add l
351   | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
352       let suri = UriManager.string_of_uriref (u, [t;c]) in
353       Some (suri, []), add l
354   | t -> None, signature_concl t
355
356 (* takes a list of lists and returns the list of all elements
357    without repetitions *)
358 let union l = 
359   let rec drop_repetitions = function
360       [] -> []
361     | [a] -> [a]
362     | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
363     | u::l -> u::(drop_repetitions l) in
364   drop_repetitions (List.sort Pervasives.compare (List.concat l))
365
366 let must_of_prefix ?(where = `Conclusion) m s =
367   let positions =
368     match where with
369     | `Conclusion -> [`InConclusion]
370     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
371   in
372   let s' = List.map (fun u -> `Obj (u, positions)) s in
373   `Obj (m, [`MainConclusion None]) :: s'
374
375 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
376
377 let get_constants (dbd:Mysql.dbd) ~where uri =
378   let uri = escape uri in
379   let positions =
380     match where with
381     | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""]
382     | `Statement ->
383         ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\"";
384          "\"MainHypothesis\""]
385   in
386   let query = 
387     sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)"
388       uri (String.concat " or " positions)
389   in
390   let result = Mysql.exec dbd query in
391   let set = ref StringSet.empty in
392   Mysql.iter result
393     (fun col ->
394       match col.(0) with
395       | Some uri -> set := StringSet.add uri !set
396       | _ -> assert false);
397   !set
398
399 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
400   let inconcl = get_constants dbd ~where u in
401   StringSet.subset inconcl only
402
403   (* Special handling of equality. The problem is filtering out theorems just
404   * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
405   * ad-hoc, no better solution found at the moment *)
406 let myspeciallist_of_facts  =
407   [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
408 let myspeciallist =
409   [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
410 (*   0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
411    0,"cic:/Coq/Init/Logic/trans_eq.con";
412    0,"cic:/Coq/Init/Logic/f_equal.con";
413    0,"cic:/Coq/Init/Logic/f_equal2.con";
414    0,"cic:/Coq/Init/Logic/f_equal3.con"]
415
416
417 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
418   List.concat
419     (List.map 
420       (fun (m,s) -> 
421         if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
422           (if facts then myspeciallist_of_facts
423            else myspeciallist)
424         else
425           let res =
426             let must = must_of_prefix ~where main s in
427             match where with
428             | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
429             | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
430           in
431           List.map (fun uri -> (m, uri)) res)
432       prefixes)
433
434   (* critical value reached, fallback to "only" constraints *)
435
436 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 
437   main prefixes constants
438 =
439   let max_prefix_length = 
440     match prefixes with
441     | [] -> assert false 
442     | (max,_)::_ -> max in
443   let maximal_prefixes = 
444     let rec filter res = function 
445         [] -> res
446       | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
447       | _::_-> res in
448     filter [] prefixes in
449   let greater_than =
450     let all =
451       union
452         (List.map 
453           (fun (m,s) -> 
454             let must = must_of_prefix ~where main s in
455             (let res = 
456               match where with
457               | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
458               | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
459             in
460             (* we tag the uri with m+1, for sorting purposes *)
461             List.map (fun uri -> (m+1, uri)) res))
462           maximal_prefixes)
463     in
464     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
465     let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
466     greater_than @ equal_to
467
468   (* real match query implementation *)
469
470 let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
471   let (main, constants) = signature_of t in
472   match main with
473   | None -> []
474   | Some (main, types) ->
475       (* the type of eq is not counted in constants_no *)
476       let types_no = List.length types in
477       let constants_no = StringSet.cardinal constants in
478       if (constants_no > critical_value) then 
479         let prefixes = prefixes just_factor t in
480         (match prefixes with
481         | Some main, all_concl ->
482             let all_constants = 
483               List.fold_right StringSet.add types (StringSet.add main constants)
484             in
485             compute_with_only ~dbd ~facts main all_concl all_constants
486          | _, _ -> [])
487       else
488         (* in this case we compute all prefixes, and we do not need
489            to apply the only constraints *)
490         let prefixes =
491           if constants_no = 0 then
492             (if types_no = 0 then
493                Some main, [0, []]
494              else
495                Some main, [0, []; types_no, types])
496           else
497             prefixes (constants_no+types_no+1) t
498         in
499         (match prefixes with
500            Some main, all_concl ->
501              compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
502 (*
503              List.concat
504                (List.map 
505                   (fun (m,s) -> 
506                     let must = must_of_prefix ~where:`Conclusion main s in
507                     let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
508                     List.map (fun uri -> (m, uri)) res)
509                   all_concl) *)
510          | _, _ -> [])
511
512 let power_upto upto consts =
513   let l = StringSet.elements consts in
514   List.sort (fun (n,_) (m,_) -> m - n)
515   (List.fold_left 
516     (fun res a ->
517        List.filter (function (n,l) -> n <= upto)
518        res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
519      [(0,[])] l)
520
521 let power consts =
522   let l = StringSet.elements consts in
523   List.sort (fun (n,_) (m,_) -> m - n)
524   (List.fold_left 
525     (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
526      [(0,[])] l)
527
528 type where = [ `Conclusion | `Statement ]
529
530 let sigmatch ~(dbd:Mysql.dbd) 
531   ?(facts=false) ?(where = `Conclusion) (main, constants) =
532   match main with
533     None -> []
534   | Some (main, types) ->
535       let constants_no = StringSet.cardinal constants in
536       if (constants_no > critical_value) then 
537         let subsets = 
538           let subsets = power_upto just_factor constants in
539           let types_no = List.length types in
540           List.map (function (n,l) -> (n+types_no,types@l)) subsets
541         in
542         let all_constants = 
543           List.fold_right StringSet.add types (StringSet.add main constants)
544         in
545         compute_with_only ~dbd ~where main subsets all_constants
546       else
547         let subsets = 
548           let subsets = power constants in
549           let types_no = List.length types in
550           if types_no > 0 then  
551           (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
552           else subsets
553         in
554         compute_exactly ~dbd ~facts ~where main subsets
555
556   (* match query wrappers *)
557
558 let cmatch'= cmatch 
559
560 let cmatch ~dbd ?(facts=false) term =
561   List.map snd
562     (List.sort
563       (fun x y -> Pervasives.compare (fst y) (fst x))
564       (cmatch' ~dbd ~facts term))
565
566 let constants_of = signature_concl
567