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