1 (* Title: "Minisubpbl/300-init-subpbl.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
7 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
8 "----------- Minisubpbl/300-init-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 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
21 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation"*)
22 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify" *)
23 (*[2], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)
24 (*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
25 1 relevant for updating ctxt *)
26 "~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
28 "~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
29 val (mI,m) = mk_tac'_ tac;
30 val Appl m = applicable_in p pt m;
31 member op = specsteps mI; (*false*)
32 (*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
33 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
34 (*val (msg, cs') = solve m (pt, pos);*)
35 "~~~~~ fun solve , args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
36 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
37 val thy' = get_obj g_domID pt (par_pblobj pt p);
38 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
40 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
41 "~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
42 = (sc, (pt, po), (fst is), (snd is), m);
43 val srls = get_simplifier cstate;
45 (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
46 "~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.Pstate (E,l,rls,a,v,asap,S,b), ctxt))
47 = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
48 (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)
49 (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
50 (*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
51 (astep_up (thy',srls,scr,d) ((E,l,a,v,asap,S,b), [(m,EmptyMout,pt,p,[])]) );*)
52 "~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,asap,S,b),ss))
53 = ((ctxt,srls,scr, (pt, p)), ((E,l,a,v,asap,S,b), m));
54 (*if*) 1 < length l (*true*);
57 ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
58 "~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Tactical.Try",_) $ e)) =
59 (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
61 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
62 (*if*) 1 < length l; (*then*)
65 ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
66 "~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ )) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
68 astep_up ysa iss (*2*: comes from e2*);
69 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
70 (*if*) 1 < length l; (*then*)
73 ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
74 "~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Tactical.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
76 astep_up ysa iss (*all has been done in (*2*) below*);
77 "~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,rls,a,v,asap,S,b),ss)) = (ysa, iss);
78 (*if*) 1 < length l; (*then*)
81 ass_up ys ((E,up,rls,a,v,asap,S,b),ss) (go up sc);
82 "~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ _))
83 = (ys, ((E,up,rls,a,v,asap,S,b),ss), (go up sc));
84 val l = drop_last l; (*comes from e, goes to Abs*)
87 Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
88 | t => error ("ass_up..HOL.Let $ _ with " ^ Rule.term2str t))
89 val i = TermC.mk_Free (i, T);
90 val E = Env.upd_env E (i, v);
92 (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss) body (*of*);
93 "~~~~~ fun assy , args:"; val (ya, ((E,l,rls,a,v,asap,S,b),ss), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
94 = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], rls,a,v,asap,S,b),ss), body);
96 (*case*) assy ya ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss) e (*of*);
97 (*======= end of scanning tacticals, a leaf =======*)
98 "~~~~~ fun assy , args:"; val ((ctxt,sr,(pt,p),ap), ((E,l,rls,a,v,asap,S,_), m), t)
99 = (ya, ((E , l @ [Celem.L, Celem.R], rls,a,v,asap,S,b), ss), e);
101 (*val (a', STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr (E, (a, v)) t (*of*);
102 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
103 = ("locate", "Isac_Knowledge", sr, (E, (a, v)), t);
105 val (a', STac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
106 "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
109 (NONE, STac (subst_atomic E t)); (*return value*)
110 "~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', STac stac))
111 = ((NONE : term option, STac (subst_atomic E t)));
113 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
115 (*return value*) (a', STac stac');
116 "~~~~~ from handle_leaf to assy return val:"; val (a', STac stac)
117 = ((a' : term option, STac stac'));
118 val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
120 (*+*)if is_e_ctxt ctxt then error "ERROR: assy returns e_ctxt" else ();
121 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
123 val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';
125 if p = ([3], Pbl) andalso not (get_ctxt pt p |> is_e_ctxt)
127 case nxt of ("Model_Problem", _) => ()
128 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"
129 else error "Minisubpbl/300-init-subpbl.sml changed";