author | wenzelm |
Sun, 09 Nov 2014 14:08:00 +0100 | |
changeset 58956 | a816aa3ff391 |
parent 58950 | d07464875dd4 |
child 60372 | b62eaac5c1af |
permissions | -rw-r--r-- |
58009 | 1 |
(* Title: Pure/par_tactical.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Parallel tacticals. |
|
5 |
*) |
|
6 |
||
7 |
signature BASIC_PAR_TACTICAL = |
|
8 |
sig |
|
9 |
val PARALLEL_CHOICE: tactic list -> tactic |
|
10 |
val PARALLEL_GOALS: tactic -> tactic |
|
11 |
val PARALLEL_ALLGOALS: (int -> tactic) -> tactic |
|
12 |
end; |
|
13 |
||
14 |
signature PAR_TACTICAL = |
|
15 |
sig |
|
16 |
include BASIC_PAR_TACTICAL |
|
17 |
end; |
|
18 |
||
19 |
structure Par_Tactical: PAR_TACTICAL = |
|
20 |
struct |
|
21 |
||
22 |
(* parallel choice of single results *) |
|
23 |
||
24 |
fun PARALLEL_CHOICE tacs st = |
|
25 |
(case Par_List.get_some (fn tac => SINGLE tac st) tacs of |
|
26 |
NONE => Seq.empty |
|
27 |
| SOME st' => Seq.single st'); |
|
28 |
||
29 |
||
30 |
(* parallel refinement of non-schematic goal by single results *) |
|
31 |
||
32 |
local |
|
33 |
||
34 |
exception FAILED of unit; |
|
35 |
||
36 |
fun retrofit st' = |
|
37 |
rotate_prems ~1 #> |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58009
diff
changeset
|
38 |
Thm.bicompose NONE {flatten = false, match = false, incremented = false} |
58009 | 39 |
(false, Goal.conclude st', Thm.nprems_of st') 1; |
40 |
||
41 |
in |
|
42 |
||
43 |
fun PARALLEL_GOALS tac = |
|
44 |
Thm.adjust_maxidx_thm ~1 #> |
|
45 |
(fn st => |
|
46 |
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1 |
|
47 |
then DETERM tac st |
|
48 |
else |
|
49 |
let |
|
50 |
fun try_tac g = |
|
51 |
(case SINGLE tac g of |
|
52 |
NONE => raise FAILED () |
|
53 |
| SOME g' => g'); |
|
54 |
||
55 |
val goals = Drule.strip_imp_prems (Thm.cprop_of st); |
|
56 |
val results = Par_List.map (try_tac o Goal.init) goals; |
|
57 |
in EVERY (map retrofit (rev results)) st end |
|
58 |
handle FAILED () => Seq.empty); |
|
59 |
||
60 |
end; |
|
61 |
||
62 |
val PARALLEL_ALLGOALS = PARALLEL_GOALS o ALLGOALS; |
|
63 |
||
64 |
end; |
|
65 |
||
66 |
structure Basic_Par_Tactical: BASIC_PAR_TACTICAL = Par_Tactical; |
|
67 |
open Basic_Par_Tactical; |
|
68 |