10 (case assoc_rls rls of |
10 (case assoc_rls rls of |
11 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) |
11 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) |
12 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; |
12 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; |
13 *) |
13 *) |
14 | Rls {scr=EmptyScr,...} => |
14 | Rls {scr=EmptyScr,...} => |
15 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
15 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
16 ^"use prep_rls for storing rule-sets !") |
16 ^"use prep_rls for storing rule-sets !") |
17 | Rls {scr=Script s,...} => |
17 | Rls {scr=Script s,...} => |
18 (* val Rls {scr=Script s,...} = assoc_rls rls; |
18 (* val Rls {scr=Script s,...} = assoc_rls rls; |
19 *) |
19 *) |
20 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) |
20 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) |
21 | Seq {scr=EmptyScr,...} => |
21 | Seq {scr=EmptyScr,...} => |
22 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
22 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
23 ^"use prep_rls for storing rule-sets !") |
23 ^"use prep_rls for storing rule-sets !") |
24 | Seq {srls=srls,scr=Script s,...} => |
24 | Seq {srls=srls,scr=Script s,...} => |
25 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) |
25 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) |
26 | init_istate (Rewrite_Set_Inst (subs, rls)) = |
26 | init_istate (Rewrite_Set_Inst (subs, rls)) = |
27 (* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p); |
27 (* val (Rewrite_Set_Inst (subs, rls)) = (get_obj g_tac pt p); |
28 *) |
28 *) |
29 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs |
29 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs |
30 in case assoc_rls rls of |
30 in case assoc_rls rls of |
31 Rls {scr=EmptyScr,...} => |
31 Rls {scr=EmptyScr,...} => |
32 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
32 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
33 ^"use prep_rls for storing rule-sets !") |
33 ^"use prep_rls for storing rule-sets !") |
34 | Rls {scr=Script s,...} => |
34 | Rls {scr=Script s,...} => |
35 let val (a1, a2) = two_scr_arg s |
35 let val (a1, a2) = two_scr_arg s |
36 in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end |
36 in (ScrState ([(a1, v), (a2, t)],[], NONE, e_term, Sundef,true)) end |
37 | Seq {scr=EmptyScr,...} => |
37 | Seq {scr=EmptyScr,...} => |
38 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
38 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
39 ^"use prep_rls for storing rule-sets !") |
39 ^"use prep_rls for storing rule-sets !") |
40 (* val Seq {scr=Script s,...} = assoc_rls rls; |
40 (* val Seq {scr=Script s,...} = assoc_rls rls; |
41 *) |
41 *) |
42 | Seq {scr=Script s,...} => |
42 | Seq {scr=Script s,...} => |
43 let val (a1, a2) = two_scr_arg s |
43 let val (a1, a2) = two_scr_arg s |
51 (case assoc_rls rls of |
51 (case assoc_rls rls of |
52 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) |
52 Rrls {scr=sc as Rfuns {init_state=ii,...},...} => (RrlsState (ii t)) |
53 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; |
53 (* val Rrls {scr=sc as Rfuns {init_state=ii,...},...} = assoc_rls rls; |
54 *) |
54 *) |
55 | Rls {scr=EmptyScr,...} => |
55 | Rls {scr=EmptyScr,...} => |
56 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
56 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
57 ^"use prep_rls for storing rule-sets !") |
57 ^"use prep_rls for storing rule-sets !") |
58 | Rls {scr=Script s,...} => |
58 | Rls {scr=Script s,...} => |
59 (* val Rls {scr=Script s,...} = assoc_rls rls; |
59 (* val Rls {scr=Script s,...} = assoc_rls rls; |
60 *) |
60 *) |
61 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) |
61 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true)) |
62 | Seq {scr=EmptyScr,...} => |
62 | Seq {scr=EmptyScr,...} => |
63 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
63 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
64 ^"use prep_rls for storing rule-sets !") |
64 ^"use prep_rls for storing rule-sets !") |
65 | Seq {srls=srls,scr=Script s,...} => |
65 | Seq {srls=srls,scr=Script s,...} => |
66 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) |
66 (ScrState ([(one_scr_arg s, t)], [], NONE, e_term, Sundef, true))) |
67 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t); |
67 (* val ((Rewrite_Set_Inst (subs, rls)), t) = ((get_obj g_tac pt p), t); |
68 *) |
68 *) |
69 | init_istate (Rewrite_Set_Inst (subs, rls)) t = |
69 | init_istate (Rewrite_Set_Inst (subs, rls)) t = |
70 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs |
70 let val (_, v)::_ = subs2subst (assoc_thy "Isac.thy") subs |
71 (*...we suppose the substitution of only _one_ bound variable*) |
71 (*...we suppose the substitution of only _one_ bound variable*) |
72 in case assoc_rls rls of |
72 in case assoc_rls rls of |
73 Rls {scr=EmptyScr,...} => |
73 Rls {scr=EmptyScr,...} => |
74 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
74 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
75 ^"use prep_rls for storing rule-sets !") |
75 ^"use prep_rls for storing rule-sets !") |
76 | Rls {scr=Script s,...} => |
76 | Rls {scr=Script s,...} => |
77 let val (form, bdv) = two_scr_arg s |
77 let val (form, bdv) = two_scr_arg s |
78 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) |
78 in (ScrState ([(form, t), (bdv, v)],[], NONE, e_term, Sundef,true)) |
79 end |
79 end |
80 | Seq {scr=EmptyScr,...} => |
80 | Seq {scr=EmptyScr,...} => |
81 raise error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
81 error ("interSteps>..>init_istate: \""^rls^"\" has EmptyScr." |
82 ^"use prep_rls for storing rule-sets !") |
82 ^"use prep_rls for storing rule-sets !") |
83 (* val Seq {scr=Script s,...} = assoc_rls rls; |
83 (* val Seq {scr=Script s,...} = assoc_rls rls; |
84 *) |
84 *) |
85 | Seq {scr=Script s,...} => |
85 | Seq {scr=Script s,...} => |
86 let val (form, bdv) = two_scr_arg s |
86 let val (form, bdv) = two_scr_arg s |
480 (istate2str (get_istate pt ([3],Frm))));*) |
480 (istate2str (get_istate pt ([3],Frm))));*) |
481 val f = Syntax.string_of_term (thy2ctxt thy) f; |
481 val f = Syntax.string_of_term (thy2ctxt thy) f; |
482 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
482 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end |
483 |
483 |
484 | generate1 thy m' _ _ _ = |
484 | generate1 thy m' _ _ _ = |
485 raise error ("generate1: not impl.for "^(tac_2str m')) |
485 error ("generate1: not impl.for "^(tac_2str m')) |
486 ; |
486 ; |
487 |
487 |
488 |
488 |
489 fun generate_hard thy m' (p,p_) pt = |
489 fun generate_hard thy m' (p,p_) pt = |
490 let |
490 let |
491 val p = case p_ of Frm => p | Res => lev_on p |
491 val p = case p_ of Frm => p | Res => lev_on p |
492 | _ => raise error ("generate_hard: call by "^(pos'2str (p,p_))); |
492 | _ => error ("generate_hard: call by "^(pos'2str (p,p_))); |
493 in generate1 thy m' e_istate (p,p_) pt end; |
493 in generate1 thy m' e_istate (p,p_) pt end; |
494 |
494 |
495 |
495 |
496 |
496 |
497 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*) |
497 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*) |
537 ::((insert_pos (lev_on p) tacis):taci list); |
537 ::((insert_pos (lev_on p) tacis):taci list); |
538 |
538 |
539 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm) |
539 fun res_from_taci (_, Rewrite'(_,_,_,_,_,_,(res, asm)), _) = (res, asm) |
540 | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm) |
540 | res_from_taci (_, Rewrite_Set'(_,_,_,_,(res, asm)), _) = (res, asm) |
541 | res_from_taci (_, tac_, _) = |
541 | res_from_taci (_, tac_, _) = |
542 raise error ("res_from_taci: called with" ^ tac_2str tac_); |
542 error ("res_from_taci: called with" ^ tac_2str tac_); |
543 |
543 |
544 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form |
544 (*.embed the tacis created by a '_deriv'ation; sys.form <> input.form |
545 tacis are in order, thus are reverted for generate.*) |
545 tacis are in order, thus are reverted for generate.*) |
546 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp); |
546 (* val (tacis, (pt, pos as (p, Frm))) = (tacis', ptp); |
547 *) |
547 *) |