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) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)
15 (*autoCalculate 1 CompleteCalcHead;*)
16 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)
17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "solveFor x"*)
18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)
19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)
20 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)
21 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
22 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
24 (*autoCalculate 1 (Steps 1);*)
25 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
27 (*+*)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 = (*get_calc cI*) ((pt, p), []) (*..continue fun me*)
36 val pos = (*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*) Library.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*) Method.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 thy' (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*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
99 val f_in = Thm.term_of f_in
100 val pos_pred = lev_back(*'*) pos
101 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
102 val f_succ = Ctree.get_curr_formula (pt, pos);
103 (*if*) f_succ = f_in (*else*);
104 val NONE =(*case*) Input_Spec.cas_input f_in (*of*);
107 LI.locate_input_term (pt, pos) f_in (*of*);
108 "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
109 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
110 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);
112 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
113 "~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);
114 val fo = Calc.current_formula ptp
115 val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
116 val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls
117 val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)
118 (*if*) found (*then*);
119 val tacis' = map (State_Steps.make_single rew_ord erls) der;
122 Derive.embed tacis' ptp;
123 "~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);
124 val (res, asm) = (State_Steps.result o last_elem) tacis
125 val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
126 (_, SOME (ist, ctxt)) => (ist, ctxt)
127 | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
128 val (f, _) = Ctree.get_obj Ctree.g_result pt p
129 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
130 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
131 (State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm),
132 (Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];
133 val {nrls, ...} = Method.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
134 val (pt, c, pos as (p, _)) =
136 Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));
137 "~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));
138 (*+*)length tacis = 8;
139 (*+*)if State_Steps.to_string tacis = "[\"\n" ^
140 "( 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" ^
141 "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,6], Res), Uistate ))\",\"\n" ^
142 "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,5], Res), Uistate ))\",\"\n" ^
143 "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2,4], Res), Uistate ))\",\"\n" ^
144 "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2,3], Res), Uistate ))\",\"\n" ^
145 "( Rewrite (\"#: 1 + x = -1 + (2 + x)\", \"1 + x = -1 + (2 + x)\"), Rewrite' , ( ([2,2], Res), Uistate ))\",\"\n" ^
146 "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2,1], Res), Uistate ))\",\"\n" ^
147 "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"
148 then () else error "Derive.embed CHANGED";
150 val (tacis', (_, tac_, (p, is))) = split_last tacis
152 (*+*)val Begin_Trans' _ = tac_;
154 val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p)
156 (*-------------------- stop step into -------------------------------------------------------*)
157 (*\------------------- end step into -------------------------------------------------------/*)
159 (*/--------------------- final test ----------------------------------------------------------\*)
160 val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))
163 (ctxt_frm |> get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"
165 (ctxt_res |> get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"
167 Istate.string_of ist_res =
168 "Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], empty, NONE, \n2 + -1 + x = 2, ORundef, false, true)"
169 then () else error "/800-append-on-Frm.sml CHANGED";
171 show_pt_tac (fst ptp''''');(*[
172 ([], Frm), solve (x + 1 = 2, x)
173 . . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
174 ([1], Frm), x + 1 = 2
175 . . . . . . . . . . Derive Test_simplify,
176 ([1,1], Frm), x + 1 = 2
177 . . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
178 ([1,1], Res), 1 + x = 2
179 . . . . . . . . . . Rewrite ("#: 1 + x = -1 + (2 + x)", "1 + x = -1 + (2 + x)"),
180 ([1,2], Res), -1 + (2 + x) = 2
181 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
182 ([1,3], Res), -1 + (x + 2) = 2
183 . . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),
184 ([1,4], Res), x + (-1 + 2) = 2
185 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
186 ([1,5], Res), x + (2 + -1) = 2
187 . . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),
188 ([1,6], Res), 2 + -1 + x = 2
189 . . . . . . . . . . Tactic.input_to_string not impl. for ?!,
190 ([1], Res), 2 + -1 + x = 2
191 . . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"]]