1 (* Copyright (C) 2000-2002, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
36 exception RefreshSequentException of exn;;
37 exception RefreshProofException of exn;;
39 module type Callbacks =
42 val sequent_viewer : unit -> TermViewer.sequent_viewer
43 val term_editor : unit -> TermEditor.term_editor
46 < sequent_viewer: TermViewer.sequent_viewer ;
49 set_term : Cic.term -> unit ;
50 metasenv: Cic.metasenv ;
51 set_metasenv : Cic.metasenv -> unit ;
52 context: Cic.context ;
53 set_context : Cic.context -> unit >
55 val output_html : string -> 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 :
64 Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
65 (* invoked when the proof assistant's status has changed to notify Hbugs *)
66 val notify_hbugs : unit -> unit
72 val intros : unit -> unit
73 val exact : ?term:string -> unit -> unit
74 val apply : ?term:string -> unit -> unit
75 val elimintrossimpl : ?term:string -> unit -> unit
76 val elimtype : ?term:string -> unit -> unit
77 val whd : unit -> unit
78 val reduce : unit -> unit
79 val simpl : unit -> unit
80 val fold_whd : ?term:string -> unit -> unit
81 val fold_reduce : ?term:string -> unit -> unit
82 val fold_simpl : ?term:string -> unit -> unit
83 val cut : ?term:string -> unit -> unit
84 val change : unit -> unit
85 val letin : ?term:string -> unit -> unit
86 val ring : unit -> unit
87 val clearbody : unit -> unit
88 val clear : unit -> unit
89 val fourier : unit -> unit
90 val rewritesimpl : ?term:string -> unit -> unit
91 val rewritebacksimpl : ?term:string -> unit -> unit
92 val replace : unit -> unit
93 val reflexivity : unit -> unit
94 val symmetry : unit -> unit
95 val transitivity : ?term:string -> unit -> unit
96 val exists : unit -> unit
97 val split : unit -> unit
98 val left : unit -> unit
99 val right : unit -> unit
100 val assumption : unit -> unit
101 val generalize : unit -> unit
102 val absurd : ?term:string -> unit -> unit
103 val contradiction : unit -> unit
104 val decompose : ?term:string -> unit -> unit
105 val injection : ?term:string -> unit -> unit
106 val discriminate : ?term:string -> unit -> unit
107 val whd_in_scratch : unit -> unit
108 val reduce_in_scratch : unit -> unit
109 val simpl_in_scratch : unit -> unit
112 module Make (C: Callbacks) : Tactics =
115 let call_tactic tactic () =
116 let savedproof = !ProofEngine.proof in
117 let savedgoal = !ProofEngine.goal in
125 RefreshSequentException e ->
127 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
128 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
129 ProofEngine.proof := savedproof ;
130 ProofEngine.goal := savedgoal ;
132 | RefreshProofException e ->
134 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
135 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
136 ProofEngine.proof := savedproof ;
137 ProofEngine.goal := savedgoal ;
142 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
143 ProofEngine.proof := savedproof ;
144 ProofEngine.goal := savedgoal
147 let call_tactic_with_input tactic ?term () =
148 let savedproof = !ProofEngine.proof in
149 let savedgoal = !ProofEngine.goal in
150 let uri,metasenv,bo,ty =
151 match !ProofEngine.proof with
153 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
155 let canonical_context =
156 match !ProofEngine.goal with
159 let (_,canonical_context,_) =
160 List.find (function (m,_,_) -> m=metano) metasenv
168 | Some t -> (C.term_editor ())#set_term t);
169 (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
171 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
175 (C.term_editor ())#reset ;
178 RefreshSequentException e ->
180 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
181 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
182 ProofEngine.proof := savedproof ;
183 ProofEngine.goal := savedgoal ;
185 | RefreshProofException e ->
187 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
188 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
189 ProofEngine.proof := savedproof ;
190 ProofEngine.goal := savedgoal ;
195 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
196 ProofEngine.proof := savedproof ;
197 ProofEngine.goal := savedgoal
199 let call_tactic_with_goal_input tactic () =
200 let module L = LogicalOperations in
201 let module G = Gdome in
202 let savedproof = !ProofEngine.proof in
203 let savedgoal = !ProofEngine.goal in
204 match (C.sequent_viewer ())#get_selected_terms with
213 RefreshSequentException e ->
215 ("<h1 color=\"red\">Exception raised during the refresh of " ^
216 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
217 ProofEngine.proof := savedproof ;
218 ProofEngine.goal := savedgoal ;
220 | RefreshProofException e ->
222 ("<h1 color=\"red\">Exception raised during the refresh of " ^
223 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
224 ProofEngine.proof := savedproof ;
225 ProofEngine.goal := savedgoal ;
230 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
231 ProofEngine.proof := savedproof ;
232 ProofEngine.goal := savedgoal ;
236 ("<h1 color=\"red\">No term selected</h1>")
239 ("<h1 color=\"red\">Many terms selected</h1>")
241 let call_tactic_with_goal_inputs tactic () =
242 let module L = LogicalOperations in
243 let module G = Gdome in
244 let savedproof = !ProofEngine.proof in
245 let savedgoal = !ProofEngine.goal in
247 match (C.sequent_viewer ())#get_selected_terms with
250 ("<h1 color=\"red\">No term selected</h1>")
257 RefreshSequentException e ->
259 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
260 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
261 ProofEngine.proof := savedproof ;
262 ProofEngine.goal := savedgoal ;
264 | RefreshProofException e ->
266 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
267 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
268 ProofEngine.proof := savedproof ;
269 ProofEngine.goal := savedgoal ;
274 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
275 ProofEngine.proof := savedproof ;
276 ProofEngine.goal := savedgoal
278 let call_tactic_with_input_and_goal_input tactic () =
279 let module L = LogicalOperations in
280 let module G = Gdome in
281 let savedproof = !ProofEngine.proof in
282 let savedgoal = !ProofEngine.goal in
283 match (C.sequent_viewer ())#get_selected_terms with
287 let uri,metasenv,bo,ty =
288 match !ProofEngine.proof with
290 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
292 let canonical_context =
293 match !ProofEngine.goal with
296 let (_,canonical_context,_) =
297 List.find (function (m,_,_) -> m=metano) metasenv
300 let (metasenv',expr) =
301 (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
303 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
304 tactic ~goal_input:term ~input:expr ;
307 (C.term_editor ())#reset ;
310 RefreshSequentException e ->
312 ("<h1 color=\"red\">Exception raised during the refresh of " ^
313 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
314 ProofEngine.proof := savedproof ;
315 ProofEngine.goal := savedgoal ;
317 | RefreshProofException e ->
319 ("<h1 color=\"red\">Exception raised during the refresh of " ^
320 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
321 ProofEngine.proof := savedproof ;
322 ProofEngine.goal := savedgoal ;
327 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
328 ProofEngine.proof := savedproof ;
329 ProofEngine.goal := savedgoal ;
333 ("<h1 color=\"red\">No term selected</h1>")
336 ("<h1 color=\"red\">Many terms selected</h1>")
338 let call_tactic_with_goal_input_in_scratch tactic () =
339 let module L = LogicalOperations in
340 let module G = Gdome in
341 let scratch_window = C.scratch_window () in
342 match scratch_window#sequent_viewer#get_selected_terms with
346 let expr = tactic term scratch_window#term in
347 scratch_window#sequent_viewer#load_sequent
348 scratch_window#metasenv (111,scratch_window#context,expr) ;
349 scratch_window#set_term expr ;
350 scratch_window#show () ;
354 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
358 ("<h1 color=\"red\">No term selected</h1>")
361 ("<h1 color=\"red\">Many terms selected</h1>")
363 let call_tactic_with_goal_inputs_in_scratch tactic () =
364 let module L = LogicalOperations in
365 let module G = Gdome in
366 let scratch_window = C.scratch_window () in
367 match scratch_window#sequent_viewer#get_selected_terms with
370 ("<h1 color=\"red\">No terms selected</h1>")
373 let expr = tactic terms scratch_window#term in
374 scratch_window#sequent_viewer#load_sequent
375 scratch_window#metasenv (111,scratch_window#context,expr) ;
376 scratch_window#set_term expr ;
377 scratch_window#show () ;
381 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
383 let call_tactic_with_hypothesis_input tactic () =
384 let module L = LogicalOperations in
385 let module G = Gdome in
386 let savedproof = !ProofEngine.proof in
387 let savedgoal = !ProofEngine.goal in
388 match (C.sequent_viewer ())#get_selected_hypotheses with
397 RefreshSequentException e ->
399 ("<h1 color=\"red\">Exception raised during the refresh of " ^
400 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
401 ProofEngine.proof := savedproof ;
402 ProofEngine.goal := savedgoal ;
404 | RefreshProofException e ->
406 ("<h1 color=\"red\">Exception raised during the refresh of " ^
407 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
408 ProofEngine.proof := savedproof ;
409 ProofEngine.goal := savedgoal ;
414 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
415 ProofEngine.proof := savedproof ;
416 ProofEngine.goal := savedgoal ;
420 ("<h1 color=\"red\">No hypothesis selected</h1>")
423 ("<h1 color=\"red\">Many hypothesis selected</h1>")
428 (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
429 let exact = call_tactic_with_input ProofEngine.exact
430 let apply = call_tactic_with_input ProofEngine.apply
431 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
432 let elimtype = call_tactic_with_input ProofEngine.elim_type
433 let whd = call_tactic_with_goal_inputs ProofEngine.whd
434 let reduce = call_tactic_with_goal_inputs ProofEngine.reduce
435 let simpl = call_tactic_with_goal_inputs ProofEngine.simpl
436 let fold_whd = call_tactic_with_input ProofEngine.fold_whd
437 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce
438 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl
440 call_tactic_with_input
441 (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback)
442 let change = call_tactic_with_input_and_goal_input ProofEngine.change
444 call_tactic_with_input
445 (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback)
446 let ring = call_tactic ProofEngine.ring
447 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody
448 let clear = call_tactic_with_hypothesis_input ProofEngine.clear
449 let fourier = call_tactic ProofEngine.fourier
450 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl
451 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl
452 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace
453 let reflexivity = call_tactic ProofEngine.reflexivity
454 let symmetry = call_tactic ProofEngine.symmetry
455 let transitivity = call_tactic_with_input ProofEngine.transitivity
456 let exists = call_tactic ProofEngine.exists
457 let split = call_tactic ProofEngine.split
458 let left = call_tactic ProofEngine.left
459 let right = call_tactic ProofEngine.right
460 let assumption = call_tactic ProofEngine.assumption
461 let injection = call_tactic_with_input ProofEngine.injection
462 let discriminate = call_tactic_with_input ProofEngine.discriminate
464 call_tactic_with_goal_inputs
465 (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
466 let absurd = call_tactic_with_input ProofEngine.absurd
467 let contradiction = call_tactic ProofEngine.contradiction
469 call_tactic_with_input
470 (ProofEngine.decompose
471 ~uris_choice_callback:C.decompose_uris_choice_callback)
473 call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
474 let reduce_in_scratch =
475 call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
476 let simpl_in_scratch =
477 call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch