--- 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 \
--- 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 @@
\<Inter> code: 0x0022c2 font: Isabelle abbrev: Inter
\<union> code: 0x00222a font: Isabelle abbrev: Un
\<Union> code: 0x0022c3 font: Isabelle abbrev: Union
-\<squnion> code: 0x002294 font: Isabelle abbrev: ||
+\<squnion> code: 0x002294 font: Isabelle abbrev: |_|
\<Squnion> code: 0x002a06 font: Isabelle abbrev: |||
\<sqinter> code: 0x002293 font: Isabelle abbrev: &&
\<Sqinter> code: 0x002a05 font: Isabelle abbrev: &&&
--- 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. *)
--- 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
--- 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
--- 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;
--- 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;
--- 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;
+
--- 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 ())));
--- 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;