X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FinvokeTactics.ml;h=13dc83f1d02dbba6531d18db4e70d5f0fdbc3321;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=31804290930e10986ab38194c8a709e3bdc9a2b6;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 318042909..13dc83f1d 100644
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
+open Printf
+
 exception RefreshSequentException of exn;;
 exception RefreshProofException of exn;;
 
@@ -51,8 +53,6 @@ module type Callbacks =
         set_metasenv : Cic.metasenv -> unit ;
         context: Cic.context ;
         set_context : Cic.context -> unit >
-    (* output messages *)
-    val output_html : string -> unit
     (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
@@ -60,8 +60,9 @@ module type Callbacks =
     val decompose_uris_choice_callback :
       (UriManager.uri * int * 'a) list ->
       (UriManager.uri * int * 'b list) list
-    val mk_fresh_name_callback :
-      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val mk_fresh_name_callback : ProofEngineTypes.mk_fresh_name_type
+    val mqi_handle : MQIConn.handle
+    val dbd:Mysql.dbd
   end
 ;;
 
@@ -105,47 +106,55 @@ module type Tactics =
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit
+   val auto : unit -> unit 
   end
 
 module Make (C: Callbacks) : Tactics =
   struct
 
+   let print_uncaught_exception e =
+     HelmLogger.log (`Error (`T (sprintf "Uncaught exception: %s"
+      (Printexc.to_string e))))
+
+   let handle_refresh_exception f savedproof savedgoal =
+     try
+       f ()
+     with
+     | RefreshSequentException e ->
+        HelmLogger.log (`Error (`T
+          (sprintf "Exception raised during the refresh of the sequent: %s"
+            (Printexc.to_string e))));
+        ProofEngine.set_proof savedproof ;
+        ProofEngine.goal := savedgoal ;
+        C.refresh_goals ()
+     | RefreshProofException e ->
+        HelmLogger.log (`Error (`T
+          (sprintf "Exception raised during the refresh of the proof: %s"
+            (Printexc.to_string e))));
+        ProofEngine.set_proof savedproof ;
+        ProofEngine.goal := savedgoal ;
+        C.refresh_goals () ;
+        C.refresh_proof ()
+     | e ->
+        print_uncaught_exception e;
+        ProofEngine.set_proof savedproof ;
+        ProofEngine.goal := savedgoal
+
    let call_tactic tactic () =
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
-     begin
-      try
-       tactic () ;
-       C.refresh_goals () ;
-       C.refresh_proof ()
-      with
-         RefreshSequentException e ->
-          C.output_html
-           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-            "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
-          ProofEngine.goal := savedgoal ;
-          C.refresh_goals ()
-       | RefreshProofException e ->
-          C.output_html
-           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-            "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
-          ProofEngine.goal := savedgoal ;
-          C.refresh_goals () ;
-          C.refresh_proof ()
-       | e ->
-          C.output_html
-           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-          ProofEngine.proof := savedproof ;
-          ProofEngine.goal := savedgoal
-     end
+    handle_refresh_exception
+      (fun () ->
+        tactic ();
+        C.refresh_goals ();
+        C.refresh_proof ())
+      savedproof savedgoal
 
    let call_tactic_with_input tactic ?term () =
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      let uri,metasenv,bo,ty =
-      match !ProofEngine.proof with
+      match ProofEngine.get_proof () with
          None -> assert false
        | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
      in
@@ -158,182 +167,93 @@ module Make (C: Callbacks) : Tactics =
            in
             canonical_context
       in
