1.1 --- a/src/Tools/isac/Interpret/solve.sml Sat Mar 19 15:18:10 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Mar 21 00:32:53 2011 +0100
1.3 @@ -142,13 +142,13 @@
1.4 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
1.5 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
1.6 *)
1.7 -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _))
1.8 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _))
1.9 (pt:ptree, (pos as (p,_))) =
1.10 let val {srls,...} = get_met mI;
1.11 val PblObj{meth=itms,...} = get_obj I pt p;
1.12 val thy' = get_obj g_domID pt p;
1.13 val thy = assoc_thy thy';
1.14 - val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
1.15 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.16 val ini = init_form thy sc env;
1.17 val p = lev_dn p;
1.18 in
1.19 @@ -156,16 +156,16 @@
1.20 SOME t => (* val SOME t = ini;
1.21 *)
1.22 let val (pos,c,_,pt) =
1.23 - generate1 thy (Apply_Method' (mI, SOME t, is))
1.24 - is (lev_on p, Frm)(*implicit Take*) pt;
1.25 - in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is),
1.26 - ((lev_on p, Frm), is))], c, (pt,pos)):calcstate')
1.27 + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
1.28 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
1.29 + in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
1.30 + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
1.31 end
1.32 | NONE => (*execute the first tac in the Script, compare solve m*)
1.33 - let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is;
1.34 + let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.35 val d = e_rls (*FIXME: get simplifier from domID*);
1.36 in
1.37 - case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of
1.38 + case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
1.39 Steps (is'', ss as (m'',f',pt',p',c')::_) =>
1.40 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
1.41 locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
1.42 @@ -175,7 +175,7 @@
1.43 let val (p,ps,f,pt) =
1.44 generate_hard (assoc_thy "Isac") m (p,Frm) pt;
1.45 in ("not-found-in-script",
1.46 - ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
1.47 + ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
1.48 (*just-before------------------------------------------------------
1.49 ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),
1.50 (pos, is))],
1.51 @@ -189,7 +189,7 @@
1.52 val p' = lev_dn_ (p,Res);
1.53 val pt = update_metID pt (par_pblobj pt p) e_metID;
1.54 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
1.55 - [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end
1.56 + [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end
1.57
1.58 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
1.59 ( m, (pt, pos));
1.60 @@ -204,20 +204,20 @@
1.61 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.62 val metID = get_obj g_metID pt pp;
1.63 val {srls=srls,scr=sc,...} = get_met metID;
1.64 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
1.65 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_);
1.66 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
1.67 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
1.68 val thy' = get_obj g_domID pt pp;
1.69 val thy = assoc_thy thy';
1.70 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
1.71 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
1.72 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
1.73
1.74 in if pp = [] then
1.75 let val is = ScrState (E,l,a,scval,scsaf,b)
1.76 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
1.77 - val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt;
1.78 + val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.79 in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
1.80 - [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end
1.81 + [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
1.82 else
1.83 let
1.84 (*resume script of parpbl, transfer value of subpbl-script*)
1.85 @@ -226,21 +226,21 @@
1.86 val thy = assoc_thy thy';
1.87 val metID = get_obj g_metID pt ppp;
1.88 val sc = (#scr o get_met) metID;
1.89 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm);
1.90 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm);
1.91 (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
1.92 val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
1.93 val _=tracing("### solve Check_postc, is'= "^
1.94 (istate2str (E,l,a,scval,scsaf,b)));*)
1.95 val ((p,p_),ps,f,pt) =
1.96 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
1.97 - (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
1.98 + (ScrState (E,l,a,scval,scsaf,b), ctxt) (pp,Res) pt;
1.99 (*val _=tracing("### solve Check_postc, is(pt')= "^
1.100 (istate2str (get_istate pt ([3],Res))));
1.101 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
1.102 (ScrState (E,l,a,scval,scsaf,b));*)
1.103 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
1.104 ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
1.105 - ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_))))
1.106 + ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
1.107 end
1.108 end
1.109 (* val (msg, cs') =
1.110 @@ -256,7 +256,7 @@
1.111 | solve (_,End_Proof'') (pt, (p,p_)) =
1.112 ("end-proof",
1.113 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
1.114 - [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_))))
1.115 + [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
1.116
1.117 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
1.118 | solve (_,End_Detail' t) (pt,(p,p_)) =
1.119 @@ -266,7 +266,7 @@
1.120 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
1.121 val thy' = get_obj g_domID pt pp
1.122 val (srls, is, sc) = from_pblobj' thy' pr pt
1.123 - val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.124 + val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
1.125 in ("ok", ((*((pp,Frm(*???*)),is,tac_),
1.126 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
1.127 tac_2tac tac_, Sundef,*)
1.128 @@ -280,10 +280,10 @@
1.129 could be detail, too !!*)
1.130 then let val ((p,p_),ps,f,pt) =
1.131 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
1.132 - m e_istate (p,p_) pt;
1.133 + m (e_istate, e_ctxt) (p,p_) pt;
1.134 in ("no-method-specified", (*Free_Solve*)
1.135 ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
1.136 - [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end
1.137 + [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end
1.138 else
1.139 let
1.140 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.141 @@ -316,7 +316,7 @@
1.142
1.143 (*FIXME.WN050821 compare solve ... nxt_solv*)
1.144 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
1.145 -fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =
1.146 +fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
1.147 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
1.148 ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);
1.149 *)
1.150 @@ -326,23 +326,23 @@
1.151 else complete_metitms oris probl [] ppc
1.152 val thy' = get_obj g_domID pt p;
1.153 val thy = assoc_thy thy';
1.154 - val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
1.155 + val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
1.156 val ini = init_form thy scr env;
1.157 in
1.158 case ini of
1.159 SOME t => (* val SOME t = ini;
1.160 *)
1.161 let val pos = ((lev_on o lev_dn) p, Frm)
1.162 - val tac_ = Apply_Method' (mI, SOME t, is);
1.163 + val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
1.164 val (pos,c,_,pt) = (*implicit Take*)
1.165 - generate1 thy tac_ is pos pt
1.166 + generate1 thy tac_ (is, ctxt) pos pt
1.167 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
1.168 - in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end
1.169 + in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
1.170 | NONE =>
1.171 - let val pt = update_env pt (fst pos) (SOME is)
1.172 + let val pt = update_env pt (fst pos) (SOME (is, ctxt))
1.173 val (tacis, c, ptp) = nxt_solve_ (pt, pos)
1.174 in (tacis @
1.175 - [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))],
1.176 + [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))],
1.177 c, ptp) end
1.178 end
1.179 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
1.180 @@ -360,12 +360,12 @@
1.181 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
1.182 val metID = get_obj g_metID pt pp;
1.183 val {srls=srls,scr=sc,...} = get_met metID;
1.184 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
1.185 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_);
1.186 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
1.187 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
1.188 val thy' = get_obj g_domID pt pp;
1.189 val thy = assoc_thy thy';
1.190 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
1.191 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
1.192 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
1.193 in if pp = [] then
1.194 let val is = ScrState (E,l,a,scval,scsaf,b)
1.195 @@ -373,8 +373,8 @@
1.196 (*val _= tracing"### nxt_solv2 Apply_Method: stored is =";
1.197 val _= tracing(istate2str is);*)
1.198 val ((p,p_),ps,f,pt) =
1.199 - generate1 thy tac_ is (pp,Res) pt;
1.200 - in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end
1.201 + generate1 thy tac_ (is, ctxt) (pp,Res) pt;
1.202 + in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
1.203 else
1.204 let
1.205 (*resume script of parpbl, transfer value of subpbl-script*)
1.206 @@ -383,14 +383,14 @@
1.207 val thy = assoc_thy thy';
1.208 val metID = get_obj g_metID pt ppp;
1.209 val {scr,...} = get_met metID;
1.210 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
1.211 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm)
1.212 val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
1.213 val is = ScrState (E,l,a,scval,scsaf,b)
1.214 (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";
1.215 val _= tracing(istate2str is);*)
1.216 - val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
1.217 + val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
1.218 (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
1.219 - in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end
1.220 + in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
1.221 end
1.222 (* tracing(istate2str(get_istate pt (p,p_)));
1.223 *)
1.224 @@ -503,8 +503,8 @@
1.225 val (ptp as (pt, (p,_))) = (pt, pos);
1.226 *)
1.227 let val (_,_,mI) = get_obj g_spec pt p;
1.228 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))
1.229 - e_istate ptp;
1.230 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.231 + (e_istate, e_ctxt) ptp;
1.232 in complete_solve auto (c@c') ptp end;
1.233 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.234 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
1.235 @@ -528,8 +528,8 @@
1.236 | (_, c', ptp') => complete_solve auto (c@c') ptp'
1.237 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
1.238 let val (_,_,mI) = get_obj g_spec pt p
1.239 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))
1.240 - e_istate ptp
1.241 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
1.242 + (e_istate, e_ctxt) ptp
1.243 in complete_solve auto (c@c') ptp end;
1.244
1.245 (*.aux.fun for detailrls with Rrls, reverse rewriting.*)
1.246 @@ -537,7 +537,7 @@
1.247 *)
1.248 fun rul_terms_2nds nds t [] = nds
1.249 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
1.250 - (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) ::
1.251 + (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
1.252 (rul_terms_2nds nds t' rts);
1.253
1.254
1.255 @@ -562,10 +562,10 @@
1.256 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
1.257 is wrong for simpl, but working ?!? *)
1.258 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
1.259 - SOME t, is)
1.260 + SOME t, is, e_ctxt)
1.261 val pos' = ((lev_on o lev_dn) p, Frm)
1.262 val thy = assoc_thy "Isac"
1.263 - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
1.264 + val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt
1.265 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
1.266 val newnds = children (get_nd pt'' p)
1.267 val pt''' = ins_chn newnds pt p