5 *) |
5 *) |
6 |
6 |
7 signature BASIC_GOAL = |
7 signature BASIC_GOAL = |
8 sig |
8 sig |
9 val parallel_proofs: int Unsynchronized.ref |
9 val parallel_proofs: int Unsynchronized.ref |
|
10 val parallel_proofs_threshold: int Unsynchronized.ref |
10 val SELECT_GOAL: tactic -> int -> tactic |
11 val SELECT_GOAL: tactic -> int -> tactic |
11 val CONJUNCTS: tactic -> int -> tactic |
12 val CONJUNCTS: tactic -> int -> tactic |
12 val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic |
13 val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic |
13 val PARALLEL_CHOICE: tactic list -> tactic |
14 val PARALLEL_CHOICE: tactic list -> tactic |
14 val PARALLEL_GOALS: tactic -> tactic |
15 val PARALLEL_GOALS: tactic -> tactic |
103 #> Raw_Simplifier.norm_hhf_protect |
104 #> Raw_Simplifier.norm_hhf_protect |
104 #> Thm.strip_shyps |
105 #> Thm.strip_shyps |
105 #> Drule.zero_var_indexes; |
106 #> Drule.zero_var_indexes; |
106 |
107 |
107 |
108 |
108 (* parallel proofs *) |
109 (* forked proofs *) |
|
110 |
|
111 val forked_proofs = Synchronized.var "forked_proofs" 0; |
|
112 |
|
113 fun forked i = |
|
114 Synchronized.change forked_proofs (fn m => |
|
115 let |
|
116 val n = m + i; |
|
117 val _ = |
|
118 Multithreading.tracing 1 (fn () => |
|
119 ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n)); |
|
120 in n end); |
109 |
121 |
110 fun fork_name name e = |
122 fun fork_name name e = |
111 singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1}) |
123 uninterruptible (fn _ => fn () => |
112 (fn () => Future.status e); |
124 let |
|
125 val _ = forked 1; |
|
126 val future = |
|
127 singleton (Future.forks {name = name, group = NONE, deps = [], pri = ~1}) |
|
128 (fn () => |
|
129 (*interruptible*) |
|
130 Exn.release |
|
131 (Exn.capture Future.status e before forked ~1 |
|
132 handle exn => (forked ~1; reraise exn))); |
|
133 in future end) (); |
113 |
134 |
114 fun fork e = fork_name "Goal.fork" e; |
135 fun fork e = fork_name "Goal.fork" e; |
115 |
136 |
116 |
137 |
|
138 (* scheduling parameters *) |
|
139 |
117 val parallel_proofs = Unsynchronized.ref 1; |
140 val parallel_proofs = Unsynchronized.ref 1; |
|
141 val parallel_proofs_threshold = Unsynchronized.ref 100; |
118 |
142 |
119 fun future_enabled () = |
143 fun future_enabled () = |
120 Multithreading.enabled () andalso is_some (Future.worker_task ()) andalso ! parallel_proofs >= 1; |
144 Multithreading.enabled () andalso ! parallel_proofs >= 1 andalso |
121 |
145 is_some (Future.worker_task ()); |
122 fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2; |
146 |
|
147 fun local_future_enabled () = |
|
148 future_enabled () andalso ! parallel_proofs >= 2 andalso |
|
149 Synchronized.value forked_proofs < ! parallel_proofs_threshold; |
123 |
150 |
124 |
151 |
125 (* future_result *) |
152 (* future_result *) |
126 |
153 |
127 fun future_result ctxt result prop = |
154 fun future_result ctxt result prop = |