-       try
-        let metasenv',expr =
-         (match term with
-         | None -> ()
-         | Some t -> (C.term_editor ())#set_term t);
-         (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
-        in
-         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
-         tactic expr ;
-         C.refresh_goals () ;
-         C.refresh_proof () ;
-         (C.term_editor ())#reset
-       with
-          RefreshSequentException e ->
-           C.output_html
-            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-             "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
-           ProofEngine.goal := savedgoal ;
-           C.refresh_goals ()
-        | RefreshProofException e ->
-           C.output_html
-            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-             "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
-           ProofEngine.goal := savedgoal ;
+       handle_refresh_exception
+        (fun () ->
+          let metasenv',expr,ugraph = (*TASSI:  FIX THIS*)
+           (match term with
+           | None -> ()
+           | Some t -> (C.term_editor ())#set_term t);
+           (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+          in
+           ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+           tactic expr ;
            C.refresh_goals () ;
-           C.refresh_proof ()
-        | e ->
-           C.output_html
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-           ProofEngine.proof := savedproof ;
-           ProofEngine.goal := savedgoal
+           C.refresh_proof () ;
+           (C.term_editor ())#reset)
+        savedproof savedgoal
 
   let call_tactic_with_goal_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
-       [term] ->
-         begin
-          try
-           tactic term ;
-           C.refresh_goals () ;
-           C.refresh_proof ()
-          with
-             RefreshSequentException e ->
-              C.output_html
-               ("<h1 color=\"red\">Exception raised during the refresh of " ^
-                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals ()
-           | RefreshProofException e ->
-              C.output_html
-               ("<h1 color=\"red\">Exception raised during the refresh of " ^
-                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals () ;
-              C.refresh_proof ()
-           | e ->
-              C.output_html
-               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-         end
-     | [] ->
-        C.output_html
-         ("<h1 color=\"red\">No term selected</h1>")
-     | _ ->
-        C.output_html
-         ("<h1 color=\"red\">Many terms selected</h1>")
+     | [term] ->
+         handle_refresh_exception
+          (fun () ->
+            tactic term ;
+            C.refresh_goals () ;
+            C.refresh_proof ())
+          savedproof savedgoal
+     | [] -> HelmLogger.log (`Error (`T "No term selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_inputs tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
-     try
-      match (C.sequent_viewer ())#get_selected_terms with
-         [] ->
-          C.output_html
-           ("<h1 color=\"red\">No term selected</h1>")
-       | terms ->
-          tactic terms ;
-          C.refresh_goals () ;
-          C.refresh_proof () ;
-     with
-        RefreshSequentException e ->
-         C.output_html
-          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
-         ProofEngine.goal := savedgoal ;
-         C.refresh_goals ()
-      | RefreshProofException e ->
-         C.output_html
-          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
-         ProofEngine.goal := savedgoal ;
-         C.refresh_goals () ;
-         C.refresh_proof ()
-      | e ->
-         C.output_html
-          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-         ProofEngine.proof := savedproof ;
-         ProofEngine.goal := savedgoal
+     handle_refresh_exception
+      (fun () ->
+        match (C.sequent_viewer ())#get_selected_terms with
+         | [] -> HelmLogger.log (`Error (`T "No term selected"))
+         | terms ->
+            tactic terms ;
+            C.refresh_goals () ;
+            C.refresh_proof ())
+      savedproof savedgoal
 
   let call_tactic_with_input_and_goal_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_terms with
        [term] ->
-         begin
-          try
-           let uri,metasenv,bo,ty =
-            match !ProofEngine.proof with
-               None -> assert false
-             | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
-           in
-            let canonical_context =
-             match !ProofEngine.goal with
-                None -> assert false
-              | Some metano ->
-                 let (_,canonical_context,_) =
-                  List.find (function (m,_,_) -> m=metano) metasenv
-                 in
-                  canonical_context in
-            let (metasenv',expr) =
-             (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
-            in
-             ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
-             tactic ~goal_input:term ~input:expr ;
-             C.refresh_goals () ;
-             C.refresh_proof () ;
-             (C.term_editor ())#reset
-          with
-             RefreshSequentException e ->
-              C.output_html
-               ("<h1 color=\"red\">Exception raised during the refresh of " ^
-                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals ()
-           | RefreshProofException e ->
-              C.output_html
-               ("<h1 color=\"red\">Exception raised during the refresh of " ^
-                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals () ;
-              C.refresh_proof ()
-           | e ->
-              C.output_html
-               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-         end
-     | [] ->
-        C.output_html
-         ("<h1 color=\"red\">No term selected</h1>")
-     | _ ->
-        C.output_html
-         ("<h1 color=\"red\">Many terms selected</h1>")
+         handle_refresh_exception
+          (fun () ->
+             let uri,metasenv,bo,ty =
+              match ProofEngine.get_proof () with
+                 None -> assert false
+               | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+             in
+              let canonical_context =
+               match !ProofEngine.goal with
+                  None -> assert false
+                | Some metano ->
+                   let (_,canonical_context,_) =
+                    List.find (function (m,_,_) -> m=metano) metasenv
+                   in
+                    canonical_context in
+              let (metasenv',expr,ugraph) =(* FIX THIS AND *)
+               (C.term_editor ())#get_metasenv_and_term
+                canonical_context metasenv
+              in
+               ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+               tactic ~goal_input:term ~input:expr ;
+               C.refresh_goals () ;
+               C.refresh_proof () ;
+               (C.term_editor ())#reset)
+          savedproof savedgoal
+     | [] -> HelmLogger.log (`Error (`T "No term selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_input_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
     let scratch_window = C.scratch_window () in
      match scratch_window#sequent_viewer#get_selected_terms with
-       [term] ->
+     | [term] ->
          begin
           try
            let expr = tactic term scratch_window#term in
@@ -342,25 +262,17 @@ module Make (C: Callbacks) : Tactics =
             scratch_window#set_term expr ;
             scratch_window#show () ;
           with
-           e ->
-            C.output_html
-             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+           e -> print_uncaught_exception e
          end
-     | [] ->
-        C.output_html
-         ("<h1 color=\"red\">No term selected</h1>")
-     | _ ->
-        C.output_html
-         ("<h1 color=\"red\">Many terms selected</h1>")
+     | [] -> HelmLogger.log (`Error (`T "No term selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))
 
   let call_tactic_with_goal_inputs_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
     let scratch_window = C.scratch_window () in
      match scratch_window#sequent_viewer#get_selected_terms with
-        [] ->
-         C.output_html
-          ("<h1 color=\"red\">No terms selected</h1>")
+      | [] -> HelmLogger.log (`Error (`T "No term selected"))
       | terms ->
          try
           let expr = tactic terms scratch_window#term in
@@ -369,50 +281,24 @@ module Make (C: Callbacks) : Tactics =
            scratch_window#set_term expr ;
            scratch_window#show () ;
          with
-          e ->
-           C.output_html
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+          e -> print_uncaught_exception e
 
   let call_tactic_with_hypothesis_input tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let savedproof = !ProofEngine.proof in
+    let savedproof = ProofEngine.get_proof () in
     let savedgoal  = !ProofEngine.goal in
      match (C.sequent_viewer ())#get_selected_hypotheses with
-       [hypothesis] ->
-         begin
-          try
-           tactic hypothesis ;
-           C.refresh_goals () ;
-           C.refresh_proof ()
-          with
-             RefreshSequentException e ->
-              C.output_html
-               ("<h1 color=\"red\">Exception raised during the refresh of " ^
-                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals ()
-           | RefreshProofException e ->
-              C.output_html
-               ("<h1 color=\"red\">Exception raised during the refresh of " ^
-                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-              C.refresh_goals () ;
-              C.refresh_proof ()
-           | e ->
-              C.output_html
-               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-              ProofEngine.proof := savedproof ;
-              ProofEngine.goal := savedgoal ;
-         end
-     | [] ->
-        C.output_html
-         ("<h1 color=\"red\">No hypothesis selected</h1>")
-     | _ ->
-        C.output_html
-         ("<h1 color=\"red\">Many hypothesis selected</h1>")
+     | [hypothesis] ->
+         handle_refresh_exception
+           (fun () ->
+             tactic hypothesis ;
+             C.refresh_goals () ;
+             C.refresh_proof ())
+           savedproof savedgoal
+     | [] -> HelmLogger.log (`Error (`T "No hypothesis selected"))
+     | _ -> HelmLogger.log (`Error (`T "Too many hypotheses selected"))
+
 
 
   let intros =
@@ -420,6 +306,7 @@ module Make (C: Callbacks) : Tactics =
     (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
   let exact = call_tactic_with_input ProofEngine.exact
   let apply = call_tactic_with_input ProofEngine.apply
+  let auto = call_tactic (ProofEngine.auto ~dbd:C.dbd)
   let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
   let elimtype = call_tactic_with_input ProofEngine.elim_type
   let whd = call_tactic_with_goal_inputs ProofEngine.whd