138 (*------------------------------------------------------------------ |
138 (*------------------------------------------------------------------ |
139 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*) |
139 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*) |
140 (*----------------------------------------------------from solve.sml*) |
140 (*----------------------------------------------------from solve.sml*) |
141 | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) = |
141 | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) = |
142 let (*val rls = the (assoc(!ruleset',rls')) |
142 let (*val rls = the (assoc(!ruleset',rls')) |
143 handle _ => raise error ("solve: '"^rls'^"' not known");*) |
143 handle _ => error ("solve: '"^rls'^"' not known");*) |
144 val thy = assoc_thy thy'; |
144 val thy = assoc_thy thy'; |
145 val (srls, sc, is) = |
145 val (srls, sc, is) = |
146 case rls of |
146 case rls of |
147 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => |
147 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => |
148 (e_rls, sc, RrlsState (ii t)) |
148 (e_rls, sc, RrlsState (ii t)) |
152 val pt = update_tac pt (fst p) (Detail_Set (id_rls rls)); |
152 val pt = update_tac pt (fst p) (Detail_Set (id_rls rls)); |
153 val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt; |
153 val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt; |
154 val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is); |
154 val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is); |
155 val aopt = applicable_in p pt nx; |
155 val aopt = applicable_in p pt nx; |
156 in case aopt of |
156 in case aopt of |
157 Notappl s => raise error ("solve Detail_Set: "^s) |
157 Notappl s => error ("solve Detail_Set: "^s) |
158 (* val Appl m = aopt; |
158 (* val Appl m = aopt; |
159 *) |
159 *) |
160 | Appl m => solve ("discardFIXME",m) p pt end |
160 | Appl m => solve ("discardFIXME",m) p pt end |
161 ------------------------------------------------------------------*) |
161 ------------------------------------------------------------------*) |
162 |
162 |
471 case locatetac tac (pt,p) of |
471 case locatetac tac (pt,p) of |
472 ("ok", (_, _, ptp)) => ptp |
472 ("ok", (_, _, ptp)) => ptp |
473 | ("unsafe-ok", (_, _, ptp)) => ptp |
473 | ("unsafe-ok", (_, _, ptp)) => ptp |
474 | ("not-applicable",_) => (pt, p) |
474 | ("not-applicable",_) => (pt, p) |
475 | ("end-of-calculation", (_, _, ptp)) => ptp |
475 | ("end-of-calculation", (_, _, ptp)) => ptp |
476 | ("failure",_) => raise error "sys-error"; |
476 | ("failure",_) => error "sys-error"; |
477 val (_, ts) = |
477 val (_, ts) = |
478 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]); |
478 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]); |
479 *) |
479 *) |
480 (case step p ((pt, e_pos'),[]) of |
480 (case step p ((pt, e_pos'),[]) of |
481 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts) |
481 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts) |
482 | ("helpless",_) => ("helpless: cannot propose tac", []) |
482 | ("helpless",_) => ("helpless: cannot propose tac", []) |
483 | ("no-fmz-spec",_) => raise error "no-fmz-spec" |
483 | ("no-fmz-spec",_) => error "no-fmz-spec" |
484 | ("end-of-calculation", (ts, _, _)) => ("",ts)) |
484 | ("end-of-calculation", (ts, _, _)) => ("",ts)) |
485 handle _ => raise error "sys-error"; |
485 handle _ => error "sys-error"; |
486 val tac = case ts of tacis as (_::_) => |
486 val tac = case ts of tacis as (_::_) => |
487 (* val tacis as (_::_) = ts; |
487 (* val tacis as (_::_) = ts; |
488 *) |
488 *) |
489 let val (tac,_,_) = last_elem tacis |
489 let val (tac,_,_) = last_elem tacis |
490 in tac end |
490 in tac end |