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