diff -r 72187c16c796 -r 023ebb7d9759 src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Sat Mar 19 15:18:10 2011 +0100 +++ b/src/Tools/isac/Interpret/solve.sml Mon Mar 21 00:32:53 2011 +0100 @@ -142,13 +142,13 @@ (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos); *) -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _)) +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) = let val {srls,...} = get_met mI; val PblObj{meth=itms,...} = get_obj I pt p; val thy' = get_obj g_domID pt p; val thy = assoc_thy thy'; - val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI; + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI; val ini = init_form thy sc env; val p = lev_dn p; in @@ -156,16 +156,16 @@ SOME t => (* val SOME t = ini; *) let val (pos,c,_,pt) = - generate1 thy (Apply_Method' (mI, SOME t, is)) - is (lev_on p, Frm)(*implicit Take*) pt; - in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is), - ((lev_on p, Frm), is))], c, (pt,pos)):calcstate') + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt)) + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt; + in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate') end | NONE => (*execute the first tac in the Script, compare solve m*) - let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is; + let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); val d = e_rls (*FIXME: get simplifier from domID*); in - case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of + case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of Steps (is'', ss as (m'',f',pt',p',c')::_) => (* val Steps (is'', ss as (m'',f',pt',p',c')::_) = locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is'; @@ -175,7 +175,7 @@ let val (p,ps,f,pt) = generate_hard (assoc_thy "Isac") m (p,Frm) pt; in ("not-found-in-script", - ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end + ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end (*just-before------------------------------------------------------ ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate), (pos, is))], @@ -189,7 +189,7 @@ val p' = lev_dn_ (p,Res); val pt = update_metID pt (par_pblobj pt p) e_metID; in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*) - [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end + [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) = ( m, (pt, pos)); @@ -204,20 +204,20 @@ handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) val metID = get_obj g_metID pt pp; val {srls=srls,scr=sc,...} = get_met metID; - val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_); (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); val _= tracing("### solve Check_postc, is= "^(istate2str is));*) val thy' = get_obj g_domID pt pp; val thy = assoc_thy thy'; - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt); (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*) in if pp = [] then let val is = ScrState (E,l,a,scval,scsaf,b) val tac_ = Check_Postcond'(pI,(scval, map term2str asm)) - val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt; + val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt; in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*) - [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end + [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end else let (*resume script of parpbl, transfer value of subpbl-script*) @@ -226,21 +226,21 @@ val thy = assoc_thy thy'; val metID = get_obj g_metID pt ppp; val sc = (#scr o get_met) metID; - val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm); + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm); (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm))); val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is)); val _=tracing("### solve Check_postc, is'= "^ (istate2str (E,l,a,scval,scsaf,b)));*) val ((p,p_),ps,f,pt) = generate1 thy (Check_Postcond' (pI, (scval, map term2str asm))) - (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt; + (ScrState (E,l,a,scval,scsaf,b), ctxt) (pp,Res) pt; (*val _=tracing("### solve Check_postc, is(pt')= "^ (istate2str (get_istate pt ([3],Res)))); val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc (ScrState (E,l,a,scval,scsaf,b));*) in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*) ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)), - ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_)))) + ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_)))) end end (* val (msg, cs') = @@ -256,7 +256,7 @@ | solve (_,End_Proof'') (pt, (p,p_)) = ("end-proof", ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*) - [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_)))) + [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_)))) (*-----------vvvvvvvvvvv could be done by generate1 ?!?*) | solve (_,End_Detail' t) (pt,(p,p_)) = @@ -266,7 +266,7 @@ (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) val thy' = get_obj g_domID pt pp val (srls, is, sc) = from_pblobj' thy' pr pt - val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is + val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is in ("ok", ((*((pp,Frm(*???*)),is,tac_), Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)), tac_2tac tac_, Sundef,*) @@ -280,10 +280,10 @@ could be detail, too !!*) then let val ((p,p_),ps,f,pt) = generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) - m e_istate (p,p_) pt; + m (e_istate, e_ctxt) (p,p_) pt; in ("no-method-specified", (*Free_Solve*) ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) - [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end + [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end else let val thy' = get_obj g_domID pt (par_pblobj pt p); @@ -316,7 +316,7 @@ (*FIXME.WN050821 compare solve ... nxt_solv*) (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) -fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) = +fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) = (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) = ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp); *) @@ -326,23 +326,23 @@ else complete_metitms oris probl [] ppc val thy' = get_obj g_domID pt p; val thy = assoc_thy thy'; - val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI; + val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI; val ini = init_form thy scr env; in case ini of SOME t => (* val SOME t = ini; *) let val pos = ((lev_on o lev_dn) p, Frm) - val tac_ = Apply_Method' (mI, SOME t, is); + val tac_ = Apply_Method' (mI, SOME t, is, ctxt); val (pos,c,_,pt) = (*implicit Take*) - generate1 thy tac_ is pos pt + generate1 thy tac_ (is, ctxt) pos pt (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*) - in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end + in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end | NONE => - let val pt = update_env pt (fst pos) (SOME is) + let val pt = update_env pt (fst pos) (SOME (is, ctxt)) val (tacis, c, ptp) = nxt_solve_ (pt, pos) in (tacis @ - [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))], + [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))], c, ptp) end end (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m); @@ -360,12 +360,12 @@ handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*) val metID = get_obj g_metID pt pp; val {srls=srls,scr=sc,...} = get_met metID; - val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_); + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_); (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_))); val _= tracing("### solve Check_postc, is= "^(istate2str is));*) val thy' = get_obj g_domID pt pp; val thy = assoc_thy thy'; - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is; + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt); (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*) in if pp = [] then let val is = ScrState (E,l,a,scval,scsaf,b) @@ -373,8 +373,8 @@ (*val _= tracing"### nxt_solv2 Apply_Method: stored is ="; val _= tracing(istate2str is);*) val ((p,p_),ps,f,pt) = - generate1 thy tac_ is (pp,Res) pt; - in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end + generate1 thy tac_ (is, ctxt) (pp,Res) pt; + in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end else let (*resume script of parpbl, transfer value of subpbl-script*) @@ -383,14 +383,14 @@ val thy = assoc_thy thy'; val metID = get_obj g_metID pt ppp; val {scr,...} = get_met metID; - val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm) + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm) val tac_ = Check_Postcond' (pI, (scval, map term2str asm)) val is = ScrState (E,l,a,scval,scsaf,b) (*val _= tracing"### nxt_solv3 Apply_Method: stored is ="; val _= tracing(istate2str is);*) - val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt; + val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt; (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*) - in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end + in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end end (* tracing(istate2str(get_istate pt (p,p_))); *) @@ -503,8 +503,8 @@ val (ptp as (pt, (p,_))) = (pt, pos); *) let val (_,_,mI) = get_obj g_spec pt p; - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) - e_istate ptp; + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) + (e_istate, e_ctxt) ptp; in complete_solve auto (c@c') ptp end; (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = @@ -528,8 +528,8 @@ | (_, c', ptp') => complete_solve auto (c@c') ptp' and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') = let val (_,_,mI) = get_obj g_spec pt p - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate)) - e_istate ptp + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) + (e_istate, e_ctxt) ptp in complete_solve auto (c@c') ptp end; (*.aux.fun for detailrls with Rrls, reverse rewriting.*) @@ -537,7 +537,7 @@ *) fun rul_terms_2nds nds t [] = nds | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) = - (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) :: + (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) :: (rul_terms_2nds nds t' rts); @@ -562,10 +562,10 @@ (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"] is wrong for simpl, but working ?!? *) val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), - SOME t, is) + SOME t, is, e_ctxt) val pos' = ((lev_on o lev_dn) p, Frm) val thy = assoc_thy "Isac" - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt + val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos') val newnds = children (get_nd pt'' p) val pt''' = ins_chn newnds pt p