1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Mar 26 16:17:21 2020 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 13:06:41 2020 +0200
1.3 @@ -549,41 +549,57 @@
1.4 raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
1.5 end
1.6 end
1.7 - | by_tactic (Tactic.Check_Postcond' (pI, _)) _ (pt, pos as (p, _)) =
1.8 +(*NEW* ) ------vvv: prog_res ( *NEW*)
1.9 + | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
1.10 +(*NEW* ) BETTER (curr_ist, curr_ctxt) -----^^^^^^^^^^^^^^^^^^^ ( *NEW*)
1.11 let
1.12 - val (ist, ctxt) = get_loc pt pos
1.13 val parent_pos = par_pblobj pt p
1.14 val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);
1.15 val prog_res =
1.16 - case find_next_step scr (pt, pos) ist ctxt of
1.17 - Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
1.18 - | End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
1.19 - | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
1.20 - val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
1.21 - Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
1.22 - | _ => get_assumptions_ pt pos)
1.23 -
1.24 - val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.25 + case find_next_step scr (pt, pos) sub_ist sub_ctxt of
1.26 +(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
1.27 + |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
1.28 +(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
1.29 +(*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
1.30 +(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
1.31 +(*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
1.32 +(*OLD*) | _ => get_assumptions_ pt pos)
1.33 +(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.34 +( *OLD*)
1.35 in
1.36 if parent_pos = []
1.37 then
1.38 let
1.39 - val is = Pstate (ist |> the_pstate |> set_act prog_res |> set_found)
1.40 - val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, ctxt) (pt, (parent_pos, Res))
1.41 +(*NEW*) val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.42 +(*NEW*)
1.43 + val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found)
1.44 + val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, sub_ctxt) (pt, (parent_pos, Res))
1.45 in
1.46 - ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, ctxt)))], ps, (pt, (p, p_))))
1.47 + ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_))))
1.48 end
1.49 else
1.50 - let (*resume program of parent PblObj, transfer value of Subproblem-program*)
1.51 - val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
1.52 - (Pstate i, c) => (i, c)
1.53 - | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
1.54 - val ctxt' = ContextC.from_subpbl_to_caller ctxt prog_res ctxt_parent
1.55 - val is' = Pstate (ist_parent |> set_act prog_res |> set_found)
1.56 - val ((p, p_), ps, _, pt) = Generate.generate1 tac (is', ctxt') (pt, (parent_pos, Res))
1.57 - in
1.58 - ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is', ctxt')))], ps, (pt, (p, p_))))
1.59 - end
1.60 + let (*resume program of parent PblObj, transfer result of Subproblem-program*)
1.61 +(*OLD* ) val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.62 +(*OLD*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
1.63 +(*OLD*) (Pstate i, c) => (i, c)
1.64 +(*OLD*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
1.65 +(*OLD*) val (ttttt, ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
1.66 +(*OLD*) val is' = Pstate (ist_parent |> set_act prog_res |> set_found)
1.67 +(*OLD*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (is', ctxt') (pt, (parent_pos, Res))
1.68 +(*OLD*) in
1.69 +(*OLD*) ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is', ctxt')))], ps, (pt, (p, p_))))
1.70 +(*OLD*) end
1.71 +( *NEW*)
1.72 +(*NEW*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
1.73 +(*NEW*) (Pstate i, c) => (i, c)
1.74 +(*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
1.75 +(*NEW*) val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
1.76 +(*NEW*) val tac = Tactic.Check_Postcond' (pI, (prog_res', [(* DROP: asms DONE BY ctxt *)]))
1.77 +(*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
1.78 +(*NEW*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res))
1.79 +(*NEW*) in
1.80 +(*NEW*) ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
1.81 +(*NEW*) end
1.82 end
1.83 | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
1.84 | by_tactic tac_ ic (pt, pos) =
1.85 @@ -605,12 +621,12 @@
1.86 case find_next_step sc (pt, pos) ist ctxt of
1.87 Next_Step (ist, ctxt, tac) =>
1.88 by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp
1.89 - | End_Program (ist, tac) =>
1.90 + | End_Program (ist, tac) => (*TODO RM ..*)
1.91 (case tac of
1.92 Tactic.End_Detail' res =>
1.93 ("ok", ([(Tactic.End_Detail,
1.94 Tactic.End_Detail' res, (pos, (ist, ctxt)))], [], ptp))
1.95 - | _ => by_tactic tac (ist, ctxt) ptp
1.96 + | _ => (*.. RM*) by_tactic tac (ist, ctxt) ptp
1.97 )
1.98 | Helpless => ("helpless", Chead.e_calcstate')
1.99 end;