27 (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list * Ctree.pos' list * Ctree.state |
27 (Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))) list * Ctree.pos' list * Ctree.state |
28 |
28 |
29 datatype next_tactic_result = |
29 datatype next_tactic_result = |
30 NStep of Ctree.state * Istate.T * Proof.context * tactic |
30 NStep of Ctree.state * Istate.T * Proof.context * tactic |
31 | Helpless | End_Program |
31 | Helpless | End_Program |
32 (*val determine_next_tactic : |
32 val determine_next_tactic: Rule.program -> Ctree.state -> Istate.T -> Proof.context |
33 Rule.program -> Ctree.state -> Istate.T -> Proof.context -> next_tactic_result *) |
|
34 val determine_next_tactic: Ctree.state -> Rule.program -> Istate.T * Proof.context |
|
35 -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe) |
33 -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe) |
36 |
34 |
37 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
35 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
38 datatype expr_val1 = |
36 datatype expr_val1 = |
39 Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T |
37 Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T |
472 then scan_dn2 cc (trans_scan_down2 ist) (Program.body_of prog) |
470 then scan_dn2 cc (trans_scan_down2 ist) (Program.body_of prog) |
473 else go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_) |
471 else go_scan_up2 (prog, cc) (trans_scan_up2 ist |> set_appy Skip_) |
474 | scan_to_tactic2 _ _ = raise ERROR "scan_to_tactic2: uncovered pattern"; |
472 | scan_to_tactic2 _ _ = raise ERROR "scan_to_tactic2: uncovered pattern"; |
475 |
473 |
476 (*decide for the next applicable Prog_Tac*) |
474 (*decide for the next applicable Prog_Tac*) |
477 fun determine_next_tactic (ptp as(pt, (p, _))) (Rule.Prog prog) (Istate.Pstate ist, ctxt) = |
475 fun determine_next_tactic (Rule.Prog prog) (ptp as(pt, (p, _))) (Istate.Pstate ist) ctxt = |
478 (case scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) of |
476 (case scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) of |
479 Term_Val2 v => (* program finished *) |
477 Term_Val2 v => (* program finished *) |
480 (case par_pbl_det pt p of |
478 (case par_pbl_det pt p of |
481 (true, p', _) => |
479 (true, p', _) => |
482 let |
480 let |
489 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe))) |
487 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ctxt), (v, Telem.Safe))) |
490 | Reject_Tac2 => |
488 | Reject_Tac2 => |
491 (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *) |
489 (Tactic.Empty_Tac_, (Istate.e_istate, ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *) |
492 | Accept_Tac2 (m', (ist as {act_arg, ...})) => |
490 | Accept_Tac2 (m', (ist as {act_arg, ...})) => |
493 (m', (Pstate ist, ctxt), (act_arg, Telem.Safe))) (* found next tac *) |
491 (m', (Pstate ist, ctxt), (act_arg, Telem.Safe))) (* found next tac *) |
494 | determine_next_tactic _ _ (is, _) = |
492 | determine_next_tactic _ _ is _ = |
495 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is)); |
493 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is)); |
496 |
494 |
497 |
495 |
498 (*** locate an input formula in the program ***) |
496 (*** locate an input formula in the program ***) |
499 |
497 |
501 Step of Ctree.state * Istate.T * Proof.context |
499 Step of Ctree.state * Istate.T * Proof.context |
502 | Not_Derivable of Chead.calcstate' |
500 | Not_Derivable of Chead.calcstate' |
503 |
501 |
504 (* FIXME.WN050821 compare fun solve ... fun begin_end_prog |
502 (* FIXME.WN050821 compare fun solve ... fun begin_end_prog |
505 begin_end_prog (Apply_Method' vvv FIXME: get args in applicable_in *) |
503 begin_end_prog (Apply_Method' vvv FIXME: get args in applicable_in *) |
506 fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, _)) (ist, ctxt) (pt, pos as (p, _)) = |
504 fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) = |
507 let |
505 let |
508 val {ppc, ...} = Specify.get_met mI; |
506 val {ppc, ...} = Specify.get_met mI; |
509 val (itms, oris, probl) = case get_obj I pt p of |
507 val (itms, oris, probl) = case get_obj I pt p of |
510 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) |
508 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) |
511 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj" |
509 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj" |
554 val pp = par_pblobj pt p |
552 val pp = par_pblobj pt p |
555 val asm = (case get_obj g_tac pt p of |
553 val asm = (case get_obj g_tac pt p of |
556 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*) |
554 Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p (*collects and instantiates asms*) |
557 | _ => get_assumptions_ pt (p, p_)) |
555 | _ => get_assumptions_ pt (p, p_)) |
558 val metID = get_obj g_metID pt pp; |
556 val metID = get_obj g_metID pt pp; |
559 val {srls = srls, scr = sc, ...} = Specify.get_met metID; |
557 val {scr = sc, ...} = Specify.get_met metID; |
560 val (loc, pst, ctxt) = case get_loc pt (p, p_) of |
558 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt) |
561 loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt) |
|
562 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc" |
559 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc" |
563 val thy' = get_obj g_domID pt pp; |
560 val thy' = get_obj g_domID pt pp; |
564 val thy = Celem.assoc_thy thy'; |
561 val thy = Celem.assoc_thy thy'; |
565 val (_, _, (scval, _)) = determine_next_tactic (pt, (p, p_)) sc loc; |
562 val (_, _, (scval, _)) = determine_next_tactic sc (pt, (p, p_)) (Istate.Pstate pst) ctxt; |
566 in |
563 in |
567 if pp = [] |
564 if pp = [] |
568 then |
565 then |
569 let |
566 let |
570 val is = Istate.Pstate (pst |> Istate.set_act scval |> Istate.set_appy Istate.Skip_) |
567 val is = Istate.Pstate (pst |> Istate.set_act scval |> Istate.set_appy Istate.Skip_) |
603 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) |
600 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) |
604 then ([], [], (pt, (p, p_))) |
601 then ([], [], (pt, (p, p_))) |
605 else |
602 else |
606 let |
603 let |
607 val thy' = get_obj g_domID pt (par_pblobj pt p); |
604 val thy' = get_obj g_domID pt (par_pblobj pt p); |
608 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; |
605 val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt; |
609 val (tac_, is, (t, _)) = determine_next_tactic (pt, pos) sc is; |
606 val (tac_, is, (t, _)) = determine_next_tactic sc (pt, pos) ist ctxt; |
610 (* TODO here ^^^ return finished/helpless/ok ?*) |
607 (* TODO here ^^^ return finished/helpless/ok ?*) |
611 in case tac_ of |
608 in case tac_ of |
612 Tactic.End_Detail' _ => |
609 Tactic.End_Detail' _ => |
613 ([(Tactic.End_Detail, Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos)) |
610 ([(Tactic.End_Detail, Tactic.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos)) |
614 | _ => begin_end_prog tac_ is ptp |
611 | _ => begin_end_prog tac_ is ptp |