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 open Printf
  37
  38 exception RefreshSequentException of exn;;
  39 exception RefreshProofException of exn;;
  40
  41 module type Callbacks =
  42   sig
  43     (* input widgets *)
  44     val sequent_viewer : unit -> TermViewer.sequent_viewer
  45     val term_editor : unit -> TermEditor.term_editor
  46     val scratch_window :
  47      unit ->
  48       < sequent_viewer: TermViewer.sequent_viewer ;
  49         show: unit -> unit ;
  50         term: Cic.term ;
  51         set_term : Cic.term -> unit ;
  52         metasenv: Cic.metasenv ;
  53         set_metasenv : Cic.metasenv -> unit ;
  54         context: Cic.context ;
  55         set_context : Cic.context -> 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 : ProofEngineTypes.mk_fresh_name_type
  64     val mqi_handle : MQIConn.handle
  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    val auto : unit -> unit
 109   end
 110
 111 module Make (C: Callbacks) : Tactics =
 112   struct
 113
 114    let print_uncaught_exception e =
 115      HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s"
 116       (Printexc.to_string e))))
 117
 118    let handle_refresh_exception f savedproof savedgoal =
 119      try
 120        f ()
 121      with
 122      | RefreshSequentException e ->
 123         HelmLogger.log (`Error (`T
 124           (sprintf "Exception raised during the refresh of the sequent: %s"
 125             (Printexc.to_string e))));
 126         ProofEngine.set_proof savedproof ;
 127         ProofEngine.goal := savedgoal ;
 128         C.refresh_goals ()
 129      | RefreshProofException e ->
 130         HelmLogger.log (`Error (`T
 131           (sprintf "Exception raised during the refresh of the proof: %s"
 132             (Printexc.to_string e))));
 133         ProofEngine.set_proof savedproof ;
 134         ProofEngine.goal := savedgoal ;
 135         C.refresh_goals () ;
 136         C.refresh_proof ()
 137      | e ->
 138         print_uncaught_exception e;
 139         ProofEngine.set_proof savedproof ;
 140         ProofEngine.goal := savedgoal
 141
 142    let call_tactic tactic () =
 143     let savedproof = ProofEngine.get_proof () in
 144     let savedgoal  = !ProofEngine.goal in
 145     handle_refresh_exception
 146       (fun () ->
 147         tactic ();
 148         C.refresh_goals ();
 149         C.refresh_proof ())
 150       savedproof savedgoal
 151
 152    let call_tactic_with_input tactic ?term () =
 153     let savedproof = ProofEngine.get_proof () in
 154     let savedgoal  = !ProofEngine.goal in
 155      let uri,metasenv,bo,ty =
 156       match ProofEngine.get_proof () with
 157          None -> assert false
 158        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 159      in
 160       let canonical_context =
 161        match !ProofEngine.goal with
 162           None -> assert false
 163         | Some metano ->
 164            let (_,canonical_context,_) =
 165             List.find (function (m,_,_) -> m=metano) metasenv
 166            in
 167             canonical_context
 168       in
 169        handle_refresh_exception
 170         (fun () ->
 171           let metasenv',expr =
 172            (match term with
 173            | None -> ()
 174            | Some t -> (C.term_editor ())#set_term t);
 175            (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
 176           in
 177            ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
 178            tactic expr ;
 179            C.refresh_goals () ;
 180            C.refresh_proof () ;
 181            (C.term_editor ())#reset)
 182         savedproof savedgoal
 183
 184   let call_tactic_with_goal_input tactic () =
 185    let module L = LogicalOperations in
 186    let module G = Gdome in
 187     let savedproof = ProofEngine.get_proof () in
 188     let savedgoal  = !ProofEngine.goal in
 189      match (C.sequent_viewer ())#get_selected_terms with
 190      | [term] ->
 191          handle_refresh_exception
 192           (fun () ->
 193             tactic term ;
 194             C.refresh_goals () ;
 195             C.refresh_proof ())
 196           savedproof savedgoal
 197      | [] -> HelmLogger.log (`Error (`T "No term selected"))
 198      | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 199
 200   let call_tactic_with_goal_inputs tactic () =
 201    let module L = LogicalOperations in
 202    let module G = Gdome in
 203     let savedproof = ProofEngine.get_proof () in
 204     let savedgoal  = !ProofEngine.goal in
 205      handle_refresh_exception
 206       (fun () ->
 207         match (C.sequent_viewer ())#get_selected_terms with
 208          | [] -> HelmLogger.log (`Error (`T "No term selected"))
 209          | terms ->
 210             tactic terms ;
 211             C.refresh_goals () ;
 212             C.refresh_proof ())
 213       savedproof savedgoal
 214
 215   let call_tactic_with_input_and_goal_input tactic () =
 216    let module L = LogicalOperations in
 217    let module G = Gdome in
 218     let savedproof = ProofEngine.get_proof () in
 219     let savedgoal  = !ProofEngine.goal in
 220      match (C.sequent_viewer ())#get_selected_terms with
 221        [term] ->
 222          handle_refresh_exception
 223           (fun () ->
 224              let uri,metasenv,bo,ty =
 225               match ProofEngine.get_proof () with
 226                  None -> assert false
 227                | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 228              in
 229               let canonical_context =
 230                match !ProofEngine.goal with
 231                   None -> assert false
 232                 | Some metano ->
 233                    let (_,canonical_context,_) =
 234                     List.find (function (m,_,_) -> m=metano) metasenv
 235                    in
 236                     canonical_context in
 237               let (metasenv',expr) =
 238                (C.term_editor ())#get_metasenv_and_term
 239                 canonical_context metasenv
 240               in
 241                ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
 242                tactic ~goal_input:term ~input:expr ;
 243                C.refresh_goals () ;
 244                C.refresh_proof () ;
 245                (C.term_editor ())#reset)
 246           savedproof savedgoal
 247      | [] -> HelmLogger.log (`Error (`T "No term selected"))
 248      | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 249
 250   let call_tactic_with_goal_input_in_scratch tactic () =
 251    let module L = LogicalOperations in
 252    let module G = Gdome in
 253     let scratch_window = C.scratch_window () in
 254      match scratch_window#sequent_viewer#get_selected_terms with
 255      | [term] ->
 256          begin
 257           try
 258            let expr = tactic term scratch_window#term in
 259             scratch_window#sequent_viewer#load_sequent
 260              scratch_window#metasenv (111,scratch_window#context,expr) ;
 261             scratch_window#set_term expr ;
 262             scratch_window#show () ;
 263           with
 264            e -> print_uncaught_exception e
 265          end
 266      | [] -> HelmLogger.log (`Error (`T "No term selected"))
 267      | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 268
 269   let call_tactic_with_goal_inputs_in_scratch tactic () =
 270    let module L = LogicalOperations in
 271    let module G = Gdome in
 272     let scratch_window = C.scratch_window () in
 273      match scratch_window#sequent_viewer#get_selected_terms with
 274       | [] -> HelmLogger.log (`Error (`T "No term selected"))
 275       | terms ->
 276          try
 277           let expr = tactic terms scratch_window#term in
 278            scratch_window#sequent_viewer#load_sequent
 279             scratch_window#metasenv (111,scratch_window#context,expr) ;
 280            scratch_window#set_term expr ;
 281            scratch_window#show () ;
 282          with
 283           e -> print_uncaught_exception e
 284
 285   let call_tactic_with_hypothesis_input tactic () =
 286    let module L = LogicalOperations in
 287    let module G = Gdome in
 288     let savedproof = ProofEngine.get_proof () in
 289     let savedgoal  = !ProofEngine.goal in
 290      match (C.sequent_viewer ())#get_selected_hypotheses with
 291      | [hypothesis] ->
 292          handle_refresh_exception
 293            (fun () ->
 294              tactic hypothesis ;
 295              C.refresh_goals () ;
 296              C.refresh_proof ())
 297            savedproof savedgoal
 298      | [] -> HelmLogger.log (`Error (`T "No hypothesis selected"))
 299      | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
 300
 301
 302
 303   let intros =
 304    call_tactic
 305     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 306   let exact = call_tactic_with_input ProofEngine.exact
 307   let apply = call_tactic_with_input ProofEngine.apply
 308   let auto = call_tactic (ProofEngine.auto C.mqi_handle)
 309   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
 310   let elimtype = call_tactic_with_input ProofEngine.elim_type
 311   let whd = call_tactic_with_goal_inputs ProofEngine.whd
 312   let reduce = call_tactic_with_goal_inputs ProofEngine.reduce
 313   let simpl = call_tactic_with_goal_inputs ProofEngine.simpl
 314   let fold_whd = call_tactic_with_input ProofEngine.fold_whd
 315   let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce
 316   let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl
 317   let cut =
 318    call_tactic_with_input
 319     (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 320   let change = call_tactic_with_input_and_goal_input ProofEngine.change
 321   let letin =
 322    call_tactic_with_input
 323     (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 324   let ring = call_tactic ProofEngine.ring
 325   let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody
 326   let clear = call_tactic_with_hypothesis_input ProofEngine.clear
 327   let fourier = call_tactic ProofEngine.fourier
 328   let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl
 329   let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl
 330   let replace = call_tactic_with_input_and_goal_input ProofEngine.replace
 331   let reflexivity = call_tactic ProofEngine.reflexivity
 332   let symmetry = call_tactic ProofEngine.symmetry
 333   let transitivity = call_tactic_with_input ProofEngine.transitivity
 334   let exists = call_tactic ProofEngine.exists
 335   let split = call_tactic ProofEngine.split
 336   let left = call_tactic ProofEngine.left
 337   let right = call_tactic ProofEngine.right
 338   let assumption = call_tactic ProofEngine.assumption
 339   let injection = call_tactic_with_input ProofEngine.injection
 340   let discriminate = call_tactic_with_input ProofEngine.discriminate
 341   let generalize =
 342    call_tactic_with_goal_inputs
 343     (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
 344   let absurd = call_tactic_with_input ProofEngine.absurd
 345   let contradiction = call_tactic ProofEngine.contradiction
 346   let decompose =
 347    call_tactic_with_input
 348     (ProofEngine.decompose
 349       ~uris_choice_callback:C.decompose_uris_choice_callback)
 350   let whd_in_scratch =
 351    call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
 352   let reduce_in_scratch =
 353    call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
 354   let simpl_in_scratch =
 355    call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
 356
 357 end
 358 ;;