src/Pure/search.ML
changeset 32738 15bb09ca0378
parent 29269 5c25a2012975
child 32939 1b5a401c78cb
     1.1 --- a/src/Pure/search.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/search.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -13,23 +13,23 @@
     1.4    val THEN_MAYBE        : tactic * tactic -> tactic
     1.5    val THEN_MAYBE'       : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
     1.6  
     1.7 -  val trace_DEPTH_FIRST : bool ref
     1.8 +  val trace_DEPTH_FIRST : bool Unsynchronized.ref
     1.9    val DEPTH_FIRST       : (thm -> bool) -> tactic -> tactic
    1.10    val DEPTH_SOLVE       : tactic -> tactic
    1.11    val DEPTH_SOLVE_1     : tactic -> tactic
    1.12    val ITER_DEEPEN       : (thm->bool) -> (int->tactic) -> tactic
    1.13    val THEN_ITER_DEEPEN  : tactic -> (thm->bool) -> (int->tactic) -> tactic
    1.14 -  val iter_deepen_limit : int ref
    1.15 +  val iter_deepen_limit : int Unsynchronized.ref
    1.16  
    1.17    val has_fewer_prems   : int -> thm -> bool
    1.18    val IF_UNSOLVED       : tactic -> tactic
    1.19    val SOLVE             : tactic -> tactic
    1.20    val DETERM_UNTIL_SOLVED: tactic -> tactic
    1.21 -  val trace_BEST_FIRST  : bool ref
    1.22 +  val trace_BEST_FIRST  : bool Unsynchronized.ref
    1.23    val BEST_FIRST        : (thm -> bool) * (thm -> int) -> tactic -> tactic
    1.24    val THEN_BEST_FIRST   : tactic -> (thm->bool) * (thm->int) -> tactic
    1.25                            -> tactic
    1.26 -  val trace_ASTAR       : bool ref
    1.27 +  val trace_ASTAR       : bool Unsynchronized.ref
    1.28    val ASTAR             : (thm -> bool) * (int->thm->int) -> tactic -> tactic
    1.29    val THEN_ASTAR        : tactic -> (thm->bool) * (int->thm->int) -> tactic
    1.30                            -> tactic
    1.31 @@ -50,7 +50,7 @@
    1.32  
    1.33  (**** Depth-first search ****)
    1.34  
    1.35 -val trace_DEPTH_FIRST = ref false;
    1.36 +val trace_DEPTH_FIRST = Unsynchronized.ref false;
    1.37  
    1.38  (*Searches until "satp" reports proof tree as satisfied.
    1.39    Suppresses duplicate solutions to minimize search space.*)
    1.40 @@ -130,7 +130,7 @@
    1.41  
    1.42  
    1.43  (*No known example (on 1-5-2007) needs even thirty*)
    1.44 -val iter_deepen_limit = ref 50;
    1.45 +val iter_deepen_limit = Unsynchronized.ref 50;
    1.46  
    1.47  (*Depth-first iterative deepening search for a state that satisfies satp
    1.48    tactic tac0 sets up the initial goal queue, while tac1 searches it.
    1.49 @@ -138,7 +138,7 @@
    1.50    to suppress solutions arising from earlier searches, as the accumulated cost
    1.51    (k) can be wrong.*)
    1.52  fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
    1.53 - let val countr = ref 0
    1.54 + let val countr = Unsynchronized.ref 0
    1.55       and tf = tracify trace_DEPTH_FIRST (tac1 1)
    1.56       and qs0 = tac0 st
    1.57       (*bnd = depth bound; inc = estimate of increment required next*)
    1.58 @@ -156,7 +156,7 @@
    1.59         | depth (bnd,inc) ((k,np,rgd,q)::qs) =
    1.60            if k>=bnd then depth (bnd,inc) qs
    1.61            else
    1.62 -          case (countr := !countr+1;
    1.63 +          case (Unsynchronized.inc countr;
    1.64                  if !trace_DEPTH_FIRST then
    1.65                      tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
    1.66                  else ();
    1.67 @@ -199,7 +199,7 @@
    1.68  
    1.69  (*** Best-first search ***)
    1.70  
    1.71 -val trace_BEST_FIRST = ref false;
    1.72 +val trace_BEST_FIRST = Unsynchronized.ref false;
    1.73  
    1.74  (*For creating output sequence*)
    1.75  fun some_of_list []     = NONE
    1.76 @@ -273,7 +273,7 @@
    1.77  fun some_of_list []     = NONE
    1.78    | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
    1.79  
    1.80 -val trace_ASTAR = ref false;
    1.81 +val trace_ASTAR = Unsynchronized.ref false;
    1.82  
    1.83  fun THEN_ASTAR tac0 (satp, costf) tac1 =
    1.84    let val tf = tracify trace_ASTAR tac1;