]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/metadataQuery.ml
new dependences
[helm.git] / helm / software / components / tactics / metadataQuery.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 (* $Id$ *)
27
28 open Printf
29
30 let nonvar uri = not (UriManager.uri_is_var uri)
31
32 module Constr = MetadataConstraints
33
34 exception Goal_is_not_an_equation
35
36 let debug = false
37 let debug_print s = if debug then prerr_endline (Lazy.force s)
38
39 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
40
41 let signature_of_hypothesis context metasenv =
42   let set, _ =
43     List.fold_right
44       (fun hyp (set,current_ctx) ->
45         match hyp with
46         | None -> set, hyp::current_ctx
47         | Some (_, Cic.Decl t) -> 
48             Constr.UriManagerSet.union set (Constr.constants_of t),
49             hyp::current_ctx
50         | Some (_, Cic.Def (t, _)) ->
51             try 
52               let ty,_ = 
53                 CicTypeChecker.type_of_aux' 
54                   metasenv current_ctx t CicUniv.oblivion_ugraph 
55               in
56               let sort,_ = 
57                 CicTypeChecker.type_of_aux' 
58                   metasenv current_ctx ty CicUniv.oblivion_ugraph 
59               in
60               let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
61               match sort with
62               | Cic.Sort Cic.Prop -> set, hyp::current_ctx
63               | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
64                      hyp::current_ctx
65             with
66             | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
67       context (Constr.UriManagerSet.empty,[]) 
68   in
69   set
70 ;;
71
72 let intersect uris siguris =
73   let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
74   let set2 =
75     List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
76   in
77   let inter = Constr.UriManagerSet.inter set1 set2 in
78   List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
79
80 (* Profiling code
81 let at_most =
82  let profiler = CicUtil.profile "at_most" in
83  fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
84
85 let sigmatch =
86  let profiler = CicUtil.profile "sigmatch" in
87  fun ~dbd ~facts ~where signature ->
88   profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
89 *)
90 let at_most = Constr.at_most
91 let sigmatch = MetadataConstraints.sigmatch
92
93 let filter_uris_forward ~dbd (main, constants) uris =
94   let main_uris =
95     match main with
96     | None -> []
97     | Some (main, types) -> main :: types
98   in
99   let full_signature =
100     List.fold_right Constr.UriManagerSet.add main_uris constants
101   in
102   List.filter (at_most ~dbd ~where:`Statement full_signature) uris
103
104 let filter_uris_backward ~dbd ~facts signature uris =
105   let siguris =
106     List.map snd 
107       (sigmatch ~dbd ~facts ~where:`Statement signature)
108   in
109     intersect uris siguris 
110
111 let compare_goal_list proof goal1 goal2 =
112   let _,metasenv, _subst, _,_, _ = proof in
113   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
114   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
115   let ty_sort1,_ = 
116     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph 
117   in
118   let ty_sort2,_ = 
119     CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph 
120   in
121   let prop1 =
122     let b,_ = 
123       CicReduction.are_convertible 
124         ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph 
125     in
126       if b then 0
127       else 1
128   in
129   let prop2 =
130     let b,_ = 
131       CicReduction.are_convertible 
132         ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph 
133     in 
134       if b then 0
135       else 1
136   in
137   prop1 - prop2
138
139 (* experimental_hint is a version of hint for experimental 
140     purposes. It uses auto_tac_verbose instead of auto tac.
141     Auto_tac verbose also returns a substitution - for the moment 
142     as a function from cic to cic, to be changed into an association
143     list in the future -. This substitution is used to build a
144     hash table of the inspected goals with their associated proofs.
145     The cose is a cut and paste of the previous one: at the end 
146     of the experimentation we shall make a choice. *)
147
148 let close_with_types s metasenv context =
149   Constr.UriManagerSet.fold 
150     (fun e bag -> 
151       let t = CicUtil.term_of_uri e in
152       let ty, _ = 
153         CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph  
154       in
155       Constr.UriManagerSet.union bag (Constr.constants_of ty)) 
156     s s
157
158 let close_with_constructors s metasenv context =
159   Constr.UriManagerSet.fold 
160     (fun e bag -> 
161       let t = CicUtil.term_of_uri e in
162       match t with
163           Cic.MutInd (uri,_,_)  
164         | Cic.MutConstruct (uri,_,_,_) ->  
165             (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
166                  Cic.InductiveDefinition(tl,_,_,_) ->
167                    snd
168                      (List.fold_left
169                         (fun (i,s) (_,_,_,cl) ->
170                            let _,s =
171                              List.fold_left 
172                                (fun (j,s) _ -> 
173                                   let curi = UriManager.uri_of_uriref uri i (Some j) in
174 (*                                     prerr_endline ("adding " ^
175  *                                     (UriManager.string_of_uri curi)); *)
176                                     j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
177                              (i+1,s)) (0,bag) tl)
178                | _ -> assert false)
179         | _ -> bag)
180     s s
181
182 (* Profiling code
183 let apply_tac_verbose =
184  let profiler = CicUtil.profile "apply_tac_verbose" in
185   fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
186
187 let sigmatch =
188  let profiler = CicUtil.profile "sigmatch" in
189  fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
190
191 let cmatch' =
192  let profiler = CicUtil.profile "cmatch'" in
193  fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
194 *)
195 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
196 let cmatch' = Constr.cmatch'
197
198 (* used only by te old auto *)
199 let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
200  let (_, metasenv, _subst, _, _, _) = proof in
201  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
202  let main, sig_constants = Constr.signature_of ty in
203  let set = signature_of_hypothesis context metasenv in
204  let set =
205   match main with
206      None -> set
207    | Some (main,l) ->
208       List.fold_right Constr.UriManagerSet.add (main::l) set in
209  let set = Constr.UriManagerSet.union set sig_constants in
210  let all_constants_closed = close_with_types set metasenv context in
211  let uris =
212   sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
213  let uris = List.filter nonvar (List.map snd uris) in
214  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
215   uris
216
217 let is_predicate u = 
218     let ty, _ = 
219       try CicTypeChecker.type_of_aux' [] []
220         (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph
221       with CicTypeChecker.TypeCheckerFailure _ -> assert false
222     in
223     let rec check_last_pi = function
224       | Cic.Prod (_,_,tgt) -> check_last_pi tgt
225       | Cic.Sort Cic.Prop -> true
226       | _ -> false
227     in
228     check_last_pi ty
229 ;;
230
231 let only constants uri =
232   prerr_endline (UriManager.string_of_uri uri);
233   let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
234   let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
235   let consts = Constr.constants_of ty in
236 (*
237   prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
238   Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^
239  UriManager.string_of_uri u)) consts;
240   Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^
241   UriManager.string_of_uri u)) constants;*)
242   Constr.UriManagerSet.subset consts constants 
243 ;;
244
245 let rec types_of_equality = function
246   | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _] 
247     when (LibraryObjects.is_eq_URI uri) -> 
248       let uri_set = Constr.constants_of ty in
249       if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
250         Constr.SetSet.empty
251       else Constr.SetSet.singleton uri_set
252   | Cic.Prod (_, s, t) -> 
253       Constr.SetSet.union (types_of_equality s) (types_of_equality t)
254   | _ -> Constr.SetSet.empty
255 ;;
256
257 let types_for_equality metasenv goal =
258   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
259   let all = types_of_equality ty in
260   let _, all = 
261     List.fold_left
262       (fun (i,acc) _ ->          
263          let ty, _ = 
264            CicTypeChecker.type_of_aux' 
265              metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in
266          let newty = types_of_equality ty in
267            (i+1,Constr.SetSet.union newty acc)) 
268       (1,all) context
269   in all
270 ;;
271            
272 let signature_of metasenv goal = 
273   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
274   let ty_set = Constr.constants_of ty in
275   let hyp_set = signature_of_hypothesis context metasenv in
276   let set = Constr.UriManagerSet.union ty_set hyp_set in
277     close_with_constructors (close_with_types set metasenv context)
278     metasenv context
279
280
281 let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
282   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
283   let ty_set = Constr.constants_of ty in
284   let hyp_set = signature_of_hypothesis context metasenv in
285   let set = Constr.UriManagerSet.union ty_set hyp_set in
286   let all_constants_closed = close_with_types set metasenv context in
287   (* we split predicates from the rest *)
288   let predicates, rest = 
289     Constr.UriManagerSet.partition is_predicate all_constants_closed
290   in
291   let uris =
292     Constr.UriManagerSet.fold
293       (fun u acc -> 
294          debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
295          let set_for_sigmatch = 
296            Constr.UriManagerSet.remove u all_constants_closed in
297          if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
298            (* equality has a special treatment *)
299            (debug_print (lazy "special treatment");
300            let tfe =
301              Constr.SetSet.elements (types_for_equality metasenv goal) 
302            in
303              List.fold_left 
304                (fun acc l ->
305                   let tyl = Constr.UriManagerSet.elements l in
306                   debug_print (lazy ("tyl: "^(String.concat "\n" 
307                         (List.map UriManager.string_of_uri tyl))));
308                   let set_for_sigmatch =
309                     Constr.UriManagerSet.diff set_for_sigmatch l in
310                   let uris =
311                     sigmatch ~dbd ~facts:false ~where:`Statement 
312                       (Some (u,tyl),set_for_sigmatch) in
313                     acc @ uris) 
314                acc tfe)
315          else
316            (debug_print (lazy "normal treatment");
317            let uris =
318              sigmatch ~dbd ~facts:false ~where:`Statement 
319                (Some (u,[]),set_for_sigmatch)
320            in
321              acc @ uris))
322       predicates []
323   in
324 (*
325   let uris =
326     sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) 
327   in
328 *)
329   let uris = List.filter nonvar (List.map snd uris) in
330   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
331   if apply_only then 
332     List.filter (only all_constants_closed) uris 
333   else uris
334 ;;
335
336 let filter_out_predicate set ctx menv =
337   Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set  
338 ;;
339
340 let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
341 (*
342   let to_string set =
343     "{\n" ^
344       (String.concat "\n"
345          (Constr.UriManagerSet.fold
346             (fun u l -> ("  "^UriManager.string_of_uri u)::l) set []))
347     ^ "\n}"
348   in
349 *)
350  let (_, metasenv, _subst, _, _, _) = proof in
351  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
352  let main, sig_constants = 
353    match signature with 
354    | None -> Constr.signature_of ty 
355    | Some s -> s
356  in
357 (*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
358 (*  match main with *)
359 (*      None -> raise Goal_is_not_an_equation *)
360 (*    | Some (m,l) -> *)
361  let l =
362    let eq_URI =
363     match LibraryObjects.eq_URI () with
364        None -> None
365      | Some s ->
366         Some
367          (UriManager.uri_of_string
368           (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
369    in
370    match eq_URI,main with
371    | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
372    | _ -> []
373  in
374  (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
375    (UriManager.string_of_uri (List.hd l))
376    (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
377  *)
378  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
379  let set = signature_of_hypothesis context metasenv in
380  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
381  let set = Constr.UriManagerSet.union set sig_constants in
382  let set = filter_out_predicate set context metasenv in
383  let set = close_with_types set metasenv context in
384  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
385  let set = close_with_constructors set metasenv context in
386  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
387  let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in
388  let uris =
389    sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in
390  let uris = List.filter nonvar (List.map snd uris) in
391  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
392  let set = List.fold_right Constr.UriManagerSet.add l set in
393  let uris = List.filter (only set) uris in
394  uris
395    (*        ) *)
396    (*        else raise Goal_is_not_an_equation *)
397
398 let experimental_hint 
399   ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
400   let (_, metasenv, _subst, _, _, _) = proof in
401   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
402   let (uris, (main, sig_constants)) =
403     match signature with
404     | Some signature -> 
405         (sigmatch ~dbd ~facts signature, signature)
406     | None -> 
407         (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
408   in 
409   let uris = List.filter nonvar (List.map snd uris) in
410   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
411   let types_constants =
412     match main with
413     | None -> Constr.UriManagerSet.empty
414     | Some (main, types) ->
415         List.fold_right Constr.UriManagerSet.add (main :: types)
416           Constr.UriManagerSet.empty
417   in
418   let all_constants =
419     let hyp_and_sug =
420       Constr.UriManagerSet.union
421         (signature_of_hypothesis context metasenv) 
422         sig_constants
423     in
424     let main = 
425       match main with
426       | None -> Constr.UriManagerSet.empty
427       | Some (main,_) -> 
428           let ty, _ = 
429             CicTypeChecker.type_of_aux' 
430               metasenv context (CicUtil.term_of_uri main)
431               CicUniv.oblivion_ugraph
432           in
433           Constr.constants_of ty
434     in
435     Constr.UriManagerSet.union main hyp_and_sug
436   in
437 (* Constr.UriManagerSet.iter debug_print hyp_constants; *)
438   let all_constants_closed = close_with_types all_constants metasenv context in
439   let other_constants = 
440     Constr.UriManagerSet.diff all_constants_closed types_constants
441   in
442   debug_print (lazy "all_constants_closed");
443   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
444   debug_print (lazy "other_constants");
445   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
446   let uris = 
447     let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
448     if ((List.length uris < pow) or (pow <= 0))
449     then begin
450       debug_print (lazy "MetadataQuery: large sig, falling back to old method");
451       filter_uris_forward ~dbd (main, other_constants) uris
452     end else
453       filter_uris_backward ~dbd ~facts (main, other_constants) uris
454   in 
455   let rec aux = function
456     | [] -> []
457     | uri :: tl ->
458         (let status' =
459             try
460               let (subst,(proof, goal_list)) =
461                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
462                   apply_tac_verbose 
463                     ~term:(CicUtil.term_of_uri uri)
464                   status
465               in
466               let goal_list =
467                 List.stable_sort (compare_goal_list proof) goal_list
468               in
469               Some (uri, (subst,(proof, goal_list)))
470             with ProofEngineTypes.Fail _ -> None
471           in
472           match status' with
473           | None -> aux tl
474           | Some status' -> status' :: aux tl)
475   in
476   List.stable_sort
477     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
478       Pervasives.compare (List.length goals1) (List.length goals2))
479     (aux uris)
480
481 let new_experimental_hint 
482   ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
483   ((proof, goal) as status)
484 =
485   let (_, metasenv,  _subst, _, _, _) = proof in
486   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
487   let (uris, (main, sig_constants)) =
488     match signature with
489     | Some signature -> 
490         (sigmatch ~dbd ~facts signature, signature)
491     | None -> 
492         (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in 
493   let universe =
494    List.fold_left
495     (fun res u -> Constr.UriManagerSet.add u res)
496     Constr.UriManagerSet.empty universe in
497   let uris =
498    List.fold_left
499     (fun res (_,u) -> Constr.UriManagerSet.add u res)
500     Constr.UriManagerSet.empty uris in
501   let uris = Constr.UriManagerSet.inter uris universe in
502   let uris = Constr.UriManagerSet.elements uris in
503   let rec aux = function
504     | [] -> []
505     | uri :: tl ->
506         (let status' =
507             try
508               let (subst,(proof, goal_list)) =
509                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
510                   apply_tac_verbose 
511                     ~term:(CicUtil.term_of_uri uri)
512                   status
513               in
514               let goal_list =
515                 List.stable_sort (compare_goal_list proof) goal_list
516               in
517               Some (uri, (subst,(proof, goal_list)))
518             with ProofEngineTypes.Fail _ -> None
519           in
520           match status' with
521           | None -> aux tl
522           | Some status' -> status' :: aux tl)
523   in
524   List.stable_sort
525     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
526       Pervasives.compare (List.length goals1) (List.length goals2))
527     (aux uris)
528