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;
45 then case nxt of ("End_Proof'", End_Proof') => ()
46 | _ => error "calculation not finished correctly 1"
47 else error "calculation not finished correctly 2";
48 show_pt pt; (* 11 lines with subpbl *)
50 "----- no thy-context at result -----";
51 (** val p = ([], Res);
52 ** initContext 1 Thy_ p
53 *** = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;
54 ** val ((pt,_),_) = get_calc 1; (* 11 lines with subpbl *)
56 ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)
58 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([2], Res));
59 (** val ((pt, p), tacis) = get_calc cI;*)
60 val ip' = lev_pred' pt ip;
61 val ("detailrls", pt, _(*lastpos*)) = (*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);
62 show_pt pt; (* added [2,1]..[2,6] *)
65 ** interSteps 1 ([3,1], Res); (* added [3,1,1] Frm + Res *)
66 ** val ((pt,_),_) = get_calc 1;
67 ** show_pt pt; (*show 6 + 2 steps added*)
69 ** if existpt' ([1,1,1], Frm) pt then ()
70 ** else error "integrate.sml: interSteps on Rewrite_Set_Inst";
73 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([3,1], Res));
74 (**val ((pt, p), tacis) = get_calc cI;*)
75 (*if*) (not o is_interpos) ip (* = false*);
76 val ip' = lev_pred' pt ip;
77 (*case*) Math_Engine.detailstep pt ip (*of*) (* LOST ([3,1,1], Frm) .. ([], Res), [x = 1]*);
79 "~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
80 val nd = Ctree.get_nd pt p
81 val cn = Ctree.children nd;
82 (*if*) null cn (* = true*);
83 (*if*) (Tac.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] (* = true*)
85 (* ?!?: in spite of exception PTREE "ins_chn: pos mustNOT be overwritten" insertion OK ?!?*)
86 (* Solve.detailrls pt pos (* LOST ([3,1,1], Frm) ff.. ([], Res), [x = 1]*) *)
88 "~~~~~ fun detailrls, args:"; val (pt, (pos as (p, _))) = (pt, pos);
89 val t = get_obj g_form pt p
90 val tac = get_obj g_tac pt p
91 val rls = (assoc_rls o Tac.rls_of) tac
92 val ctxt = get_ctxt pt pos;
94 val is = Generate.init_istate tac t
95 val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
96 val pos' = ((lev_on o lev_dn) p, Frm)
97 val thy = Celem.assoc_thy "Isac"
98 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *);
100 show_pt pt'; (* cut ctree after ([3,1,1], Frm) *)
102 (* val (_,_, (pt'', _)) =*) complete_solve CompleteSubpbl [] (pt', pos')
104 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (CompleteSubpbl, [], (pt', pos'));
105 (*if*) p = ([], Res) (* = false*);
106 (*if*) member op = [Pbl,Met] p_ (* = false*);
107 (*case*) do_solve_step ptp (*of*)
109 "~~~~~ and do_solve_step, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
110 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false isabisac = ?*);
111 val thy' = get_obj g_domID pt (par_pblobj pt p);
112 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
113 (* val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
115 "~~~~~ fun determine_next_tactic, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
116 (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
117 (*if*) l = [] (* = true *);
118 appy thy ptp E [Celem.R] body NONE v;
120 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Repeat"(*2*),_) $ e), a, v) =
121 (thy, ptp, E, [Celem.R], body, NONE, v);
122 appy thy ptp E (l @ [Celem.R]) e a v;
124 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a), _, v) =
125 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
126 (*case*) appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v (*of*);
128 "~~~~~ fun appy, args:"; val (thy, ptp, E, l,(Const ("Script.Try"(*1*),_) $ e), a, v) =
129 (thy, ptp, E, (l @ [Celem.L, Celem.L, Celem.R]), e1, (SOME a), v);
130 (*case*) appy thy ptp E (l @ [Celem.R]) e a v (*of*);
132 "~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Repeat"(*2*),_) $ e), a, v) =
133 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
134 appy thy ptp E (l @ [Celem.R]) e a v;
136 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
137 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
138 val (a', LTool.STac stac) = (*case*) handle_leaf "next " th sr E a v t (*of*)
139 val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
141 (**)Rewrite_Inst ([_(*"(''bdv'', x)"*)], ("risolate_bdv_add", _)) => ();
142 (*case*) Applicable.applicable_in p pt m (*of*);
144 "~~~~~ fun applicable_in, args:"; val ((p, p_), pt, (m as Tac.Rewrite_Inst (subs, thm''))) =
146 (*if*) member op = [Pbl, Met] p_ (* = false in isabisac*);
147 val pp = par_pblobj pt p;
148 val thy' = get_obj g_domID pt pp;
149 val thy = Celem.assoc_thy thy';
150 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
151 val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
152 Frm => (get_obj g_form pt p, p)
153 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
154 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
155 val subst = Selem.subs2subst thy subs;
156 val SOME (f',asm) = (*case*) Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f (*of*)
158 Chead.Appl (Tac.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))