]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/autoTactic.ml
added `Coer print_kind
[helm.git] / helm / ocaml / tactics / autoTactic.ml
1 (* Copyright (C) 2002, 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://cs.unibo.it/helm/.
24  *)
25
26 (* Da rimuovere, solo per debug*)
27 let print_context ctx =
28     let print_name =
29      function
30         Cic.Name n -> n
31       | Cic.Anonymous -> "_"
32     in
33      List.fold_right
34       (fun i (output,context) ->
35         let (newoutput,context') =
36          match i with
37             Some (n,Cic.Decl t) ->
38               print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
39           | Some (n,Cic.Def (t,None)) ->
40               print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
41           | None ->
42               "_ ?= _\n", None::context
43           | Some (_,Cic.Def (_,Some _)) -> assert false
44         in
45          output^newoutput,context'
46       ) ctx ("",[])
47   ;;
48
49
50 let search_theorems_in_context status =
51   let (proof, goal) = status in
52   let module C = Cic in
53   let module R = CicReduction in
54   let module S = CicSubstitution in
55   let module PET = ProofEngineTypes in 
56   let module PT = PrimitiveTactics in 
57   let _,metasenv,_,_ = proof in
58   let _,context,ty = CicUtil.lookup_meta goal metasenv in
59   let rec find n = function 
60       [] -> []
61     | hd::tl ->
62         let res =
63           try 
64             Some (PET.apply_tactic
65                     (PT.apply_tac ~term:(C.Rel n)) status ) 
66           with 
67             PET.Fail _ -> None in
68         (match res with
69           Some res -> res::(find (n+1) tl)
70         | None -> find (n+1) tl)
71   in
72   try 
73     find 1 context
74   with Failure s -> 
75     []
76 ;;     
77
78 let depth = 9;;
79 let width = 9;;
80
81 let new_search_theorems f proof goal depth gtl sign =
82   let choices = f (proof,goal)
83   in 
84   List.map 
85     (function (proof, goallist) ->
86        (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
87     choices 
88 ;;
89
90 exception NoOtherChoices;;
91 let rec auto dbd = function
92     [] -> []
93   | (proof, [], sign)::tl -> (proof, [], sign)::tl
94   | (proof, (goal,0)::_, _)::tl -> auto dbd tl
95   | (proof, (((goal,depth)::gtl) as allg), sign)::tl -> 
96       (* first we check if the metavariable has not been already
97          closed as a side effect by some other application *)
98       let facts = (depth = 1) in 
99       let name,metasenv,p,statement = proof in
100       let meta_inf = 
101         (try 
102            let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
103              Some (ey, ty)
104          with _ -> None) in
105       match meta_inf with
106           Some (ey, ty) ->
107             (* the goal is still there *)
108             (* 
109             prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
110             prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
111             prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
112             *)
113             (* if the goal contains metavariables we use the input
114                signature for at_most constraints *)
115             let is_meta_closed = CicUtil.is_meta_closed ty in
116             let sign, new_sign =
117               if is_meta_closed then
118                 None, Some (MetadataConstraints.signature_of ty)
119               else sign,sign in (* maybe the union ? *)
120             let local_choices =
121               new_search_theorems 
122                 search_theorems_in_context 
123                 proof goal (depth-1) [] new_sign in
124             let global_choices =
125               new_search_theorems 
126                 (fun status -> 
127                    List.map snd 
128                    (MetadataQuery.hint 
129                       ~dbd ~facts:facts ?signature:sign status))
130                 proof goal (depth-1) [] new_sign in
131             (* we proceed depth-first on the current goal. This is
132                a MAJOR optimization, since in case of success, and
133                if the goal is meta_closed, we may just drop the alternatives
134                tl1, avoiding useless backtracking. *)
135             let all_choices =
136               local_choices@global_choices in
137               (match (auto dbd all_choices) 
138                with
139                    [] -> auto dbd tl
140                  | (proof,[],_)::tl1 -> 
141                      let all_choices =
142                        let gtl' = List.map fst gtl in
143                          if (gtl = [] || is_meta_closed) then 
144                            (proof,gtl,sign)::tl
145                          else
146                            let tl2 = 
147                              (List.map 
148                                 (function (p,l,s) -> (p,l@gtl,s)) tl1)
149                            in                    
150                              (proof,gtl,sign)::tl2@tl in
151                        auto dbd all_choices
152                  | _ -> assert false)
153         | None -> auto dbd ((proof,gtl,sign)::tl) 
154 ;; 
155
156
157 let auto_tac  ~(dbd:Mysql.dbd) =
158   let auto_tac dbh (proof,goal) =
159   prerr_endline "Entro in Auto";
160   match (auto dbd [(proof, [(goal,depth)],None)]) with
161       [] ->  prerr_endline("Auto failed");
162         raise (ProofEngineTypes.Fail "No Applicable theorem")
163     | (proof,[],_)::_ ->  
164         prerr_endline "AUTO_TAC HA FINITO";
165         (proof,[])
166     | _ -> assert false
167   in
168   ProofEngineTypes.mk_tactic (auto_tac dbd)
169 ;;
170
171
172 (************************** EXPERIMENTAL VERSION ****************************)
173
174 (* In this versions of auto_tac we maintain an hash table of all inspected
175    goals. We assume that the context is invariant for application. 
176    To this aim, it is essential to sall hint_verbose, that in turns calls
177    apply_verbose. *)
178
179
180
181 type exitus = 
182     No of int 
183   | Yes of Cic.term * int 
184   | NotYetInspected
185         
186 let inspected_goals = Hashtbl.create 503;;
187
188 let compare_goal_list proof goal1 goal2 =
189   let _,metasenv,_,_ = proof in
190   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
191   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
192   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 
193                      CicUniv.empty_ugraph in
194   let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 
195                      CicUniv.empty_ugraph in
196   let prop1 =
197     let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 
198                 CicUniv.empty_ugraph in
199       if b then 0 else 1
200   in
201   let prop2 =
202     let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 
203                 CicUniv.empty_ugraph in
204       if b then 0 else 1
205   in
206   prop1 - prop2
207
208 let search_theorems_in_context status =
209   let (proof, goal) = status in
210   let module C = Cic in
211   let module R = CicReduction in
212   let module S = CicSubstitution in
213   let module PET = ProofEngineTypes in 
214   let module PT = PrimitiveTactics in 
215   let _,metasenv,_,_ = proof in
216   let _,context,ty = CicUtil.lookup_meta goal metasenv in
217   let rec find n = function 
218       [] -> []
219     | hd::tl ->
220         let res =
221           try
222             let (subst,(proof, goal_list)) =
223               PT.apply_tac_verbose ~term:(C.Rel n) status  in
224             let goal_list =
225               List.stable_sort (compare_goal_list proof) goal_list in
226             Some (subst,(proof, goal_list))
227           with 
228             PET.Fail _ -> None in
229         (match res with
230           Some res -> res::(find (n+1) tl)
231         | None -> find (n+1) tl)
232   in
233   try 
234     find 1 context
235   with Failure s -> 
236     []
237 ;;     
238
239 let new_search_theorems f proof goal depth sign =
240   let choices = f (proof,goal)
241   in 
242   List.map 
243     (function (subst,(proof, goallist)) ->
244        (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
245     choices 
246 ;;
247
248 exception NoOtherChoices;;
249
250 let rec auto_single dbd proof goal ey ty depth width sign
251   =
252   if depth = 0 then [] else
253   let facts = (depth = 1) in  
254   let _,metasenv,_,_ = proof in
255     (* first of all we check if the goal has been already
256        inspected *)
257   let exitus =
258     try Hashtbl.find inspected_goals ty
259     with Not_found -> NotYetInspected in
260   let is_meta_closed = CicUtil.is_meta_closed ty in
261     begin
262       match exitus with
263           Yes (bo,_) ->
264             (*
265               prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
266               prerr_endline (CicPp.ppterm ty);
267             *)
268             let subst_in =
269               (* if we just apply the subtitution, the type 
270                  is irrelevant: we may use Implicit, since it will 
271                  be dropped *)
272               CicMetaSubst.apply_subst 
273                 [(goal,(ey, bo, Cic.Implicit None))] in
274             let (proof,_) = 
275               ProofEngineHelpers.subst_meta_and_metasenv_in_proof 
276                 proof goal subst_in metasenv in
277               [(subst_in,(proof,[],sign))]
278         | No d when (d >= depth) -> 
279             (*
280               prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
281             *)
282             [] (* the empty list means no choices, i.e. failure *)
283         | No _ 
284         | NotYetInspected -> 
285             (*
286               prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
287               prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
288               prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
289             *)
290             let sign, new_sign =
291               if is_meta_closed then
292                 None, Some (MetadataConstraints.signature_of ty)
293               else sign,sign in (* maybe the union ? *)
294             let local_choices =
295               new_search_theorems 
296                 search_theorems_in_context 
297                 proof goal (depth-1) new_sign in
298             let global_choices =
299               new_search_theorems 
300                 (fun status -> 
301                    List.map snd 
302                    (MetadataQuery.experimental_hint 
303                       ~dbd ~facts:facts ?signature:sign status))
304                 proof goal (depth-1) new_sign in 
305             let all_choices =
306               local_choices@global_choices in
307             let sorted_choices =
308               List.stable_sort
309                 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
310                    Pervasives.compare 
311                    (List.length goals1) (List.length goals2))
312                 all_choices in
313               (match (auto_new dbd width sorted_choices) 
314                with
315                    [] -> 
316                      (* no proof has been found; we update the
317                         hastable *)
318                      (* if is_meta_closed then *)
319                        Hashtbl.add inspected_goals ty (No depth);
320                      []
321                  | (subst,(proof,[],sign))::tl1 -> 
322                      (* a proof for goal has been found:
323                         in order to get the proof we apply subst to
324                         Meta[goal] *)
325                      if is_meta_closed  then
326                        begin 
327                          let irl = 
328                            CicMkImplicit.identity_relocation_list_for_metavariable ey in
329                          let meta_proof = 
330                            subst (Cic.Meta(goal,irl)) in
331                            Hashtbl.add inspected_goals 
332                              ty (Yes (meta_proof,depth));
333 (*
334                            begin
335                              let cty,_ = 
336                                CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
337                              in
338                                if not (cty = ty) then
339                                  begin
340                                    prerr_endline ("ty =  "^CicPp.ppterm ty);
341                                    prerr_endline ("cty =  "^CicPp.ppterm cty);
342                                    assert false
343                                  end
344                                    Hashtbl.add inspected_goals 
345                                    ty (Yes (meta_proof,depth));
346                            end;
347 *)
348                        end;
349                      (subst,(proof,[],sign))::tl1
350                  | _ -> assert false)
351     end
352       
353 and auto_new dbd width = function
354     [] -> []
355   | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
356   | (subst,(proof, (goal,0)::_, _))::tl -> auto_new dbd width tl
357   | (subst,(proof, (goal,depth)::goals, _))::tl when 
358       (List.length goals) > width -> auto_new dbd width tl 
359   | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
360       let _,metasenv,p,_ = proof in
361       let meta_inf =
362         try
363           let (_, ey ,ty) =
364             CicUtil.lookup_meta goal metasenv in
365             Some (ey,ty)
366         with _ -> None in
367         match meta_inf with 
368             Some (ey,ty) ->
369             let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
370             begin
371             match (auto_single dbd proof goal ey ty depth 
372                          (width - (List.length gtl)) sign) 
373                 with
374                     [] -> auto_new dbd width tl
375                   | (local_subst,(proof,[],sign))::tl1 -> 
376                       let new_subst f t = f (subst t) in
377                       let is_meta_closed = CicUtil.is_meta_closed ty in
378                       let all_choices =
379                         if is_meta_closed then 
380                           (new_subst local_subst,(proof,gtl,sign))::tl
381                         else
382                           let tl2 = 
383                             (List.map 
384                                (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
385                           in                     
386                             (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
387                       let sorted_choices = all_choices in
388 (*
389                         List.stable_sort
390                           (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
391                              Pervasives.compare 
392                              (List.length goals1) (List.length goals2))
393                           all_choices in *)
394                         
395                         auto_new dbd width sorted_choices 
396                   | _ -> assert false
397             end
398           | None -> auto_new dbd width ((subst,(proof, gtl, sign))::tl)
399 ;; 
400
401
402 let auto_tac_new  ~(dbd:Mysql.dbd) =
403   let auto_tac dbd (proof,goal) =
404   Hashtbl.clear inspected_goals;
405   prerr_endline "Entro in Auto";
406   let id t = t in
407   match (auto_new dbd width [id,(proof, [(goal,depth)],None)]) with
408       [] ->  prerr_endline("Auto failed");
409         raise (ProofEngineTypes.Fail "No Applicable theorem")
410     | (_,(proof,[],_))::_ ->  
411         prerr_endline "AUTO_TAC HA FINITO";
412         let _,_,p,_ = proof in
413         prerr_endline (CicPp.ppterm p);
414         (proof,[])
415     | _ -> assert false
416   in
417   ProofEngineTypes.mk_tactic (auto_tac dbd)
418 ;;
419
420