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     (* invoked when the proof assistant's status has changed to notify Hbugs *)
  66     val notify_hbugs : unit -> unit
  67   end
  68 ;;
  69
  70 module type Tactics =
  71   sig
  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
 110   end
 111
 112 module Make (C: Callbacks) : Tactics =
 113   struct
 114
 115    let call_tactic tactic () =
 116     let savedproof = !ProofEngine.proof in
 117     let savedgoal  = !ProofEngine.goal in
 118      begin
 119       try
 120        tactic () ;
 121        C.refresh_goals () ;
 122        C.refresh_proof () ;
 123        C.notify_hbugs ()
 124       with
 125          RefreshSequentException e ->
 126           C.output_html
 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 ;
 131           C.refresh_goals ()
 132        | RefreshProofException e ->
 133           C.output_html
 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 ;
 138           C.refresh_goals () ;
 139           C.refresh_proof ()
 140        | e ->
 141           C.output_html
 142            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 143           ProofEngine.proof := savedproof ;
 144           ProofEngine.goal := savedgoal
 145      end
 146
 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
 152          None -> assert false
 153        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 154      in
 155       let canonical_context =
 156        match !ProofEngine.goal with
 157           None -> assert false
 158         | Some metano ->
 159            let (_,canonical_context,_) =
 160             List.find (function (m,_,_) -> m=metano) metasenv
 161            in
 162             canonical_context
 163       in
 164        try
 165         let metasenv',expr =
 166          (match term with
 167          | None -> ()
 168          | Some t -> (C.term_editor ())#set_term t);
 169          (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
 170         in
 171          ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 172          tactic expr ;
 173          C.refresh_goals () ;
 174          C.refresh_proof () ;
 175          (C.term_editor ())#reset ;
 176          C.notify_hbugs ()
 177        with
 178           RefreshSequentException e ->
 179            C.output_html
 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 ;
 184            C.refresh_goals ()
 185         | RefreshProofException e ->
 186            C.output_html
 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 ;
 191            C.refresh_goals () ;
 192            C.refresh_proof ()
 193         | e ->
 194            C.output_html
 195             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 196            ProofEngine.proof := savedproof ;
 197            ProofEngine.goal := savedgoal
 198
 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
 205        [term] ->
 206          begin
 207           try
 208            tactic term ;
 209            C.refresh_goals () ;
 210            C.refresh_proof () ;
 211            C.notify_hbugs ()
 212           with
 213              RefreshSequentException e ->
 214               C.output_html
 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 ;
 219               C.refresh_goals ()
 220            | RefreshProofException e ->
 221               C.output_html
 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 ;
 226               C.refresh_goals () ;
 227               C.refresh_proof ()
 228            | e ->
 229               C.output_html
 230                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 231               ProofEngine.proof := savedproof ;
 232               ProofEngine.goal := savedgoal ;
 233          end
 234      | [] ->
 235         C.output_html
 236          ("<h1 color=\"red\">No term selected</h1>")
 237      | _ ->
 238         C.output_html
 239          ("<h1 color=\"red\">Many terms selected</h1>")
 240
 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
 246      try
 247       match (C.sequent_viewer ())#get_selected_terms with
 248          [] ->
 249           C.output_html
 250            ("<h1 color=\"red\">No term selected</h1>")
 251        | terms ->
 252           tactic terms ;
 253           C.refresh_goals () ;
 254           C.refresh_proof () ;
 255           C.notify_hbugs ()
 256      with
 257         RefreshSequentException e ->
 258          C.output_html
 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 ;
 263          C.refresh_goals ()
 264       | RefreshProofException e ->
 265          C.output_html
 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 ;
 270          C.refresh_goals () ;
 271          C.refresh_proof ()
 272       | e ->
 273          C.output_html
 274           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 275          ProofEngine.proof := savedproof ;
 276          ProofEngine.goal := savedgoal
 277
 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
 284        [term] ->
 285          begin
 286           try
 287            let uri,metasenv,bo,ty =
 288             match !ProofEngine.proof with
 289                None -> assert false
 290              | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 291            in
 292             let canonical_context =
 293              match !ProofEngine.goal with
 294                 None -> assert false
 295               | Some metano ->
 296                  let (_,canonical_context,_) =
 297                   List.find (function (m,_,_) -> m=metano) metasenv
 298                  in
 299                   canonical_context in
 300             let (metasenv',expr) =
 301              (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
 302             in
 303              ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 304              tactic ~goal_input:term ~input:expr ;
 305              C.refresh_goals () ;
 306              C.refresh_proof () ;
 307              (C.term_editor ())#reset ;
 308              C.notify_hbugs ()
 309           with
 310              RefreshSequentException e ->
 311               C.output_html
 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 ;
 316               C.refresh_goals ()
 317            | RefreshProofException e ->
 318               C.output_html
 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 ;
 323               C.refresh_goals () ;
 324               C.refresh_proof ()
 325            | e ->
 326               C.output_html
 327                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 328               ProofEngine.proof := savedproof ;
 329               ProofEngine.goal := savedgoal ;
 330          end
 331      | [] ->
 332         C.output_html
 333          ("<h1 color=\"red\">No term selected</h1>")
 334      | _ ->
 335         C.output_html
 336          ("<h1 color=\"red\">Many terms selected</h1>")
 337
 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
 343        [term] ->
 344          begin
 345           try
 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 () ;
 351           with
 352            e ->
 353             C.output_html
 354              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 355          end
 356      | [] ->
 357         C.output_html
 358          ("<h1 color=\"red\">No term selected</h1>")
 359      | _ ->
 360         C.output_html
 361          ("<h1 color=\"red\">Many terms selected</h1>")
 362
 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
 368         [] ->
 369          C.output_html
 370           ("<h1 color=\"red\">No terms selected</h1>")
 371       | terms ->
 372          try
 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 () ;
 378          with
 379           e ->
 380            C.output_html
 381             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 382
 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
 389        [hypothesis] ->
 390          begin
 391           try
 392            tactic hypothesis ;
 393            C.refresh_goals () ;
 394            C.refresh_proof () ;
 395            C.notify_hbugs ()
 396           with
 397              RefreshSequentException e ->
 398               C.output_html
 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 ;
 403               C.refresh_goals ()
 404            | RefreshProofException e ->
 405               C.output_html
 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 ;
 410               C.refresh_goals () ;
 411               C.refresh_proof ()
 412            | e ->
 413               C.output_html
 414                ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 415               ProofEngine.proof := savedproof ;
 416               ProofEngine.goal := savedgoal ;
 417          end
 418      | [] ->
 419         C.output_html
 420          ("<h1 color=\"red\">No hypothesis selected</h1>")
 421      | _ ->
 422         C.output_html
 423          ("<h1 color=\"red\">Many hypothesis selected</h1>")
 424
 425
 426   let intros =
 427    call_tactic
 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
 439   let cut =
 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
 443   let letin =
 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
 463   let generalize =
 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
 468   let decompose =
 469    call_tactic_with_input
 470     (ProofEngine.decompose
 471       ~uris_choice_callback:C.decompose_uris_choice_callback)
 472   let whd_in_scratch =
 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
 478
 479 end
 480 ;;