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