--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 29/01/2003 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+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 >
+ (* output messages *)
+ val output_html : string -> 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 :
+ Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+ 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
+ end
+
+module Make (C: Callbacks) : Tactics =
+ struct
+
+ let call_tactic tactic () =
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ begin
+ try
+ tactic () ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ with
+ RefreshSequentException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal
+ end
+
+ let call_tactic_with_input tactic ?term () =
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ let uri,metasenv,bo,ty =
+ match !ProofEngine.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
+ try
+ let metasenv',expr =
+ (match term with
+ | None -> ()
+ | Some t -> (C.term_editor ())#set_term t);
+ (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+ in
+ ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ tactic expr ;
+ C.refresh_goals () ;
+ C.refresh_proof () ;
+ (C.term_editor ())#reset
+ with
+ RefreshSequentException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal
+
+ let call_tactic_with_goal_input tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match (C.sequent_viewer ())#get_selected_terms with
+ [term] ->
+ begin
+ try
+ tactic term ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ with
+ RefreshSequentException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of " ^
+ "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of " ^
+ "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | [] ->
+ C.output_html
+ ("<h1 color=\"red\">No term selected</h1>")
+ | _ ->
+ C.output_html
+ ("<h1 color=\"red\">Many terms selected</h1>")
+
+ let call_tactic_with_goal_inputs tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ try
+ match (C.sequent_viewer ())#get_selected_terms with
+ [] ->
+ C.output_html
+ ("<h1 color=\"red\">No term selected</h1>")
+ | terms ->
+ tactic terms ;
+ C.refresh_goals () ;
+ C.refresh_proof () ;
+ with
+ RefreshSequentException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal
+
+ let call_tactic_with_input_and_goal_input tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match (C.sequent_viewer ())#get_selected_terms with
+ [term] ->
+ begin
+ try
+ let uri,metasenv,bo,ty =
+ match !ProofEngine.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) =
+ (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+ in
+ ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ tactic ~goal_input:term ~input:expr ;
+ C.refresh_goals () ;
+ C.refresh_proof () ;
+ (C.term_editor ())#reset
+ with
+ RefreshSequentException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of " ^
+ "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of " ^
+ "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | [] ->
+ C.output_html
+ ("<h1 color=\"red\">No term selected</h1>")
+ | _ ->
+ C.output_html
+ ("<h1 color=\"red\">Many terms selected</h1>")
+
+ 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 ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | [] ->
+ C.output_html
+ ("<h1 color=\"red\">No term selected</h1>")
+ | _ ->
+ C.output_html
+ ("<h1 color=\"red\">Many terms selected</h1>")
+
+ 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
+ [] ->
+ C.output_html
+ ("<h1 color=\"red\">No terms selected</h1>")
+ | 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 ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+
+ let call_tactic_with_hypothesis_input tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match (C.sequent_viewer ())#get_selected_hypotheses with
+ [hypothesis] ->
+ begin
+ try
+ tactic hypothesis ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ with
+ RefreshSequentException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of " ^
+ "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html
+ ("<h1 color=\"red\">Exception raised during the refresh of " ^
+ "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | [] ->
+ C.output_html
+ ("<h1 color=\"red\">No hypothesis selected</h1>")
+ | _ ->
+ C.output_html
+ ("<h1 color=\"red\">Many hypothesis selected</h1>")
+
+
+ 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 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
+;;
projects / helm.git / blobdiff