# HG changeset patch # User haftmann # Date 1256273630 -7200 # Node ID c6693f51e4e4fbec1435d6cdab65895ea61cf036 # Parent e6eda76ad49e4d84cb990d5d08848c65221e4b3b# Parent f654dafa021e110dfeed0967009034f69ddf740b merged diff -r f654dafa021e -r c6693f51e4e4 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Thu Oct 22 16:50:24 2009 +0200 +++ b/Admin/isatest/isatest-stats Fri Oct 23 06:53:50 2009 +0200 @@ -18,7 +18,7 @@ HOL-Decision_Procs \ HOL-Extraction \ HOL-Hoare \ - HOL-HoareParallel \ + HOL-Hoare_Parallel \ HOL-Lambda \ HOL-Library \ HOL-Metis_Examples \ diff -r f654dafa021e -r c6693f51e4e4 etc/symbols --- a/etc/symbols Thu Oct 22 16:50:24 2009 +0200 +++ b/etc/symbols Fri Oct 23 06:53:50 2009 +0200 @@ -244,7 +244,7 @@ \ code: 0x0022c2 font: Isabelle abbrev: Inter \ code: 0x00222a font: Isabelle abbrev: Un \ code: 0x0022c3 font: Isabelle abbrev: Union -\ code: 0x002294 font: Isabelle abbrev: || +\ code: 0x002294 font: Isabelle abbrev: |_| \ code: 0x002a06 font: Isabelle abbrev: ||| \ code: 0x002293 font: Isabelle abbrev: && \ code: 0x002a05 font: Isabelle abbrev: &&& diff -r f654dafa021e -r c6693f51e4e4 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Oct 23 06:53:50 2009 +0200 @@ -537,8 +537,8 @@ fun token s = Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ") val numeral = Scan.one isnum - val decimalint = Scan.bulk numeral >> (rat_of_string o implode) - val decimalfrac = Scan.bulk numeral + val decimalint = Scan.repeat numeral >> (rat_of_string o implode) + val decimalfrac = Scan.repeat numeral >> (fn s => rat_of_string(implode s) // pow10 (length s)) val decimalsig = decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac) @@ -564,7 +564,9 @@ (* Parse back csdp output. *) fun ignore inp = ((),[]) - fun csdpoutput inp = ((decimal -- Scan.bulk (Scan.$$ " " |-- Scan.option decimal) >> (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp + fun csdpoutput inp = + ((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >> + (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp val parse_csdpoutput = mkparser csdpoutput (* Run prover on a problem in linear form. *) diff -r f654dafa021e -r c6693f51e4e4 src/HOLCF/Universal.thy --- a/src/HOLCF/Universal.thy Thu Oct 22 16:50:24 2009 +0200 +++ b/src/HOLCF/Universal.thy Fri Oct 23 06:53:50 2009 +0200 @@ -805,7 +805,7 @@ lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x" unfolding basis_prj_def - apply (subst f_inv_onto_f [where f=basis_emb]) + apply (subst f_inv_into_f [where f=basis_emb]) apply (rule ubasis_until) apply (rule range_eqI [where x=compact_bot]) apply simp diff -r f654dafa021e -r c6693f51e4e4 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Fri Oct 23 06:53:50 2009 +0200 @@ -153,9 +153,7 @@ Exn.capture (fn () => Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) () else Exn.Exn Exn.Interrupt; - val _ = Synchronized.change result - (fn NONE => SOME res - | SOME _ => raise Fail "Duplicate assignment of future value"); + val _ = Synchronized.assign result (K (SOME res)); in (case res of Exn.Exn exn => (Task_Queue.cancel_group group exn; false) @@ -349,8 +347,7 @@ | SOME res => res); fun join_wait x = - Synchronized.guarded_access (result_of x) - (fn NONE => NONE | some => SOME ((), some)); + Synchronized.readonly_access (result_of x) (fn NONE => NONE | SOME _ => SOME ()); fun join_next deps = (*requires SYNCHRONIZED*) if null deps then NONE diff -r f654dafa021e -r c6693f51e4e4 src/Pure/Concurrent/synchronized.ML --- a/src/Pure/Concurrent/synchronized.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/Pure/Concurrent/synchronized.ML Fri Oct 23 06:53:50 2009 +0200 @@ -11,8 +11,10 @@ val value: 'a var -> 'a val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b + val readonly_access: 'a var -> ('a -> 'b option) -> 'b val change_result: 'a var -> ('a -> 'b * 'a) -> 'b val change: 'a var -> ('a -> 'a) -> unit + val assign: 'a var -> ('a -> 'a) -> unit end; structure Synchronized: SYNCHRONIZED = @@ -37,29 +39,48 @@ (* synchronized access *) -fun timed_access (Var {name, lock, cond, var}) time_limit f = +fun access {time_limit, readonly, finish} (Var {name, lock, cond, var}) f = SimpleThread.synchronized name lock (fn () => let fun try_change () = let val x = ! var in (case f x of - SOME (y, x') => (var := x'; SOME y) - | NONE => + NONE => (case Multithreading.sync_wait NONE (time_limit x) cond lock of Exn.Result true => try_change () | Exn.Result false => NONE - | Exn.Exn exn => reraise exn)) + | Exn.Exn exn => reraise exn) + | SOME (y, x') => + if readonly then SOME y + else + let + val _ = magic_immutability_test var + andalso raise Fail ("Attempt to change finished variable " ^ quote name); + val _ = var := x'; + val _ = if finish then magic_immutability_mark var else (); + in SOME y end) end; val res = try_change (); val _ = ConditionVar.broadcast cond; in res end); +fun timed_access var time_limit f = + access {time_limit = time_limit, readonly = false, finish = false} var f; + fun guarded_access var f = the (timed_access var (K NONE) f); +fun readonly_access var f = + the (access {time_limit = K NONE, readonly = true, finish = false} var + (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x)))); + (* unconditional change *) fun change_result var f = guarded_access var (SOME o f); fun change var f = change_result var (fn x => ((), f x)); +fun assign var f = + the (access {time_limit = K NONE, readonly = false, finish = true} var + (fn x => SOME ((), f x))); + end; diff -r f654dafa021e -r c6693f51e4e4 src/Pure/Concurrent/synchronized_sequential.ML --- a/src/Pure/Concurrent/synchronized_sequential.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/Pure/Concurrent/synchronized_sequential.ML Fri Oct 23 06:53:50 2009 +0200 @@ -20,8 +20,13 @@ fun guarded_access var f = the (timed_access var (K NONE) f); +fun readonly_access var f = + guarded_access var (fn x => (case f x of NONE => NONE | SOME y => SOME (y, x))); + fun change_result var f = guarded_access var (SOME o f); fun change var f = change_result var (fn x => ((), f x)); +val assign = change; + end; end; diff -r f654dafa021e -r c6693f51e4e4 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Fri Oct 23 06:53:50 2009 +0200 @@ -128,3 +128,12 @@ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; in Exn.release res end; + +(* magic immutability -- for internal use only! *) + +fun magic_immutability_mark (r: 'a Unsynchronized.ref) = + ignore (RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r); + +fun magic_immutability_test (r: 'a Unsynchronized.ref) = + Word8.andb (0wx40, RunCall.run_call1 RuntimeCalls.POLY_SYS_get_flags r) = 0w0; + diff -r f654dafa021e -r c6693f51e4e4 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Fri Oct 23 06:53:50 2009 +0200 @@ -66,6 +66,10 @@ (Control.primaryPrompt := p1; Control.secondaryPrompt := p2); (*dummy implementation*) +fun magic_immutability_test _ = false; +fun magic_immutability_mark _ = (); + +(*dummy implementation*) fun profile (n: int) f x = f x; (*dummy implementation*) @@ -177,8 +181,6 @@ val system_out = (fn (output, rc) => (output, mk_int rc)) o system_out; - -(*Convert a process ID to a decimal string (chiefly for tracing)*) fun process_id pid = Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ()))); diff -r f654dafa021e -r c6693f51e4e4 src/Pure/library.ML --- a/src/Pure/library.ML Thu Oct 22 16:50:24 2009 +0200 +++ b/src/Pure/library.ML Fri Oct 23 06:53:50 2009 +0200 @@ -466,7 +466,7 @@ fun map_range f i = let - fun mapp k = + fun mapp (k: int) = if k < i then f k :: mapp (k + 1) else []; in mapp 0 end;