1 (* Title: "Minisubplb/400-start-meth-subpbl.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";
7 "----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";
8 "----------- Minisubpbl/400-start-meth-subpbl.sml ----------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
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; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
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;
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
32 (*//--1 begin step into relevant call ---------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-------\\
33 1 relevant for all Apply_Method *)
34 (*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt no initialised by specify, PblObj{ctxt,...}" else ();
35 (*+*)if get_ctxt pt p |> ContextC.is_empty then error "ctxt NOT initialised by Subproblem'}" else ();
36 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
38 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
40 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
41 Step.by_tactic tac (pt, p) (*of*);
42 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
43 val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
44 (*if*) Tactic.for_specify' m; (*false*)
46 Step_Solve.by_tactic m ptp;
47 "~~~~~ fun by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p, _))))
49 val itms = case get_obj I pt p of
50 PblObj {meth=itms, ...} => itms
51 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
52 val thy' = get_obj g_domID pt p;
53 val thy = ThyC.get_theory thy';
54 val srls = LItool.get_simplifier (pt, pos)
55 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
56 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
57 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
59 (*+*)val (pt, p) = case Step.by_tactic tac (pt, pos) of
60 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
61 (*+*)val SOME t = parseNEW (get_ctxt pt p) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
63 "~~~~~ from Step_Solve.by_tactic to..to me return"; val (pt, p) = (pt'''', p'''');
65 val ("ok", ([(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), _, (_, (Pstate _, _)))], _, _)) = (*case*)
66 Step.do_next p ((pt, e_pos'), []) (*of*);
67 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p'''', ((pt'''', e_pos'), []))
68 val pIopt = get_pblID (pt,ip);
70 Library.member op = [Pbl,Met] p_ (*= false*);
72 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
73 val thy' = get_obj g_domID pt (par_pblobj pt p);
74 val (is, sc) = resume_prog thy' (p,p_) pt;
76 "~~~~~ fun find_next_step , args:"; val ((thy, _), (ptp as (pt, (p, _))), sc, (Istate.Pstate ist, _(*ctxt*)))
77 = ((thy',srls), (pt,pos), sc, is);
79 (*+*)val SOME t = parseNEW (get_ctxt pt pos) "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
80 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
82 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = Rewrite_Set_Inst isolate_bdv*);
84 if p = ([3, 1], Frm) andalso f2str f = "-1 + x = 0" andalso
85 Tactic.input_to_string nxt = "Rewrite_Set_Inst ([(''bdv'', x)], \"isolate_bdv\")"
86 then () else error "Minisubpbl/400-start-meth-subpbl changed";