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