83 The abstraction over state prevents needless divergence in recursion. |
83 The abstraction over state prevents needless divergence in recursion. |
84 The 9999 should be a parameter, to delay treatment of flexible goals. *) |
84 The 9999 should be a parameter, to delay treatment of flexible goals. *) |
85 |
85 |
86 fun RESOLVE_THEN rules = |
86 fun RESOLVE_THEN rules = |
87 let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules; |
87 let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules; |
88 fun tac nextac i = STATE (fn state => |
88 fun tac nextac i state = state |> |
89 filseq_resolve_tac rls0 9999 i |
89 (filseq_resolve_tac rls0 9999 i |
90 ORELSE |
90 ORELSE |
91 (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i)) |
91 (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i)) |
92 ORELSE |
92 ORELSE |
93 (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1)) |
93 (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1)) |
94 THEN TRY(nextac i)) ) |
94 THEN TRY(nextac i))) |
95 in tac end; |
95 in tac end; |
96 |
96 |
97 |
97 |
98 |
98 |
99 (*repeated resolution applied to the designated goal*) |
99 (*repeated resolution applied to the designated goal*) |
200 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac; |
200 val fres_unsafe_tac = fresolve_tac unsafe_rls THEN' aside_tac; |
201 val fres_bound_tac = fresolve_tac bound_rls; |
201 val fres_bound_tac = fresolve_tac bound_rls; |
202 |
202 |
203 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac |
203 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac |
204 else tf(i) THEN tac(i-1) |
204 else tf(i) THEN tac(i-1) |
205 in STATE(fn state=> tac(nprems_of state)) end; |
205 in fn st => tac (nprems_of st) st end; |
206 |
206 |
207 (* Depth first search bounded by d *) |
207 (* Depth first search bounded by d *) |
208 fun solven_tac d n = STATE (fn state => |
208 fun solven_tac d n state = state |> |
209 if d<0 then no_tac |
209 (if d<0 then no_tac |
210 else if (nprems_of state = 0) then all_tac |
210 else if (nprems_of state = 0) then all_tac |
211 else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE |
211 else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE |
212 ((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND |
212 ((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND |
213 (fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1))))); |
213 (fres_bound_tac n THEN UPTOGOAL n (solven_tac (d-1))))); |
214 |
214 |
215 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1; |
215 fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1; |
216 |
216 |
217 fun step_tac n = STATE (fn state => |
217 fun step_tac n = |
218 if (nprems_of state = 0) then all_tac |
218 COND (has_fewer_prems 1) all_tac |
219 else (DETERM(fres_safe_tac n)) ORELSE |
219 (DETERM(fres_safe_tac n) ORELSE |
220 (fres_unsafe_tac n APPEND fres_bound_tac n)); |
220 (fres_unsafe_tac n APPEND fres_bound_tac n)); |
221 |
221 |
222 end; |
222 end; |
223 end; |
223 end; |