]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tactics/metadataQuery.ml
Serious bug fixed in simplify: sometimes terms wwere not closed because of
[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.empty_ugraph 
55               in
56               let sort,_ = 
57                 CicTypeChecker.type_of_aux' 
58                   metasenv current_ctx ty CicUniv.empty_ugraph 
59               in
60               match sort with
61               | Cic.Sort Cic.Prop -> set, hyp::current_ctx
62               | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
63                      hyp::current_ctx
64             with
65             | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
66       context (Constr.UriManagerSet.empty,[]) 
67   in
68   set
69 ;;
70
71 let intersect uris siguris =
72   let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
73   let set2 =
74     List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
75   in
76   let inter = Constr.UriManagerSet.inter set1 set2 in
77   List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
78
79 (* Profiling code
80 let at_most =
81  let profiler = CicUtil.profile "at_most" in
82  fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
83
84 let sigmatch =
85  let profiler = CicUtil.profile "sigmatch" in
86  fun ~dbd ~facts ~where signature ->
87   profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
88 *)
89 let at_most = Constr.at_most
90 let sigmatch = MetadataConstraints.sigmatch
91
92 let filter_uris_forward ~dbd (main, constants) uris =
93   let main_uris =
94     match main with
95     | None -> []
96     | Some (main, types) -> main :: types
97   in
98   let full_signature =
99     List.fold_right Constr.UriManagerSet.add main_uris constants
100   in
101   List.filter (at_most ~dbd ~where:`Statement full_signature) uris
102
103 let filter_uris_backward ~dbd ~facts signature uris =
104   let siguris =
105     List.map snd 
106       (sigmatch ~dbd ~facts ~where:`Statement signature)
107   in
108     intersect uris siguris 
109
110 let compare_goal_list proof goal1 goal2 =
111   let _,metasenv,_,_ = proof in
112   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
113   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
114   let ty_sort1,_ = 
115     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph 
116   in
117   let ty_sort2,_ = 
118     CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph 
119   in
120   let prop1 =
121     let b,_ = 
122       CicReduction.are_convertible 
123         ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph 
124     in
125       if b then 0
126       else 1
127   in
128   let prop2 =
129     let b,_ = 
130       CicReduction.are_convertible 
131         ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph 
132     in 
133       if b then 0
134       else 1
135   in
136   prop1 - prop2
137
138 (* experimental_hint is a version of hint for experimental 
139     purposes. It uses auto_tac_verbose instead of auto tac.
140     Auto_tac verbose also returns a substitution - for the moment 
141     as a function from cic to cic, to be changed into an association
142     list in the future -. This substitution is used to build a
143     hash table of the inspected goals with their associated proofs.
144     The cose is a cut and paste of the previous one: at the end 
145     of the experimentation we shall make a choice. *)
146
147 let close_with_types s metasenv context =
148   Constr.UriManagerSet.fold 
149     (fun e bag -> 
150       let t = CicUtil.term_of_uri e in
151       let ty, _ = 
152         CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph  
153       in
154       Constr.UriManagerSet.union bag (Constr.constants_of ty)) 
155     s s
156
157 let close_with_constructors s metasenv context =
158   Constr.UriManagerSet.fold 
159     (fun e bag -> 
160       let t = CicUtil.term_of_uri e in
161       match t with
162           Cic.MutInd (uri,_,_)  
163         | Cic.MutConstruct (uri,_,_,_) ->  
164             (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
165                  Cic.InductiveDefinition(tl,_,_,_) ->
166                    snd
167                      (List.fold_left
168                         (fun (i,s) (_,_,_,cl) ->
169                            let _,s =
170                              List.fold_left 
171                                (fun (j,s) _ -> 
172                                   let curi = UriManager.uri_of_uriref uri i (Some j) in
173                                     j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
174                              (i+1,s)) (0,bag) tl)
175                | _ -> assert false)
176         | _ -> bag)
177     s s
178
179 (* Profiling code
180 let apply_tac_verbose =
181  let profiler = CicUtil.profile "apply_tac_verbose" in
182   fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
183
184 let sigmatch =
185  let profiler = CicUtil.profile "sigmatch" in
186  fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
187
188 let cmatch' =
189  let profiler = CicUtil.profile "cmatch'" in
190  fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
191 *)
192 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
193 let cmatch' = Constr.cmatch'
194
195 let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
196  let (_, metasenv, _, _) = proof in
197  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
198  let main, sig_constants = Constr.signature_of ty in
199  let set = signature_of_hypothesis context metasenv in
200  let set =
201   match main with
202      None -> set
203    | Some (main,l) ->
204       List.fold_right Constr.UriManagerSet.add (main::l) set in
205  let set = Constr.UriManagerSet.union set sig_constants in
206  let all_constants_closed = close_with_types set metasenv context in
207  let uris =
208   sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
209  let uris = List.filter nonvar (List.map snd uris) in
210  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
211   uris
212 ;;
213
214 let filter_predicate set ctx menv =
215   let is_predicate t = 
216     let ty, _ = 
217       try CicTypeChecker.type_of_aux' [] []
218         (CicUtil.term_of_uri t) CicUniv.empty_ugraph
219       with CicTypeChecker.TypeCheckerFailure _ -> assert false
220     in
221     let rec check_last_pi = function
222       | Cic.Prod (_,_,tgt) -> check_last_pi tgt
223       | Cic.Sort Cic.Prop -> true
224       | _ -> false
225     in
226     not (check_last_pi ty)
227   in
228   Constr.UriManagerSet.filter is_predicate set  
229 ;;
230
231 let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
232 (*   let to_string set =
233     "{ " ^
234       (String.concat ", "
235          (Constr.UriManagerSet.fold
236             (fun u l -> (UriManager.string_of_uri u)::l) set []))
237     ^ " }"
238   in *)
239  let (_, metasenv, _, _) = proof in
240  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
241  let main, sig_constants = 
242    match signature with 
243    | None -> Constr.signature_of ty 
244    | Some s -> s
245  in
246 (*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
247 (*  match main with *)
248 (*      None -> raise Goal_is_not_an_equation *)
249 (*    | Some (m,l) -> *)
250  let l =
251    let eq_URI =
252     match LibraryObjects.eq_URI () with
253        None -> None
254      | Some s ->
255         Some
256          (UriManager.uri_of_string
257           (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
258    in
259    match eq_URI,main with
260    | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
261    | _ -> []
262  in
263  (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
264    (UriManager.string_of_uri (List.hd l))
265    (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
266  *)
267  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
268  let set = signature_of_hypothesis context metasenv in
269  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
270  let set = Constr.UriManagerSet.union set sig_constants in
271  let set = filter_predicate set context metasenv in
272  let set = close_with_types set metasenv context in
273  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
274  let set = close_with_constructors set metasenv context in
275  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
276  let set = List.fold_right Constr.UriManagerSet.remove l set in
277  let uris =
278    sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
279  let uris = List.filter nonvar (List.map snd uris) in
280  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
281  uris
282    (*        ) *)
283    (*        else raise Goal_is_not_an_equation *)
284
285 let experimental_hint 
286   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
287   let (_, metasenv, _, _) = proof in
288   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
289   let (uris, (main, sig_constants)) =
290     match signature with
291     | Some signature -> 
292         (sigmatch ~dbd ~facts signature, signature)
293     | None -> 
294         (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
295   in 
296   let uris = List.filter nonvar (List.map snd uris) in
297   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
298   let types_constants =
299     match main with
300     | None -> Constr.UriManagerSet.empty
301     | Some (main, types) ->
302         List.fold_right Constr.UriManagerSet.add (main :: types)
303           Constr.UriManagerSet.empty
304   in
305   let all_constants =
306     let hyp_and_sug =
307       Constr.UriManagerSet.union
308         (signature_of_hypothesis context metasenv) 
309         sig_constants
310     in
311     let main = 
312       match main with
313       | None -> Constr.UriManagerSet.empty
314       | Some (main,_) -> 
315           let ty, _ = 
316             CicTypeChecker.type_of_aux' 
317               metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
318           in
319           Constr.constants_of ty
320     in
321     Constr.UriManagerSet.union main hyp_and_sug
322   in
323 (* Constr.UriManagerSet.iter debug_print hyp_constants; *)
324   let all_constants_closed = close_with_types all_constants metasenv context in
325   let other_constants = 
326     Constr.UriManagerSet.diff all_constants_closed types_constants
327   in
328   debug_print (lazy "all_constants_closed");
329   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
330   debug_print (lazy "other_constants");
331   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
332   let uris = 
333     let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
334     if ((List.length uris < pow) or (pow <= 0))
335     then begin
336       debug_print (lazy "MetadataQuery: large sig, falling back to old method");
337       filter_uris_forward ~dbd (main, other_constants) uris
338     end else
339       filter_uris_backward ~dbd ~facts (main, other_constants) uris
340   in 
341   let rec aux = function
342     | [] -> []
343     | uri :: tl ->
344         (let status' =
345             try
346               let (subst,(proof, goal_list)) =
347                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
348                   apply_tac_verbose 
349                     ~term:(CicUtil.term_of_uri uri)
350                   status
351               in
352               let goal_list =
353                 List.stable_sort (compare_goal_list proof) goal_list
354               in
355               Some (uri, (subst,(proof, goal_list)))
356             with ProofEngineTypes.Fail _ -> None
357           in
358           match status' with
359           | None -> aux tl
360           | Some status' -> status' :: aux tl)
361   in
362   List.stable_sort
363     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
364       Pervasives.compare (List.length goals1) (List.length goals2))
365     (aux uris)
366
367 let new_experimental_hint 
368   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
369   ((proof, goal) as status)
370 =
371   let (_, metasenv, _, _) = proof in
372   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
373   let (uris, (main, sig_constants)) =
374     match signature with
375     | Some signature -> 
376         (sigmatch ~dbd ~facts signature, signature)
377     | None -> 
378         (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in 
379   let universe =
380    List.fold_left
381     (fun res u -> Constr.UriManagerSet.add u res)
382     Constr.UriManagerSet.empty universe in
383   let uris =
384    List.fold_left
385     (fun res (_,u) -> Constr.UriManagerSet.add u res)
386     Constr.UriManagerSet.empty uris in
387   let uris = Constr.UriManagerSet.inter uris universe in
388   let uris = Constr.UriManagerSet.elements uris in
389   let rec aux = function
390     | [] -> []
391     | uri :: tl ->
392         (let status' =
393             try
394               let (subst,(proof, goal_list)) =
395                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
396                   apply_tac_verbose 
397                     ~term:(CicUtil.term_of_uri uri)
398                   status
399               in
400               let goal_list =
401                 List.stable_sort (compare_goal_list proof) goal_list
402               in
403               Some (uri, (subst,(proof, goal_list)))
404             with ProofEngineTypes.Fail _ -> None
405           in
406           match status' with
407           | None -> aux tl
408           | Some status' -> status' :: aux tl)
409   in
410   List.stable_sort
411     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
412       Pervasives.compare (List.length goals1) (List.length goals2))
413     (aux uris)
414