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 exception RefreshSequentException of exn;;
  37 exception RefreshProofException of exn;;
  38
  39 module type Callbacks =
  40   sig
  41     (* input widgets *)
  42     val sequent_viewer : unit -> TermViewer.sequent_viewer
  43     val term_editor : unit -> TermEditor.term_editor
  44     val scratch_window :
  45      unit ->
  46       < sequent_viewer: TermViewer.sequent_viewer ;
  47         show: unit -> unit ;
  48         term: Cic.term ;
  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 >
  54     (* output messages *)
  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   end
  66 ;;
  67
  68 module Make(C:Callbacks) =
  69   struct
  70
  71    let call_tactic tactic () =
  72     let savedproof = !ProofEngine.proof in
  73     let savedgoal  = !ProofEngine.goal in
  74      begin
  75       try
  76        tactic () ;
  77        C.refresh_goals () ;
  78        C.refresh_proof ()
  79       with
  80          RefreshSequentException e ->
  81           C.output_html
  82            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
  83             "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
  84           ProofEngine.proof := savedproof ;
  85           ProofEngine.goal := savedgoal ;
  86           C.refresh_goals ()
  87        | RefreshProofException e ->
  88           C.output_html
  89            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
  90             "proof: " ^ Printexc.to_string e ^ "</h1>") ;
  91           ProofEngine.proof := savedproof ;
  92           ProofEngine.goal := savedgoal ;
  93           C.refresh_goals () ;
  94           C.refresh_proof ()
  95        | e ->
  96           C.output_html
  97            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
  98           ProofEngine.proof := savedproof ;
  99           ProofEngine.goal := savedgoal
 100      end
 101
 102    let call_tactic_with_input tactic () =
 103     let savedproof = !ProofEngine.proof in
 104     let savedgoal  = !ProofEngine.goal in
 105      let uri,metasenv,bo,ty =
 106       match !ProofEngine.proof with
 107          None -> assert false
 108        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 109      in
 110       let canonical_context =
 111        match !ProofEngine.goal with
 112           None -> assert false
 113         | Some metano ->
 114            let (_,canonical_context,_) =
 115             List.find (function (m,_,_) -> m=metano) metasenv
 116            in
 117             canonical_context
 118       in
 119        try
 120         let metasenv',expr =
 121          (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
 122         in
 123          ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 124          tactic expr ;
 125          C.refresh_goals () ;
 126          C.refresh_proof () ;
 127          (C.term_editor ())#reset
 128        with
 129           RefreshSequentException e ->
 130            C.output_html
 131             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 132              "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 133            ProofEngine.proof := savedproof ;
 134            ProofEngine.goal := savedgoal ;
 135            C.refresh_goals ()
 136         | RefreshProofException e ->
 137            C.output_html
 138             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 139              "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 140            ProofEngine.proof := savedproof ;
 141            ProofEngine.goal := savedgoal ;
 142            C.refresh_goals () ;
 143            C.refresh_proof ()
 144         | e ->
 145            C.output_html
 146             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 147            ProofEngine.proof := savedproof ;
 148            ProofEngine.goal := savedgoal
 149
 150   let call_tactic_with_goal_input tactic () =
 151    let module L = LogicalOperations in
 152    let module G = Gdome in
 153     let savedproof = !ProofEngine.proof in
 154     let savedgoal  = !ProofEngine.goal in
 155      match (C.sequent_viewer ())#get_selected_terms with
 156        [term] ->
 157          begin
 158           try
 159            tactic term ;
 160            C.refresh_goals () ;
 161            C.refresh_proof ()
 162           with
 163              RefreshSequentException e ->
 164               C.output_html
 165                ("<h1 color=\"red\">Exception raised during the refresh of " ^
 166                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 167               ProofEngine.proof := savedproof ;
 168               ProofEngine.goal := savedgoal ;
 169               C.refresh_goals ()
 170            | RefreshProofException e ->
 171               C.output_html
 172                ("<h1 color=\"red\">Exception raised during the refresh of " ^
 173                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
 174               ProofEngine.proof := savedproof ;
 175               ProofEngine.goal := savedgoal ;
 176               C.refresh_goals () ;
 177               C.refresh_proof ()
 178            | e ->
 179               C.output_html
 180                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 181               ProofEngine.proof := savedproof ;
 182               ProofEngine.goal := savedgoal ;
 183          end
 184      | [] ->
 185         C.output_html
 186          ("<h1 color=\"red\">No term selected</h1>")
 187      | _ ->
 188         C.output_html
 189          ("<h1 color=\"red\">Many terms selected</h1>")
 190
 191   let call_tactic_with_goal_inputs tactic () =
 192    let module L = LogicalOperations in
 193    let module G = Gdome in
 194     let savedproof = !ProofEngine.proof in
 195     let savedgoal  = !ProofEngine.goal in
 196      try
 197       match (C.sequent_viewer ())#get_selected_terms with
 198          [] ->
 199           C.output_html
 200            ("<h1 color=\"red\">No term selected</h1>")
 201        | terms ->
 202           tactic terms ;
 203           C.refresh_goals () ;
 204           C.refresh_proof ()
 205      with
 206         RefreshSequentException e ->
 207          C.output_html
 208           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 209            "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 210          ProofEngine.proof := savedproof ;
 211          ProofEngine.goal := savedgoal ;
 212          C.refresh_goals ()
 213       | RefreshProofException e ->
 214          C.output_html
 215           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 216            "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 217          ProofEngine.proof := savedproof ;
 218          ProofEngine.goal := savedgoal ;
 219          C.refresh_goals () ;
 220          C.refresh_proof ()
 221       | e ->
 222          C.output_html
 223           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 224          ProofEngine.proof := savedproof ;
 225          ProofEngine.goal := savedgoal
 226
 227   let call_tactic_with_input_and_goal_input tactic () =
 228    let module L = LogicalOperations in
 229    let module G = Gdome in
 230     let savedproof = !ProofEngine.proof in
 231     let savedgoal  = !ProofEngine.goal in
 232      match (C.sequent_viewer ())#get_selected_terms with
 233        [term] ->
 234          begin
 235           try
 236            let uri,metasenv,bo,ty =
 237             match !ProofEngine.proof with
 238                None -> assert false
 239              | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 240            in
 241             let canonical_context =
 242              match !ProofEngine.goal with
 243                 None -> assert false
 244               | Some metano ->
 245                  let (_,canonical_context,_) =
 246                   List.find (function (m,_,_) -> m=metano) metasenv
 247                  in
 248                   canonical_context in
 249             let (metasenv',expr) =
 250              (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
 251             in
 252              ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 253              tactic ~goal_input:term ~input:expr ;
 254              C.refresh_goals () ;
 255              C.refresh_proof () ;
 256              (C.term_editor ())#reset
 257           with
 258              RefreshSequentException e ->
 259               C.output_html
 260                ("<h1 color=\"red\">Exception raised during the refresh of " ^
 261                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 262               ProofEngine.proof := savedproof ;
 263               ProofEngine.goal := savedgoal ;
 264               C.refresh_goals ()
 265            | RefreshProofException e ->
 266               C.output_html
 267                ("<h1 color=\"red\">Exception raised during the refresh of " ^
 268                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
 269               ProofEngine.proof := savedproof ;
 270               ProofEngine.goal := savedgoal ;
 271               C.refresh_goals () ;
 272               C.refresh_proof ()
 273            | e ->
 274               C.output_html
 275                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 276               ProofEngine.proof := savedproof ;
 277               ProofEngine.goal := savedgoal ;
 278          end
 279      | [] ->
 280         C.output_html
 281          ("<h1 color=\"red\">No term selected</h1>")
 282      | _ ->
 283         C.output_html
 284          ("<h1 color=\"red\">Many terms selected</h1>")
 285
 286   let call_tactic_with_goal_input_in_scratch tactic () =
 287    let module L = LogicalOperations in
 288    let module G = Gdome in
 289     let savedproof = !ProofEngine.proof in
 290     let savedgoal  = !ProofEngine.goal in
 291     let scratch_window = C.scratch_window () in
 292      match scratch_window#sequent_viewer#get_selected_terms with
 293        [term] ->
 294          begin
 295           try
 296            let expr = tactic term scratch_window#term in
 297             scratch_window#sequent_viewer#load_sequent
 298              scratch_window#metasenv (111,scratch_window#context,expr) ;
 299             scratch_window#set_term expr ;
 300             scratch_window#show () ;
 301           with
 302            e ->
 303             C.output_html
 304              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 305          end
 306      | [] ->
 307         C.output_html
 308          ("<h1 color=\"red\">No term selected</h1>")
 309      | _ ->
 310         C.output_html
 311          ("<h1 color=\"red\">Many terms selected</h1>")
 312
 313   let call_tactic_with_goal_inputs_in_scratch tactic () =
 314    let module L = LogicalOperations in
 315    let module G = Gdome in
 316     let scratch_window = C.scratch_window () in
 317     let savedproof = !ProofEngine.proof in
 318     let savedgoal  = !ProofEngine.goal in
 319      match scratch_window#sequent_viewer#get_selected_terms with
 320         [] ->
 321          C.output_html
 322           ("<h1 color=\"red\">No term selected</h1>")
 323       | terms ->
 324          try
 325           let expr = tactic terms scratch_window#term in
 326            scratch_window#sequent_viewer#load_sequent
 327             scratch_window#metasenv (111,scratch_window#context,expr) ;
 328            scratch_window#set_term expr ;
 329            scratch_window#show () ;
 330          with
 331           e ->
 332            C.output_html
 333             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 334
 335   let call_tactic_with_hypothesis_input tactic () =
 336    let module L = LogicalOperations in
 337    let module G = Gdome in
 338     let savedproof = !ProofEngine.proof in
 339     let savedgoal  = !ProofEngine.goal in
 340      match (C.sequent_viewer ())#get_selected_hypotheses with
 341        [hypothesis] ->
 342          begin
 343           try
 344            tactic hypothesis ;
 345            C.refresh_goals () ;
 346            C.refresh_proof ()
 347           with
 348              RefreshSequentException e ->
 349               C.output_html
 350                ("<h1 color=\"red\">Exception raised during the refresh of " ^
 351                 "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 352               ProofEngine.proof := savedproof ;
 353               ProofEngine.goal := savedgoal ;
 354               C.refresh_goals ()
 355            | RefreshProofException e ->
 356               C.output_html
 357                ("<h1 color=\"red\">Exception raised during the refresh of " ^
 358                 "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
 359               ProofEngine.proof := savedproof ;
 360               ProofEngine.goal := savedgoal ;
 361               C.refresh_goals () ;
 362               C.refresh_proof ()
 363            | e ->
 364               C.output_html
 365                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 366               ProofEngine.proof := savedproof ;
 367               ProofEngine.goal := savedgoal ;
 368          end
 369      | [] ->
 370         C.output_html
 371          ("<h1 color=\"red\">No hypothesis selected</h1>")
 372      | _ ->
 373         C.output_html
 374          ("<h1 color=\"red\">Many hypothesis selected</h1>")
 375
 376
 377   let intros =
 378    call_tactic
 379     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 380   let exact = call_tactic_with_input ProofEngine.exact
 381   let apply = call_tactic_with_input ProofEngine.apply
 382   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
 383   let elimtype = call_tactic_with_input ProofEngine.elim_type
 384   let whd = call_tactic_with_goal_inputs ProofEngine.whd
 385   let reduce = call_tactic_with_goal_inputs ProofEngine.reduce
 386   let simpl = call_tactic_with_goal_inputs ProofEngine.simpl
 387   let fold_whd = call_tactic_with_input ProofEngine.fold_whd
 388   let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce
 389   let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl
 390   let cut =
 391    call_tactic_with_input
 392     (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 393   let change = call_tactic_with_input_and_goal_input ProofEngine.change
 394   let letin =
 395    call_tactic_with_input
 396     (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 397   let ring = call_tactic ProofEngine.ring
 398   let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody
 399   let clear = call_tactic_with_hypothesis_input ProofEngine.clear
 400   let fourier = call_tactic ProofEngine.fourier
 401   let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl
 402   let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl
 403   let replace = call_tactic_with_input_and_goal_input ProofEngine.replace
 404   let reflexivity = call_tactic ProofEngine.reflexivity
 405   let symmetry = call_tactic ProofEngine.symmetry
 406   let transitivity = call_tactic_with_input ProofEngine.transitivity
 407   let exists = call_tactic ProofEngine.exists
 408   let split = call_tactic ProofEngine.split
 409   let left = call_tactic ProofEngine.left
 410   let right = call_tactic ProofEngine.right
 411   let assumption = call_tactic ProofEngine.assumption
 412   let generalize =
 413    call_tactic_with_goal_inputs
 414     (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 415   let absurd = call_tactic_with_input ProofEngine.absurd
 416   let contradiction = call_tactic ProofEngine.contradiction
 417   let decompose =
 418    call_tactic_with_input
 419     (ProofEngine.decompose
 420       ~uris_choice_callback:C.decompose_uris_choice_callback)
 421   let whd_in_scratch =
 422    call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
 423   let reduce_in_scratch =
 424    call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
 425   let simpl_in_scratch =
 426    call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
 427
 428 end
 429 ;;