(* Copyright (C) 2000-2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) (* 29/01/2003 *) (* *) (* *) (******************************************************************************) open Printf exception RefreshSequentException of exn;; exception RefreshProofException of exn;; module type Callbacks = sig (* input widgets *) val sequent_viewer : unit -> TermViewer.sequent_viewer val term_editor : unit -> TermEditor.term_editor val scratch_window : unit -> < sequent_viewer: TermViewer.sequent_viewer ; show: unit -> unit ; term: Cic.term ; set_term : Cic.term -> unit ; metasenv: Cic.metasenv ; set_metasenv : Cic.metasenv -> unit ; context: Cic.context ; set_context : Cic.context -> unit > (* GUI refresh functions *) val refresh_proof : unit -> unit val refresh_goals : unit -> unit (* callbacks for user-tactics interaction *) val decompose_uris_choice_callback : (UriManager.uri * int * 'a) list -> (UriManager.uri * int * 'b list) list val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type val mqi_handle : MQIConn.handle val dbd:Mysql.dbd end ;; module type Tactics = sig val intros : unit -> unit val exact : ?term:string -> unit -> unit val apply : ?term:string -> unit -> unit val elimintrossimpl : ?term:string -> unit -> unit val elimtype : ?term:string -> unit -> unit val whd : unit -> unit val reduce : unit -> unit val simpl : unit -> unit val fold_whd : ?term:string -> unit -> unit val fold_reduce : ?term:string -> unit -> unit val fold_simpl : ?term:string -> unit -> unit val cut : ?term:string -> unit -> unit val change : unit -> unit val letin : ?term:string -> unit -> unit val ring : unit -> unit val clearbody : unit -> unit val clear : unit -> unit val fourier : unit -> unit val rewritesimpl : ?term:string -> unit -> unit val rewritebacksimpl : ?term:string -> unit -> unit val replace : unit -> unit val reflexivity : unit -> unit val symmetry : unit -> unit val transitivity : ?term:string -> unit -> unit val exists : unit -> unit val split : unit -> unit val left : unit -> unit val right : unit -> unit val assumption : unit -> unit val generalize : unit -> unit val absurd : ?term:string -> unit -> unit val contradiction : unit -> unit val decompose : ?term:string -> unit -> unit val injection : ?term:string -> unit -> unit val discriminate : ?term:string -> unit -> unit val whd_in_scratch : unit -> unit val reduce_in_scratch : unit -> unit val simpl_in_scratch : unit -> unit val auto : unit -> unit end module Make (C: Callbacks) : Tactics = struct let print_uncaught_exception e = HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s" (Printexc.to_string e)))) let handle_refresh_exception f savedproof savedgoal = try f () with | RefreshSequentException e -> HelmLogger.log (`Error (`T (sprintf "Exception raised during the refresh of the sequent: %s" (Printexc.to_string e)))); ProofEngine.set_proof savedproof ; ProofEngine.goal := savedgoal ; C.refresh_goals () | RefreshProofException e -> HelmLogger.log (`Error (`T (sprintf "Exception raised during the refresh of the proof: %s" (Printexc.to_string e)))); ProofEngine.set_proof savedproof ; ProofEngine.goal := savedgoal ; C.refresh_goals () ; C.refresh_proof () | e -> print_uncaught_exception e; ProofEngine.set_proof savedproof ; ProofEngine.goal := savedgoal let call_tactic tactic () = let savedproof = ProofEngine.get_proof () in let savedgoal = !ProofEngine.goal in handle_refresh_exception (fun () -> tactic (); C.refresh_goals (); C.refresh_proof ()) savedproof savedgoal let call_tactic_with_input tactic ?term () = let savedproof = ProofEngine.get_proof () in let savedgoal = !ProofEngine.goal in let uri,metasenv,bo,ty = match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in let canonical_context = match !ProofEngine.goal with None -> assert false | Some metano -> let (_,canonical_context,_) = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context in handle_refresh_exception (fun () -> let metasenv',expr,ugraph = (*TASSI: FIX THIS*) (match term with | None -> () | Some t -> (C.term_editor ())#set_term t); (C.term_editor ())#get_metasenv_and_term canonical_context metasenv in ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ; tactic expr ; C.refresh_goals () ; C.refresh_proof () ; (C.term_editor ())#reset) savedproof savedgoal let call_tactic_with_goal_input tactic () = let module L = LogicalOperations in let module G = Gdome in let savedproof = ProofEngine.get_proof () in let savedgoal = !ProofEngine.goal in match (C.sequent_viewer ())#get_selected_terms with | [term] -> handle_refresh_exception (fun () -> tactic term ; C.refresh_goals () ; C.refresh_proof ()) savedproof savedgoal | [] -> HelmLogger.log (`Error (`T "No term selected")) | _ -> HelmLogger.log (`Error (`T "Too many terms selected")) let call_tactic_with_goal_inputs tactic () = let module L = LogicalOperations in let module G = Gdome in let savedproof = ProofEngine.get_proof () in let savedgoal = !ProofEngine.goal in handle_refresh_exception (fun () -> match (C.sequent_viewer ())#get_selected_terms with | [] -> HelmLogger.log (`Error (`T "No term selected")) | terms -> tactic terms ; C.refresh_goals () ; C.refresh_proof ()) savedproof savedgoal let call_tactic_with_input_and_goal_input tactic () = let module L = LogicalOperations in let module G = Gdome in let savedproof = ProofEngine.get_proof () in let savedgoal = !ProofEngine.goal in match (C.sequent_viewer ())#get_selected_terms with [term] -> handle_refresh_exception (fun () -> let uri,metasenv,bo,ty = match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in let canonical_context = match !ProofEngine.goal with None -> assert false | Some metano -> let (_,canonical_context,_) = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context in let (metasenv',expr,ugraph) =(* FIX THIS AND *) (C.term_editor ())#get_metasenv_and_term canonical_context metasenv in ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ; tactic ~goal_input:term ~input:expr ; C.refresh_goals () ; C.refresh_proof () ; (C.term_editor ())#reset) savedproof savedgoal | [] -> HelmLogger.log (`Error (`T "No term selected")) | _ -> HelmLogger.log (`Error (`T "Too many terms selected")) let call_tactic_with_goal_input_in_scratch tactic () = let module L = LogicalOperations in let module G = Gdome in let scratch_window = C.scratch_window () in match scratch_window#sequent_viewer#get_selected_terms with | [term] -> begin try let expr = tactic term scratch_window#term in scratch_window#sequent_viewer#load_sequent scratch_window#metasenv (111,scratch_window#context,expr) ; scratch_window#set_term expr ; scratch_window#show () ; with e -> print_uncaught_exception e end | [] -> HelmLogger.log (`Error (`T "No term selected")) | _ -> HelmLogger.log (`Error (`T "Too many terms selected")) let call_tactic_with_goal_inputs_in_scratch tactic () = let module L = LogicalOperations in let module G = Gdome in let scratch_window = C.scratch_window () in match scratch_window#sequent_viewer#get_selected_terms with | [] -> HelmLogger.log (`Error (`T "No term selected")) | terms -> try let expr = tactic terms scratch_window#term in scratch_window#sequent_viewer#load_sequent scratch_window#metasenv (111,scratch_window#context,expr) ; scratch_window#set_term expr ; scratch_window#show () ; with e -> print_uncaught_exception e let call_tactic_with_hypothesis_input tactic () = let module L = LogicalOperations in let module G = Gdome in let savedproof = ProofEngine.get_proof () in let savedgoal = !ProofEngine.goal in match (C.sequent_viewer ())#get_selected_hypotheses with | [hypothesis] -> handle_refresh_exception (fun () -> tactic hypothesis ; C.refresh_goals () ; C.refresh_proof ()) savedproof savedgoal | [] -> HelmLogger.log (`Error (`T "No hypothesis selected")) | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected")) let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback) let exact = call_tactic_with_input ProofEngine.exact let apply = call_tactic_with_input ProofEngine.apply let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd) let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl let elimtype = call_tactic_with_input ProofEngine.elim_type let whd = call_tactic_with_goal_inputs ProofEngine.whd let reduce = call_tactic_with_goal_inputs ProofEngine.reduce let simpl = call_tactic_with_goal_inputs ProofEngine.simpl let fold_whd = call_tactic_with_input ProofEngine.fold_whd let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback) let change = call_tactic_with_input_and_goal_input ProofEngine.change let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback) let ring = call_tactic ProofEngine.ring let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody let clear = call_tactic_with_hypothesis_input ProofEngine.clear let fourier = call_tactic ProofEngine.fourier let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl let replace = call_tactic_with_input_and_goal_input ProofEngine.replace let reflexivity = call_tactic ProofEngine.reflexivity let symmetry = call_tactic ProofEngine.symmetry let transitivity = call_tactic_with_input ProofEngine.transitivity let exists = call_tactic ProofEngine.exists let split = call_tactic ProofEngine.split let left = call_tactic ProofEngine.left let right = call_tactic ProofEngine.right let assumption = call_tactic ProofEngine.assumption let injection = call_tactic_with_input ProofEngine.injection let discriminate = call_tactic_with_input ProofEngine.discriminate let generalize = call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback) let absurd = call_tactic_with_input ProofEngine.absurd let contradiction = call_tactic ProofEngine.contradiction let decompose = call_tactic_with_input (ProofEngine.decompose ~uris_choice_callback:C.decompose_uris_choice_callback) let whd_in_scratch = call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch let reduce_in_scratch = call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch let simpl_in_scratch = call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch end ;;