src/Sequents/modal.ML

--- a/src/Sequents/modal.ML	Sat Dec 20 19:12:41 2014 +0100
+++ b/src/Sequents/modal.ML	Sat Dec 20 22:23:37 2014 +0100
@@ -7,22 +7,22 @@
 
 signature MODAL_PROVER_RULE =
 sig
-    val rewrite_rls      : thm list
-    val safe_rls         : thm list
-    val unsafe_rls       : thm list
-    val bound_rls        : thm list
-    val aside_rls        : thm list
+  val rewrite_rls      : thm list
+  val safe_rls         : thm list
+  val unsafe_rls       : thm list
+  val bound_rls        : thm list
+  val aside_rls        : thm list
 end;
 
-signature MODAL_PROVER = 
+signature MODAL_PROVER =
 sig
-    val rule_tac   : thm list -> int ->tactic
-    val step_tac   : int -> tactic
-    val solven_tac : int -> int -> tactic
-    val solve_tac  : Proof.context -> int -> tactic
+  val rule_tac   : Proof.context -> thm list -> int ->tactic
+  val step_tac   : Proof.context -> int -> tactic
+  val solven_tac : Proof.context -> int -> int -> tactic
+  val solve_tac  : Proof.context -> int -> tactic
 end;
 
-functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER = 
+functor Modal_ProverFun (Modal_Rule: MODAL_PROVER_RULE) : MODAL_PROVER =
 struct
 
 (*Returns the list of all formulas in the sequent*)
@@ -35,7 +35,7 @@
   Assumes each formula in seqc is surrounded by sequence variables
   -- checks that each concl formula looks like some subgoal formula.*)
 fun could_res (seqp,seqc) =
-      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc)) 
+      forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
                               (forms_of_seq seqp))
              (forms_of_seq seqc);
 
@@ -59,11 +59,12 @@
 
 (* NB No back tracking possible with aside rules *)
 
-fun aside_tac n = DETERM(REPEAT (filt_resolve_tac Modal_Rule.aside_rls 999 n));
-fun rule_tac rls n = fresolve_tac rls n THEN aside_tac n;
+val aside_net = Tactic.build_net Modal_Rule.aside_rls;
+fun aside_tac ctxt n = DETERM (REPEAT (filt_resolve_from_net_tac ctxt 999 aside_net n));
+fun rule_tac ctxt rls n = fresolve_tac rls n THEN aside_tac ctxt n;
 
 val fres_safe_tac = fresolve_tac Modal_Rule.safe_rls;
-val fres_unsafe_tac = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac;
+fun fres_unsafe_tac ctxt = fresolve_tac Modal_Rule.unsafe_rls THEN' aside_tac ctxt;
 val fres_bound_tac = fresolve_tac Modal_Rule.bound_rls;
 
 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
@@ -71,18 +72,19 @@
                     in fn st => tac (nprems_of st) st end;
 
 (* Depth first search bounded by d *)
-fun solven_tac d n state = state |>
-       (if d<0 then no_tac
-        else if (nprems_of state = 0) then all_tac 
-        else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
-                 ((fres_unsafe_tac n  THEN UPTOGOAL n (solven_tac d)) APPEND
-                   (fres_bound_tac n  THEN UPTOGOAL n (solven_tac (d-1)))));
+fun solven_tac ctxt d n st = st |>
+ (if d < 0 then no_tac
+  else if nprems_of st = 0 then all_tac
+  else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE
+           ((fres_unsafe_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt d)) APPEND
+             (fres_bound_tac n  THEN UPTOGOAL n (solven_tac ctxt (d - 1)))));
 
-fun solve_tac ctxt d = rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac d 1;
+fun solve_tac ctxt d =
+  rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1;
 
-fun step_tac n = 
-    COND (has_fewer_prems 1) all_tac 
-         (DETERM(fres_safe_tac n) ORELSE 
-          (fres_unsafe_tac n APPEND fres_bound_tac n));
+fun step_tac ctxt n =
+  COND (has_fewer_prems 1) all_tac
+       (DETERM(fres_safe_tac n) ORELSE
+        (fres_unsafe_tac ctxt n APPEND fres_bound_tac n));
 
 end;