1 (* Title: "Minisubpbl/250-Rewrite_Set-from-method.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
7 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
8 "----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";
9 (*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)
10 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
12 ("Test", ["sqroot-test", "univariate", "equation", "test"],
13 ["Test", "squ-equ-test-subpbl1"]);
14 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];(*Model_Problem*)
15 (*autoCalculate 1 CompleteCalcHead;*)
16 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "equality (x + 1 = 2)" = nxt;
17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "solveFor x" = nxt;
18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Find "solutions L" = nxt;
19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Specify_Theory "Test" = nxt;
20 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = nxt;
21 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
22 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = nxt;
24 (*autoCalculate 1 (Steps 1);*)
25 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Rewrite_Set "norm_equation" = nxt;
27 (*+*)Test_Tool.show_pt_tac pt; (*isa==REP [
28 ([], Frm), solve (x + 1 = 2, x)
29 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
31 . . . . . . . . . . Empty_Tac] *)
33 (*appendFormula 1 "2+ - 1 + x = 2";*)
34 "~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ - 1 + x = 2");
35 val cs = (*States.get_calc cI*) ((pt, p), []) (*..continue fun me*)
36 val pos = (*States.get_pos cI 1*) p (*..continue fun me*)
38 val ("ok", cs' as (_, _, ptp''''')) = (*case*)
39 Step.do_next pos cs (*of*);
40 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (pos, cs);
41 val pIopt = Ctree.get_pblID (pt, ip);
42 (*if*) ip = ([], Pos.Res) (*else*);
43 val _ = (*case*) tacis (*of*);
44 val SOME _ = (*case*) pIopt (*of*);
46 Step.switch_specify_solve p_ (pt, ip);
47 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
48 (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
50 LI.do_next (pt, input_pos);
51 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
52 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
53 val thy' = get_obj g_domID pt (par_pblobj pt p);
54 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
56 val Next_Step (ist, ctxt, tac) = (*case*) (**..Ctree NOT updated yet**)
57 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
59 (*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =
60 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
61 "~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
62 val pos = next_in_prog' pos;
64 (** )val (pos', c, _, pt) =( **)
65 Step.add tac_ is (pt, pos);
66 "~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
67 = (tac_, is, (pt, pos));
68 (*+*)pos = ([1], Frm);
70 (** )val (pt, c) =( **)
71 cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f
72 (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;
73 "~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
74 = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
75 (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);
76 (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
77 val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
78 val (pt, cs) = cut_tree(*!*)pt (p, Frm);
80 append_atomic p (SOME ic_form, ic_res) f r f' s pt;
81 "~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
82 = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
83 (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);
85 ((ic_form, SOME ic_res), f); (*return from if*)
87 insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
88 result = f', ostate = s}) pt p (*return from append_atomic*);
89 "~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)
90 = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,
91 result = f', ostate = s}) pt p);
93 (*/--------------------- step into Deriv.embed -----------------------------------------------\*)
94 val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =
96 Step_Solve.by_term ptp (encode ifo) (*of*);
97 "~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));
98 val SOME f_in =(*case*) ParseC.term_opt (get_ctxt pt pos) istr (*of*);
99 val pos_pred = lev_back(*'*) pos
100 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
101 val f_succ = Ctree.get_curr_formula (pt, pos);
102 (*if*) f_succ = f_in (*else*);
103 val NONE =(*case*) CAS_Cmd.input f_in (*of*);
106 LI.locate_input_term (pt, pos) f_in (*of*);
107 "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
108 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
109 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);
111 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
112 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
113 val fo = Calc.current_formula ptp
114 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
115 val {rew_ord, asm_rls, rules, ...} = Rule_Set.rep rew_rls
118 Derive.steps ctxt rew_ord asm_rls rules fo ifo; (*<---------------*)
119 (*//------------------ step into Derive.steps ----------------------------------------------\\*)
120 "~~~~~ fun steps , args:"; val (ctxt, rew_ord, asm_rls, rules, fo, ifo) =
121 (ctxt, rew_ord, asm_rls, rules, fo, ifo);
122 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
123 | derivat dt = (#1 o #3 o last_elem) dt
124 fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
125 val fod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE fo
126 val ifod = Derive.do_one ctxt asm_rls rules (snd rew_ord) NONE ifo
128 (*case*) (fod, ifod) (*of*);
129 (*if*) derivat fod = derivat ifod (*common normal form found*) (*then*);
130 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
132 (*/--- local to steps ---\*)
133 fun rev_deriv' ctxt (t, r, (t', a)) = (t', ThmC.make_sym_rule ctxt r, (t, a));
134 (*\--- local to steps ---/*)
135 val return = (true, fod' @ (map
136 (rev_deriv' ctxt) rifod'));
137 "~~~~~ fun rev_deriv' , args:"; val (ctxt, (t, r, (t', a))) = (ctxt, nth 1 rifod');
140 ThmC.make_sym_rule ctxt r, (t, a));
141 "~~~~~ fun make_sym_rule_PIDE , args:"; val (ctxt ,(Rule.Thm (thmID, thm))) = (ctxt, r);
143 val thm' = sym_thm thm
144 val thmID' = case Symbol.explode thmID of
145 "s" :: "y" :: "m" :: "_" :: id => implode id
146 | "#" :: ":" :: _ => "#: " ^ string_of_thm ctxt thm'
147 | _ => "sym_" ^ thmID;
148 (*-------------------- stop step into Derive.steps -------------------------------------------*)
149 (*\\------------------ step into Derive.steps ----------------------------------------------//*)
151 (*if*) found (*then*);
152 val tacis' = map (State_Steps.make_single ctxt rew_ord asm_rls) der;
155 Derive.embed tacis' ptp;
156 "~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
157 val (res, asm) = ((State_Steps.result ctxt) o last_elem) tacis
158 val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
159 (_, SOME (ist, ctxt)) => (ist, ctxt)
160 | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
161 val (f, _) = Ctree.get_obj Ctree.g_result pt p
162 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
163 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
164 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
165 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
166 val {rew_rls, ...} = MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
168 val (pt, c, pos as (p, _)) =
169 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
170 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
171 (*+*)length tacis = 8;
172 (*+*)if State_Steps.to_string ctxt tacis = "[\"\n" ^
173 "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^
174 "(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true) ))\", \"\n" ^
175 "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 6], Res), Uistate ))\", \"\n" ^
176 "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 5], Res), Uistate ))\", \"\n" ^
177 "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2, 4], Res), Uistate ))\", \"\n" ^
178 "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 3], Res), Uistate ))\", \"\n" ^
179 "( Rewrite (\"#: 1 + x = - 1 + (2 + x)\", \"1 + x = - 1 + (2 + x)\"), Rewrite' , ( ([2, 2], Res), Uistate ))\", \"\n" ^
180 "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2, 1], Res), Uistate ))\", \"\n" ^
181 "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
182 (*+*)then () else error "Derive.embed CHANGED";
184 val (tacis', (_, tac_, (p, is))) = split_last tacis
186 (*+*)val Begin_Trans' _ = tac_;
187 (*-------------------- stop step into -------------------------------------------------------*)
188 (*\------------------- end step into -------------------------------------------------------/*)
191 Specify_Step.add tac_ is (pt, p);
192 "~~~~~ fun add , args:"; val ((Tactic.Begin_Trans' t), l, (pt, (p, Frm))) =
194 val (pt, c) = Ctree.cappend_form pt p l t
195 val pt = Ctree.update_branch pt p Ctree.TransitiveB
196 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
197 val (pt, c') = Ctree.cappend_form pt p l t
198 val return = ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term ctxt t), pt)
200 (*/--------------------- final test ----------------------------------------------------------\*)
201 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
204 (ctxt_frm |> ContextC.get_assumptions |> UnparseC.terms ctxt) = "[precond_rootmet x]"
206 (ctxt_res |> ContextC.get_assumptions |> UnparseC.terms ctxt) = "[precond_rootmet x]"
208 Istate.string_of ctxt ist_res =
209 "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"
210 then () else error "/800-append-on-Frm.sml CHANGED";
212 Test_Tool.show_pt_tac (fst ptp''''');(*[
213 ([], Frm), solve (x + 1 = 2, x)
214 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
215 ([1], Frm), x + 1 = 2
216 . . . . . . . . . . Derive Test_simplify,
217 ([1,1], Frm), x + 1 = 2
218 . . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
219 ([1,1], Res), 1 + x = 2
220 . . . . . . . . . . Rewrite ("#: 1 + x = - 1 + (2 + x)", "1 + x = - 1 + (2 + x)"),
221 ([1,2], Res), - 1 + (2 + x) = 2
222 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
223 ([1,3], Res), - 1 + (x + 2) = 2
224 . . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
225 ([1,4], Res), x + (- 1 + 2) = 2
226 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
227 ([1,5], Res), x + (2 + - 1) = 2
228 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
229 ([1,6], Res), 2 + - 1 + x = 2
230 . . . . . . . . . . Tactic.input_to_string not impl. for ?!,
231 ([1], Res), 2 + - 1 + x = 2
232 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]]