src/Tools/Compute_Oracle/am_interpreter.ML
changeset 32740 9dd0a2f83429
parent 31971 8c1b845ed105
child 32960 69916a850301
     1.1 --- a/src/Tools/Compute_Oracle/am_interpreter.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  signature AM_BARRAS = 
     1.5  sig
     1.6    include ABSTRACT_MACHINE
     1.7 -  val max_reductions : int option ref
     1.8 +  val max_reductions : int option Unsynchronized.ref
     1.9  end
    1.10  
    1.11  structure AM_Interpreter : AM_BARRAS = struct
    1.12 @@ -129,12 +129,12 @@
    1.13  fun cont (Continue _) = true
    1.14    | cont _ = false
    1.15  
    1.16 -val max_reductions = ref (NONE : int option)
    1.17 +val max_reductions = Unsynchronized.ref (NONE : int option)
    1.18  
    1.19  fun do_reduction reduce p =
    1.20      let
    1.21 -	val s = ref (Continue p)
    1.22 -	val counter = ref 0
    1.23 +	val s = Unsynchronized.ref (Continue p)
    1.24 +	val counter = Unsynchronized.ref 0
    1.25  	val _ = case !max_reductions of 
    1.26  		    NONE => while cont (!s) do (s := reduce (proj_C (!s)))
    1.27  		  | SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1)