src/Provers/blast.ML

 
 
 (* global state information *)
 
 datatype state = State of
- {thy: theory,
+ {ctxt: Proof.context,
   fullTrace: branch list list Unsynchronized.ref,
   trail: term option Unsynchronized.ref list Unsynchronized.ref,
   ntrail: int Unsynchronized.ref,
   nclosed: int Unsynchronized.ref,
   ntried: int Unsynchronized.ref}
 
 fun reject_const thy c =
   is_some (Sign.const_type thy c) andalso
     error ("blast: theory contains illegal constant " ^ quote c);
 
-fun initialize thy =
- (reject_const thy "*Goal*";
-  reject_const thy "*False*";
-  State
-   {thy = thy,
-    fullTrace = Unsynchronized.ref [],
-    trail = Unsynchronized.ref [],
-    ntrail = Unsynchronized.ref 0,
-    nclosed = Unsynchronized.ref 0, (*branches closed: number of branches closed during the search*)
-    ntried = Unsynchronized.ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*)
+fun initialize ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val _ = reject_const thy "*Goal*";
+    val _ = reject_const thy "*False*";
+  in
+    State
+     {ctxt = ctxt,
+      fullTrace = Unsynchronized.ref [],
+      trail = Unsynchronized.ref [],
+      ntrail = Unsynchronized.ref 0,
+      nclosed = Unsynchronized.ref 0, (*number of branches closed during the search*)
+      ntried = Unsynchronized.ref 1} (*number of branches created by splitting (counting from 1)*)
+  end;
 
 
 
 (** Basic syntactic operations **)
 

 fun mkGoal P = Const ("*Goal*", []) $ P;
 
 fun isGoal (Const ("*Goal*", _) $ _) = true
   | isGoal _ = false;
 
-val TruepropC = Object_Logic.judgment_name Data.thy;
+val TruepropC = Object_Logic.judgment_name Data.thy;  (* FIXME *)
 val TruepropT = Sign.the_const_type Data.thy TruepropC;
 
 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
 
 fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm

 fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
 
 (*Tableau rule from elimination rule.
   Flag "upd" says that the inference updated the branch.
   Flag "dup" requests duplication of the affected formula.*)
-fun fromRule thy vars rl =
-  let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
+fun fromRule ctxt vars rl =
+  let val thy = Proof_Context.theory_of ctxt
+      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars
       fun tac (upd, dup,rot) i =
         emtac upd (if dup then rev_dup_elim rl else rl) i
         THEN
         rot_subgoals_tac (rot, #2 trl) i
   in Option.SOME (trl, tac) end
   handle
     ElimBadPrem => (*reject: prems don't preserve conclusion*)
-      (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
+      (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl);
         Option.NONE)
   | ElimBadConcl => (*ignore: conclusion is not just a variable*)
       (if !trace then
         (warning ("Ignoring ill-formed elimination rule:\n" ^
-          "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
+          "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl))
        else ();
        Option.NONE);
 
 
 (*** Conversion of Introduction Rules ***)

 (*Tableau rule from introduction rule.
   Flag "upd" says that the inference updated the branch.
   Flag "dup" requests duplication of the affected formula.
   Since haz rules are now delayed, "dup" is always FALSE for
   introduction rules.*)
-fun fromIntrRule thy vars rl =
-  let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
+fun fromIntrRule ctxt vars rl =
+  let val thy = Proof_Context.theory_of ctxt
+      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
       fun tac (upd,dup,rot) i =
          rmtac upd (if dup then Classical.dup_intr rl else rl) i
          THEN
          rot_subgoals_tac (rot, #2 trl) i
   in (trl, tac) end;

   | toTerm d (Var _)       = dummyVar
   | toTerm d (Abs(a,_))    = dummyVar
   | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
 
 
-fun netMkRules thy P vars (nps: netpair list) =
+fun netMkRules ctxt P vars (nps: netpair list) =
   case P of
       (Const ("*Goal*", _) $ G) =>
         let val pG = mk_Trueprop (toTerm 2 G)
             val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
-        in  map (fromIntrRule thy vars o #2) (order_list intrs)  end
+        in  map (fromIntrRule ctxt vars o #2) (order_list intrs)  end
     | _ =>
         let val pP = mk_Trueprop (toTerm 3 P)
             val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
-        in  map_filter (fromRule thy vars o #2) (order_list elims)  end;
+        in  map_filter (fromRule ctxt vars o #2) (order_list elims)  end;
 
 
 (*Normalize a branch--for tracing*)
 fun norm2 (G,md) = (norm G, md);
 

   | showTerm d (Abs(a,t))    = if d=0 then dummyVar
                                else Term.Abs(a, dummyT, showTerm (d-1) t)
   | showTerm d (f $ u)       = if d=0 then dummyVar
                                else Term.$ (showTerm d f, showTerm (d-1) u);
 
-fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
+fun string_of ctxt d t = Syntax.string_of_term ctxt (showTerm d t);
 
 (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   Ex(P) is duplicated as the assumption ~Ex(P). *)
 fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
   | negOfGoal G = G;

 
 (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
                       rotate_tac ~1 i;
 
-fun traceTerm thy t =
-  let val t' = norm (negOfGoal t)
-      val stm = string_of thy 8 t'
+fun traceTerm ctxt t =
+  let val thy = Proof_Context.theory_of ctxt
+      val t' = norm (negOfGoal t)
+      val stm = string_of ctxt 8 t'
   in
       case topType thy t' of
           NONE   => stm   (*no type to attach*)
-        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
+        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ ctxt T
   end;
 
 
 (*Print tracing information at each iteration of prover*)
-fun tracing (State {thy, fullTrace, ...}) brs =
-  let fun printPairs (((G,_)::_,_)::_)  = Output.tracing (traceTerm thy G)
-        | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm thy H ^ "\t (Unsafe)")
+fun tracing (State {ctxt, fullTrace, ...}) brs =
+  let fun printPairs (((G,_)::_,_)::_)  = Output.tracing (traceTerm ctxt G)
+        | printPairs (([],(H,_)::_)::_) = Output.tracing (traceTerm ctxt H ^ "\t (Unsafe)")
         | printPairs _                 = ()
       fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
             (fullTrace := brs0 :: !fullTrace;
              List.app (fn _ => Output.tracing "+") brs;
              Output.tracing (" [" ^ string_of_int lim ^ "] ");

   end;
 
 fun traceMsg s = if !trace then writeln s else ();
 
 (*Tracing: variables updated in the last branch operation?*)
-fun traceVars (State {thy, ntrail, trail, ...}) ntrl =
+fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl =
   if !trace then
       (case !ntrail-ntrl of
             0 => ()
           | 1 => Output.tracing "\t1 variable UPDATED:"
           | n => Output.tracing ("\t" ^ string_of_int n ^ " variables UPDATED:");
        (*display the instantiations themselves, though no variable names*)
-       List.app (fn v => Output.tracing ("   " ^ string_of thy 4 (the (!v))))
+       List.app (fn v => Output.tracing ("   " ^ string_of ctxt 4 (the (!v))))
            (List.take(!trail, !ntrail-ntrl));
-       writeln"")
+       writeln "")
     else ();
 
 (*Tracing: how many new branches are created?*)
 fun traceNew prems =
     if !trace then

      | _             => raise DEST_EQ;
 
 (*Substitute through the branch if an equality goal (else raise DEST_EQ).
   Moves affected literals back into the branch, but it is not clear where
   they should go: this could make proofs fail.*)
-fun equalSubst thy (G, {pairs, lits, vars, lim}) =
+fun equalSubst ctxt (G, {pairs, lits, vars, lim}) =
   let val (t,u) = orientGoal(dest_eq G)
       val subst = subst_atomic (t,u)
       fun subst2(G,md) = (subst G, md)
       (*substitute throughout list; extract affected formulae*)
       fun subForm ((G,md), (changed, pairs)) =

             in  if nlit aconv lit then (changed, nlit::nlits)
                                   else ((nlit,true)::changed, nlits)
             end
       val (changed, lits') = List.foldr subLit ([], []) lits
       val (changed', pairs') = List.foldr subFrame (changed, []) pairs
-  in  if !trace then writeln ("Substituting " ^ traceTerm thy u ^
-                              " for " ^ traceTerm thy t ^ " in branch" )
+  in  if !trace then writeln ("Substituting " ^ traceTerm ctxt u ^
+                              " for " ^ traceTerm ctxt t ^ " in branch" )
       else ();
       {pairs = (changed',[])::pairs',   (*affected formulas, and others*)
        lits  = lits',                   (*unaffected literals*)
        vars  = vars,
        lim   = lim}

   end;
 
 (*Were there Skolem terms in the premise?  Must NOT chase Vars*)
 fun hasSkolem (Skolem _)     = true
   | hasSkolem (Abs (_,body)) = hasSkolem body
-  | hasSkolem (f$t)          =  hasSkolem f orelse hasSkolem t
+  | hasSkolem (f$t)          = hasSkolem f orelse hasSkolem t
   | hasSkolem _              = false;
 
 (*Attach the right "may duplicate" flag to new formulae: if they contain
   Skolem terms then allow duplication.*)
 fun joinMd md [] = []

 (*Tableau prover based on leanTaP.  Argument is a list of branches.  Each
   branch contains a list of unexpanded formulae, a list of literals, and a
   bound on unsafe expansions.
  "start" is CPU time at start, for printing search time
 *)
-fun prove (state, start, ctxt, brs, cont) =
- let val State {thy, ntrail, nclosed, ntried, ...} = state;
+fun prove (state, start, brs, cont) =
+ let val State {ctxt, ntrail, nclosed, ntried, ...} = state;
      val {safe0_netpair, safep_netpair, haz_netpair, ...} =
        Classical.rep_cs (Classical.claset_of ctxt);
      val safeList = [safe0_netpair, safep_netpair]
      and hazList  = [haz_netpair]
      fun prv (tacs, trs, choices, []) =

           let exception PRV (*backtrack to precisely this recursion!*)
               val ntrl = !ntrail
               val nbrs = length brs0
               val nxtVars = nextVars brs
               val G = norm G
-              val rules = netMkRules thy G vars safeList
+              val rules = netMkRules ctxt G vars safeList
               (*Make a new branch, decrementing "lim" if instantiations occur*)
               fun newBr (vars',lim') prems =
                   map (fn prem =>
                        if (exists isGoal prem)
                        then {pairs = ((joinMd md prem, []) ::

           in tracing state brs0;
              if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
              else
              prv (Data.hyp_subst_tac (!trace) :: tacs,
                   brs0::trs,  choices,
-                  equalSubst thy
+                  equalSubst ctxt
                     (G, {pairs = (br,haz)::pairs,
                          lits  = lits, vars  = vars, lim   = lim})
                     :: brs)
              handle DEST_EQ =>   closeF lits
               handle CLOSEF =>   closeFl ((br,haz)::pairs)
                 handle CLOSEF => deeper rules
                   handle NEWBRANCHES =>
-                   (case netMkRules thy G vars hazList of
+                   (case netMkRules ctxt G vars hazList of
                        [] => (*there are no plausible haz rules*)
                              (traceMsg "moving formula to literals";
                               prv (tacs, brs0::trs, choices,
                                    {pairs = (br,haz)::pairs,
                                     lits  = addLit(G,lits),

                        lits, vars, lim} :: brs) =
              (*no safe steps possible at any level: apply a haz rule*)
           let exception PRV (*backtrack to precisely this recursion!*)
               val H = norm H
               val ntrl = !ntrail
-              val rules = netMkRules thy H vars hazList
+              val rules = netMkRules ctxt H vars hazList
               (*new premises of haz rules may NOT be duplicated*)
               fun newPrem (vars,P,dup,lim') prem =
                   let val Gs' = map (fn Q => (Q,false)) prem
                       and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
                       and lits' = if (exists isGoal prem)

 (*Tactic using tableau engine and proof reconstruction.
  "start" is CPU time at start, for printing SEARCH time
         (also prints reconstruction time)
  "lim" is depth limit.*)
 fun timing_depth_tac start ctxt lim i st0 =
-  let val thy = Thm.theory_of_thm st0
-      val state = initialize thy
+  let val thy = Proof_Context.theory_of ctxt
+      val state = initialize ctxt
       val st = st0
         |> rotate_prems (i - 1)
         |> Conv.gconv_rule Object_Logic.atomize_prems 1
       val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
       val hyps  = strip_imp_prems skoprem

                        then writeln (Timing.message (Timing.result start) ^ " for reconstruction")
                        else ();
                        Seq.make(fn()=> cell))
           end
   in
-    prove (state, start, ctxt, [initBranch (mkGoal concl :: hyps, lim)], cont)
+    prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
     |> Seq.map (rotate_prems (1 - i))
   end
   handle PROVE => Seq.empty;
 
 (*Public version with fixed depth*)
 fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
 
 val (depth_limit, setup_depth_limit) =
-  Attrib.config_int_global @{binding blast_depth_limit} (K 20);
+  Attrib.config_int @{binding blast_depth_limit} (K 20);
 
 fun blast_tac ctxt i st =
-    ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
-        (timing_depth_tac (Timing.start ()) ctxt) 0) i
-     THEN flexflex_tac) st
-    handle TRANS s =>
-      ((if !trace then warning ("blast: " ^ s) else ());
-       Seq.empty);
+  ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i
+    THEN flexflex_tac) st
+  handle TRANS s => (if !trace then warning ("blast: " ^ s) else (); Seq.empty);
 
 
 
 (*** For debugging: these apply the prover to a subgoal and return
      the resulting tactics, trace, etc.                            ***)

 fun readGoal ctxt s =
   Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal;
 
 fun tryIt ctxt lim s =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val state as State {fullTrace = ft, ...} = initialize thy;
-    val res = timeap prove
-      (state, Timing.start (), ctxt, [initBranch ([readGoal ctxt s], lim)], I);
+    val state as State {fullTrace = ft, ...} = initialize ctxt;
+    val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I);
     val _ = fullTrace := !ft;
   in res end;
 
 
 (** method setup **)