1.1 --- a/src/Tools/isac/Interpret/solve.sml Wed May 04 14:07:51 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu May 05 09:23:32 2011 +0200
1.3 @@ -184,67 +184,52 @@
1.4 end
1.5
1.6 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
1.7 - let (*val _=tracing"###solve Free_Solve";*)
1.8 - val p' = lev_dn_ (p,Res);
1.9 - val pt = update_metID pt (par_pblobj pt p) e_metID;
1.10 - in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
1.11 - [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end
1.12 + let (*val _=tracing"###solve Free_Solve";*)
1.13 + val p' = lev_dn_ (p,Res);
1.14 + val pt = update_metID pt (par_pblobj pt p) e_metID;
1.15 + in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p')))
1.16 + end
1.17
1.18 -(* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
1.19 - ( m, (pt, pos));
1.20 - *)
1.21 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
1.22 - let (*val _=tracing"###solve Check_Postcond";*)
1.23 - val pp = par_pblobj pt p
1.24 - val asm = (case get_obj g_tac pt p of
1.25 - Check_elementwise _ => (*collects and instantiates asms*)
1.26 - (snd o (get_obj g_result pt)) p
1.27 - | _ => get_assumptions_ pt (p,p_))
1.28 - handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.29 - val metID = get_obj g_metID pt pp;
1.30 - val {srls=srls,scr=sc,...} = get_met metID;
1.31 - val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
1.32 - (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
1.33 - val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
1.34 - val thy' = get_obj g_domID pt pp;
1.35 - val thy = assoc_thy thy';
1.36 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.37 - (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
1.38 + let (*val _=tracing"###solve Check_Postcond";*)
1.39 + val pp = par_pblobj pt p
1.40 + val asm =
1.41 + (case get_obj g_tac pt p of
1.42 + Check_elementwise _ => (*collects and instantiates asms*)
1.43 + (snd o (get_obj g_result pt)) p
1.44 + | _ => get_assumptions_ pt (p,p_))
1.45 + handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.46 + val metID = get_obj g_metID pt pp;
1.47 + val {srls=srls,scr=sc,...} = get_met metID;
1.48 + val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
1.49 + val thy' = get_obj g_domID pt pp;
1.50 + val thy = assoc_thy thy';
1.51 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
1.52 + in
1.53 + if pp = []
1.54 + then
1.55 + let
1.56 + val is = ScrState (E,l,a,scval,scsaf,b)
1.57 + val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.58 + val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.59 + in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
1.60 + else
1.61 + let (*resume script of parpbl, transfer value of subpbl-script*)
1.62 + val ppp = par_pblobj pt (lev_up p);
1.63 + val thy' = get_obj g_domID pt ppp;
1.64 + val thy = assoc_thy thy';
1.65 + val metID = get_obj g_metID pt ppp;
1.66 + val sc = (#scr o get_met) metID;
1.67 + val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
1.68 + val ctxt'' = transfer_from_subproblem ctxt ctxt'
1.69 + val ((p,p_),ps,f,pt) =
1.70 + generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
1.71 + (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
1.72 + in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
1.73 + ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
1.74 + end
1.75 + end
1.76
1.77 - in if pp = [] then
1.78 - let val is = ScrState (E,l,a,scval,scsaf,b)
1.79 - val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.80 - val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.81 - in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
1.82 - [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
1.83 - else
1.84 - let
1.85 - (*resume script of parpbl, transfer value of subpbl-script*)
1.86 - val ppp = par_pblobj pt (lev_up p);
1.87 - val thy' = get_obj g_domID pt ppp;
1.88 - val thy = assoc_thy thy';
1.89 - val metID = get_obj g_metID pt ppp;
1.90 - val sc = (#scr o get_met) metID;
1.91 - val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
1.92 - val ctxt'' = transfer_from_subproblem ctxt ctxt'
1.93 - val ((p,p_),ps,f,pt) =
1.94 - generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
1.95 - (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
1.96 - in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
1.97 - ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
1.98 - ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
1.99 - end
1.100 - end
1.101 -(* val (msg, cs') =
1.102 - ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
1.103 - ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
1.104 - val (_,(pt',p')) = cs';
1.105 - (tracing o istate2str) (get_istate pt' p');
1.106 - (term2str o fst) (get_obj g_result pt' (fst p'));
1.107 - *)
1.108 -
1.109 -(* tracing(istate2str(get_istate pt (p,p_)));
1.110 - *)
1.111 | solve (_,End_Proof'') (pt, (p,p_)) =
1.112 ("end-proof",
1.113 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)