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