182 -----------------------------------------------------------------*) |
182 -----------------------------------------------------------------*) |
183 end |
183 end |
184 end |
184 end |
185 |
185 |
186 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) = |
186 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) = |
187 let (*val _=tracing"###solve Free_Solve";*) |
187 let (*val _=tracing"###solve Free_Solve";*) |
188 val p' = lev_dn_ (p,Res); |
188 val p' = lev_dn_ (p,Res); |
189 val pt = update_metID pt (par_pblobj pt p) e_metID; |
189 val pt = update_metID pt (par_pblobj pt p) e_metID; |
190 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*) |
190 in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) |
191 [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end |
191 end |
192 |
192 |
193 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) = |
|
194 ( m, (pt, pos)); |
|
195 *) |
|
196 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) = |
193 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) = |
197 let (*val _=tracing"###solve Check_Postcond";*) |
194 let (*val _=tracing"###solve Check_Postcond";*) |
198 val pp = par_pblobj pt p |
195 val pp = par_pblobj pt p |
199 val asm = (case get_obj g_tac pt p of |
196 val asm = |
200 Check_elementwise _ => (*collects and instantiates asms*) |
197 (case get_obj g_tac pt p of |
201 (snd o (get_obj g_result pt)) p |
198 Check_elementwise _ => (*collects and instantiates asms*) |
202 | _ => get_assumptions_ pt (p,p_)) |
199 (snd o (get_obj g_result pt)) p |
203 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) |
200 | _ => get_assumptions_ pt (p,p_)) |
204 val metID = get_obj g_metID pt pp; |
201 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) |
205 val {srls=srls,scr=sc,...} = get_met metID; |
202 val metID = get_obj g_metID pt pp; |
206 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); |
203 val {srls=srls,scr=sc,...} = get_met metID; |
207 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); |
204 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); |
208 val _= tracing("### solve Check_postc, is= "^(istate2str is));*) |
205 val thy' = get_obj g_domID pt pp; |
209 val thy' = get_obj g_domID pt pp; |
|
210 val thy = assoc_thy thy'; |
|
211 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc; |
|
212 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*) |
|
213 |
|
214 in if pp = [] then |
|
215 let val is = ScrState (E,l,a,scval,scsaf,b) |
|
216 val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) |
|
217 val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt; |
|
218 in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*) |
|
219 [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end |
|
220 else |
|
221 let |
|
222 (*resume script of parpbl, transfer value of subpbl-script*) |
|
223 val ppp = par_pblobj pt (lev_up p); |
|
224 val thy' = get_obj g_domID pt ppp; |
|
225 val thy = assoc_thy thy'; |
206 val thy = assoc_thy thy'; |
226 val metID = get_obj g_metID pt ppp; |
207 val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc; |
227 val sc = (#scr o get_met) metID; |
208 in |
228 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); |
209 if pp = [] |
229 val ctxt'' = transfer_from_subproblem ctxt ctxt' |
210 then |
230 val ((p,p_),ps,f,pt) = |
211 let |
231 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm))) |
212 val is = ScrState (E,l,a,scval,scsaf,b) |
232 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt; |
213 val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) |
233 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*) |
214 val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt; |
234 ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)), |
215 in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end |
235 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_)))) |
216 else |
236 end |
217 let (*resume script of parpbl, transfer value of subpbl-script*) |
237 end |
218 val ppp = par_pblobj pt (lev_up p); |
238 (* val (msg, cs') = |
219 val thy' = get_obj g_domID pt ppp; |
239 ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))), |
220 val thy = assoc_thy thy'; |
240 ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_)))); |
221 val metID = get_obj g_metID pt ppp; |
241 val (_,(pt',p')) = cs'; |
222 val sc = (#scr o get_met) metID; |
242 (tracing o istate2str) (get_istate pt' p'); |
223 val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); |
243 (term2str o fst) (get_obj g_result pt' (fst p')); |
224 val ctxt'' = transfer_from_subproblem ctxt ctxt' |
244 *) |
225 val ((p,p_),ps,f,pt) = |
245 |
226 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm))) |
246 (* tracing(istate2str(get_istate pt (p,p_))); |
227 (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt; |
247 *) |
228 in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)), |
|
229 ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_)))) |
|
230 end |
|
231 end |
|
232 |
248 | solve (_,End_Proof'') (pt, (p,p_)) = |
233 | solve (_,End_Proof'') (pt, (p,p_)) = |
249 ("end-proof", |
234 ("end-proof", |
250 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*) |
235 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*) |
251 [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_)))) |
236 [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_)))) |
252 |
237 |