1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Dec 18 12:40:49 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Dec 18 14:48:43 2019 +0100
1.3 @@ -492,19 +492,19 @@
1.4 | Accept_Tac2 (m', (ist as {act_arg, ...}), ctxt) =>
1.5 (m', (Pstate ist, Tactic.insert_assumptions m' ctxt), (act_arg, Telem.Safe)))(*found tac*)
1.6 *)
1.7 -(*NEW*) Accept_Tac2 (tac, ist, ctxt) =>
1.8 -(*NEW*) Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
1.9 -(*NEW*)| Term_Val2 prog_result =>
1.10 -(*NEW*) (case par_pbl_det pt p of
1.11 -(*NEW*) (true, p', _) =>
1.12 -(*NEW*) let
1.13 -(*NEW*) val (_, pblID, _) = get_obj g_spec pt p';
1.14 -(*NEW*) in
1.15 -(*NEW*) End_Program (Istate.Pstate ist, Tactic.Check_Postcond' (pblID, (prog_result, [(*???*)])))
1.16 -(*NEW*) end
1.17 -(*NEW*) | _ => End_Program (Istate.Pstate ist, Tactic.End_Detail' (Rule.e_term,[])))
1.18 -(*NEW*)| Reject_Tac2 => Helpless)
1.19 -(*NEW*)
1.20 + Accept_Tac2 (tac, ist, ctxt) =>
1.21 + Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac)
1.22 + | Term_Val2 prog_result =>
1.23 + (case par_pbl_det pt p of
1.24 + (true, p', _) =>
1.25 + let
1.26 + val (_, pblID, _) = get_obj g_spec pt p';
1.27 + in
1.28 + End_Program (Istate.Pstate ist, Tactic.Check_Postcond' (pblID, (prog_result, [(*???*)])))
1.29 + end
1.30 + | _ => End_Program (Istate.Pstate ist, Tactic.End_Detail' (Rule.e_term,[])))
1.31 + | Reject_Tac2 => Helpless)
1.32 +
1.33 | find_next_tactic _ _ is _ =
1.34 raise ERROR ("find_next_tactic: not impl for " ^ Istate.istate2str is);
1.35
1.36 @@ -553,17 +553,15 @@
1.37 | begin_end_prog (Tactic.Check_Postcond' (pI, (prog_res, _))) _ (pt, (p, p_)) =
1.38 let
1.39 val pp = par_pblobj pt p
1.40 - val asm = (case get_obj g_tac pt p of (*collects and instantiates asms*)
1.41 - Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
1.42 - | _ => get_assumptions_ pt (p, p_))
1.43 - val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.44 - (*TODO?: extend Tactic.Check_Postcond' (pI, (prog_res, asm), ^^^^^ scsaf) ?*)
1.45 + val thy = Celem.assoc_thy (get_obj g_domID pt pp);
1.46 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
1.47 | _ => error "begin_end_prog Check_Postcond': uncovered case get_loc"
1.48 - val thy' = get_obj g_domID pt pp;
1.49 - val thy = Celem.assoc_thy thy';
1.50 + val asm = (case get_obj g_tac pt p of (*collects and instantiates asms*)
1.51 + Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
1.52 + | _ => get_assumptions_ pt (p, p_))
1.53 + val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
1.54 in
1.55 - if pp = [] (*TODO?: if unnecessary?*)
1.56 + if pp = []
1.57 then
1.58 let
1.59 val is = Istate.Pstate (pst |> Istate.set_act prog_res |> Istate.set_appy Istate.Skip_)
1.60 @@ -571,9 +569,7 @@
1.61 in ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt)))], ps, (pt, (p, p_))) end
1.62 else
1.63 let (*resume script of parent PblObj, transfer value of subpbl-script*)
1.64 - val ppp = par_pblobj pt (lev_up p);
1.65 - val thy' = get_obj g_domID pt ppp;
1.66 - val thy = Celem.assoc_thy thy';
1.67 + val thy = Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt (lev_up p)));
1.68
1.69 val (pst', ctxt') = case get_loc pt (pp, Frm) of
1.70 (Istate.Pstate pst', ctxt') => (pst', ctxt')
1.71 @@ -583,6 +579,9 @@
1.72 val ((p, p_), ps, _, pt) = Generate.generate1 thy tac (is, ctxt'') (pp, Res) pt;
1.73 in ([(Tactic.Check_Postcond pI, tac, ((pp, Res), (is, ctxt'')))], ps, (pt, (p, p_))) end
1.74 end
1.75 +
1.76 +
1.77 +
1.78 | begin_end_prog (Tactic.End_Proof'') _ ptp = ([], [], ptp)
1.79 | begin_end_prog tac_ is (pt, pos) =
1.80 let
1.81 @@ -595,7 +594,7 @@
1.82 ([(Tactic.input_from_T tac_, tac_, (pos, is))], c, (pt, pos'))
1.83 end
1.84 (*find_next_tactic from program, begin_end_prog will update the ctree*)
1.85 -and do_solve_step (ptp as (pt, pos as (p, p_))) = (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
1.86 +and do_solve_step (ptp as (pt, pos as (p, p_))) =
1.87 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
1.88 then ([], [], (pt, (p, p_)))
1.89 else
2.1 --- a/src/Tools/isac/MathEngine/solve.sml Wed Dec 18 12:40:49 2019 +0100
2.2 +++ b/src/Tools/isac/MathEngine/solve.sml Wed Dec 18 14:48:43 2019 +0100
2.3 @@ -169,49 +169,21 @@
2.4 in
2.5 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.e_ctxt)))], [], (pt,p')))
2.6 end
2.7 - | solve ("Check_Postcond", Tactic.Check_Postcond' (pI, _)) (pt, (p, p_)) =
2.8 + | solve ("Check_Postcond", Tactic.Check_Postcond' (pI, _)) (ptp as (pt, (p, p_))) =
2.9 let
2.10 val pp = par_pblobj pt p
2.11 - val asm =
2.12 - (case get_obj g_tac pt p of (*collects and instantiates asms*)
2.13 - Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
2.14 - | _ => get_assumptions_ pt (p,p_))
2.15 - handle _ => []
2.16 - val metID = get_obj g_metID pt pp;
2.17 - val {scr = sc as Rule.Prog prog, ...} = Specify.get_met metID;
2.18 + val {scr, ...} = Specify.get_met (get_obj g_metID pt pp);
2.19 val (pst, ctxt) = case get_loc pt (p, p_) of (Istate.Pstate pst, ctxt) => (pst, ctxt)
2.20 | _ => error "solve Check_Postcond: uncovered case get_loc"
2.21 -
2.22 - val thy' = get_obj g_domID pt pp;
2.23 - val thy = Celem.assoc_thy thy';
2.24 - val scval =
2.25 - case LucinNEW.find_next_tactic (sc) (pt, (p, p_)) (Istate.Pstate pst) ctxt of
2.26 - LucinNEW.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (scval, _))) => scval
2.27 - | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (scval, _))) => scval
2.28 + val prog_res =
2.29 + case LucinNEW.find_next_tactic scr (pt, (p, p_)) (Istate.Pstate pst) ctxt of
2.30 + LucinNEW.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
2.31 + | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
2.32 | _ => raise ERROR ("solve Check_Postcond " ^ strs2str' pI)
2.33 - in
2.34 - if pp = []
2.35 - then
2.36 - let
2.37 - val is = Istate.Pstate (pst |> Istate.set_act scval |> Istate.set_appy Istate.Skip_)
2.38 - val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
2.39 - (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)
2.40 - val (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
2.41 - in ("ok", ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) end
2.42 - else
2.43 - let (*resume script of parpbl, transfer value of subpbl-script*)
2.44 - val ppp = par_pblobj pt (lev_up p);
2.45 - val thy' = get_obj g_domID pt ppp;
2.46 - val thy = Celem.assoc_thy thy';
2.47 - val (pst', ctxt') = case get_loc pt (pp, Frm) of
2.48 - (Istate.Pstate pst', ctxt') => (pst', ctxt')
2.49 - | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
2.50 - val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
2.51 - val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))
2.52 - (Istate.Pstate (pst' |> Istate.set_act scval |> Istate.set_appy Istate.Skip_), ctxt'') (pp,Res) pt;
2.53 - in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),
2.54 - ((pp, Res), (Istate.Pstate (pst' |> Istate.set_act scval |> Istate.set_appy Istate.Skip_), ctxt'')))], ps, (pt, (p, p_)))) end
2.55 - end
2.56 + in (*for Applicable.applicable_in not yet available -----------vvvvv*)
2.57 + ("ok", LucinNEW.begin_end_prog (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
2.58 + (Istate.e_istate, ContextC.e_ctxt) ptp)
2.59 + end
2.60 | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =
2.61 ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
2.62 | solve (_, Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
3.1 --- a/src/Tools/isac/TODO.thy Wed Dec 18 12:40:49 2019 +0100
3.2 +++ b/src/Tools/isac/TODO.thy Wed Dec 18 14:48:43 2019 +0100
3.3 @@ -85,6 +85,7 @@
3.4 \item Step_Specify in Specify/step-specify.sml in analogy to Interpret/... TODO
3.5 \begin{itemize}
3.6 \item Step_Specify.check <-- Applicable.applicable_in
3.7 + inserts all data into Tactic.T available -- not all are at time of call!
3.8 \item Step_Specify.add <-- Generate.generate1
3.9 \item Step_Specify.by_tactic : Tactic.input -> Ctree.state -> step_result
3.10 \item Step_Specify.by_formula: ?term? -> Ctree.state -> step_result
3.11 @@ -93,6 +94,7 @@
3.12 \item Step_Solve in Interpret/step-solve.sml
3.13 \begin{itemize}
3.14 \item Step_Solve.check <-- Applicable.applicable_in
3.15 + inserts all data into Tactic.T available -- not all are at time of call!
3.16 \item Step_Solve.add <-- Generate.generate1
3.17 \item Step_Solve.by_tactic : Tactic.input -> Ctree.state -> step_result
3.18 ^^^^LucinNEW,begin_end_prog
3.19 @@ -103,6 +105,7 @@
3.20 \item Step in MathEngine/step.sml
3.21 \begin{itemize}
3.22 \item Step.check : Step_Specify.check | Step_Solve.check depending on pos'
3.23 + inserts all data into Tactic.T available -- not all are at time of call!
3.24 \item Step.add : Step_Specify.add | Step_Solve.add depending on pos'
3.25 \item Step.by_tactic : Step_Specify.by_tactic | Step_Solve.by_tactic depending on pos'
3.26 \item Step.by_formula: Step_Specify.by_formula | Step_Solve.by_formula depending on pos'