41 (*if*) Tactic.for_specify' m; (*false*) |
41 (*if*) Tactic.for_specify' m; (*false*) |
42 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp); |
42 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp); |
43 |
43 |
44 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_)))) |
44 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_)))) |
45 = (m, (pt, pos)); |
45 = (m, (pt, pos)); |
46 val {srls, ...} = MethodC.from_store mI; |
46 val {srls, ...} = MethodC.from_store_PIDE ctxt mI; |
47 val itms = case get_obj I pt p of |
47 val itms = case get_obj I pt p of |
48 PblObj {meth=itms, ...} => itms |
48 PblObj {meth=itms, ...} => itms |
49 | _ => error "solve Apply_Method: uncovered case get_obj" |
49 | _ => error "solve Apply_Method: uncovered case get_obj" |
50 val thy' = get_obj g_domID pt p; |
50 val thy' = get_obj g_domID pt p; |
51 val thy = ThyC.get_theory thy'; |
51 val thy = ThyC.get_theory thy'; |
118 Step_Solve.by_tactic m ptp; |
118 Step_Solve.by_tactic m ptp; |
119 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp); |
119 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp); |
120 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_)); |
120 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_)); |
121 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*) |
121 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*) |
122 val thy' = get_obj g_domID pt (par_pblobj pt p); |
122 val thy' = get_obj g_domID pt (par_pblobj pt p); |
123 val (is, sc) = LItool.resume_prog thy' (p,p_) pt; |
123 val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt; |
124 |
124 |
125 locate_input_tactic sc (pt, po) (fst is) (snd is) m; |
125 locate_input_tactic sc (pt, po) (fst is) (snd is) m; |
126 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac) |
126 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac) |
127 = (sc, (pt, po), (fst is), (snd is), m); |
127 = (sc, (pt, po), (fst is), (snd is), m); |
128 val srls = get_simplifier cstate; |
128 val srls = get_simplifier cstate; |
283 (**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*) |
283 (**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*) |
284 Step_Solve.by_tactic m (pt, p); |
284 Step_Solve.by_tactic m (pt, p); |
285 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); |
285 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p)); |
286 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
286 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
287 val thy' = get_obj g_domID pt (par_pblobj pt p); |
287 val thy' = get_obj g_domID pt (par_pblobj pt p); |
288 val (is, sc) = LItool.resume_prog thy' (p,p_) pt; |
288 val (is, sc) = LItool.resume_prog_PIDE (p,p_) pt; |
289 |
289 |
290 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); |
290 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*); |
291 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac) |
291 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac) |
292 = (sc, (pt, po), (fst is), (snd is), m); |
292 = (sc, (pt, po), (fst is), (snd is), m); |
293 val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*); |
293 val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*); |
380 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) = |
380 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) = |
381 Step_Solve.do_next (pt, ip); |
381 Step_Solve.do_next (pt, ip); |
382 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
382 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
383 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
383 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
384 val thy' = get_obj g_domID pt (par_pblobj pt p); |
384 val thy' = get_obj g_domID pt (par_pblobj pt p); |
385 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; |
385 val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt; |
386 |
386 |
387 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) = |
387 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) = |
388 LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
388 LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
389 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) |
389 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) |
390 = (sc, (pt, pos), ist, ctxt); |
390 = (sc, (pt, pos), ist, ctxt); |
431 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) = |
431 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) = |
432 Step_Solve.do_next (pt, ip); |
432 Step_Solve.do_next (pt, ip); |
433 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
433 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); |
434 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
434 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*); |
435 val thy' = get_obj g_domID pt (par_pblobj pt p); |
435 val thy' = get_obj g_domID pt (par_pblobj pt p); |
436 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt; |
436 val ((ist, ctxt), sc) = LItool.resume_prog_PIDE (p,p_) pt; |
437 |
437 |
438 (** )val End_Program (ist, tac) = |
438 (** )val End_Program (ist, tac) = |
439 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
439 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*); |
440 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) |
440 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt) |
441 = (sc, (pt, pos), ist, ctxt); |
441 = (sc, (pt, pos), ist, ctxt); |
442 |
442 |
443 (* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*) |
443 (* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*) |
444 (** )val Term_Val prog_result = |
444 (**)val Term_Val prog_result = |
445 ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); |
445 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*); |
446 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) |
446 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...}))) |
447 = ((prog, (ptp, ctxt)), (Pstate ist)); |
447 = ((prog, (ptp, ctxt)), (Pstate ist)); |
448 (*if*) path = [] (*else*); |
448 (*if*) path = [] (*else*); |
449 |
449 |
450 go_scan_up (prog, cc) (trans_scan_up ist |> set_found); |
450 go_scan_up (prog, cc) (trans_scan_up ist |> set_found); |
456 Term_Val act_arg (*return from go_scan_up*); |
456 Term_Val act_arg (*return from go_scan_up*); |
457 "~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg); |
457 "~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg); |
458 |
458 |
459 Term_Val prog_result (*return from scan_to_tactic*); |
459 Term_Val prog_result (*return from scan_to_tactic*); |
460 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result); |
460 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result); |
461 val (true, p', _) = (*case*) parent_node pt pos (*of*); |
461 val (true, p' as [], Rule_Set.Empty, _) = (*case*) parent_node_PIDE pt pos (*of*); |
462 val (_, pblID, _) = get_obj g_spec pt p'; |
462 val (_, pblID, _) = get_obj g_spec pt p'; |
463 |
463 |
464 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result)) |
464 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result)) |
465 (*return from find_next_step*); |
465 (*return from find_next_step*); |
466 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac)) |
466 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac)) |