]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/invokeTactics.ml
- bugfix: sequences like ".(" are now lexed, correctly, as
[helm.git] / helm / gTopLevel / invokeTactics.ml
1 (* Copyright (C) 2000-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 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 29/01/2003                                 *)
32 (*                                                                            *)
33 (*                                                                            *)
34 (******************************************************************************)
35
36 open Printf
37
38 exception RefreshSequentException of exn;;
39 exception RefreshProofException of exn;;
40
41 module type Callbacks =
42   sig
43     (* input widgets *)
44     val sequent_viewer : unit -> TermViewer.sequent_viewer
45     val term_editor : unit -> TermEditor.term_editor
46     val scratch_window :
47      unit ->
48       < sequent_viewer: TermViewer.sequent_viewer ;
49         show: unit -> unit ;
50         term: Cic.term ;
51         set_term : Cic.term -> unit ;
52         metasenv: Cic.metasenv ;
53         set_metasenv : Cic.metasenv -> unit ;
54         context: Cic.context ;
55         set_context : Cic.context -> unit >
56     (* GUI refresh functions *)
57     val refresh_proof : unit -> unit
58     val refresh_goals : unit -> unit
59     (* callbacks for user-tactics interaction *)
60     val decompose_uris_choice_callback :
61       (UriManager.uri * int * 'a) list ->
62       (UriManager.uri * int * 'b list) list
63     val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
64     val mqi_handle : MQIConn.handle
65   end
66 ;;
67
68 module type Tactics =
69   sig
70    val intros : unit -> unit
71    val exact : ?term:string -> unit -> unit
72    val apply : ?term:string -> unit -> unit
73    val elimintrossimpl : ?term:string -> unit -> unit
74    val elimtype : ?term:string -> unit -> unit
75    val whd : unit -> unit
76    val reduce : unit -> unit
77    val simpl : unit -> unit
78    val fold_whd : ?term:string -> unit -> unit
79    val fold_reduce : ?term:string -> unit -> unit
80    val fold_simpl : ?term:string -> unit -> unit
81    val cut : ?term:string -> unit -> unit
82    val change : unit -> unit
83    val letin : ?term:string -> unit -> unit
84    val ring : unit -> unit
85    val clearbody : unit -> unit
86    val clear : unit -> unit
87    val fourier : unit -> unit
88    val rewritesimpl : ?term:string -> unit -> unit
89    val rewritebacksimpl : ?term:string -> unit -> unit
90    val replace : unit -> unit
91    val reflexivity : unit -> unit
92    val symmetry : unit -> unit
93    val transitivity : ?term:string -> unit -> unit
94    val exists : unit -> unit
95    val split : unit -> unit
96    val left : unit -> unit
97    val right : unit -> unit
98    val assumption : unit -> unit
99    val generalize : unit -> unit
100    val absurd : ?term:string -> unit -> unit
101    val contradiction : unit -> unit
102    val decompose : ?term:string -> unit -> unit
103    val injection : ?term:string -> unit -> unit
104    val discriminate : ?term:string -> unit -> unit
105    val whd_in_scratch : unit -> unit
106    val reduce_in_scratch : unit -> unit
107    val simpl_in_scratch : unit -> unit
108    val auto : unit -> unit 
109   end
110
111 module Make (C: Callbacks) : Tactics =
112   struct
113
114    let print_uncaught_exception e =
115      HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s"
116       (Printexc.to_string e))))
117
118    let handle_refresh_exception f savedproof savedgoal =
119      try
120        f ()
121      with
122      | RefreshSequentException e ->
123         HelmLogger.log (`Error (`T
124           (sprintf "Exception raised during the refresh of the sequent: %s"
125             (Printexc.to_string e))));
126         ProofEngine.set_proof savedproof ;
127         ProofEngine.goal := savedgoal ;
128         C.refresh_goals ()
129      | RefreshProofException e ->
130         HelmLogger.log (`Error (`T
131           (sprintf "Exception raised during the refresh of the proof: %s"
132             (Printexc.to_string e))));
133         ProofEngine.set_proof savedproof ;
134         ProofEngine.goal := savedgoal ;
135         C.refresh_goals () ;
136         C.refresh_proof ()
137      | e ->
138         print_uncaught_exception e;
139         ProofEngine.set_proof savedproof ;
140         ProofEngine.goal := savedgoal
141
142    let call_tactic tactic () =
143     let savedproof = ProofEngine.get_proof () in
144     let savedgoal  = !ProofEngine.goal in
145     handle_refresh_exception
146       (fun () ->
147         tactic ();
148         C.refresh_goals ();
149         C.refresh_proof ())
150       savedproof savedgoal
151
152    let call_tactic_with_input tactic ?term () =
153     let savedproof = ProofEngine.get_proof () in
154     let savedgoal  = !ProofEngine.goal in
155      let uri,metasenv,bo,ty =
156       match ProofEngine.get_proof () with
157          None -> assert false
158        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
159      in
160       let canonical_context =
161        match !ProofEngine.goal with
162           None -> assert false
163         | Some metano ->
164            let (_,canonical_context,_) =
165             List.find (function (m,_,_) -> m=metano) metasenv
166            in
167             canonical_context
168       in
169        handle_refresh_exception
170         (fun () ->
171           let metasenv',expr =
172            (match term with
173            | None -> ()
174            | Some t -> (C.term_editor ())#set_term t);
175            (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
176           in
177            ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
178            tactic expr ;
179            C.refresh_goals () ;
180            C.refresh_proof () ;
181            (C.term_editor ())#reset)
182         savedproof savedgoal
183
184   let call_tactic_with_goal_input tactic () =
185    let module L = LogicalOperations in
186    let module G = Gdome in
187     let savedproof = ProofEngine.get_proof () in
188     let savedgoal  = !ProofEngine.goal in
189      match (C.sequent_viewer ())#get_selected_terms with
190      | [term] ->
191          handle_refresh_exception
192           (fun () ->
193             tactic term ;
194             C.refresh_goals () ;
195             C.refresh_proof ())
196           savedproof savedgoal
197      | [] -> HelmLogger.log (`Error (`T "No term selected"))
198      | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
199
200   let call_tactic_with_goal_inputs tactic () =
201    let module L = LogicalOperations in
202    let module G = Gdome in
203     let savedproof = ProofEngine.get_proof () in
204     let savedgoal  = !ProofEngine.goal in
205      handle_refresh_exception
206       (fun () ->
207         match (C.sequent_viewer ())#get_selected_terms with
208          | [] -> HelmLogger.log (`Error (`T "No term selected"))
209          | terms ->
210             tactic terms ;
211             C.refresh_goals () ;
212             C.refresh_proof ())
213       savedproof savedgoal
214
215   let call_tactic_with_input_and_goal_input tactic () =
216    let module L = LogicalOperations in
217    let module G = Gdome in
218     let savedproof = ProofEngine.get_proof () in
219     let savedgoal  = !ProofEngine.goal in
220      match (C.sequent_viewer ())#get_selected_terms with
221        [term] ->
222          handle_refresh_exception
223           (fun () ->
224              let uri,metasenv,bo,ty =
225               match ProofEngine.get_proof () with
226                  None -> assert false
227                | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
228              in
229               let canonical_context =
230                match !ProofEngine.goal with
231                   None -> assert false
232                 | Some metano ->
233                    let (_,canonical_context,_) =
234                     List.find (function (m,_,_) -> m=metano) metasenv
235                    in
236                     canonical_context in
237               let (metasenv',expr) =
238                (C.term_editor ())#get_metasenv_and_term
239                 canonical_context metasenv
240               in
241                ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
242                tactic ~goal_input:term ~input:expr ;
243                C.refresh_goals () ;
244                C.refresh_proof () ;
245                (C.term_editor ())#reset)
246           savedproof savedgoal
247      | [] -> HelmLogger.log (`Error (`T "No term selected"))
248      | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
249
250   let call_tactic_with_goal_input_in_scratch tactic () =
251    let module L = LogicalOperations in
252    let module G = Gdome in
253     let scratch_window = C.scratch_window () in
254      match scratch_window#sequent_viewer#get_selected_terms with
255      | [term] ->
256          begin
257           try
258            let expr = tactic term scratch_window#term in
259             scratch_window#sequent_viewer#load_sequent
260              scratch_window#metasenv (111,scratch_window#context,expr) ;
261             scratch_window#set_term expr ;
262             scratch_window#show () ;
263           with
264            e -> print_uncaught_exception e
265          end
266      | [] -> HelmLogger.log (`Error (`T "No term selected"))
267      | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
268
269   let call_tactic_with_goal_inputs_in_scratch tactic () =
270    let module L = LogicalOperations in
271    let module G = Gdome in
272     let scratch_window = C.scratch_window () in
273      match scratch_window#sequent_viewer#get_selected_terms with
274       | [] -> HelmLogger.log (`Error (`T "No term selected"))
275       | terms ->
276          try
277           let expr = tactic terms scratch_window#term in
278            scratch_window#sequent_viewer#load_sequent
279             scratch_window#metasenv (111,scratch_window#context,expr) ;
280            scratch_window#set_term expr ;
281            scratch_window#show () ;
282          with
283           e -> print_uncaught_exception e
284
285   let call_tactic_with_hypothesis_input tactic () =
286    let module L = LogicalOperations in
287    let module G = Gdome in
288     let savedproof = ProofEngine.get_proof () in
289     let savedgoal  = !ProofEngine.goal in
290      match (C.sequent_viewer ())#get_selected_hypotheses with
291      | [hypothesis] ->
292          handle_refresh_exception
293            (fun () ->
294              tactic hypothesis ;
295              C.refresh_goals () ;
296              C.refresh_proof ())
297            savedproof savedgoal
298      | [] -> HelmLogger.log (`Error (`T "No hypothesis selected"))
299      | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
300
301
302
303   let intros =
304    call_tactic
305     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
306   let exact = call_tactic_with_input ProofEngine.exact
307   let apply = call_tactic_with_input ProofEngine.apply
308   let auto = call_tactic (ProofEngine.auto C.mqi_handle)
309   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
310   let elimtype = call_tactic_with_input ProofEngine.elim_type
311   let whd = call_tactic_with_goal_inputs ProofEngine.whd
312   let reduce = call_tactic_with_goal_inputs ProofEngine.reduce
313   let simpl = call_tactic_with_goal_inputs ProofEngine.simpl
314   let fold_whd = call_tactic_with_input ProofEngine.fold_whd
315   let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce
316   let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl
317   let cut =
318    call_tactic_with_input
319     (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback)
320   let change = call_tactic_with_input_and_goal_input ProofEngine.change
321   let letin =
322    call_tactic_with_input
323     (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback)
324   let ring = call_tactic ProofEngine.ring
325   let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody
326   let clear = call_tactic_with_hypothesis_input ProofEngine.clear
327   let fourier = call_tactic ProofEngine.fourier
328   let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl
329   let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl
330   let replace = call_tactic_with_input_and_goal_input ProofEngine.replace
331   let reflexivity = call_tactic ProofEngine.reflexivity
332   let symmetry = call_tactic ProofEngine.symmetry
333   let transitivity = call_tactic_with_input ProofEngine.transitivity
334   let exists = call_tactic ProofEngine.exists
335   let split = call_tactic ProofEngine.split
336   let left = call_tactic ProofEngine.left
337   let right = call_tactic ProofEngine.right
338   let assumption = call_tactic ProofEngine.assumption
339   let injection = call_tactic_with_input ProofEngine.injection
340   let discriminate = call_tactic_with_input ProofEngine.discriminate
341   let generalize =
342    call_tactic_with_goal_inputs
343     (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
344   let absurd = call_tactic_with_input ProofEngine.absurd
345   let contradiction = call_tactic ProofEngine.contradiction
346   let decompose =
347    call_tactic_with_input
348     (ProofEngine.decompose
349       ~uris_choice_callback:C.decompose_uris_choice_callback)
350   let whd_in_scratch =
351    call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
352   let reduce_in_scratch =
353    call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
354   let simpl_in_scratch =
355    call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
356   
357 end
358 ;;