# HG changeset patch
# User wenzelm
# Date 1254416366 -7200
# Node ID 2729c803332628a86e0b845031fb3f2ce61be650
# Parent  f7f94bb9ac94ede031834800d77f09b8974afd9b# Parent  4ed308181f7fb44bfa2273859ffffc7c2a652f40
merged

diff -r f7f94bb9ac94 -r 2729c8033326 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/HOL/IsaMakefile	Thu Oct 01 18:59:26 2009 +0200
@@ -192,6 +192,7 @@
   Tools/sat_funcs.ML \
   Tools/sat_solver.ML \
   Tools/split_rule.ML \
+  Tools/transfer.ML \
   Tools/typecopy.ML \
   Tools/typedef_codegen.ML \
   Tools/typedef.ML \
@@ -258,12 +259,12 @@
   Tools/Qelim/presburger.ML \
   Tools/Qelim/qelim.ML \
   Tools/recdef.ML \
+  Tools/choice_specification.ML \
   Tools/res_atp.ML \
   Tools/res_axioms.ML \
   Tools/res_clause.ML \
   Tools/res_hol_clause.ML \
   Tools/res_reconstruct.ML \
-  Tools/choice_specification.ML \
   Tools/string_code.ML \
   Tools/string_syntax.ML \
   Tools/TFL/casesplit.ML \
@@ -308,7 +309,6 @@
   Taylor.thy \
   Transcendental.thy \
   Tools/float_syntax.ML \
-  Tools/transfer.ML \
   Tools/Qelim/ferrante_rackoff_data.ML \
   Tools/Qelim/ferrante_rackoff.ML \
   Tools/Qelim/langford_data.ML \
diff -r f7f94bb9ac94 -r 2729c8033326 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/HOL/Tools/transfer.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -1,5 +1,5 @@
 (*  Author:     Amine Chaieb, University of Cambridge, 2009
-                Jeremy Avigad, Carnegie Mellon University
+    Author:     Jeremy Avigad, Carnegie Mellon University
 *)
 
 signature TRANSFER =
@@ -14,10 +14,8 @@
 structure Transfer : TRANSFER =
 struct
 
-val eq_thm = Thm.eq_thm;
-
 type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
-  guess : bool, hints : string list}; 
+  guess : bool, hints : string list};
 type data = simpset * (thm * entry) list;
 
 structure Data = GenericDataFun
@@ -26,36 +24,34 @@
   val empty = (HOL_ss, []);
   val extend  = I;
   fun merge _ ((ss1, e1), (ss2, e2)) =
-    (merge_ss (ss1, ss2), AList.merge eq_thm (K true) (e1, e2));
+    (merge_ss (ss1, ss2), AList.merge Thm.eq_thm (K true) (e1, e2));
 );
 
 val get = Data.get o Context.Proof;
 
-fun del_data key = apsnd (remove (eq_fst eq_thm) (key, []));
+fun del_data key = apsnd (remove (eq_fst Thm.eq_thm) (key, []));
 
 val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute 
