separate Solve_Step.add, rearrange code, prep. Specify_Step
1 (* Title: 700-interSteps.sml
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
5 "----------- Minisubplb/700-interSteps.sml -----------------------";
6 "----------- Minisubplb/700-interSteps.sml -----------------------";
7 "----------- Minisubplb/700-interSteps.sml -----------------------";
8 (** adaption from rewtools.sml --- initContext..Thy_, fun context_thm ---,
9 *into a functional representation, i.e. we outcomment statements with side-effects:
11 ** CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
12 ** ("Test", ["sqroot-test","univariate","equation","test"],
13 ** ["Test","squ-equ-test-subpbl1"]))];
14 ** Iterator 1; moveActiveRoot 1;
15 ** autoCalculate 1 CompleteCalc;
17 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
18 ("Test", ["sqroot-test","univariate","equation","test"],
19 ["Test","squ-equ-test-subpbl1"]))];
20 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
23 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
25 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
37 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
39 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
40 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
42 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
43 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
46 (*+*)then case nxt of End_Proof' => ()
47 (*+*) | _ => error "calculation not finished correctly 1"
48 (*+*)else error "calculation not finished correctly 2";
49 (*+*)show_pt pt; (* 11 lines with subpbl *)
51 "----- no thy-context at result -----";
52 (** val p = ([], Res);
53 ** initContext 1 Thy_ p
54 *** = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;
55 ** val ((pt,_),_) = get_calc 1; (* 11 lines with subpbl *)
57 ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)
59 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([2], Res));
60 (** val ((pt, p), tacis) = get_calc cI;*)
61 val ip' = lev_pred' pt ip;
64 (*+*)ip' = ([1], Res);
66 (*+*)show_pt pt; (* 11 lines, as produced by autoCalculate CompleteCalc *)
68 val ("detailrls", pt''''', _) = (*case*) Detail_Step.go pt ip (*of*);
70 (*+*)show_pt pt'''''; (* added [2,1]..[2,6] after ([1], Res)*)
72 (*//-------------------------- 1. go down along calls to error ------------------------------\\*)
73 "~~~~~ fun go , args:"; val (pt, (pos as (p, _))) = (pt, ip);
75 (*+*)pos = ([2], Res);
77 val nd = Ctree.get_nd pt p
78 val cn = Ctree.children nd
80 (*if*) null cn (*then*);
81 (*if*) (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] (*then*);
83 Detail_Step.detailrls pt pos;
84 "~~~~~ fun detailrls , args:"; val (pt, (pos as (p, _))) = (pt, pos);
85 val t = get_obj g_form pt p
86 val tac = get_obj g_tac pt p
87 val rls = (assoc_rls o Tactic.rls_of) tac
88 val ctxt = get_ctxt pt pos
89 val _ = (*case*) rls (*of*);
90 val is = Generate.init_istate tac t
92 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
94 val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
95 val pos' = ((lev_on o lev_dn) p, Frm)
96 val thy = ThyC.get_theory "Isac_Knowledge"
97 val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *);
99 (** )val (_,_, (pt'', _)) =( **)
100 complete_solve CompleteSubpbl [] (pt', pos');
101 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
102 = (CompleteSubpbl, [], (pt', pos'));
103 (*if*) p = ([], Res) (*else*);
104 (*if*) Library.member op = [Pbl,Met] p_ (*else*);
106 val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) =
107 (*case*) Step_Solve.do_next ptp (*of*);
109 (*+*)c' = [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)];
110 (*+*)show_pt (fst ptp');(*[
111 (([], Frm), solve (x + 1 = 2, x)),
112 (([1], Frm), x + 1 = 2),
113 (([1], Res), x + 1 + -1 * 2 = 0),
114 (([2,1], Frm), x + 1 + -1 * 2 = 0),
115 (([2,1], Res), 1 + x + -1 * 2 = 0)]*)
117 (*+*)val (keep_c', keep_ptp') = (c', ptp');
118 "~~~~~ and Step_Solve.do_next , args:"; val () = ();
120 NOTE: prog.xxx found by LItool.resume_prog from Rule_Set.Repeat {scr = Prog xxx, ...}*)
122 (*+*)val (c', ptp') = (keep_c', keep_ptp');
124 (** )val (_, c', ptp') =( **)
125 complete_solve auto (c @ c') ptp';
126 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
127 = (auto, (c @ c'), ptp');
128 (*if*) p = ([], Res) (*else*);
129 (*if*) Library.member op = [Pbl,Met] p_ (*else*);
131 val (_, ([(Rewrite ("add.assoc", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
132 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
133 = (auto, (c @ c'), ptp');
134 (*if*) p = ([], Res) (*else*);
135 (*if*) Library.member op = [Pbl,Met] p_ (*else*);
136 val (_, ([(Calculate "TIMES", _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
138 show_pt (fst ptp'); (* added [2,1]..[2,3], more to come *)
139 (*\\-------------------------- 1. go down along calls to error ------------------------------//*)
142 ** interSteps 1 ([3,1], Res);
144 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([3,1], Res));
145 (**val ((pt, p), tacis) = get_calc cI;*)
146 val ip' = lev_pred' pt ip;
148 (*+*)ip = ([3, 1], Res);
149 (*+*)ip' = ([3, 1], Frm);
151 val ("detailrls", pt, _) = (*case*) Detail_Step.go pt''''' ip (*of*);
153 show_pt pt; (* added ([3,1,1], Frm), ([3,1,1], Res) after ([3,1], Frm)*)
155 (*---------- final test ----------------------------------------------------------\\*)
156 if pr_ctree pr_short pt =
157 ". ----- pblobj -----\n1" ^
159 "2. x + 1 + -1 * 2 = 0\n" ^
160 "2.1. x + 1 + -1 * 2 = 0\n" ^
161 "2.2. 1 + x + -1 * 2 = 0\n" ^
162 "2.3. 1 + (x + -1 * 2) = 0\n" ^
163 "2.4. 1 + (x + -2) = 0\n" ^
164 "2.5. 1 + (-2 + x) = 0\n" ^
165 "2.6. -2 + (1 + x) = 0\n" ^
166 "3. ----- pblobj -----\n" ^
167 "3.1. -1 + x = 0\n" ^
168 "3.1.1. -1 + x = 0\n" ^
169 (*([3,1,1], Res), x = 0 + -1 * -1) only shown by show_pt*)
170 "3.2. x = 0 + -1 * -1\n" ^(* another difference to show_pt*)
172 (*". [x = 1]" only shown by show_pt*)
173 then () else error "intermediate steps CHANGED";