1 (*//------------------ begin step into ------------------------------------------------------\\*)
2 (*\\------------------ end step into --------------------------------------------------------//*)
3 (* Title: "Minisubpbl/300-init-subpbl.sml"
4 Author: Walther Neuper 1105
5 (c) copyright due to lincense terms.
8 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
9 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
10 "----------- Minisubpbl/300-init-subpbl.sml ----------------------";
11 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
13 ("Test", ["sqroot-test","univariate","equation","test"],
14 ["Test","squ-equ-test-subpbl1"]);
15 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
16 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;
22 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
23 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation"*)
24 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify" *)
25 (*[2], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)
26 (*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
27 1 relevant for updating ctxt *)
28 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
30 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
31 Step.by_tactic tac (pt, p) (*of*);
32 get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)
33 "~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
34 val Appl m = applicable_in p pt tac;
35 (*if*) Tactic.for_specify' m; (*false*)
38 Step_Solve.by_tactic m (pt, p);
39 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, p));
40 (*if*) e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
41 val thy' = get_obj g_domID pt (par_pblobj pt p);
42 val (is, sc) = resume_prog thy' (p,p_) pt;
44 val Safe_Step (Pstate ist''''', ctxt''''', tac'_''''') =
45 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
46 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog prog, cstate, istate, ctxt, tac)
47 = (sc, (pt, po), (fst is), (snd is), m);
49 val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
50 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
51 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Pstate (ist as {path, ...})))
52 = ((prog, (cstate, ctxt, tac)), istate);
53 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
55 go_scan_up1 (prog, cctt) ist;
56 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, act_arg, ...}))
57 = ((prog, cctt), ist);
58 (*if*) 1 < length path (*true*);
60 scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
61 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Try"(*2*), _) $ _))
62 = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
65 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
67 (*if*) 1 < length path (*true*);
69 scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
70 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
71 = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
73 go_scan_up1 pcct ist (*2*: comes from e2*);
74 "~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
76 (*if*) 1 < length path (*true*);
78 scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
79 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _))
80 = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
82 go_scan_up1 pcct ist (*all has been done in (*2*) below*);
83 "~~~~~ fun go_scan_up1, args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
85 (*if*) 1 < length path (*true*);
87 scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog);
88 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _))
89 = (pcct, (ist |> path_up), (at_location (path_up' path) prog));
90 val (i, body) = check_Let_up ist prog;
92 (*case*) scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*);
93 "~~~~~ fun scan_dn1 , args:"; val (cct, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
94 = (cct, (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef), body);
96 (*case*) scan_dn1 cct (ist |> path_down [L, R]) e (*of*);
97 (*======= end of scanning tacticals, a leaf =======*)
98 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
99 = (cct, (ist |> path_down [L, R]), e);
101 val (Program.Tac _, NONE) = (*case*)
102 check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
103 "~~~~~ fun check_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
104 = ("locate", ctxt, eval, (get_subst ist), t);
106 val (Program.Tac stac, a) = (*case*) Prog_Tac.eval_leaf E a v t (*of*);
107 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
110 (Program.Tac (subst_atomic E t), NONE); (*return value*)
111 "~~~~~ from fun eval_leaf \<longrightarrow> fun check_leaf return val:"; val ((Program.Tac stac, a'))
112 = ((Program.Tac (subst_atomic E t), NONE : term option));
114 Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
115 (subst_atomic (Env.update_opt E (a,v)) stac);
117 (Program.Tac stac', a'); (*return from check_leaf*)
118 "~~~~~ from fun check_leaf \<longrightarrow> fun scan_dn1 return val:"; val (Program.Tac prog_tac, form_arg)
119 = (Program.Tac stac', a' : term option);
121 (Program.Tac prog_tac, form_arg) (*return from check_leaf*);
123 check_tac1 cct ist (prog_tac, form_arg) (*return from scan_dn1*);
124 "~~~~~ from fun scan_dn1\<longrightarrow>fun scan_up1 HOL.Let(*1*), return:"; val (Accept_Tac1 iss)
125 = (check_tac1 cct ist (prog_tac, form_arg));
127 (*+*)val (pstate, ctxt, tac) = iss;
128 (*+*)if ContextC.is_empty ctxt then error "ERROR: scan_dn1 should NOT return ContextC.empty" else ();
129 "~~~~~ from fun scan_up1 HOL.Let(*1*), --------------------------------- NO return:"; val () = ();
131 (*+*)if ContextC.is_empty ctxt''''' then error "locate_input_tactic should NOT return ContextC.empty" else ();
133 "~~~~~ from fun locate_input_tactic \<longrightarrow>Step_Solve.by_tactic , return:"; val (LI.Safe_Step (istate, ctxt, tac))
134 = (Safe_Step (Pstate ist''''', ctxt''''', tac'_'''''));
135 val p' = next_in_prog po
136 val (p'', _, _,pt') =
138 Generate.generate1 tac (istate, ctxt) (pt, (p', p_));
139 "~~~~~ fun generate1 , args:"; val (thy, (Tactic.Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt_specify, f)),
140 (l as (_, ctxt)), (pos as (p, p_)), pt)
141 = ((Celem.assoc_thy "Isac_Knowledge"), tac, (istate, ctxt), (p', p_), pt);
142 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
143 (oris, (domID, pblID, metID), hdl, ctxt_specify);
145 (*+*)if ContextC.is_empty ctxt_specify then error "ERROR: generate1 should NOT get input ContextC.empty" else ();
146 (*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "generate1 MUST store ctxt"
148 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
150 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Model_Problem*)
152 if p = ([3], Pbl) andalso not (get_ctxt pt p |> ContextC.is_empty)
154 case nxt of (Model_Problem) => ()
155 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"
156 else error "Minisubpbl/300-init-subpbl.sml changed";