+val add_ss = Thm.declaration_attribute
    (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
 
-val del_ss = Thm.declaration_attribute 
+val del_ss = Thm.declaration_attribute
    (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
 
 val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
 
 fun merge_update eq m (k,v) [] = [(k,v)]
-  | merge_update eq m (k,v) ((k',v')::al) = 
+  | merge_update eq m (k,v) ((k',v')::al) =
            if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
 
-fun C f x y = f y x
-
-fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} = 
+fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
  HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
 
-fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th = 
- let 
+fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
+ let
   val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
-  val (aT,bT) = 
-     let val T = typ_of (ctyp_of_term a) 
+  val (aT,bT) =
+     let val T = typ_of (ctyp_of_term a)
      in (Term.range_type T, Term.domain_type T)
      end
   val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
@@ -65,60 +61,64 @@
   val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
   val cis = map (Thm.capply a) cfis
   val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
-  val th1 = Drule.cterm_instantiate (cns~~ cis) th
-  val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
-  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e)) 
+  val th1 = Drule.cterm_instantiate (cns ~~ cis) th
+  val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1)
+  val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
                                          (fold_rev implies_intr (map cprop_of hs) th2)
 in hd (Variable.export ctxt''' ctxt0 [th3]) end;
 
 local
-fun transfer_ruleh a D leave ctxt th = 
+fun transfer_ruleh a D leave ctxt th =
  let val (ss,al) = get ctxt
      val a0 = cterm_of (ProofContext.theory_of ctxt) a
      val D0 = cterm_of (ProofContext.theory_of ctxt) D
-     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th' 
+     fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
                  in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
                  end
  in case get_first h al of
       SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
     | NONE => error "Transfer: corresponding instance not found in context-data"
  end
-in fun transfer_rule (a,D) leave (gctxt,th) = 
+in fun transfer_rule (a,D) leave (gctxt,th) =
    (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
 end;
 
 fun  splits P [] = []
-   | splits P (xxs as (x::xs)) = 
+   | splits P (xxs as (x::xs)) =
     let val pss = filter (P x) xxs
         val qss = filter_out (P x) xxs
     in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
     end
 
-fun all_transfers leave (gctxt,th) = 
- let 
+fun all_transfers leave (gctxt,th) =
+ let
   val ctxt = Context.proof_of gctxt
   val tys = map snd (Term.add_vars (prop_of th) [])
   val _ = if null tys then error "transfer: Unable to guess instance" else ()
-  val tyss = splits (curry Type.could_unify) tys 
+  val tyss = splits (curry Type.could_unify) tys
   val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
   val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
-  val insts = 
-    map_filter (fn tys => 
-          get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k)) 
-                                  then SOME (get_aD k, ss) 
-                                  else NONE) (snd (get ctxt))) tyss
-  val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
+  val insts =
+    map_filter (fn tys =>
+      get_first (fn (k,ss) =>
+        if Type.could_unify (hd tys, range_type (get_ty k))
+        then SOME (get_aD k, ss)
+        else NONE) (snd (get ctxt))) tyss
+  val _ =
+    if null insts then
+      error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction"
+    else ()
   val ths = map  (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
   val cth = Conjunction.intr_balanced ths
  in (gctxt, cth)
  end;
 
-fun transfer_rule_by_hint ls leave (gctxt,th) = 
- let 
+fun transfer_rule_by_hint ls leave (gctxt,th) =
+ let
   val ctxt = Context.proof_of gctxt
   val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
-  val insts = 
-    map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls 
+  val insts =
+    map_filter (fn (k,e) => if exists (member (op =) (#hints e)) ls
           then SOME (get_aD k, e) else NONE)
         (snd (get ctxt))
   val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
@@ -128,53 +128,58 @@
  end;
 
 
-fun transferred_attribute ls NONE leave = 
+fun transferred_attribute ls NONE leave =
          if null ls then all_transfers leave else transfer_rule_by_hint ls leave
   | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
 
-                                                    (* Add data to the context *)
+
+(* Add data to the context *)
+
 fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
-                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
+                      ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
                        {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
- = 
+ =
  let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
- {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2, 
+ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
   ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
-  hints = subtract (op = : string*string -> bool) hints0 
+  hints = subtract (op = : string*string -> bool) hints0
             (hints1 union_string hints2)}
  end;
 
 local
  val h = curry (merge Thm.eq_thm)
 in
-fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1}, 
-                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) = 
+fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+                   {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
     {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
-end; 
+end;
 
 fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
   Thm.declaration_attribute (fn key => fn context => context |> Data.map
-   (fn (ss, al) => 
+   (fn (ss, al) =>
      let
-      val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key) 
-                in 0 end) 
-                handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
+      val _ = Thm.match (transM_pat, Thm.dest_arg (Thm.cprop_of key))
+        handle Pattern.MATCH =>
+          error "Attribute expected Theorem of the form : TransferMorphism A a B b"
       val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
       val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
-      val entry = 
-        if g then 
+      val entry =
+        if g then
          let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
              val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
-             val inj' = if null inja then #inj (case AList.lookup eq_thm al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual") 
-                        else inja
+             val inj' =
+               if null inja then
+                #inj
+                  (case AList.lookup Thm.eq_thm al key of SOME e => e
+                  | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
+               else inja
              val ret' = merge Thm.eq_thm (reta,  map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
-         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end 
+         in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
         else e0
-    in (ss, merge_update eq_thm (gen_merge_entries ed) (key, entry) al)
+    in (ss, merge_update Thm.eq_thm (gen_merge_entries ed) (key, entry) al)
     end));
 
 
-
 (* concrete syntax *)
 
 local
@@ -199,7 +204,7 @@
 
 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
 val terms = thms >> map Drule.dest_term
-val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd) 
+val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
 val name = Scan.lift Args.name
 val names = Scan.repeat (Scan.unless any_keyword name)
 fun optional scan = Scan.optional scan []
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -30,6 +30,7 @@
   type task = Task_Queue.task
   type group = Task_Queue.group
   val is_worker: unit -> bool
+  val worker_task: unit -> Task_Queue.task option
   val worker_group: unit -> Task_Queue.group option
   type 'a future
   val task_of: 'a future -> task
@@ -71,6 +72,7 @@
 end;
 
 val is_worker = is_some o thread_data;
+val worker_task = Option.map #2 o thread_data;
 val worker_group = Option.map #3 o thread_data;
 
 
@@ -347,7 +349,8 @@
   | SOME res => res);
 
 fun join_wait x =
-  Synchronized.guarded_access (result_of x) (fn NONE => NONE | some => SOME ((), some));
+  Synchronized.guarded_access (result_of x)
+    (fn NONE => NONE | some => SOME ((), some));
 
 fun join_next deps = (*requires SYNCHRONIZED*)
   if null deps then NONE
@@ -357,10 +360,14 @@
     | (NONE, deps') => (worker_wait work_finished; join_next deps')
     | (SOME work, deps') => SOME (work, deps'));
 
-fun join_work deps =
-  (case SYNCHRONIZED "join" (fn () => join_next deps) of
-    NONE => ()
-  | SOME (work, deps') => (execute "join" work; join_work deps'));
+fun execute_work NONE = ()
+  | execute_work (SOME (work, deps')) = (execute "join" work; join_work deps')
+and join_work deps =
+  execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
+
+fun join_depend task deps =
+  execute_work (SYNCHRONIZED "join" (fn () =>
+    (Unsynchronized.change queue (Task_Queue.depend task deps); join_next deps)));
 
 in
 
@@ -368,11 +375,11 @@
   if forall is_finished xs then map get_result xs
   else if Multithreading.self_critical () then
     error "Cannot join future values within critical section"
-  else uninterruptible (fn _ => fn () =>
-     (if is_worker ()
-      then join_work (map task_of xs)
-      else List.app join_wait xs;
-      map get_result xs)) ();
+  else
+    (case worker_task () of
+      SOME task => join_depend task (map task_of xs)
+    | NONE => List.app join_wait xs;
+    map get_result xs);
 
 end;
 
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/lazy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Pure/Concurrent/lazy.ML
+    Author:     Makarius
+
+Lazy evaluation based on futures.
+*)
+
+signature LAZY =
+sig
+  type 'a lazy
+  val peek: 'a lazy -> 'a Exn.result option
+  val lazy: (unit -> 'a) -> 'a lazy
+  val value: 'a -> 'a lazy
+  val force_result: 'a lazy -> 'a Exn.result
+  val force: 'a lazy -> 'a
+  val map_force: ('a -> 'b) -> 'a lazy -> 'b lazy
+end;
+
+structure Lazy: LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Future of 'a future;
+
+abstype 'a lazy = Lazy of 'a expr Synchronized.var
+with
+
+fun peek (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => NONE
+  | Future x => Future.peek x);
+
+fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
+
+
+(* force result *)
+
+fun force_result (Lazy var) =
+  (case peek (Lazy var) of
+    SOME res => res
+  | NONE =>
+      Synchronized.guarded_access var
+        (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end
+          | Future x => SOME (x, Future x))
+      |> Future.join_result);
+
+fun force r = Exn.release (force_result r);
+
+fun map_force f = value o f o force;
+
+end;
+end;
+
+type 'a lazy = 'a Lazy.lazy;
+
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/lazy_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,43 @@
+(*  Title:      Pure/Concurrent/lazy_sequential.ML
+    Author:     Florian Haftmann and Makarius, TU Muenchen
+
+Lazy evaluation with memoing (sequential version).
+*)
+
+structure Lazy: LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Result of 'a Exn.result;
+
+abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
+with
+
+fun peek (Lazy r) =
+  (case ! r of
+    Expr _ => NONE
+  | Result x => SOME x);
+
+fun lazy e = Lazy (Unsynchronized.ref (Expr e));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
+
+
+(* force result *)
+
+fun force_result (Lazy r) =
+  (case ! r of
+    Expr e => Exn.capture e ()
+  | Result res => res);
+
+fun force r = Exn.release (force_result r);
+
+fun map_force f = value o f o force;
+
+end;
+end;
+
+type 'a lazy = 'a Lazy.lazy;
+
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/par_list_dummy.ML
--- a/src/Pure/Concurrent/par_list_dummy.ML	Thu Oct 01 18:58:47 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/Concurrent/par_list_dummy.ML
-    Author:     Makarius
-
-Dummy version of parallel list combinators -- plain sequential evaluation.
-*)
-
-structure Par_List: PAR_LIST =
-struct
-
-val map = map;
-val get_some = get_first;
-val find_some = find_first;
-val exists = exists;
-val forall = forall;
-
-end;
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/par_list_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_list_sequential.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/Concurrent/par_list_sequential.ML
+    Author:     Makarius
+
+Dummy version of parallel list combinators -- plain sequential evaluation.
+*)
+
+structure Par_List: PAR_LIST =
+struct
+
+val map = map;
+val get_some = get_first;
+val find_some = find_first;
+val exists = exists;
+val forall = forall;
+
+end;
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/synchronized_dummy.ML
--- a/src/Pure/Concurrent/synchronized_dummy.ML	Thu Oct 01 18:58:47 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      Pure/Concurrent/synchronized_dummy.ML
-    Author:     Makarius
-
-Dummy version of state variables -- plain refs for sequential access.
-*)
-
-structure Synchronized: SYNCHRONIZED =
-struct
-
-datatype 'a var = Var of 'a Unsynchronized.ref;
-
-fun var _ x = Var (Unsynchronized.ref x);
-fun value (Var var) = ! var;
-
-fun timed_access (Var var) _ f =
-  (case f (! var) of
-    SOME (y, x') => (var := x'; SOME y)
-  | NONE => Thread.unavailable ());
-
-fun guarded_access var f = the (timed_access var (K NONE) f);
-
-fun change_result var f = guarded_access var (SOME o f);
-fun change var f = change_result var (fn x => ((), f x));
-
-end;
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/synchronized_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized_sequential.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,27 @@
+(*  Title:      Pure/Concurrent/synchronized_sequential.ML
+    Author:     Makarius
+
+Sequential version of state variables -- plain refs.
+*)
+
+structure Synchronized: SYNCHRONIZED =
+struct
+
+abstype 'a var = Var of 'a Unsynchronized.ref
+with
+
+fun var _ x = Var (Unsynchronized.ref x);
+fun value (Var var) = ! var;
+
+fun timed_access (Var var) _ f =
+  (case f (! var) of
+    SOME (y, x') => (var := x'; SOME y)
+  | NONE => Thread.unavailable ());
+
+fun guarded_access var f = the (timed_access var (K NONE) f);
+
+fun change_result var f = guarded_access var (SOME o f);
+fun change var f = change_result var (fn x => ((), f x));
+
+end;
+end;
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -27,6 +27,7 @@
   val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
+  val depend: task -> task list -> queue -> queue
   val dequeue_towards: Thread.thread -> task list -> queue ->
     (((task * group * (bool -> bool) list) option * task list) * queue)
   val finish: task -> queue -> bool * queue
@@ -101,6 +102,11 @@
 fun add_job task dep (jobs: jobs) =
   Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
 
+fun add_dep task dep (jobs: jobs) =
+  if Task_Graph.is_edge jobs (task, dep) then
+    raise Fail "Cyclic dependency of future tasks"
+  else add_job task dep jobs;
+
 fun get_deps (jobs: jobs) task =
   Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => [];
 
@@ -205,6 +211,9 @@
 
 (* dequeue_towards -- adhoc dependencies *)
 
+fun depend task deps (Queue {groups, jobs, ...}) =
+  make_queue groups (fold (add_dep task) deps jobs) Unknown;
+
 fun dequeue_towards thread deps (queue as Queue {groups, jobs, ...}) =
   let
     fun ready task =
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/General/lazy.ML
--- a/src/Pure/General/lazy.ML	Thu Oct 01 18:58:47 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(*  Title:      Pure/General/lazy.ML
-    Author:     Florian Haftmann and Makarius, TU Muenchen
-
-Lazy evaluation with memoing.  Concurrency may lead to multiple
-attempts of evaluation -- the first result persists.
-*)
-
-signature LAZY =
-sig
-  type 'a lazy
-  val same: 'a lazy * 'a lazy -> bool
-  val lazy: (unit -> 'a) -> 'a lazy
-  val value: 'a -> 'a lazy
-  val peek: 'a lazy -> 'a Exn.result option
-  val force_result: 'a lazy -> 'a Exn.result
-  val force: 'a lazy -> 'a
-  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
-end
-
-structure Lazy :> LAZY =
-struct
-
-(* datatype *)
-
-datatype 'a T =
-  Lazy of unit -> 'a |
-  Result of 'a Exn.result;
-
-type 'a lazy = 'a T Unsynchronized.ref;
-
-fun same (r1: 'a lazy, r2) = r1 = r2;
-
-fun lazy e = Unsynchronized.ref (Lazy e);
-fun value x = Unsynchronized.ref (Result (Exn.Result x));
-
-fun peek r =
-  (case ! r of
-    Lazy _ => NONE
-  | Result res => SOME res);
-
-
-(* force result *)
-
-fun force_result r =
-  let
-    (*potentially concurrent evaluation*)
-    val res =
-      (case ! r of
-        Lazy e => Exn.capture e ()
-      | Result res => res);
-    (*assign result -- first one persists*)
-    val res' = NAMED_CRITICAL "lazy" (fn () =>
-      (case ! r of
-        Lazy _ => (r := Result res; res)
-      | Result res' => res'));
-  in res' end;
-
-fun force r = Exn.release (force_result r);
-
-fun map_force f = value o f o force;
-
-end;
-
-type 'a lazy = 'a Lazy.lazy;
-
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/IsaMakefile	Thu Oct 01 18:59:26 2009 +0200
@@ -43,18 +43,19 @@
 Pure: $(OUT)/Pure
 
 $(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML			\
+  Concurrent/lazy.ML Concurrent/lazy_sequential.ML			\
   Concurrent/mailbox.ML Concurrent/par_list.ML				\
-  Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
-  Concurrent/synchronized.ML Concurrent/synchronized_dummy.ML		\
+  Concurrent/par_list_sequential.ML Concurrent/simple_thread.ML		\
+  Concurrent/synchronized.ML Concurrent/synchronized_sequential.ML	\
   Concurrent/task_queue.ML General/alist.ML General/antiquote.ML	\
   General/balanced_tree.ML General/basics.ML General/binding.ML		\
   General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\
-  General/integer.ML General/lazy.ML General/long_name.ML		\
-  General/markup.ML General/name_space.ML General/ord_list.ML		\
-  General/output.ML General/path.ML General/position.ML			\
-  General/pretty.ML General/print_mode.ML General/properties.ML		\
-  General/queue.ML General/same.ML General/scan.ML General/secure.ML	\
-  General/seq.ML General/source.ML General/stack.ML General/symbol.ML	\
+  General/integer.ML General/long_name.ML General/markup.ML		\
+  General/name_space.ML General/ord_list.ML General/output.ML		\
+  General/path.ML General/position.ML General/pretty.ML			\
+  General/print_mode.ML General/properties.ML General/queue.ML		\
+  General/same.ML General/scan.ML General/secure.ML General/seq.ML	\
+  General/source.ML General/stack.ML General/symbol.ML			\
   General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
   General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
   Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -45,7 +45,6 @@
 use "General/long_name.ML";
 use "General/binding.ML";
 use "General/name_space.ML";
-use "General/lazy.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/buffer.ML";
@@ -58,12 +57,17 @@
 
 use "Concurrent/simple_thread.ML";
 use "Concurrent/synchronized.ML";
-if Multithreading.available then () else use "Concurrent/synchronized_dummy.ML";
+if Multithreading.available then ()
+else use "Concurrent/synchronized_sequential.ML";
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
+use "Concurrent/lazy.ML";
+if Multithreading.available then ()
+else use "Concurrent/lazy_sequential.ML";
 use "Concurrent/par_list.ML";
-if Multithreading.available then () else use "Concurrent/par_list_dummy.ML";
+if Multithreading.available then ()
+else use "Concurrent/par_list_sequential.ML";
 
 
 (* fundamental structures *)
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
+    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -55,9 +55,10 @@
       fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
       |> sort_distinct (string_ord o pairself #1);
 
-    val tab = Proofterm.fold_body_thms
-      (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
-      (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
+    val tab =
+      Proofterm.fold_body_thms
+        (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
+        (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
     fun is_unused (name, th) =
       not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
 
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -364,7 +364,7 @@
 
 local
 
-fun schedule_futures task_graph =
+fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   let
     val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
       (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
@@ -397,7 +397,7 @@
         val _ = after_load ();
       in [] end handle exn => (kill_thy name; [exn]));
 
-  in ignore (Exn.release_all (map Exn.Exn (rev exns))) end;
+  in ignore (Exn.release_all (map Exn.Exn (rev exns))) end) ();
 
 fun schedule_seq tasks =
   Graph.topological_order tasks
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -73,7 +73,7 @@
 
 (* check files *)
 
-fun check_ext exts paths dir src_path =
+fun check_ext exts paths src_path =
   let
     val path = Path.expand src_path;
     val _ = Path.is_current path andalso error "Bad file specification";
@@ -84,15 +84,15 @@
     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
   in get_first try_prfx paths end;
 
-fun check_file dir path = check_ext [] (search_path dir path) dir path;
-fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;
+fun check_file dir path = check_ext [] (search_path dir path) path;
+fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
 
 fun check_thy dir name =
   let
     val thy_file = thy_path name;
     val paths = search_path dir thy_file;
   in
-    (case check_ext [] paths dir thy_file of
+    (case check_ext [] paths thy_file of
       NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
         " in " ^ commas_quote (map Path.implode paths))
     | SOME thy_id => thy_id)
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -40,8 +40,7 @@
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
-  val fold_body_thms: (serial * (string * term * proof_body) -> 'a -> 'a) ->
-    proof_body list -> 'a -> 'a
+  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   val join_bodies: proof_body list -> unit
   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
@@ -110,7 +109,7 @@
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
   val promise_proof: theory -> serial -> term -> proof
-  val fulfill_proof: theory -> serial -> (serial * proof_body) list -> proof_body -> proof_body
+  val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
@@ -182,7 +181,7 @@
           let
             val body' = Future.join body;
             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-          in (f (i, (name, prop, body')) x', seen') end));
+          in (f (name, prop, body') x', seen') end));
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
@@ -1279,16 +1278,12 @@
         | _ => false));
   in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
 
-fun fulfill_proof _ _ [] body0 = body0
-  | fulfill_proof thy id ps body0 =
+fun fulfill_proof _ [] body0 = body0
+  | fulfill_proof thy ps body0 =
       let
         val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
-        val bodies = map snd ps;
-        val _ = fold_body_thms (fn (i, (name, _, _)) => fn () =>
-          if i = id then error ("Cyclic reference to theorem " ^ quote name)
-          else ()) bodies ();
-        val oracles = fold (fn PBody {oracles, ...} => merge_oracles oracles) bodies oracles0;
-        val thms = fold (fn PBody {thms, ...} => merge_thms thms) bodies thms0;
+        val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
         val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
 
         fun fill (Promise (i, prop, Ts)) =
@@ -1300,18 +1295,18 @@
         val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
       in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
-fun fulfill_proof_future _ _ [] body = Future.value body
-  | fulfill_proof_future thy id promises body =
+fun fulfill_proof_future _ [] body = Future.value body
+  | fulfill_proof_future thy promises body =
       Future.fork_deps (map snd promises) (fn () =>
-        fulfill_proof thy id (map (apsnd Future.join) promises) body);
+        fulfill_proof thy (map (apsnd Future.join) promises) body);
 
 
 (***** theorems *****)
 
-fun thm_proof thy name hyps prop promises body =
+fun thm_proof thy name hyps concl promises body =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
-    val prop = Logic.list_implies (hyps, prop);
+    val prop = Logic.list_implies (hyps, concl);
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
@@ -1323,9 +1318,7 @@
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () =
-      let val id = serial ()
-      in (id, name, prop, fulfill_proof_future thy id promises body0) end;
+    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
     val (i, name, prop, body') =
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>
diff -r f7f94bb9ac94 -r 2729c8033326 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/thm.ML	Thu Oct 01 18:59:26 2009 +0200
@@ -540,7 +540,7 @@
 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Pt.fulfill_proof (Theory.deref thy_ref) ~1
+  Pt.fulfill_proof (Theory.deref thy_ref)
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));