equal
deleted
inserted
replaced
7 |
7 |
8 infix 1 THEN_MAYBE THEN_MAYBE'; |
8 infix 1 THEN_MAYBE THEN_MAYBE'; |
9 |
9 |
10 signature SEARCH = |
10 signature SEARCH = |
11 sig |
11 sig |
|
12 val DEEPEN : int*int -> (int->int->tactic) -> int -> int -> tactic |
|
13 |
12 val THEN_MAYBE : tactic * tactic -> tactic |
14 val THEN_MAYBE : tactic * tactic -> tactic |
13 val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic) |
15 val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic) |
14 |
16 |
15 val trace_DEPTH_FIRST : bool ref |
17 val trace_DEPTH_FIRST : bool ref |
16 val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic |
18 val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic |
81 (*Uses depth-first search to solve ALL subgoals*) |
83 (*Uses depth-first search to solve ALL subgoals*) |
82 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); |
84 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); |
83 |
85 |
84 |
86 |
85 |
87 |
86 (**** Iterative deepening ****) |
88 (**** Iterative deepening with pruning ****) |
87 |
89 |
88 fun has_vars (Var _) = true |
90 fun has_vars (Var _) = true |
89 | has_vars (Abs (_,_,t)) = has_vars t |
91 | has_vars (Abs (_,_,t)) = has_vars t |
90 | has_vars (f$t) = has_vars f orelse has_vars t |
92 | has_vars (f$t) = has_vars f orelse has_vars t |
91 | has_vars _ = false; |
93 | has_vars _ = false; |
159 in depth (0,5) [] end); |
161 in depth (0,5) [] end); |
160 |
162 |
161 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; |
163 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; |
162 |
164 |
163 |
165 |
|
166 (*Simple iterative deepening tactical. It merely "deepens" any search tactic |
|
167 using increment "inc" up to limit "lim". *) |
|
168 fun DEEPEN (inc,lim) tacf m i = |
|
169 let fun dpn m = STATE(fn state => |
|
170 if has_fewer_prems i state then no_tac |
|
171 else if m>lim then |
|
172 (writeln "Giving up..."; no_tac) |
|
173 else (writeln ("Depth = " ^ string_of_int m); |
|
174 tacf m i ORELSE dpn (m+inc))) |
|
175 in dpn m end; |
|
176 |
164 (*** Best-first search ***) |
177 (*** Best-first search ***) |
165 |
178 |
166 val trace_BEST_FIRST = ref false; |
179 val trace_BEST_FIRST = ref false; |
167 |
180 |
168 (*Insertion into priority queue of states *) |
181 (*Insertion into priority queue of states *) |