41 | NasNap of term * Env.T; |
41 | NasNap of term * Env.T; |
42 val assoc2str : assoc -> string |
42 val assoc2str : assoc -> string |
43 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
43 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
44 datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T |
44 datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip of term * Env.T |
45 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate' |
45 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate' |
46 val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy |
46 val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy |
47 val appy: Rule.theory' * Rule.rls -> Ctree.state -> Istate.pstate -> term -> appy |
47 val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy |
48 val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> term -> appy |
48 val nstep_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.pstate -> Istate.appy_ -> appy |
49 datatype asap = Aundef | AssOnly | AssGen; |
49 datatype asap = Aundef | AssOnly | AssGen; |
50 val go : Celem.loc_ -> term -> term |
50 val go : Celem.loc_ -> term -> term |
51 val go_up: Celem.loc_ -> term -> term |
51 val go_up: Celem.loc_ -> term -> term |
52 val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy |
52 val execute_progr_1 : Rule.theory' * Rule.rls -> Ctree.state -> Rule.program -> Istate.T -> appy |
53 val execute_progr_2 : Rule.rls -> Tactic.T -> Ctree.state -> Rule.program * 'a -> Istate.T * Proof.context -> assoc |
53 val execute_progr_2 : Rule.rls -> Tactic.T -> Ctree.state -> Rule.program * 'a -> Istate.T * Proof.context -> assoc |
54 val check_Let_up : Celem.loc_ -> term -> term * term |
54 val check_Let_up : Celem.loc_ -> term -> term * term |
277 nxt_up thy ptp (Rule.Prog sc) (ist |> path_up) ay (go_up (get_path ist) sc) |
277 nxt_up thy ptp (Rule.Prog sc) (ist |> path_up) ay (go_up (get_path ist) sc) |
278 else (*interpreted to end*) |
278 else (*interpreted to end*) |
279 if ay = Skip_ then Skip (get_act_env ist) else Napp (get_env ist) |
279 if ay = Skip_ then Skip (get_act_env ist) else Napp (get_env ist) |
280 | nstep_up _ _ _ ist _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str (get_path ist)) |
280 | nstep_up _ _ _ ist _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str (get_path ist)) |
281 |
281 |
282 fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate (E, l, rls, a, v, _, _)) = |
282 fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.Pstate ist) = |
283 if l = [] |
283 if 0 = length (get_path ist) |
284 then appy thy ptp (E, [R], rls, NONE, v, AppUndef_, false) (Program.body_of prog) |
284 then appy thy ptp (trans_scan_down2 ist) (Program.body_of prog) |
285 else nstep_up thy ptp sc (E, l, rls, a, v, AppUndef_, false) Skip_ |
285 else nstep_up thy ptp sc (trans_scan_down2 ist) Skip_ |
286 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern"; |
286 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern"; |
287 |
287 |
288 (* decide for the next applicable Prog_Tac in the program *) |
288 (* decide for the next applicable Prog_Tac in the program *) |
289 fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate (E,l,rls,a,v,s,_), ctxt) = |
289 fun determine_next_tactic thy (ptp as (pt, (p, _))) sc (Istate.Pstate ist, ctxt) = |
290 (case execute_progr_1 thy ptp sc (Istate.Pstate (E,l,rls,a,v,s,false)) of |
290 (case execute_progr_1 thy ptp sc (Istate.Pstate ist) of |
291 Skip (v, _) => (* program finished *) |
291 Skip (v, _) => (* program finished *) |
292 (case par_pbl_det pt p of |
292 (case par_pbl_det pt p of |
293 (true, p', _) => |
293 (true, p', _) => |
294 let |
294 let |
295 val (_,pblID,_) = get_obj g_spec pt p'; |
295 val (_,pblID,_) = get_obj g_spec pt p'; |
490 else (NasNap (get_act_env ist)) |
490 else (NasNap (get_act_env ist)) |
491 | astep_up _ (ist, _) = error ("astep_up: uncovered fun-def with " ^ Celem.loc_2str (get_path ist)) |
491 | astep_up _ (ist, _) = error ("astep_up: uncovered fun-def with " ^ Celem.loc_2str (get_path ist)) |
492 |
492 |
493 fun execute_progr_2 _ m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate ist, ctxt) = |
493 fun execute_progr_2 _ m (pt, p) (scr as Rule.Prog sc, _) (Istate.Pstate ist, ctxt) = |
494 if get_path ist = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) |
494 if get_path ist = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) |
495 then assy (ctxt,Rule.e_rls, (pt, p), Aundef) (ist |> upd_path [R], m) (Program.body_of sc) |
495 then assy (ctxt,Rule.e_rls, (pt, p), Aundef(*\<rightarrow> Istate*)) (ist |> upd_path [R], m) (Program.body_of sc) |
496 else astep_up (ctxt,Rule.e_rls,scr, (pt, p)) (ist, m) |
496 else astep_up (ctxt,Rule.e_rls,scr, (pt, p)) (ist, m) |
497 | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def" |
497 | execute_progr_2 _ _ _ _ _ = raise ERROR "execute_progr_2: uncovered pattern in fun.def" |
498 |
498 |
499 fun locate_input_tactic (progr as Rule.Prog _) cstate istate ctxt tac = |
499 fun locate_input_tactic (progr as Rule.Prog _) cstate istate ctxt tac = |
500 let |
500 let |
582 (* Telem.safe should go on to Check_Postcond' vvvvv *) |
582 (* Telem.safe should go on to Check_Postcond' vvvvv *) |
583 in |
583 in |
584 if pp = [] |
584 if pp = [] |
585 then |
585 then |
586 let |
586 let |
587 (*val is = Istate.Pstate (E, l, Rule.e_rls, a, scval, Istate.Skip_, b)*) |
|
588 val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_) |
587 val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_) |
589 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm)) |
588 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm)) |
590 (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *) |
589 (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *) |
591 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt; |
590 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt; |
592 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end |
591 in ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end |