tuned signature;
authorwenzelm
Mon Jan 31 23:02:53 2011 +0100 (2011-01-31)
changeset 416747da257539a8d
parent 41673 1c191a39549f
child 41675 0f0f6212d6c6
tuned signature;
tuned vacous forks;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/goal.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Mon Jan 31 22:57:01 2011 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Mon Jan 31 23:02:53 2011 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4    val group_of: 'a future -> group
     1.5    val peek: 'a future -> 'a Exn.result option
     1.6    val is_finished: 'a future -> bool
     1.7 -  val bulk: {name: string, group: group option, deps: task list, pri: int} ->
     1.8 +  val forks: {name: string, group: group option, deps: task list, pri: int} ->
     1.9      (unit -> 'a) list -> 'a future list
    1.10    val fork_pri: int -> (unit -> 'a) -> 'a future
    1.11    val fork: (unit -> 'a) -> 'a future
    1.12 @@ -400,31 +400,33 @@
    1.13  
    1.14  (* fork *)
    1.15  
    1.16 -fun bulk {name, group, deps, pri} es =
    1.17 -  let
    1.18 -    val grp =
    1.19 -      (case group of
    1.20 -        NONE => worker_subgroup ()
    1.21 -      | SOME grp => grp);
    1.22 -    fun enqueue e (minimal, queue) =
    1.23 -      let
    1.24 -        val (result, job) = future_job grp e;
    1.25 -        val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
    1.26 -        val future = Future {promised = false, task = task, group = grp, result = result};
    1.27 -      in (future, (minimal orelse minimal', queue')) end;
    1.28 -  in
    1.29 -    SYNCHRONIZED "enqueue" (fn () =>
    1.30 -      let
    1.31 -        val (futures, minimal) =
    1.32 -          Unsynchronized.change_result queue (fn q =>
    1.33 -            let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
    1.34 -            in ((futures, minimal), q') end);
    1.35 -        val _ = if minimal then signal work_available else ();
    1.36 -        val _ = scheduler_check ();
    1.37 -      in futures end)
    1.38 -  end;
    1.39 +fun forks {name, group, deps, pri} es =
    1.40 +  if null es then []
    1.41 +  else
    1.42 +    let
    1.43 +      val grp =
    1.44 +        (case group of
    1.45 +          NONE => worker_subgroup ()
    1.46 +        | SOME grp => grp);
    1.47 +      fun enqueue e (minimal, queue) =
    1.48 +        let
    1.49 +          val (result, job) = future_job grp e;
    1.50 +          val ((task, minimal'), queue') = Task_Queue.enqueue name grp deps pri job queue;
    1.51 +          val future = Future {promised = false, task = task, group = grp, result = result};
    1.52 +        in (future, (minimal orelse minimal', queue')) end;
    1.53 +    in
    1.54 +      SYNCHRONIZED "enqueue" (fn () =>
    1.55 +        let
    1.56 +          val (futures, minimal) =
    1.57 +            Unsynchronized.change_result queue (fn q =>
    1.58 +              let val (futures, (minimal, q')) = fold_map enqueue es (false, q)
    1.59 +              in ((futures, minimal), q') end);
    1.60 +          val _ = if minimal then signal work_available else ();
    1.61 +          val _ = scheduler_check ();
    1.62 +        in futures end)
    1.63 +    end;
    1.64  
    1.65 -fun fork_pri pri e = singleton (bulk {name = "", group = NONE, deps = [], pri = pri}) e;
    1.66 +fun fork_pri pri e = singleton (forks {name = "", group = NONE, deps = [], pri = pri}) e;
    1.67  fun fork e = fork_pri 0 e;
    1.68  
    1.69  
    1.70 @@ -501,7 +503,7 @@
    1.71      if extended then Future {promised = false, task = task, group = group, result = result}
    1.72      else
    1.73        singleton
    1.74 -        (bulk {name = "Future.map", group = SOME group,
    1.75 +        (forks {name = "Future.map", group = SOME group,
    1.76            deps = [task], pri = Task_Queue.pri_of_task task})
    1.77          (fn () => f (join x))
    1.78    end;
     2.1 --- a/src/Pure/Concurrent/par_list.ML	Mon Jan 31 22:57:01 2011 +0100
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Mon Jan 31 23:02:53 2011 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4      let
     2.5        val group = Task_Queue.new_group (Future.worker_group ());
     2.6        val futures =
     2.7 -        Future.bulk {name = name, group = SOME group, deps = [], pri = 0}
     2.8 +        Future.forks {name = name, group = SOME group, deps = [], pri = 0}
     2.9            (map (fn x => fn () => f x) xs);
    2.10        val results = Future.join_results futures
    2.11          handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
     3.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jan 31 22:57:01 2011 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jan 31 23:02:53 2011 +0100
     3.3 @@ -664,7 +664,7 @@
     3.4          val future_proof = Proof.global_future_proof
     3.5            (fn prf =>
     3.6              singleton
     3.7 -              (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
     3.8 +              (Future.forks {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
     3.9                (fn () =>
    3.10                  let val (states, result_state) =
    3.11                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
     4.1 --- a/src/Pure/PIDE/document.ML	Mon Jan 31 22:57:01 2011 +0100
     4.2 +++ b/src/Pure/PIDE/document.ML	Mon Jan 31 23:02:53 2011 +0100
     4.3 @@ -209,7 +209,7 @@
     4.4  fun async_state tr st =
     4.5    ignore
     4.6      (singleton
     4.7 -      (Future.bulk {name = "Document.async_state",
     4.8 +      (Future.forks {name = "Document.async_state",
     4.9          group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
    4.10        (fn () =>
    4.11          Toplevel.setmp_thread_position tr
    4.12 @@ -339,7 +339,7 @@
    4.13        val _ = cancel state;
    4.14  
    4.15        val execution' = (* FIXME proper node deps *)
    4.16 -        Future.bulk {name = "Document.execute", group = NONE, deps = [], pri = 1}
    4.17 +        Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
    4.18            [fn () =>
    4.19              let
    4.20                val _ = await_cancellation state;
     5.1 --- a/src/Pure/Thy/thy_info.ML	Mon Jan 31 22:57:01 2011 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Jan 31 23:02:53 2011 +0100
     5.3 @@ -187,7 +187,7 @@
     5.4  
     5.5              val future =
     5.6                singleton
     5.7 -                (Future.bulk {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
     5.8 +                (Future.forks {name = "theory " ^ name, group = NONE, deps = task_deps, pri = 0})
     5.9                  (fn () =>
    5.10                    (case map_filter failed deps of
    5.11                      [] => body (map (#1 o Future.join o get) parents)
     6.1 --- a/src/Pure/goal.ML	Mon Jan 31 22:57:01 2011 +0100
     6.2 +++ b/src/Pure/goal.ML	Mon Jan 31 23:02:53 2011 +0100
     6.3 @@ -107,7 +107,7 @@
     6.4  (* parallel proofs *)
     6.5  
     6.6  fun fork e =
     6.7 -  singleton (Future.bulk {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
     6.8 +  singleton (Future.forks {name = "Goal.fork", group = NONE, deps = [], pri = ~1})
     6.9      (fn () => Future.status e);
    6.10  
    6.11  val parallel_proofs = Unsynchronized.ref 1;
     7.1 --- a/src/Pure/proofterm.ML	Mon Jan 31 22:57:01 2011 +0100
     7.2 +++ b/src/Pure/proofterm.ML	Mon Jan 31 23:02:53 2011 +0100
     7.3 @@ -1390,7 +1390,7 @@
     7.4        else Future.map postproc body
     7.5    | fulfill_proof_future thy promises postproc body =
     7.6        singleton
     7.7 -        (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
     7.8 +        (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
     7.9              deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
    7.10          (fn () =>
    7.11            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    7.12 @@ -1448,7 +1448,7 @@
    7.13        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    7.14        else
    7.15          singleton
    7.16 -          (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
    7.17 +          (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
    7.18            (make_body0 o full_proof0);
    7.19  
    7.20      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);