src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Thu Sep 09 00:23:55 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 09 11:10:16 2004 +0200
@@ -5,6 +5,9 @@
 Proof states and methods.
 *)
 
+
+(*Jia Meng: added in atp_hook and modified enter_forward. *)
+
 signature BASIC_PROOF =
 sig
   val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
@@ -37,6 +40,7 @@
   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state
+  val atp_hook: (Thm.thm list * Thm.thm -> unit) ref
   val enter_forward: state -> state
   val verbose: bool ref
   val show_main_goal: bool ref
@@ -121,11 +125,16 @@
   val end_block: state -> state Seq.seq
   val next_block: state -> state
   val thisN: string
+  val call_atp: bool ref;
+
+
 end;
 
 structure Proof: PROOF =
 struct
 
+(*Jia Meng: by default, no ATP is called. *)
+val call_atp = ref false;
 
 (** proof state **)
 
@@ -298,7 +307,7 @@
 fun get_mode (State (Node {mode, ...}, _)) = mode;
 fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
 
-val enter_forward = put_mode Forward;
+val enter_forward_aux = put_mode Forward;
 val enter_forward_chain = put_mode ForwardChain;
 val enter_backward = put_mode Backward;
 
@@ -316,6 +325,31 @@
 val assert_no_chain = assert_mode (not_equal ForwardChain);
 
 
+(*Jia Meng: a hook to be used for calling ATPs. *)
+val atp_hook = ref (fn (prems,state): (Thm.thm list * Thm.thm) => ());
+
+(*Jia Meng: the modified version of enter_forward. *)
+(*Jia Meng: atp: Proof.state -> unit *)
+local
+ fun atp state = 
+  let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
+      val prems = ProofContext.prems_of ctxt  
+  in
+      (!atp_hook) (prems,thm)          
+  end;
+  
+
+in
+
+ fun enter_forward state = 
+   if (!call_atp) then 
+   ((atp state; enter_forward_aux state)
+                           handle (STATE _) => enter_forward_aux state)
+       else (enter_forward_aux state);
+
+end;
+
+
 (* blocks *)
 
 fun level (State (_, nodes)) = length nodes;