27 1 relevant for updating ctxt *) |
27 1 relevant for updating ctxt *) |
28 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt'''); |
28 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''', p''', [], pt'''); |
29 |
29 |
30 val ("ok", (_, _, (pt'''', p''''))) = (*case*) |
30 val ("ok", (_, _, (pt'''', p''''))) = (*case*) |
31 Step.by_tactic tac (pt, p) (*of*); |
31 Step.by_tactic tac (pt, p) (*of*); |
32 get_ctxt pt'''' p'''' |> is_e_ctxt; (*should NOT be true after this step*) |
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''')); |
33 "~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p''')); |
34 val Appl m = applicable_in p pt tac; |
34 val Appl m = applicable_in p pt tac; |
35 (*if*) Tactic.for_specify' m; (*false*) |
35 (*if*) Tactic.for_specify' m; (*false*) |
36 |
36 |
37 (*val (msg, cs') =*) |
37 (*val (msg, cs') =*) |
123 check_tac1 cct ist (prog_tac, form_arg) (*return from scan_dn1*); |
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) |
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)); |
125 = (check_tac1 cct ist (prog_tac, form_arg)); |
126 |
126 |
127 (*+*)val (pstate, ctxt, tac) = iss; |
127 (*+*)val (pstate, ctxt, tac) = iss; |
128 (*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 should NOT return e_ctxt" else (); |
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 () = (); |
129 "~~~~~ from fun scan_up1 HOL.Let(*1*), --------------------------------- NO return:"; val () = (); |
130 |
130 |
131 (*+*)if is_e_ctxt ctxt''''' then error "locate_input_tactic should NOT return e_ctxt" else (); |
131 (*+*)if ContextC.is_empty ctxt''''' then error "locate_input_tactic should NOT return ContextC.empty" else (); |
132 |
132 |
133 "~~~~~ from fun locate_input_tactic \<longrightarrow>Step_Solve.by_tactic , return:"; val (LI.Safe_Step (istate, ctxt, tac)) |
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'_''''')); |
134 = (Safe_Step (Pstate ist''''', ctxt''''', tac'_''''')); |
135 val p' = next_in_prog po |
135 val p' = next_in_prog po |
136 val (p'', _, _,pt') = |
136 val (p'', _, _,pt') = |
140 (l as (_, ctxt)), (pos as (p, p_)), pt) |
140 (l as (_, ctxt)), (pos as (p, p_)), pt) |
141 = ((Celem.assoc_thy "Isac_Knowledge"), tac, (istate, ctxt), (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)) |
142 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID)) |
143 (oris, (domID, pblID, metID), hdl, ctxt_specify); |
143 (oris, (domID, pblID, metID), hdl, ctxt_specify); |
144 |
144 |
145 (*+*)if is_e_ctxt ctxt_specify then error "ERROR: generate1 should NOT get input e_ctxt" else (); |
145 (*+*)if ContextC.is_empty ctxt_specify then error "ERROR: generate1 should NOT get input ContextC.empty" else (); |
146 (*+*)if (get_ctxt pt pos |> is_e_ctxt) then error "generate1 MUST store ctxt" |
146 (*+*)if (get_ctxt pt pos |> ContextC.is_empty) then error "generate1 MUST store ctxt" |
147 (*+*)else (); |
147 (*+*)else (); |
148 (*\\--1 end step into relevant call ----------------------------------------------------------//*) |
148 (*\\--1 end step into relevant call ----------------------------------------------------------//*) |
149 |
149 |
150 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Model_Problem*) |
150 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';(*nxt = Model_Problem*) |
151 |
151 |
152 if p = ([3], Pbl) andalso not (get_ctxt pt p |> is_e_ctxt) |
152 if p = ([3], Pbl) andalso not (get_ctxt pt p |> ContextC.is_empty) |
153 then |
153 then |
154 case nxt of (Model_Problem) => () |
154 case nxt of (Model_Problem) => () |
155 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem" |
155 | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem" |
156 else error "Minisubpbl/300-init-subpbl.sml changed"; |
156 else error "Minisubpbl/300-init-subpbl.sml changed"; |