separate Solve_Step.add, rearrange code, prep. Specify_Step
1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Sat May 02 17:39:04 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 04 09:25:51 2020 +0200
1.3 @@ -350,7 +350,7 @@
1.4 let
1.5 val ctxt = get_ctxt pt pold
1.6 val (p, c, _, pt) =
1.7 - Generate.generate1 m (Istate.Uistate, ctxt) (pt, ip)
1.8 + Step.add m (Istate.Uistate, ctxt) (pt, ip)
1.9 in upd_calc cI ((pt, p), []);
1.10 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
1.11 end)
2.1 --- a/src/Tools/isac/Interpret/derive.sml Sat May 02 17:39:04 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/derive.sml Mon May 04 09:25:51 2020 +0200
2.3 @@ -21,6 +21,7 @@
2.4 (*val concat_deriv *)
2.5 val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
2.6 bool * der list
2.7 + val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
2.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.9 (* NONE *)
2.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.11 @@ -141,4 +142,44 @@
2.12 else (false, [])
2.13 end
2.14
2.15 +(* embed the tacis created by a '_deriv'ation; sys.form <> input.form
2.16 + tacis are in order, thus are reverted for generate *)
2.17 +fun embed tacis (pt, pos as (p, Pos.Frm)) =
2.18 + (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
2.19 + and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
2.20 + let
2.21 + val (res, asm) = (State_Steps.result o last_elem) tacis
2.22 + val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
2.23 + (SOME (ist, ctxt), _) => (ist, ctxt)
2.24 + | (NONE, _) => error "Derive.embed Frm: uncovered case get_obj"
2.25 + val form = Ctree.get_obj Ctree.g_form pt p
2.26 + (*val p = lev_on p; ---------------only difference to (..,Res) below*)
2.27 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
2.28 + (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
2.29 + (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))]
2.30 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
2.31 + val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
2.32 + val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
2.33 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
2.34 + in (c, (pt, pos)) end
2.35 + | embed tacis (pt, (p, Pos.Res)) =
2.36 + (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
2.37 + and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
2.38 + let
2.39 + val (res, asm) = (State_Steps.result o last_elem) tacis
2.40 + val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
2.41 + (_, SOME (ist, ctxt)) => (ist, ctxt)
2.42 + | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
2.43 + val (f, _) = Ctree.get_obj Ctree.g_result pt p
2.44 + val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
2.45 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
2.46 + (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
2.47 + (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
2.48 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
2.49 + val (pt, c, pos as (p, _)) = Solve_Step.s_add_general (rev tacis) (pt, [], (p, Pos.Res))
2.50 + val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
2.51 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
2.52 + in (c, (pt, pos)) end
2.53 + | embed _ _ = error "Derive.embed: uncovered definition"
2.54 +
2.55 (**)end(**)
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 02 17:39:04 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon May 04 09:25:51 2020 +0200
3.3 @@ -517,7 +517,7 @@
3.4 SOME t =>
3.5 let (* implicit Take *)
3.6 val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
3.7 - val (pos, c, _, pt) = Generate.generate1 show_add (is, ctxt) (pt, pos)
3.8 + val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos)
3.9 in
3.10 ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
3.11 end
3.12 @@ -532,14 +532,14 @@
3.13 Tactic.Take' t =>
3.14 let (* explicit Take *)
3.15 val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
3.16 - val (pos, c, _, pt) = Generate.generate1 show_add (ist', ctxt') (pt, pos)
3.17 + val (pos, c, _, pt) = Solve_Step.add show_add (ist', ctxt') (pt, pos)
3.18 in
3.19 ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
3.20 end
3.21 | add as Tactic.Subproblem' (_, _, headline, _, _, _) =>
3.22 let (* Subproblem *)
3.23 val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
3.24 - val (pos, c, _, pt) = Generate.generate1 add (ist', ctxt') (pt, pos)
3.25 + val (pos, c, _, pt) = Solve_Step.add add (ist', ctxt') (pt, pos)
3.26 in
3.27 ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
3.28 end
3.29 @@ -561,7 +561,7 @@
3.30 let
3.31 val tac = Tactic.Check_Postcond' (pI, prog_res)
3.32 val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found)
3.33 - val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, sub_ctxt) (pt, (parent_pos, Res))
3.34 + val ((p, p_), ps, _, pt) = Solve_Step.add_general tac (is, sub_ctxt) (pt, (parent_pos, Res))
3.35 in
3.36 ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_))))
3.37 end
3.38 @@ -573,7 +573,7 @@
3.39 val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
3.40 val tac = Tactic.Check_Postcond' (pI, prog_res')
3.41 val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
3.42 - val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res))
3.43 + val ((p, p_), ps, _, pt) = Solve_Step.add_general tac (ist', ctxt') (pt, (parent_pos, Res))
3.44 in
3.45 ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
3.46 end
3.47 @@ -582,7 +582,7 @@
3.48 | by_tactic tac_ ic (pt, pos) =
3.49 let
3.50 val pos = next_in_prog' pos
3.51 - val (pos', c, _, pt) = Generate.generate1 tac_ ic (pt, pos);
3.52 + val (pos', c, _, pt) = Solve_Step.add_general tac_ ic (pt, pos);
3.53 in
3.54 ("ok", ([(Tactic.input_from_T tac_, tac_, (pos, ic))], c, (pt, pos')))
3.55 end
3.56 @@ -628,7 +628,7 @@
3.57 then
3.58 let
3.59 val tacis' = map (State_Steps.make_single rew_ord erls) der;
3.60 - val (c', ptp) = Generate.embed_deriv tacis' ptp;
3.61 + val (c', ptp) = Derive.embed tacis' ptp;
3.62 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
3.63 else
3.64 if pos = ([], Pos.Res) (*TODO: we should stop earlier with trying subproblems *)
4.1 --- a/src/Tools/isac/Interpret/solve-step.sml Sat May 02 17:39:04 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Mon May 04 09:25:51 2020 +0200
4.3 @@ -9,6 +9,10 @@
4.4 sig
4.5 val check: Tactic.input -> Calc.T -> Applicable.T
4.6 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
4.7 + val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
4.8 + val s_add_general: State_Steps.T ->
4.9 + Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
4.10 +
4.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.12 (*NONE*)
4.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.14 @@ -25,7 +29,20 @@
4.15 check tactics (input by the user, mostly) for applicability
4.16 and determine as much of the result of the tactic as possible initially.
4.17 *)
4.18 -fun check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
4.19 +fun check (Tactic.Apply_Method mI) (pt, (p, _)) =
4.20 + let
4.21 + val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
4.22 + Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
4.23 + | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
4.24 + val {where_, ...} = Specify.get_pbt pI
4.25 + val pres = map (Model.mk_env probl |> subst_atomic) where_
4.26 + val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
4.27 + then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
4.28 + else ctxt
4.29 + in
4.30 + Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
4.31 + end
4.32 + | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
4.33 let
4.34 val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
4.35 val f = Calc.current_formula cs;
4.36 @@ -163,7 +180,13 @@
4.37 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
4.38 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
4.39
4.40 -fun add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
4.41 +fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
4.42 + (case topt of
4.43 + SOME t =>
4.44 + let val (pt, c) = Ctree.cappend_form pt p (is, ctxt) t
4.45 + in (pos, c, Generate.EmptyMout, pt) end
4.46 + | NONE => (pos, [], Generate.EmptyMout, pt))
4.47 + | add (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
4.48 let
4.49 val p =
4.50 let val (ps, p') = split_last p (* no connex to prev.ppobj *)
4.51 @@ -261,13 +284,31 @@
4.52 end
4.53 | add (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f))
4.54 (l as (_, ctxt)) (pt, (p, _)) =
4.55 + let
4.56 + val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
4.57 + (oris, (domID, pblID, metID), hdl, ctxt_specify)
4.58 + val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
4.59 + in
4.60 + ((p, Pos.Pbl), c, Generate.FormKF f, pt)
4.61 + end
4.62 + | add m' _ (_, pos) =
4.63 + raise ERROR ("Solve_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
4.64 +
4.65 +(* LI switches between solve-phase and specify-phase *)
4.66 +fun add_general tac ic cs =
4.67 + if Tactic.for_specify' tac
4.68 + then Generate.generate1 tac ic cs
4.69 + else add tac ic cs
4.70 +
4.71 +(* tacis are in reverse order from do_next/specify_: last = fst to insert *)
4.72 +fun s_add_general [] ptp = ptp
4.73 + | s_add_general tacis (pt, c, _) =
4.74 let
4.75 - val (pt, c) = Ctree.cappend_problem pt p l (fmz_, (domID, pblID, metID))
4.76 - (oris, (domID, pblID, metID), hdl, ctxt_specify)
4.77 - val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
4.78 + val (tacis', (_, tac_, (p, is))) = split_last tacis
4.79 + val (p',c',_,pt') = add_general tac_ is (pt, p)
4.80 in
4.81 - ((p, Pos.Pbl), c, Generate.FormKF f, pt)
4.82 + s_add_general tacis' (pt', c@c', p')
4.83 end
4.84 - | add m' _ _ = raise ERROR ("add: not impl.for " ^ Tactic.string_of m')
4.85 +
4.86
4.87 (**)end(**);
5.1 --- a/src/Tools/isac/Interpret/step-solve.sml Sat May 02 17:39:04 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Mon May 04 09:25:51 2020 +0200
5.3 @@ -40,8 +40,7 @@
5.4 then
5.5 let
5.6 val ctxt = get_ctxt pt po
5.7 - val ((p, p_), ps, _, pt) =
5.8 - Generate.generate1 m (Istate.empty, ctxt) (pt, (p, p_))
5.9 + val ((p, p_), ps, _, pt) = Solve_Step.add_general m (Istate.empty, ctxt) (pt, (p, p_))
5.10 in ("no-method-specified", (*Free_Solve*)
5.11 ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
5.12 end
5.13 @@ -54,8 +53,7 @@
5.14 LI.Safe_Step (istate, ctxt, tac) =>
5.15 let
5.16 val p' = next_in_prog po
5.17 - val (p'', _, _,pt') =
5.18 - Generate.generate1 tac (istate, ctxt) (pt, (p', p_))
5.19 + val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_))
5.20 in
5.21 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
5.22 [(*Ctree NOT cut*)], (pt', p'')))
5.23 @@ -66,8 +64,7 @@
5.24 case p_ of Frm => p
5.25 | Res => lev_on p
5.26 | _ => error ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
5.27 - val (p'', _, _,pt') =
5.28 - Generate.generate1 tac (istate, ctxt) (pt, (p', p_));
5.29 + val (p'', _, _,pt') = Solve_Step.add_general tac (istate, ctxt) (pt, (p', p_));
5.30 in
5.31 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
5.32 [(*Ctree NOT cut*)], (pt', p'')))
6.1 --- a/src/Tools/isac/MathEngBasic/position.sml Sat May 02 17:39:04 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/position.sml Mon May 04 09:25:51 2020 +0200
6.3 @@ -27,9 +27,11 @@
6.4 val lev_back' : pos' -> pos' (* for inform.sml *)
6.5 val lev_back : pos' -> pos' (* for inform.sml *)
6.6 val start_new_level: pos' -> pos'
6.7 + val new_on_level: pos' -> bool
6.8 val next_in_prog': pos' -> pos'
6.9 val next_in_prog: pos' -> pos
6.10 - val on_specification : pos_ -> bool
6.11 + val on_specification : pos' -> bool
6.12 + val on_specification': pos' -> bool
6.13
6.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.15 val pos's2str: pos' list -> string
6.16 @@ -121,6 +123,10 @@
6.17 if last_elem p <= 1 then (p, Frm)
6.18 else ((drop_last p) @ [(nth (length p) p) - 1], Res);
6.19 fun start_new_level (p, _) = ((lev_on o lev_dn) p, Frm)
6.20 +fun new_on_level (p, Frm) =
6.21 + if last_elem p = 1 then true else false
6.22 + | new_on_level _ = false
6.23 +
6.24 fun next_in_prog' (pos as (_, Met)) = start_new_level pos
6.25 | next_in_prog' (p, Res) = (lev_on p, Res)
6.26 | next_in_prog' pos = pos
6.27 @@ -129,9 +135,9 @@
6.28 | next_in_prog pos = raise ERROR ("Step_Solve.by_tactic: call by " ^ pos'2str pos);
6.29
6.30 (*WN.12.5.03: quick-and-dirty repair for listexpressions*)
6.31 -fun on_specification Pbl = true
6.32 - | on_specification Met = true
6.33 +fun on_specification (_, Pbl) = true
6.34 + | on_specification (_, Met) = true
6.35 | on_specification _ = false;
6.36 +fun on_specification' p = on_specification p orelse new_on_level p;
6.37
6.38 -
6.39 -end
6.40 +(**)end(**)
7.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Sat May 02 17:39:04 2020 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon May 04 09:25:51 2020 +0200
7.3 @@ -12,7 +12,6 @@
7.4 datatype T =
7.5 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
7.6 | Add_Relation' of TermC.as_string * Model.itm list
7.7 - | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
7.8 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
7.9 | Model_Problem' of Problem.id * Model.itm list * Model.itm list
7.10 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
7.11 @@ -21,6 +20,7 @@
7.12 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
7.13 | Specify_Theory' of ThyC.id
7.14 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
7.15 + | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
7.16 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
7.17 | Check_Postcond' of Problem.id * term
7.18 | Check_elementwise' of term * TermC.as_string * Selem.result
7.19 @@ -45,7 +45,6 @@
7.20 datatype input =
7.21 Add_Find of TermC.as_string | Add_Given of TermC.as_string
7.22 | Add_Relation of TermC.as_string
7.23 - | Apply_Method of Method.id
7.24 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
7.25 | Model_Problem
7.26 | Refine_Problem of Problem.id
7.27 @@ -54,6 +53,7 @@
7.28 | Specify_Problem of Problem.id
7.29 | Specify_Theory of ThyC.id
7.30 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
7.31 + | Apply_Method of Method.id
7.32 | Calculate of string
7.33 | Check_Postcond of Problem.id
7.34 | Check_elementwise of TermC.as_string
7.35 @@ -110,7 +110,6 @@
7.36
7.37 datatype input =
7.38 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
7.39 - | Apply_Method of Method.id
7.40 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
7.41 | Model_Problem
7.42 | Refine_Problem of Problem.id
7.43 @@ -119,6 +118,7 @@
7.44 | Specify_Problem of Problem.id
7.45 | Specify_Theory of ThyC.id
7.46 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
7.47 + | Apply_Method of Method.id
7.48 | Calculate of string
7.49 | Check_Postcond of Problem.id
7.50 | Check_elementwise of TermC.as_string
7.51 @@ -162,6 +162,8 @@
7.52 | Rewrite_Set_Inst (subs, rls) =>
7.53 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
7.54 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
7.55 + | Begin_Trans => "Begin_Trans"
7.56 + | End_Trans => "End_Trans"
7.57 | End_Detail => "End_Detail"
7.58 | Derive rls' => "Derive " ^ rls'
7.59 | Calculate op_ => "Calculate " ^ op_
7.60 @@ -295,11 +297,6 @@
7.61 datatype T =
7.62 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
7.63 | Add_Relation' of TermC.as_string * Model.itm list (* for Step.do_next *)
7.64 - | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
7.65 - Method.id * (* id in the Know_Store *)
7.66 - term option * (* first formula in the (sub-)Problem TODO: rm option *)
7.67 - Istate_Def.T * (* for starting the Program *)
7.68 - Proof.context (* for starting the Program *)
7.69 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
7.70 | Model_Problem' of (* first step in specify-phase *)
7.71 Problem.id * (* id in the Know_Store *)
7.72 @@ -319,6 +316,11 @@
7.73 (bool * term) list)) (* individual preconditions marked true/false *)
7.74 | Specify_Theory' of ThyC.id
7.75 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
7.76 + | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
7.77 + Method.id * (* id in the Know_Store *)
7.78 + term option * (* first formula in the (sub-)Problem TODO: rm option *)
7.79 + Istate_Def.T * (* for starting the Program *)
7.80 + Proof.context (* for starting the Program *)
7.81 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
7.82 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
7.83 Problem.id * (* id of the Problem to be checked *)
7.84 @@ -450,31 +452,32 @@
7.85
7.86 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
7.87
7.88 -fun for_specify Model_Problem = true
7.89 +fun for_specify (Add_Find _) = true
7.90 + | for_specify (Add_Given _) = true
7.91 + | for_specify (Add_Relation _) = true
7.92 + | for_specify (Del_Find _) = true
7.93 + | for_specify (Del_Given _) = true
7.94 + | for_specify (Del_Relation _) = true
7.95 + | for_specify Model_Problem = true
7.96 + | for_specify (Refine_Problem _) = true
7.97 | for_specify (Refine_Tacitly _) = true
7.98 - | for_specify (Refine_Problem _) = true
7.99 - | for_specify (Add_Given _) = true
7.100 - | for_specify (Del_Given _) = true
7.101 - | for_specify (Add_Find _) = true
7.102 - | for_specify (Del_Find _) = true
7.103 - | for_specify (Add_Relation _) = true
7.104 - | for_specify (Del_Relation _) = true
7.105 + | for_specify (Specify_Method _) = true
7.106 + | for_specify (Specify_Problem _) = true
7.107 | for_specify (Specify_Theory _) = true
7.108 - | for_specify (Specify_Problem _) = true
7.109 - | for_specify (Specify_Method _) = true
7.110 | for_specify _ = false
7.111 -fun for_specify' (Model_Problem' _) = true
7.112 +
7.113 +fun for_specify' (Add_Find' _) = true
7.114 + | for_specify' (Add_Given' _) = true
7.115 + | for_specify' (Add_Relation' _) = true
7.116 + | for_specify' (Del_Find' _) = true
7.117 + | for_specify' (Del_Given' _) = true
7.118 + | for_specify' (Del_Relation' _) = true
7.119 + | for_specify' (Model_Problem' _) = true
7.120 + | for_specify' (Refine_Problem' _) = true
7.121 | for_specify' (Refine_Tacitly' _) = true
7.122 - | for_specify' (Refine_Problem' _) = true
7.123 - | for_specify' (Add_Given' _) = true
7.124 - | for_specify' (Del_Given' _) = true
7.125 - | for_specify' (Add_Find' _) = true
7.126 - | for_specify' (Del_Find' _) = true
7.127 - | for_specify' (Add_Relation' _) = true
7.128 - | for_specify' (Del_Relation' _) = true
7.129 + | for_specify' (Specify_Method' _) = true
7.130 + | for_specify' (Specify_Problem' _) = true
7.131 | for_specify' (Specify_Theory' _) = true
7.132 - | for_specify' (Specify_Problem' _) = true
7.133 - | for_specify' (Specify_Method' _) = true
7.134 | for_specify' _ = false
7.135
7.136 (**)end(**)
8.1 --- a/src/Tools/isac/MathEngine/detail-step.sml Sat May 02 17:39:04 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Mon May 04 09:25:51 2020 +0200
8.3 @@ -45,7 +45,7 @@
8.4 val is = Generate.init_istate tac t
8.5 val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
8.6 val pos' = ((lev_on o lev_dn) p, Frm)
8.7 - val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *)
8.8 + val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *)
8.9 val (_,_, (pt'', _)) = Solve.complete_solve Solve.CompleteSubpbl [] (pt', pos')
8.10 val newnds = children (get_nd pt'' p)
8.11 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
9.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Sat May 02 17:39:04 2020 +0200
9.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Mon May 04 09:25:51 2020 +0200
9.3 @@ -21,8 +21,8 @@
9.4 (* fetch _all_ tactics from a program *)
9.5 fun from_prog _ ([], Res) =
9.6 raise PTREE "no tactics applicable at the end of a calculation"
9.7 - | from_prog pt (p,p_) =
9.8 - if Pos.on_specification p_
9.9 + | from_prog pt (pos as (p, p_)) =
9.10 + if Pos.on_specification pos
9.11 then [get_obj g_tac pt p]
9.12 else
9.13 let
9.14 @@ -43,8 +43,8 @@
9.15 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
9.16 fun specific_from_prog _ (([], Res) : pos') =
9.17 raise PTREE "no tactics applicable at the end of a calculation"
9.18 - | specific_from_prog pt (p, p_) =
9.19 - if Pos.on_specification p_
9.20 + | specific_from_prog pt (pos as (p, p_)) =
9.21 + if Pos.on_specification pos
9.22 then [get_obj g_tac pt p]
9.23 else
9.24 let
10.1 --- a/src/Tools/isac/MathEngine/step.sml Sat May 02 17:39:04 2020 +0200
10.2 +++ b/src/Tools/isac/MathEngine/step.sml Mon May 04 09:25:51 2020 +0200
10.3 @@ -12,6 +12,7 @@
10.4 val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'
10.5 (*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate' NOT for specify*)
10.6 val check: Tactic.input -> Calc.T -> Applicable.T
10.7 + val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
10.8
10.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.10 (*NONE*)
10.11 @@ -29,9 +30,14 @@
10.12 (** check a tactic for applicability **)
10.13
10.14 fun check tac (ctree, pos) =
10.15 - if Pos.on_specification (snd pos)
10.16 + if Tactic.for_specify tac
10.17 then Specify_Step.check tac (ctree, pos)
10.18 - else Solve_Step.check tac (ctree, pos)
10.19 + else Solve_Step.check tac (ctree, pos);
10.20 +
10.21 +
10.22 +(** add a step to a calculation **)
10.23 +
10.24 +val add = Solve_Step.add_general;
10.25
10.26
10.27 (* survey on results of by_tactic, find_next, by_term:
10.28 @@ -62,7 +68,7 @@
10.29 fun switch_specify_solve state_pos (pt, input_pos) =
10.30 let
10.31 val result =
10.32 - if Library.member op = [Pos.Pbl, Pos.Met] state_pos
10.33 + if Pos.on_specification ([], state_pos)
10.34 then specify_do_next (pt, input_pos)
10.35 else LI.do_next (pt, input_pos)
10.36 in
10.37 @@ -83,7 +89,7 @@
10.38 (_ :: _) =>
10.39 if ip = p (*the request is done where ptp waits for*)
10.40 then
10.41 - let val (pt', c', p') = Generate.generate tacis (pt, [], p)
10.42 + let val (pt', c', p') = Solve_Step.s_add_general tacis (pt, [], p)
10.43 in ("ok", (tacis, c', (pt', p'))) end
10.44 else
10.45 switch_specify_solve p_ (pt, ip)
11.1 --- a/src/Tools/isac/Specify/generate.sml Sat May 02 17:39:04 2020 +0200
11.2 +++ b/src/Tools/isac/Specify/generate.sml Mon May 04 09:25:51 2020 +0200
11.3 @@ -18,10 +18,7 @@
11.4 val init_istate: Tactic.input -> term -> Istate_Def.T
11.5 val init_pbl: (string * (term * 'a)) list -> Model.itm list
11.6 val init_pbl': (string * (term * term)) list -> Model.itm list
11.7 - val embed_deriv: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
11.8 val generate1: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> test_out
11.9 - val generate: State_Steps.T ->
11.10 - Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
11.11 val generate_hard:
11.12 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> test_out
11.13 val generate_inconsistent_rew: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
11.14 @@ -192,22 +189,6 @@
11.15 in
11.16 (pos, [], PpcKF (Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
11.17 end
11.18 - | generate1 (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
11.19 - (case topt of
11.20 - SOME t =>
11.21 - let val (pt, c) = cappend_form pt p (is, ctxt) t
11.22 - in (pos, c, EmptyMout, pt) end
11.23 - | NONE => (pos, [], EmptyMout, pt))
11.24 - (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
11.25 - | generate1 (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
11.26 - let
11.27 - val p =
11.28 - let val (ps, p') = split_last p (* no connex to prev.ppobj *)
11.29 - in if p' = 0 then ps @ [1] else p end
11.30 - val (pt, c) = cappend_form pt p l t
11.31 - in
11.32 - ((p, Frm): pos', c, FormKF (UnparseC.term t), pt)
11.33 - end
11.34 | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =
11.35 let
11.36 val (pt, c) = cappend_form pt p l t
11.37 @@ -218,16 +199,28 @@
11.38 in
11.39 ((p, Frm), c @ c', FormKF (UnparseC.term t), pt)
11.40 end
11.41 - | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Res)) =
11.42 - (*append after existing PrfObj vvvvvvvvvvvvv*)
11.43 - generate1 (Tactic.Begin_Trans' t) l (pt, (lev_on p, Frm))
11.44 - | generate1 (Tactic.End_Trans' tasm) l (pt, (p, _)) =
11.45 + | generate1 (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
11.46 let
11.47 val p' = lev_up p
11.48 val (pt, c) = append_result pt p' l tasm Complete
11.49 in
11.50 ((p', Res), c, FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
11.51 end
11.52 + | generate1 m' _ (_, pos) =
11.53 + raise ERROR ("generate1: not impl.for " ^ Tactic.string_of m' ^ " at " ^ pos'2str pos)
11.54 +(* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv* )
11.55 + | generate1 (Tactic.Take' t) l (pt, (p, _)) = (* val (Take' t) = m; *)
11.56 + let
11.57 + val p =
11.58 + let val (ps, p') = split_last p (* no connex to prev.ppobj *)
11.59 + in if p' = 0 then ps @ [1] else p end
11.60 + val (pt, c) = cappend_form pt p l t
11.61 + in
11.62 + ((p, Frm): pos', c, FormKF (UnparseC.term t), pt)
11.63 + end
11.64 + | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Res)) =
11.65 + (*append after existing PrfObj vvvvvvvvvvvvv*)
11.66 + generate1 (Tactic.Begin_Trans' t) l (pt, (lev_on p, Frm))
11.67 | generate1 (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
11.68 let
11.69 val (pt, c) = cappend_atomic pt p (is, ctxt) f
11.70 @@ -305,6 +298,7 @@
11.71 ((p, Pbl), c, FormKF f, pt)
11.72 end
11.73 | generate1 m' _ _ = error ("generate1: not impl.for " ^ Tactic.string_of m')
11.74 +( * ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
11.75
11.76 fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
11.77 let
11.78 @@ -327,52 +321,4 @@
11.79 generate1 m' (Istate_Def.empty, ContextC.empty) (pt, (p, p_))
11.80 end
11.81
11.82 -(* tacis are in reverse order from do_next/specify_: last = fst to insert *)
11.83 -fun generate ([]: State_Steps.T) ptp = ptp
11.84 - | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*)) =
11.85 - let
11.86 - val (tacis', (_, tac_, (p, is))) = split_last tacis
11.87 - val (p',c',_,pt') = generate1 tac_ is (pt, p)
11.88 - in
11.89 - generate tacis' (pt', c@c', p')
11.90 - end
11.91 -
11.92 -(* embed the tacis created by a '_deriv'ation; sys.form <> input.form
11.93 - tacis are in order, thus are reverted for generate *)
11.94 -fun embed_deriv tacis (pt, pos as (p, Frm)) =
11.95 - (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
11.96 - and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
11.97 - let
11.98 - val (res, asm) = (State_Steps.result o last_elem) tacis
11.99 - val (ist, ctxt) = case get_obj g_loc pt p of
11.100 - (SOME (ist, ctxt), _) => (ist, ctxt)
11.101 - | (NONE, _) => error "embed_deriv Frm: uncovered case get_obj"
11.102 - val form = get_obj g_form pt p
11.103 - (*val p = lev_on p; ---------------only difference to (..,Res) below*)
11.104 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
11.105 - (State_Steps.insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
11.106 - (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))]
11.107 - val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
11.108 - val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
11.109 - val pt = update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
11.110 - val pt = update_branch pt p TransitiveB
11.111 - in (c, (pt, pos: pos')) end
11.112 - | embed_deriv tacis (pt, (p, Res)) =
11.113 - (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
11.114 - and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
11.115 - let val (res, asm) = (State_Steps.result o last_elem) tacis
11.116 - val (ist, ctxt) = case get_obj g_loc pt p of
11.117 - (_, SOME (ist, ctxt)) => (ist, ctxt)
11.118 - | (_, NONE) => error "embed_deriv Frm: uncovered case get_obj"
11.119 - val (f, _) = get_obj g_result pt p
11.120 - val p = lev_on p(*---------------only difference to (..,Frm) above*);
11.121 - val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Frm), (Istate_Def.Uistate, ctxt))) ::
11.122 - (State_Steps.insert_pos ((lev_on o lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
11.123 - (pos_plus (length tacis) (lev_dn p, Res), (new_val res ist, ctxt)))];
11.124 - val {nrls, ...} = Specify.get_met (get_obj g_metID pt (par_pblobj pt p))
11.125 - val (pt, c, pos as (p, _)) = generate (rev tacis) (pt, [], (p, Res))
11.126 - val pt = update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
11.127 - val pt = update_branch pt p TransitiveB
11.128 - in (c, (pt, pos)) end
11.129 - | embed_deriv _ _ = error "embed_deriv: uncovered definition"
11.130 -end
11.131 \ No newline at end of file
11.132 +(**)end(**)
11.133 \ No newline at end of file
12.1 --- a/src/Tools/isac/Specify/specify-step.sml Sat May 02 17:39:04 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/specify-step.sml Mon May 04 09:25:51 2020 +0200
12.3 @@ -28,19 +28,6 @@
12.4 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
12.5 | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))
12.6 | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))
12.7 - | check (Tactic.Apply_Method mI) (pt, (p, _)) =
12.8 - let
12.9 - val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
12.10 - Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
12.11 - | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
12.12 - val {where_, ...} = Specify.get_pbt pI
12.13 - val pres = map (Model.mk_env probl |> subst_atomic) where_
12.14 - val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
12.15 - then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
12.16 - else ctxt
12.17 - in
12.18 - Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
12.19 - end
12.20 (*required for corner cases, e.g. test setup in inssort.sml*)
12.21 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
12.22 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
12.23 @@ -100,5 +87,84 @@
12.24 | check tac (_, pos) =
12.25 raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);
12.26
12.27 +fun generate1 (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
12.28 + let
12.29 + val pt = Ctree.update_pbl pt p itms
12.30 + val pt = Ctree.update_met pt p met
12.31 + in
12.32 + (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
12.33 + end
12.34 + | generate1 (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
12.35 + (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [][]),
12.36 + case p_ of
12.37 + Pos.Pbl => Ctree.update_pbl pt p itmlist
12.38 + | Pos.Met => Ctree.update_met pt p itmlist
12.39 + | _ => error ("uncovered case " ^ Pos.pos_2str p_))
12.40 + (* WN110515 probably declare_constraints with input item (without dsc) --
12.41 + -- important when specifying without formalisation *)
12.42 + | generate1 (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
12.43 + (pos, [], (Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] [])),
12.44 + case p_ of
12.45 + Pos.Pbl => Ctree.update_pbl pt p itmlist
12.46 + | Pos.Met => Ctree.update_met pt p itmlist
12.47 + | _ => error ("uncovered case " ^ Pos.pos_2str p_))
12.48 + (*WN110515 probably declare_constraints with input item (without dsc)*)
12.49 + | generate1 (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
12.50 + (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []),
12.51 + case p_ of
12.52 + Pos.Pbl => Ctree.update_pbl pt p itmlist
12.53 + | Pos.Met => Ctree.update_met pt p itmlist
12.54 + | _ => error ("uncovered case " ^ Pos.pos_2str p_))
12.55 + | generate1 (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
12.56 + (pos, [] , Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []),
12.57 + Ctree.update_domID pt p domID)
12.58 + | generate1 (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
12.59 + let
12.60 + val pt = Ctree.update_pbl pt p itms
12.61 + val pt = Ctree.update_pblID pt p pI
12.62 + in
12.63 + ((p, Pos.Pbl), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
12.64 + end
12.65 + | generate1 (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
12.66 + let
12.67 + val pt = Ctree.update_oris pt p oris
12.68 + val pt = Ctree.update_met pt p itms
12.69 + val pt = Ctree.update_metID pt p mID
12.70 + in
12.71 + ((p, Pos.Met), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
12.72 + end
12.73 + | generate1 (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
12.74 + let
12.75 + val pt = Ctree.update_pbl pt p pbl
12.76 + val pt = Ctree.update_orispec pt p (domID, pIre, metID)
12.77 + in
12.78 + (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
12.79 + end
12.80 + | generate1 (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =
12.81 + let
12.82 + val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p
12.83 + val pt = Ctree.update_spec pt p (dI, pI, mI)
12.84 + in
12.85 + (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
12.86 + end
12.87 + | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =
12.88 + let
12.89 + val (pt, c) = Ctree.cappend_form pt p l t
12.90 + val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*)
12.91 + (* replace the old PrfOjb ~~~~~ *)
12.92 + val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
12.93 + val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*)
12.94 + in
12.95 + ((p, Frm), c @ c', Generate.FormKF (UnparseC.term t), pt)
12.96 + end
12.97 + | generate1 (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
12.98 + let
12.99 + val p' = Pos.lev_up p
12.100 + val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
12.101 + in
12.102 + ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
12.103 + end
12.104 + | generate1 m' _ (_, pos) =
12.105 + raise ERROR ("generate1: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)
12.106
12.107 (**)end(**);
13.1 --- a/src/Tools/isac/TODO.thy Sat May 02 17:39:04 2020 +0200
13.2 +++ b/src/Tools/isac/TODO.thy Mon May 04 09:25:51 2020 +0200
13.3 @@ -115,14 +115,8 @@
13.4 use this also for me, not only for me_ist_ctxt; del. me
13.5 this requires much updating in all test/*
13.6 \item xxx
13.7 - \item xxx
13.8 - \item generate, generate1: NO thy as arg.
13.9 - Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
13.10 - redesign return value (originally for output by fun me?)
13.11 - \item xxx
13.12 \item shift tests into NEW model.sml (upd, upds_envv, ..)
13.13 \item xxx
13.14 - \item xxx
13.15 \item clarify handling of contexts ctxt ContextC
13.16 \begin{itemize}
13.17 \item xxx
13.18 @@ -298,7 +292,6 @@
13.19 \begin{itemize}
13.20 \item *.check | *.add
13.21 Specify_Step.add <-- Generate.generate1
13.22 - Solve_Step.add <-- Generate.generate1
13.23 \item xxx
13.24 \end{itemize}
13.25 \item xxx
14.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Sat May 02 17:39:04 2020 +0200
14.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Mon May 04 09:25:51 2020 +0200
14.3 @@ -283,7 +283,7 @@
14.4 = (xxxxx);
14.5 (*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res')
14.6 (*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
14.7 -(*NEW*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res));
14.8 +(*NEW*) val ((p, p_), ps, _, pt) = Step.add tac (ist', ctxt') (pt, (parent_pos, Res));
14.9
14.10 (*NEW*) ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
14.11 (*return from xxx*);
15.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sat May 02 17:39:04 2020 +0200
15.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon May 04 09:25:51 2020 +0200
15.3 @@ -237,7 +237,7 @@
15.4 (*if*) ip = ([], Pos.Res);(*else*)
15.5 val (_::_) = (*case*) tacis (*of*);
15.6 (*isa==REP*) (*if*) ip = p;(*then*)
15.7 - (*val (pt',c',p') =*) Generate.generate tacis (pt,[],p);
15.8 + (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);
15.9 (*//------------------------------------- final test -----------------------------------------\\*)
15.10 val ("ok", [], ptp as (pt, p)) = xxxx;
15.11
16.1 --- a/test/Tools/isac/Interpret/li-tool.sml Sat May 02 17:39:04 2020 +0200
16.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Mon May 04 09:25:51 2020 +0200
16.3 @@ -129,7 +129,7 @@
16.4 *)
16.5
16.6 "~~~~~ fun specific_from_prog , args:"; val (pt, (p, p_)) = (pt, p);
16.7 -Pos.on_specification p_ = false;
16.8 + (*if*) Pos.on_specification (p, p_) (*else*);
16.9 val pp = par_pblobj pt p
16.10 val thy' = (get_obj g_domID pt pp):ThyC.id
16.11 val thy = ThyC.get_theory thy'
17.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat May 02 17:39:04 2020 +0200
17.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon May 04 09:25:51 2020 +0200
17.3 @@ -169,7 +169,7 @@
17.4
17.5 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
17.6 val (p'', _, _,pt') =
17.7 - Generate.generate1 tac (istate, ctxt) (pt, (lev_on p, Pbl));
17.8 + Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
17.9 (*in*)
17.10
17.11 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
18.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Sat May 02 17:39:04 2020 +0200
18.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Mon May 04 09:25:51 2020 +0200
18.3 @@ -43,7 +43,7 @@
18.4 (*[3], Pbl*)autoCalculate 1 (Steps 1); (* out of SubProblem *)
18.5 (*[3], Met*)autoCalculate 1 CompleteCalcHead;
18.6 (*[3, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
18.7 -(*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*)
18.8 +(*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: Step.add: not impl.for Empty_Tac_*)
18.9 (*[3, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
18.10 (*[3, 2], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
18.11 (*[3, 3], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
18.12 @@ -56,7 +56,7 @@
18.13 (*[3, 8, 1], Frm*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
18.14 (*[3, 8, 1], Res*)autoCalculate 1 (Steps 1); (* solve SubProblem *)
18.15 (*(**)autoCalculate 1 (Steps 1);
18.16 -*** generate1: not impl.for Empty_Tac_
18.17 +*** Step.add: not impl.for Empty_Tac_
18.18 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
18.19
18.20 val ((pt,_),_) = get_calc 1;
19.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Sat May 02 17:39:04 2020 +0200
19.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Mon May 04 09:25:51 2020 +0200
19.3 @@ -342,7 +342,7 @@
19.4 val (_, (ist, ctxt), sc) =
19.5 LItool.resume_prog thy' (p,p_) pt;
19.6 "~~~~~ fun resume_prog , args:"; val (thy, (p, p_), pt) = (thy', (p,p_), pt);
19.7 - (*if*) Pos.on_specification p_ (*else*);
19.8 + (*if*) Pos.on_specification (p, p_) (*else*);
19.9 val (pbl, p', rls') = parent_node pt p
19.10 (*if*) pbl (*then*);
19.11 val metID = get_obj g_metID pt p'
20.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Sat May 02 17:39:04 2020 +0200
20.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 04 09:25:51 2020 +0200
20.3 @@ -204,10 +204,10 @@
20.4 val is = init_istate tac t
20.5 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
20.6 is wrong for simpl, but working ?!? *)
20.7 - val tac_ = Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
20.8 + val tac_ = Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
20.9 val pos' = ((lev_on o lev_dn) p, Frm)
20.10 val thy = ThyC.get_theory "Isac_Knowledge"
20.11 - val (_,_,_,pt') = (*implicit Take*)generate1 tac_ (is, ctxt) (pt, pos');
20.12 + val (_,_,_,pt') = (*implicit Take*)Step.add tac_ (is, ctxt) (pt, pos');
20.13 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
20.14 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
20.15 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
20.16 @@ -247,10 +247,10 @@
20.17 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
20.18 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
20.19 | _ => pos;
20.20 -generate1 tac_ is pos pt;
20.21 +Step.add tac_ is pos pt;
20.22 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
20.23 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
20.24 -"~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
20.25 +"~~~~~ fun add, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
20.26 (is, ctxt), (p,p_), pt) = ((ThyC.get_theory "Isac_Knowledge"), tac_, is, pos, pt);
20.27 val (pt,c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
20.28 (Rewrite thm') (f',asm) Complete;
21.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Sat May 02 17:39:04 2020 +0200
21.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Mon May 04 09:25:51 2020 +0200
21.3 @@ -17,6 +17,7 @@
21.4 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Theory "Test"*)
21.5 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
21.6 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
21.7 +
21.8 (*//------------------ begin step into ------------------------------------------------------\\*)
21.9 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*\<rightarrow>Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
21.10
21.11 @@ -59,17 +60,47 @@
21.12
21.13 (*val ("ok", ([(Apply_Method ["Test", "squ-equ-test-subpbl1"], _, _)], _, (_, _))) =*)
21.14 val xxxxx =
21.15 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
21.16 - ist_ctxt (pt, (p, p_'));
21.17 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'));
21.18 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
21.19 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
21.20 + val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
21.21 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
21.22 + | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
21.23 + val {ppc, ...} = Specify.get_met mI;
21.24 + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
21.25 + val itms = Specify.hack_until_review_Specify_1 mI itms
21.26 + val srls = LItool.get_simplifier (pt, pos)
21.27 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
21.28 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
21.29 + | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
21.30 + val ini = LItool.implicit_take prog env;
21.31 + val pos = start_new_level pos
21.32 + val SOME t = (*case*) ini (*of*);
21.33 + val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
21.34 + val (pos, c, _, pt) = Solve_Step.add show_add (is, ctxt) (pt, pos);
21.35 +(*-------------------- stop step into -------------------------------------------------------*)
21.36 +
21.37 "~~~~~ from fun specify_do_next \<longrightarrow>fun switch_specify_solve \<longrightarrow>fun do_next \<longrightarrow>fun me , return:";
21.38 val (_, (ts as (_, _, _) :: _, _, _)) = (xxxxx);
21.39 val tacis as (_::_) = (*case*) ts (*of*);
21.40 val (tac, _, _) = last_elem tacis;
21.41
21.42 (p, [] : NEW, TESTg_form (pt'''''_', p'''''_'), tac, Telem.Sundef, pt) (*return from me*);
21.43 -(*\\------------------ end step into --------------------------------------------------------//*)
21.44 +(*\------------------- end step into 1 -----------------------------------------------------/*)
21.45 +
21.46 +(*/------------------- begin step into 2 ---------------------------------------------------\*)
21.47 +val (p'''''_',_,f'''''_',nxt'''''_',_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = ("Rewrite_Set"*)
21.48 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', [], pt''''');
21.49 + (*case*)
21.50 + Step.by_tactic tac (pt, p) (*of*);
21.51 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
21.52 + val Applicable.Yes tac' = (*case*) Step.check tac (pt, p) (*of*);
21.53 +(*-------------------- stop step into -------------------------------------------------------*)
21.54 +
21.55 +(*\------------------- end step into 2 -----------------------------------------------------/*)
21.56
21.57 (* final test ...*)
21.58 -val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = ("Rewrite_Set"*)
21.59 -case nxt of (Rewrite_Set "norm_equation") => ()
21.60 -| _ => error "minisubpbl: Method not started in root-problem";
21.61 +if p'''''_' = ([1], Frm) andalso f2str f'''''_' = "x + 1 = 2"
21.62 +then case nxt'''''_' of (Rewrite_Set "norm_equation") => ()
21.63 + | _ => error "minisubpbl: Method not started in root-problem 1"
21.64 +else error "minisubpbl: Method not started in root-problem 2";
22.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sat May 02 17:39:04 2020 +0200
22.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon May 04 09:25:51 2020 +0200
22.3 @@ -20,19 +20,14 @@
22.4 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
22.5 (*[1], Frm*)val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (*nxt'''' = Rewrite_Set "norm_equation"*)
22.6
22.7 -(*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
22.8 - 1 relevant for original decomposition *)
22.9 +(*/------------------- begin step into 1 ---------------------------------------------------\*)
22.10 (*[1], Res*)val (p'''_',_,f,nxt'''_',_,pt'''_') = me nxt'''' p'''' [] pt'''';(*nxt = Rewrite_Set "Test_simplify"*)
22.11
22.12 -if p'''' = ([1], Frm) andalso f'''' = FormKF "x + 1 = 2"
22.13 -then case nxt'''' of Rewrite_Set _ => () | _ => error "start of test CHANGED 1"
22.14 -else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
22.15 +(*+*)if p'''' = ([1], Frm) andalso f'''' = FormKF "x + 1 = 2"
22.16 +(*+*)then case nxt'''' of Rewrite_Set _ => () | _ => error "start of test CHANGED 1"
22.17 +(*+*)else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
22.18
22.19 -(* val (p,_,f,nxt,_,pt) = ERROR WAS: nxt = ("Empty_Tac",..*) me nxt p [] pt;
22.20 -(* ERROR WAS: scan_dn1: call by ([3], Pbl) *)
22.21 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
22.22 -
22.23 -(*ERROR WAS: scan_dn1: call by ([3], Pbl)*)
22.24 val ("ok", (_, _, ptp''''')) = (*case*)
22.25 Step.by_tactic tac (pt, p) (*of*);
22.26 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
22.27 @@ -121,12 +116,10 @@
22.28 scan_up yyy (ist |> path_up) (go_up path prog);
22.29 "~~~~~ fun scan_up , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _)) =
22.30 (yyy, (ist |> path_up), (go_up path prog));
22.31 -
22.32 -(*\\--1 end step into relevant call ----------------------------------------------------------//*)
22.33 +(*\------------------- end step into 1 -----------------------------------------------------/*)
22.34
22.35 -(* nxt'''_' = Rewrite_Set "Test_simplify"
22.36 - //--2 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
22.37 - 2 relevant for exception TERM raised (line 297 of "term.ML"): dest_Free -1 + x = 0 *)
22.38 +(* nxt'''_' = Rewrite_Set "Test_simplify"*)
22.39 +(*/------------------- begin step into 2 ---------------------------------------------------\*)
22.40 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt'''_' p'''_' [] pt'''_';(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
22.41 (*+*)val p'''''_'' = p; (* keep for final test*)
22.42 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt'''_', p'''_', [], pt'''_');
22.43 @@ -232,7 +225,7 @@
22.44 val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
22.45 val dI = Context.theory_name (Stool.common_subthy (ThyC.get_theory dI, rootthy pt));
22.46 val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> Library.distinct op =);
22.47 -(*\\--2 end step into relevant call ----------------------------------------------------------//*)
22.48 +(*\------------------- end step into 2 -----------------------------------------------------/*)
22.49
22.50 val p = p'''''_''; (*kept from before stepping into detail*)
22.51
23.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sat May 02 17:39:04 2020 +0200
23.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon May 04 09:25:51 2020 +0200
23.3 @@ -135,15 +135,15 @@
23.4 val p' = next_in_prog po
23.5 val (p'', _, _,pt') =
23.6
23.7 - Generate.generate1 tac (istate, ctxt) (pt, (p', p_));
23.8 -"~~~~~ fun generate1 , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
23.9 + Step.add tac (istate, ctxt) (pt, (p', p_));
23.10 +"~~~~~ fun add , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
23.11 (l as (_, ctxt)), (pos as (p, p_)), pt)
23.12 = ((ThyC.get_theory "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
23.13 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
23.14 (oris, (domID, pblID, metID), hdl, ctxt_specify);
23.15
23.16 -(*+*)if ContextC.is_empty ctxt_specify then error "ERROR: generate1 should NOT get input ContextC.empty" else ();
23.17 -(*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "generate1 MUST store ctxt"
23.18 +(*+*)if ContextC.is_empty ctxt_specify then error "ERROR: Step.add should NOT get input ContextC.empty" else ();
23.19 +(*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "Step.add MUST store ctxt"
23.20 (*+*)else ();
23.21 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
23.22
24.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Sat May 02 17:39:04 2020 +0200
24.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon May 04 09:25:51 2020 +0200
24.3 @@ -78,7 +78,7 @@
24.4 (*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res')
24.5 (*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
24.6 ;
24.7 -"~~~~~ fun generate1 , args:"; val ((Check_Postcond' (_, scval)), l, (pt, (p, _))) =
24.8 +"~~~~~ fun add , args:"; val ((Check_Postcond' (_, scval)), l, (pt, (p, _))) =
24.9 (tac, (ist', ctxt'), (pt, (parent_pos, Res)));
24.10 val (pt,c) = append_result pt p l (scval, asm) Complete;
24.11
25.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Sat May 02 17:39:04 2020 +0200
25.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon May 04 09:25:51 2020 +0200
25.3 @@ -91,10 +91,10 @@
25.4
25.5 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
25.6
25.7 - val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
25.8 + val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
25.9 val pos' = ((lev_on o lev_dn) p, Frm)
25.10 val thy = ThyC.get_theory "Isac_Knowledge"
25.11 - val (_, _, _, pt') = Generate.generate1 tac_ (is, ctxt) (pt, pos') (* implicit Take *);
25.12 + val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *);
25.13
25.14 (** )val (_,_, (pt'', _)) =( **)
25.15 complete_solve CompleteSubpbl [] (pt', pos');
26.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Sat May 02 17:39:04 2020 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Mon May 04 09:25:51 2020 +0200
26.3 @@ -62,9 +62,10 @@
26.4 val pos = next_in_prog' pos;
26.5
26.6 (** )val (pos', c, _, pt) =( **)
26.7 - Generate.generate1 tac_ is (pt, pos);
26.8 -"~~~~~ fun generate1 , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
26.9 + Step.add tac_ is (pt, pos);
26.10 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
26.11 = (tac_, is, (pt, pos));
26.12 +(*+*)pos = ([1], Frm);
26.13
26.14 (** )val (pt, c) =( **)
26.15 cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
26.16 @@ -84,15 +85,78 @@
26.17 ((ic_form, SOME ic_res), f); (*return from if*)
26.18
26.19 insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
26.20 - result = f', ostate = s}) pt p (*return from append_atomic*); (*isa==REP*)
26.21 -"~~~~~ from fun append_atomic \<longrightarrow>funcappend_atomic , return:"; val (pt)
26.22 + result = f', ostate = s}) pt p (*return from append_atomic*);
26.23 +"~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)
26.24 = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
26.25 result = f', ostate = s}) pt p);
26.26
26.27 -(*/--------------------- final test ----------------------------------------------------------\\*)
26.28 +(*/--------------------- step into Deriv.embed -----------------------------------------------\*)
26.29 val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
26.30 - (*case*) Step_Solve.by_term ptp (encode ifo) (*of*);
26.31 + (*case*)
26.32 +Step_Solve.by_term ptp (encode ifo) (*of*);
26.33 +"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
26.34 + val SOME f_in =(*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
26.35 + val f_in = Thm.term_of f_in
26.36 + val pos_pred = lev_back(*'*) pos
26.37 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
26.38 + val f_succ = Ctree.get_curr_formula (pt, pos);
26.39 + (*if*) f_succ = f_in (*else*);
26.40 + val NONE =(*case*) In_Chead.cas_input f_in (*of*);
26.41
26.42 + (*case*)
26.43 + LI.locate_input_term (pt, pos) f_in (*of*);
26.44 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
26.45 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
26.46 + val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);
26.47 +
26.48 + (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
26.49 +"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
26.50 + val fo = Calc.current_formula ptp
26.51 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
26.52 + val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
26.53 + val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
26.54 + (*if*) found (*then*);
26.55 + val tacis' = map (State_Steps.make_single rew_ord erls) der;
26.56 +
26.57 + val (c', ptp) =
26.58 + Derive.embed tacis' ptp;
26.59 +"~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
26.60 + val (res, asm) = (State_Steps.result o last_elem) tacis
26.61 + val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
26.62 + (_, SOME (ist, ctxt)) => (ist, ctxt)
26.63 + | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
26.64 + val (f, _) = Ctree.get_obj Ctree.g_result pt p
26.65 + val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
26.66 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
26.67 + (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
26.68 + (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
26.69 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
26.70 + val (pt, c, pos as (p, _)) =
26.71 +
26.72 +Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
26.73 +"~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
26.74 +(*+*)length tacis = 8;
26.75 +(*+*)if State_Steps.to_string tacis = "[\"\n" ^
26.76 + "( End_Trans, End_Trans' xxx, ( ([2,6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], empty, NONE, \n2 + -1 + x = 2, ORundef, false, true) ))\",\"\n" ^
26.77 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,6], Res), Uistate ))\",\"\n" ^
26.78 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,5], Res), Uistate ))\",\"\n" ^
26.79 + "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2,4], Res), Uistate ))\",\"\n" ^
26.80 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,3], Res), Uistate ))\",\"\n" ^
26.81 + "( Rewrite (\"#: 1 + x = -1 + (2 + x)\", \"1 + x = -1 + (2 + x)\"), Rewrite' , ( ([2,2], Res), Uistate ))\",\"\n" ^
26.82 + "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2,1], Res), Uistate ))\",\"\n" ^
26.83 + "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
26.84 +then () else error "Derive.embed CHANGED";
26.85 +
26.86 + val (tacis', (_, tac_, (p, is))) = split_last tacis
26.87 +
26.88 +(*+*)val Begin_Trans' _ = tac_;
26.89 +
26.90 + val (p',c',_,pt') = generate1 tac_ is (pt, p)
26.91 +
26.92 +(*-------------------- stop step into -------------------------------------------------------*)
26.93 +(*\------------------- end step into -------------------------------------------------------/*)
26.94 +
26.95 +(*/--------------------- final test ----------------------------------------------------------\*)
26.96 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
26.97 ;
26.98 if
27.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Sat May 02 17:39:04 2020 +0200
27.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon May 04 09:25:51 2020 +0200
27.3 @@ -30,7 +30,7 @@
27.4 val t = @{term "ttt :: real"};
27.5
27.6 Auto_Prog.gen thy' t rls;
27.7 -"~~~~~ fun generate , args:"; val (thy, t, rls) = (thy', t, rls);
27.8 +"~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls);
27.9 val prog = case rls of
27.10 Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
27.11 | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules
28.1 --- a/test/Tools/isac/Test_Isac_Short.thy Sat May 02 17:39:04 2020 +0200
28.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon May 04 09:25:51 2020 +0200
28.3 @@ -186,7 +186,7 @@
28.4 ML_file "BaseDefinitions/error-fill-def.sml"
28.5 ML_file "BaseDefinitions/rule-set.sml"
28.6 ML_file "BaseDefinitions/check-unique.sml"
28.7 -(*called by Know_Store*)
28.8 +(*called by Know_Store..*)
28.9 ML_file "BaseDefinitions/calcelems.sml"
28.10 ML_file "BaseDefinitions/termC.sml"
28.11 ML_file "BaseDefinitions/substitution.sml"
28.12 @@ -195,6 +195,7 @@
28.13 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
28.14 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
28.15 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
28.16 +
28.17 ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
28.18 ML_file "ProgLang/listC.sml"
28.19 ML_file "ProgLang/prog_expr.sml"
29.1 --- a/test/Tools/isac/Test_Some.thy Sat May 02 17:39:04 2020 +0200
29.2 +++ b/test/Tools/isac/Test_Some.thy Mon May 04 09:25:51 2020 +0200
29.3 @@ -65,8 +65,10 @@
29.4 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
29.5 "xx"
29.6 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
29.7 -(*/------- step into -----------------------------------------------------------------------\*)
29.8 -(*\------- step into -----------------------------------------------------------------------/*)
29.9 +(*/------------------- begin step into -----------------------------------------------------\*)
29.10 +(*-------------------- stop step into -------------------------------------------------------*)
29.11 +(*\------------------- end step into -------------------------------------------------------/*)
29.12 +(* final test ...*)
29.13 \<close> ML \<open>
29.14 \<close>
29.15 ML \<open>
29.16 @@ -91,11 +93,227 @@
29.17 ML \<open>
29.18 \<close> ML \<open>
29.19 \<close> ML \<open>
29.20 +\<close> ML \<open>
29.21 \<close>
29.22
29.23 section \<open>===================================================================================\<close>
29.24 ML \<open>
29.25 \<close> ML \<open>
29.26 +(* Title: "Minisubpbl/250-Rewrite_Set-from-method.sml"
29.27 + Author: Walther Neuper 1105
29.28 + (c) copyright due to lincense terms.
29.29 +*)
29.30 +
29.31 +"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
29.32 +"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
29.33 +"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
29.34 +(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
29.35 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
29.36 +val (dI',pI',mI') =
29.37 + ("Test", ["sqroot-test","univariate","equation","test"],
29.38 + ["Test","squ-equ-test-subpbl1"]);
29.39 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)
29.40 + (*autoCalculate 1 CompleteCalcHead;*)
29.41 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
29.42 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
29.43 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
29.44 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
29.45 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
29.46 + (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
29.47 + (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
29.48 +
29.49 + (*autoCalculate 1 (Steps 1);*)
29.50 + (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
29.51 +
29.52 +(*+*)show_pt_tac pt; (*isa==REP [
29.53 +([], Frm), solve (x + 1 = 2, x)
29.54 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
29.55 +([1], Frm), x + 1 = 2
29.56 +. . . . . . . . . . Empty_Tac] *)
29.57 +
29.58 + (*appendFormula 1 "2+ -1 + x = 2";*)
29.59 +"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ -1 + x = 2");
29.60 + val cs = (*get_calc cI*) ((pt, p), []) (*..continue fun me*)
29.61 + val pos = (*get_pos cI 1*) p (*..continue fun me*)
29.62 +
29.63 + val ("ok", cs' as (_, _, ptp''''')) = (*case*)
29.64 + Step.do_next pos cs (*of*);
29.65 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
29.66 + val pIopt = Ctree.get_pblID (pt, ip);
29.67 + (*if*) ip = ([], Pos.Res) (*else*);
29.68 + val _ = (*case*) tacis (*of*);
29.69 + val SOME _ = (*case*) pIopt (*of*);
29.70 +
29.71 + Step.switch_specify_solve p_ (pt, ip);
29.72 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
29.73 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
29.74 +
29.75 + LI.do_next (pt, input_pos);
29.76 +"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
29.77 + (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
29.78 + val thy' = get_obj g_domID pt (par_pblobj pt p);
29.79 + val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
29.80 +
29.81 +val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
29.82 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
29.83 +
29.84 +(*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =
29.85 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
29.86 +"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
29.87 + val pos = next_in_prog' pos;
29.88 +
29.89 + (** )val (pos', c, _, pt) =( **)
29.90 + Step.add tac_ is (pt, pos);
29.91 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
29.92 + = (tac_, is, (pt, pos));
29.93 +(*+*)pos = ([1], Frm);
29.94 +
29.95 + (** )val (pt, c) =( **)
29.96 + cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
29.97 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;
29.98 +"~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
29.99 + = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
29.100 + (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);
29.101 + (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
29.102 + val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
29.103 + val (pt, cs) = cut_tree(*!*)pt (p, Frm);
29.104 + (** )val pt = ( **)
29.105 + append_atomic p (SOME ic_form, ic_res) f r f' s pt;
29.106 +"~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
29.107 + = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
29.108 + (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);
29.109 + val (iss, f) =
29.110 + ((ic_form, SOME ic_res), f); (*return from if*)
29.111 +
29.112 + insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
29.113 + result = f', ostate = s}) pt p (*return from append_atomic*);
29.114 +"~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)
29.115 + = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
29.116 + result = f', ostate = s}) pt p);
29.117 +\<close> ML \<open>
29.118 +\<close> ML \<open>
29.119 +\<close> ML \<open>
29.120 +\<close> ML \<open>
29.121 +\<close> ML \<open>
29.122 +
29.123 +(*/--------------------- step into Deriv.embed -----------------------------------------------\*)
29.124 + val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
29.125 + (*case*)
29.126 +Step_Solve.by_term ptp (encode ifo) (*of*);
29.127 +"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
29.128 + val SOME f_in =(*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
29.129 + val f_in = Thm.term_of f_in
29.130 + val pos_pred = lev_back(*'*) pos
29.131 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
29.132 + val f_succ = Ctree.get_curr_formula (pt, pos);
29.133 + (*if*) f_succ = f_in (*else*);
29.134 + val NONE =(*case*) In_Chead.cas_input f_in (*of*);
29.135 +
29.136 + (*case*)
29.137 + LI.locate_input_term (pt, pos) f_in (*of*);
29.138 +\<close> ML \<open>
29.139 +"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
29.140 + val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
29.141 + val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)
29.142 +
29.143 +\<close> ML \<open> (*generate1: not impl.for Rewrite' at ([1,1], Res)*)
29.144 + (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
29.145 +\<close> ML \<open>
29.146 +"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
29.147 + val fo = Calc.current_formula ptp
29.148 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
29.149 + val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
29.150 + val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
29.151 + (*if*) found (*then*);
29.152 + val tacis' = map (State_Steps.make_single rew_ord erls) der;
29.153 +
29.154 +\<close> ML \<open> (*generate1: not impl.for Rewrite' at ([1,1], Res)*)
29.155 + val (c', ptp) =
29.156 + Derive.embed tacis' ptp;
29.157 +"~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
29.158 + val (res, asm) = (State_Steps.result o last_elem) tacis
29.159 + val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
29.160 + (_, SOME (ist, ctxt)) => (ist, ctxt)
29.161 + | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
29.162 + val (f, _) = Ctree.get_obj Ctree.g_result pt p
29.163 + val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
29.164 + val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
29.165 + (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
29.166 + (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
29.167 + val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
29.168 + val (pt, c, pos as (p, _)) =
29.169 +
29.170 +Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
29.171 +"~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
29.172 +\<close> ML \<open>
29.173 +(*+*)length tacis = 8;
29.174 +\<close> ML \<open>
29.175 +(*+*)if State_Steps.to_string tacis = "[\"\n" ^
29.176 + "( End_Trans, End_Trans' xxx, ( ([2,6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], empty, NONE, \n2 + -1 + x = 2, ORundef, false, true) ))\",\"\n" ^
29.177 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,6], Res), Uistate ))\",\"\n" ^
29.178 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,5], Res), Uistate ))\",\"\n" ^
29.179 + "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2,4], Res), Uistate ))\",\"\n" ^
29.180 + "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,3], Res), Uistate ))\",\"\n" ^
29.181 + "( Rewrite (\"#: 1 + x = -1 + (2 + x)\", \"1 + x = -1 + (2 + x)\"), Rewrite' , ( ([2,2], Res), Uistate ))\",\"\n" ^
29.182 + "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2,1], Res), Uistate ))\",\"\n" ^
29.183 + "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
29.184 +then () else error "Derive.embed CHANGED";
29.185 +\<close> ML \<open>
29.186 +
29.187 + val (tacis', (_, tac_, (p, is))) = split_last tacis
29.188 +
29.189 +(*+*)val Begin_Trans' _ = tac_;
29.190 +
29.191 + val (p',c',_,pt') = generate1 tac_ is (pt, p)
29.192 +
29.193 +
29.194 +(*-------------------- stop step into -------------------------------------------------------*)
29.195 +(*\------------------- end step into -------------------------------------------------------/*)
29.196 +(*/--------------------- final test ----------------------------------------------------------\*)
29.197 +
29.198 +val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
29.199 +;
29.200 +if
29.201 + (ctxt_frm |> get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"
29.202 + andalso
29.203 + (ctxt_res |> get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"
29.204 + andalso
29.205 + Istate.string_of ist_res =
29.206 + "Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], empty, NONE, \n2 + -1 + x = 2, ORundef, false, true)"
29.207 +then () else error "/800-append-on-Frm.sml CHANGED";
29.208 +
29.209 +show_pt_tac (fst ptp''''');(*[
29.210 +([], Frm), solve (x + 1 = 2, x)
29.211 +. . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
29.212 +([1], Frm), x + 1 = 2
29.213 +. . . . . . . . . . Derive Test_simplify,
29.214 +([1,1], Frm), x + 1 = 2
29.215 +. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
29.216 +([1,1], Res), 1 + x = 2
29.217 +. . . . . . . . . . Rewrite ("#: 1 + x = -1 + (2 + x)", "1 + x = -1 + (2 + x)"),
29.218 +([1,2], Res), -1 + (2 + x) = 2
29.219 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
29.220 +([1,3], Res), -1 + (x + 2) = 2
29.221 +. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
29.222 +([1,4], Res), x + (-1 + 2) = 2
29.223 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
29.224 +([1,5], Res), x + (2 + -1) = 2
29.225 +. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
29.226 +([1,6], Res), 2 + -1 + x = 2
29.227 +. . . . . . . . . . Tactic.input_to_string not impl. for ?!,
29.228 +([1], Res), 2 + -1 + x = 2
29.229 +. . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]
29.230 +*)
29.231 +\<close> ML \<open>
29.232 +\<close> ML \<open>
29.233 +\<close> ML \<open>
29.234 +\<close> ML \<open>
29.235 +encode
29.236 +\<close> ML \<open>
29.237 +\<close> ML \<open>
29.238 +\<close> ML \<open>
29.239 +\<close> ML \<open>
29.240 +\<close> ML \<open>
29.241 \<close> ML \<open>
29.242 \<close>
29.243