intermed. context integration: Isac compiles.
1.1 --- a/src/Tools/isac/Frontend/interface.sml Sat Mar 19 15:18:10 2011 +0100
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Mar 21 00:32:53 2011 +0100
1.3 @@ -412,7 +412,7 @@
1.4 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
1.5 guh ^ "'")
1.6 else let val (ptp as (pt,pold),_) = get_calc cI
1.7 - val is = get_istate pt ip
1.8 + val (is,_) = get_istate pt ip
1.9 val subs = subs_from is "dummy" guh
1.10 val tac = guh2rewtac guh subs
1.11 in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
1.12 @@ -436,7 +436,7 @@
1.13 "' not-applicable")
1.14 | Appl m =>
1.15 let val (p,c,_,pt) = generate1 (assoc_thy"Isac")
1.16 - m Uistate ip pt
1.17 + m (Uistate, e_ctxt) ip pt
1.18 in upd_calc cI ((pt,p),[]);
1.19 autocalculateOK2xml cI pold (if null c then pold
1.20 else last_elem c) p
1.21 @@ -783,7 +783,7 @@
1.22 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
1.23 guh ^ "'")
1.24 else let val (ptp as (pt,_),_) = get_calc cI
1.25 - val is = get_istate pt pos
1.26 + val (is,_) = get_istate pt pos
1.27 val subs = subs_from is "dummy" guh
1.28 val tac = guh2rewtac guh subs
1.29 in contextthyOK2xml cI (context_thy (pt, pos) tac) end
2.1 --- a/src/Tools/isac/Interpret/appl.sml Sat Mar 19 15:18:10 2011 +0100
2.2 +++ b/src/Tools/isac/Interpret/appl.sml Mon Mar 21 00:32:53 2011 +0100
2.3 @@ -343,7 +343,7 @@
2.4 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
2.5 then Notappl ((tac2str (Apply_Method mI))^
2.6 " not for pos "^(pos'2str (p,p_)))
2.7 - else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
2.8 + else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), e_ctxt))
2.9
2.10 | applicable_in (p,p_) pt (Check_Postcond pI) =
2.11 if member op = [Pbl,Met] p_
3.1 --- a/src/Tools/isac/Interpret/calchead.sml Sat Mar 19 15:18:10 2011 +0100
3.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Mar 21 00:32:53 2011 +0100
3.3 @@ -206,11 +206,11 @@
3.4
3.5
3.6
3.7 -(*---------------------------------------------------------------------*)
3.8 +(*---------------------------------------------------------------------
3.9 structure CalcHead (**): CALC_HEAD(**) =
3.10
3.11 struct
3.12 -(*---------------------------------------------------------------------*)
3.13 +---------------------------------------------------------------------*)
3.14
3.15 (* datatypes *)
3.16
3.17 @@ -1055,7 +1055,7 @@
3.18 "#Given" => Add_Given' (ct, met')
3.19 | "#Find" => Add_Find' (ct, met')
3.20 | "#Relate"=> Add_Relation'(ct, met'))
3.21 - Uistate (p,Met) pt
3.22 + (Uistate, e_ctxt) (p,Met) pt
3.23 val pre' = check_preconds thy prls pre met'
3.24 val pb = foldl and_ (true, map fst pre')
3.25 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
3.26 @@ -1097,7 +1097,7 @@
3.27 "#Given" => Add_Given' (ct, pbl')
3.28 | "#Find" => Add_Find' (ct, pbl')
3.29 | "#Relate"=> Add_Relation'(ct, pbl'))
3.30 - Uistate (p,Pbl) pt
3.31 + (Uistate, e_ctxt) (p,Pbl) pt
3.32 val pre = check_preconds thy prls where_ pbl'
3.33 val pb = foldl and_ (true, map fst pre)
3.34 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
3.35 @@ -1140,7 +1140,7 @@
3.36 val thy = assoc_thy dI';
3.37 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
3.38 else prep_ori fmz thy ((#ppc o get_pbt) pI');
3.39 - val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
3.40 + val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
3.41 (oris,(dI',pI',mI'),e_term);
3.42 val {ppc,prls,where_,...} = get_pbt pI'
3.43 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
3.44 @@ -1173,7 +1173,7 @@
3.45 val pre = check_preconds thy prls where_ pbl
3.46 val pb = foldl and_ (true, map fst pre)
3.47 val ((p,_),_,_,pt) =
3.48 - generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
3.49 + generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
3.50 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
3.51 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
3.52 in ((p,Pbl), ((p,p_),Uistate),
3.53 @@ -1197,7 +1197,7 @@
3.54 if length met = 0 then e_metID else hd met)
3.55 val ((p,_),_,_,pt) =
3.56 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
3.57 - Uistate pos pt
3.58 + (Uistate, e_ctxt) pos pt
3.59 (*val pre = check_preconds thy prls where_ pbl
3.60 val pb = foldl and_ (true, map fst pre)*)
3.61 val (pbl, pre, pb) = ([], [], false)
3.62 @@ -1208,7 +1208,7 @@
3.63
3.64 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
3.65 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
3.66 - (Refine_Problem' rfd) Uistate pos pt
3.67 + (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
3.68 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
3.69 Model_Problem, Safe, pt) end
3.70
3.71 @@ -1222,7 +1222,7 @@
3.72 val pt = update_pblID pt p pI;*)
3.73 val thy = assoc_thy dI
3.74 val ((p,Pbl),_,_,pt)=
3.75 - generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
3.76 + generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
3.77 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
3.78 val mI'' = if mI=e_metID then mI' else mI;
3.79 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
3.80 @@ -1250,7 +1250,7 @@
3.81 (*val pt = update_met pt p itms;
3.82 val pt = update_metID pt p mID*)
3.83 val (pos,_,_,pt)=
3.84 - generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
3.85 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
3.86 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
3.87 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
3.88 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
3.89 @@ -1294,7 +1294,7 @@
3.90 let
3.91 (*val pt = update_domID pt p domID;11.8.03*)
3.92 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
3.93 - Uistate (p,p_) pt
3.94 + (Uistate, e_ctxt) (p,p_) pt
3.95 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
3.96 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
3.97 (ppc,mpc) (domID,pI,mI);
3.98 @@ -1330,15 +1330,15 @@
3.99 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
3.100 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
3.101 val ((p,Pbl),c,_,pt') =
3.102 - generate1 thy tac_ Uistate (p,Pbl) pt
3.103 - in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
3.104 + generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
3.105 + in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
3.106
3.107 | Err msg =>
3.108 (*TODO.WN03 pass error-msgs to the frontend..
3.109 FIXME ..and dont abuse a tactic for that purpose*)
3.110 ([(Tac msg,
3.111 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
3.112 - (e_pos', e_istate))], [], ptp)
3.113 + (e_pos', (e_istate, e_ctxt)))], [], ptp)
3.114 end
3.115
3.116 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
3.117 @@ -1361,8 +1361,8 @@
3.118 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
3.119 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
3.120 val ((p,Met),c,_,pt') =
3.121 - generate1 thy tac_ Uistate (p,Met) pt
3.122 - in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
3.123 + generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
3.124 + in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
3.125
3.126 | Err msg => ([(*tacis*)], [], ptp)
3.127 (*nxt_me collects tacis until not hide; here just no progress*)
3.128 @@ -1463,8 +1463,8 @@
3.129 | _ => complete_mod_ (oris, mpc, ppc, probl)
3.130 (*----------------------------------------------------------------*)
3.131 val tac_ = Model_Problem' (pI, pbl, met)
3.132 - val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
3.133 - in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
3.134 + val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
3.135 + in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
3.136
3.137 (* val Add_Find ct = tac;
3.138 *)
3.139 @@ -1485,9 +1485,9 @@
3.140 val thy = assoc_thy dI
3.141 val (pos,c,_,pt) =
3.142 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
3.143 - Uistate pos pt
3.144 + (Uistate, e_ctxt) pos pt
3.145 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
3.146 - (pos, Uistate))], c, (pt,pos)) end
3.147 + (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
3.148 | NONE => ([], [], ptp)
3.149 end
3.150
3.151 @@ -1500,9 +1500,9 @@
3.152 | SOME (rfd as (pI',_)) =>
3.153 let val (pos,c,_,pt) =
3.154 generate1 (assoc_thy thy)
3.155 - (Refine_Problem' rfd) Uistate pos pt
3.156 + (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
3.157 in ([(Refine_Problem pI, Refine_Problem' rfd,
3.158 - (pos, Uistate))], c, (pt,pos)) end
3.159 + (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
3.160 end
3.161
3.162 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
3.163 @@ -1516,9 +1516,9 @@
3.164 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
3.165 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
3.166 val ((p,Pbl),c,_,pt)=
3.167 - generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
3.168 + generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
3.169 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
3.170 - (pos,Uistate))], c, (pt,pos)) end
3.171 + (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
3.172
3.173 (*transfers oris (not required in pbl) to met-model for script-env
3.174 FIXME.WN.8.03: application of several mIDs to SAME model?*)
3.175 @@ -1533,26 +1533,26 @@
3.176 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
3.177 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
3.178 val (pos,c,_,pt)=
3.179 - generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
3.180 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
3.181 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
3.182 - (pos,Uistate))], c, (pt,pos)) end
3.183 + (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
3.184
3.185 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
3.186 let val (dI',_,_) = get_obj g_spec pt p
3.187 val (pos,c,_,pt) =
3.188 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
3.189 - Uistate pos pt
3.190 + (Uistate, e_ctxt) pos pt
3.191 in (*FIXXXME: check if pbl can still be parsed*)
3.192 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
3.193 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
3.194 (pt, pos)) end
3.195
3.196 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
3.197 let val (dI',_,_) = get_obj g_spec pt p
3.198 val (pos,c,_,pt) =
3.199 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
3.200 - Uistate pos pt
3.201 + (Uistate, e_ctxt) pos pt
3.202 in (*FIXXXME: check if met can still be parsed*)
3.203 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
3.204 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
3.205 (pt, pos)) end
3.206
3.207 | nxt_specif m' _ =
3.208 @@ -1579,7 +1579,7 @@
3.209 val thy = assoc_thy dI
3.210 val mI = if mI = [] then hd met else mI
3.211 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
3.212 - val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
3.213 + val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
3.214 ([], (dI,pI,mI), hdl)
3.215 val pt = update_spec pt [] (dI,pI,mI)
3.216 val pits = init_pbl' ppc
3.217 @@ -1589,14 +1589,14 @@
3.218 let val {ppc,...} = get_met mI
3.219 val dI = if dI = "" then "Isac" else dI
3.220 val thy = assoc_thy dI
3.221 - val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
3.222 + val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
3.223 ([], (dI,pI,mI), e_term(*FIXME met*))
3.224 val pt = update_spec pt [] (dI,pI,mI)
3.225 val mits = init_pbl' ppc
3.226 val pt = update_met pt [] mits
3.227 in ((pt, ([], Met)), []) : calcstate end
3.228 else (* new example, pepare for interactive modeling *)
3.229 - let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
3.230 + let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
3.231 ([], e_spec, e_term)
3.232 in ((pt,([],Pbl)), []) : calcstate end
3.233 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
3.234 @@ -1615,7 +1615,7 @@
3.235 NONE => pblterm dI pI
3.236 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
3.237 ~~~ vals_of_oris pors) t
3.238 - val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
3.239 + val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
3.240 (pors, (dI, pI, mI), hdl)
3.241 in ((pt, ([], Pbl)),
3.242 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
3.243 @@ -2090,9 +2090,9 @@
3.244 val pt = update_spec pt p e_spec
3.245 in (pt, (p,Pbl):pos') end;
3.246
3.247 -(*---------------------------------------------------------------------*)
3.248 +(*---------------------------------------------------------------------
3.249 end
3.250
3.251 open CalcHead;
3.252 -(*---------------------------------------------------------------------*)
3.253 +---------------------------------------------------------------------*)
3.254
4.1 --- a/src/Tools/isac/Interpret/ctree.sml Sat Mar 19 15:18:10 2011 +0100
4.2 +++ b/src/Tools/isac/Interpret/ctree.sml Mon Mar 21 00:32:53 2011 +0100
4.3 @@ -276,6 +276,7 @@
4.4 | ScrState of scrstate (*for script interpreter*)
4.5 | RrlsState of rrlsstate; (*for reverse rewriting*)
4.6 val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false)):istate;
4.7 +val e_ctxt = ProofContext.init_global @{theory};
4.8
4.9 type iist = istate option * istate option;
4.10 (*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*)
4.11 @@ -566,7 +567,8 @@
4.12 itm list (*... updated from pbl to met*)
4.13 | Apply_Method' of metID *
4.14 (term option) * (*init_form*)
4.15 - istate
4.16 + istate *
4.17 + Proof.context
4.18 | Check_Postcond' of
4.19 pblID *
4.20 (term * (*returnvalue of script in solve*)
4.21 @@ -656,7 +658,7 @@
4.22 | Specify_Method' (pI,oris,itms) =>
4.23 "Specify_Method' ("^metID2str pI^", "^oris2str oris^", )"
4.24
4.25 - | Apply_Method' (metID,_,_) => "Apply_Method' "^(strs2str metID)
4.26 + | Apply_Method' (metID,_,_,_) => "Apply_Method' "^(strs2str metID)
4.27 | Check_Postcond' (pblID,(scval,asm)) =>
4.28 "Check_Postcond' "^(spair2str(strs2str pblID,
4.29 spair2str (term2str scval, strs2str asm)))
4.30 @@ -732,7 +734,7 @@
4.31 (*^^^FIXME.WN0607 rename this field*)
4.32 form : term,
4.33 tac : tac, (* also in istate*)
4.34 - loc : istate option * istate option, (*for form, result
4.35 + loc : (istate * Proof.context) option * (istate * Proof.context) option, (*for form, result
4.36 13.8.02: (NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
4.37 branch: branch,
4.38 result: term * term list,
4.39 @@ -753,8 +755,8 @@
4.40 probl : itm list, (*itms explicitly input*)
4.41 meth : itm list, (*itms automatically added to copy of probl
4.42 TODO: input like to 'probl'*)
4.43 - env : istate option,(*for problem with initac in script*)
4.44 - loc : istate option * istate option, (*for pbl+met * result*)
4.45 + env : (istate * Proof.context) option,(*for problem with initac in script*)
4.46 + loc : (istate * Proof.context) option * (istate * Proof.context) option, (*for pbl+met * result*)
4.47 branch: branch,
4.48 result: term * term list,
4.49 ostate: ostate}; (*Complete <=> result is _proven_ OK*)
4.50 @@ -1332,16 +1334,16 @@
4.51 let val (lfrm,lres) = get_obj g_loc pt p
4.52 in if lfrm = e_istate then lres else lfrm end; 5.10.00: too liberal ?*)
4.53 (*13.8.02: options, because istate is no equalitype any more*)
4.54 -fun get_loc EmptyPtree _ = e_istate
4.55 +fun get_loc EmptyPtree _ = (e_istate, e_ctxt)
4.56 | get_loc pt (p,Res) =
4.57 (case get_obj g_loc pt p of
4.58 (SOME i, NONE) => i
4.59 - | (NONE , NONE) => e_istate
4.60 + | (NONE , NONE) => (e_istate, e_ctxt)
4.61 | (_ , SOME i) => i)
4.62 | get_loc pt (p,_) =
4.63 (case get_obj g_loc pt p of
4.64 (NONE , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
4.65 - | (NONE , NONE) => e_istate
4.66 + | (NONE , NONE) => (e_istate, e_ctxt)
4.67 | (SOME i, _) => i);
4.68 val get_istate = get_loc; (*3.5.02*)
4.69
4.70 @@ -2038,7 +2040,7 @@
4.71 let val (ist_form, f) = (get_loc pt (p,Frm),
4.72 get_obj g_form pt p)
4.73 val (pt, cs) = cut_tree pt (p,Frm)
4.74 - val pt = append_atomic p e_istate f r f' s pt
4.75 + val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
4.76 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
4.77 in (pt, cs) end
4.78 else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
4.79 @@ -2140,7 +2142,7 @@
4.80 )
4.81 | cappend_problem pt p loc fmz ori =
4.82 ((*tracing("###cappend_problem: pos ="^pos2str p);*)
4.83 - apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
4.84 + apfst (append_problem p (loc:(istate * Proof.context)) fmz ori) (cut_tree pt (p,Frm))
4.85 );
4.86
4.87 (*.get the theory explicitly specified for the rootpbl;
5.1 --- a/src/Tools/isac/Interpret/generate.sml Sat Mar 19 15:18:10 2011 +0100
5.2 +++ b/src/Tools/isac/Interpret/generate.sml Mon Mar 21 00:32:53 2011 +0100
5.3 @@ -102,11 +102,11 @@
5.4 (tac * (*for comparison with input tac*)
5.5 tac_ * (*for ptree generation*)
5.6 (pos' * (*after applying tac_, for ptree generation*)
5.7 - istate)); (*after applying tac_, for ptree generation*)
5.8 -val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', e_istate)): taci;
5.9 + (istate * Proof.context))); (*after applying tac_, for ptree generation*)
5.10 +val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci;
5.11 (* val (tac, tac_, (pos', istate))::_ = tacis';
5.12 *)
5.13 -fun taci2str ((tac, tac_, (pos', istate)):taci) =
5.14 +fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
5.15 "( "^tac2str tac^", "^tac_2str tac_^", ( "^pos'2str pos'
5.16 ^", "^istate2str istate^" ))";
5.17 fun tacis2str tacis = (strs2str o (map (linefeed o taci2str))) tacis;
5.18 @@ -259,25 +259,25 @@
5.19
5.20 (*generate 1 ppobj in ptree*)
5.21 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
5.22 -fun generate1 thy (Add_Given' (_, itmlist)) Uistate (pos as (p,p_)) pt =
5.23 +fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p,p_)) pt =
5.24 (pos:pos',[],Form' (PpcKF (0,EdUndef,0,Nundef,
5.25 (Upblmet,itms2itemppc thy [][]))),
5.26 case p_ of Pbl => update_pbl pt p itmlist
5.27 | Met => update_met pt p itmlist)
5.28 - | generate1 thy (Add_Find' (_, itmlist)) Uistate (pos as (p,p_)) pt =
5.29 + | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
5.30 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.31 case p_ of Pbl => update_pbl pt p itmlist
5.32 | Met => update_met pt p itmlist)
5.33 - | generate1 thy (Add_Relation' (_, itmlist)) Uistate (pos as (p,p_)) pt =
5.34 + | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
5.35 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.36 case p_ of Pbl => update_pbl pt p itmlist
5.37 | Met => update_met pt p itmlist)
5.38
5.39 - | generate1 thy (Specify_Theory' domID) Uistate (pos as (p,_)) pt =
5.40 + | generate1 thy (Specify_Theory' domID) _ (pos as (p,_)) pt =
5.41 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.42 update_domID pt p domID)
5.43
5.44 - | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate
5.45 + | generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) _
5.46 (pos as (p,_)) pt =
5.47 let val pt = update_pbl pt p itms
5.48 val pt = update_pblID pt p pI
5.49 @@ -285,7 +285,7 @@
5.50 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.51 pt) end
5.52
5.53 - | generate1 thy (Specify_Method' (mID, oris, itms)) Uistate
5.54 + | generate1 thy (Specify_Method' (mID, oris, itms)) _
5.55 (pos as (p,_)) pt =
5.56 let val pt = update_oris pt p oris
5.57 val pt = update_met pt p itms
5.58 @@ -294,7 +294,7 @@
5.59 Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.60 pt) end
5.61
5.62 - | generate1 thy (Model_Problem' (_, itms, met)) Uistate (pos as (p,_)) pt =
5.63 + | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
5.64 (* val (itms,pos as (p,_)) = (pbl, pos);
5.65 *)
5.66 let val pt = update_pbl pt p itms
5.67 @@ -303,32 +303,32 @@
5.68 (Upblmet,itms2itemppc thy [][]))), pt) end
5.69
5.70 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
5.71 - Uistate (pos as (p,_)) pt =
5.72 + _ (pos as (p,_)) pt =
5.73 let val pt = update_pbl pt p pbl
5.74 val pt = update_orispec pt p (domID,pIre,metID)
5.75 in (pos,[],
5.76 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
5.77 pt) end
5.78
5.79 - | generate1 thy (Refine_Problem' (pI,_)) Uistate (pos as (p,_)) pt =
5.80 + | generate1 thy (Refine_Problem' (pI,_)) _ (pos as (p,_)) pt =
5.81 let val (dI,_,mI) = get_obj g_spec pt p
5.82 val pt = update_spec pt p (dI, pI, mI)
5.83 in (pos,[],
5.84 Form'(PpcKF(0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),pt)
5.85 end
5.86
5.87 - | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt =
5.88 + | generate1 thy (Apply_Method' (_,topt, is, ctxt)) _ (pos as (p,p_)) pt =
5.89 ((*tracing("###generate1 Apply_Method': pos = "^pos'2str (p,p_));
5.90 tracing("###generate1 Apply_Method': topt= "^termopt2str topt);
5.91 tracing("###generate1 Apply_Method': is = "^istate2str is);*)
5.92 case topt of
5.93 SOME t =>
5.94 - let val (pt,c) = cappend_form pt p is t
5.95 + let val (pt,c) = cappend_form pt p (is, ctxt) t
5.96 (*val _= tracing("###generate1 Apply_Method: after cappend")*)
5.97 in (pos,c, EmptyMout,pt)
5.98 end
5.99 | NONE =>
5.100 - (pos,[],EmptyMout,update_env pt p (SOME is)))
5.101 + (pos,[],EmptyMout,update_env pt p (SOME (is, ctxt))))
5.102 (* val (thy, (Take' t), l, (p,p_), pt) =
5.103 ((assoc_thy "Isac"), tac_, is, pos, pt);
5.104 *)
5.105 @@ -409,10 +409,11 @@
5.106 let val (pt,c) = cappend_form pt p l f
5.107 val pt = update_branch pt p TransitiveB (*040312*)
5.108
5.109 + val ctxt = e_ctxt;
5.110 val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
5.111 - val tac_ = Apply_Method' (e_metID, SOME t, is)
5.112 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
5.113 val pos' = ((lev_on o lev_dn) p, Frm)
5.114 - in (*implicit Take*) generate1 thy tac_ is pos' pt end
5.115 + in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
5.116
5.117 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
5.118 let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
5.119 @@ -427,10 +428,11 @@
5.120 let val (pt,c) = cappend_form pt p l f
5.121 val pt = update_branch pt p TransitiveB (*040312*)
5.122
5.123 + val ctxt = e_ctxt;
5.124 val is = init_istate (Rewrite_Set (id_rls rls)) f
5.125 - val tac_ = Apply_Method' (e_metID, SOME t, is)
5.126 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
5.127 val pos' = ((lev_on o lev_dn) p, Frm)
5.128 - in (*implicit Take*) generate1 thy tac_ is pos' pt end
5.129 + in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
5.130
5.131 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
5.132 let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
5.133 @@ -485,12 +487,11 @@
5.134 error ("generate1: not impl.for "^(tac_2str m'))
5.135 ;
5.136
5.137 -
5.138 fun generate_hard thy m' (p,p_) pt =
5.139 let
5.140 val p = case p_ of Frm => p | Res => lev_on p
5.141 | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
5.142 - in generate1 thy m' e_istate (p,p_) pt end;
5.143 + in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
5.144
5.145
5.146
5.147 @@ -549,14 +550,14 @@
5.148 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
5.149 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
5.150 let val (res, asm) = (res_from_taci o last_elem) tacis
5.151 - val (SOME ist,_) = get_obj g_loc pt p
5.152 + val (SOME (ist, ctxt),_) = get_obj g_loc pt p
5.153 val form = get_obj g_form pt p
5.154 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
5.155 - val tacis = (Begin_Trans, Begin_Trans' form, (pos, Uistate))
5.156 + val tacis = (Begin_Trans, Begin_Trans' form, (pos, (Uistate, e_ctxt)))
5.157 ::(insert_pos ((lev_on o lev_dn) p) tacis)
5.158 @ [(End_Trans, End_Trans' (res, asm),
5.159 (pos_plus (length tacis) (lev_dn p, Res),
5.160 - new_val res ist))]
5.161 + (new_val res ist, ctxt)))]
5.162 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
5.163 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
5.164 val pt = update_tac pt p (Derive (id_rls nrls))
5.165 @@ -570,14 +571,14 @@
5.166 (*inform at Res: append a Transitive-PrfObj FIXME?0402 other branch-types ?
5.167 and transfer the istate (from _after_ compare_deriv) from Res to new Res*)
5.168 let val (res, asm) = (res_from_taci o last_elem) tacis
5.169 - val (_, SOME ist) = get_obj g_loc pt p
5.170 + val (_, SOME (ist, ctxt)) = get_obj g_loc pt p
5.171 val (f,a) = get_obj g_result pt p
5.172 val p = lev_on p(*---------------only difference to (..,Frm) above*);
5.173 - val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), Uistate))
5.174 + val tacis = (Begin_Trans, Begin_Trans' f, ((p, Frm), (Uistate, e_ctxt)))
5.175 ::(insert_pos ((lev_on o lev_dn) p) tacis)
5.176 @ [(End_Trans, End_Trans' (res, asm),
5.177 (pos_plus (length tacis) (lev_dn p, Res),
5.178 - new_val res ist))];
5.179 + (new_val res ist, ctxt)))];
5.180 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
5.181 val (pt, c, pos as (p,_)) = generate (rev tacis) (pt, [], (p, Res))
5.182 val pt = update_tac pt p (Derive (id_rls nrls))
6.1 --- a/src/Tools/isac/Interpret/inform.sml Sat Mar 19 15:18:10 2011 +0100
6.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Mar 21 00:32:53 2011 +0100
6.3 @@ -211,7 +211,7 @@
6.4 val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
6.5 val spec = (dI, pI, mI)
6.6 val (pt,_) =
6.7 - cappend_problem e_ptree [] e_istate ([], e_spec)
6.8 + cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
6.9 ([], e_spec, hdt)
6.10 val pt = update_spec pt [] spec
6.11 val pt = update_pbl pt [] pits
6.12 @@ -598,11 +598,11 @@
6.13 (Rewrite (rule2thm' r),
6.14 Rewrite' ("Isac", fst ro, erls, false,
6.15 rule2thm' r, t, (t', a)),
6.16 - (e_pos'(*to be updated before generate tacis!!!*), Uistate))
6.17 + (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
6.18 | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
6.19 (Rewrite_Set (rule2rls' r),
6.20 Rewrite_Set' ("Isac", false, rls, t, (t', a)),
6.21 - (e_pos'(*to be updated before generate tacis!!!*), Uistate));
6.22 + (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)));
6.23
6.24 (*fo = ifo excluded already in inform*)
6.25 fun concat_deriv rew_ord erls rules fo ifo =
6.26 @@ -679,8 +679,8 @@
6.27 ((Subproblem _, _, _)::_) =>
6.28 let val ptp as (pt, (p,_)) = all_modspec ptp
6.29 val mI = get_obj g_metID pt p
6.30 - in nxt_solv (Apply_Method' (mI, NONE, e_istate))
6.31 - e_istate ptp end
6.32 + in nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
6.33 + (e_istate, e_ctxt) ptp end
6.34 | _ => cs';
6.35 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
6.36 end;
7.1 --- a/src/Tools/isac/Interpret/mathengine.sml Sat Mar 19 15:18:10 2011 +0100
7.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Mar 21 00:32:53 2011 +0100
7.3 @@ -186,7 +186,7 @@
7.4 Apply_Method mI =>
7.5 (* val Apply_Method mI = tac;
7.6 *)
7.7 - nxt_solv (Apply_Method' (mI, NONE, e_istate)) e_istate ptp
7.8 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
7.9 | _ => nxt_specif tac ptp end
7.10 end;
7.11
8.1 --- a/src/Tools/isac/Interpret/script.sml Sat Mar 19 15:18:10 2011 +0100
8.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Mar 21 00:32:53 2011 +0100
8.3 @@ -69,7 +69,7 @@
8.4 val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
8.5 val is = RrlsState (f',f'',rss,rts)
8.6 val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
8.7 - val (p', cid, mout, pt') = generate1 thy m is p pt
8.8 + val (p', cid, mout, pt') = generate1 thy m (is, e_ctxt) p pt
8.9 in (is, (m, mout, pt', p', cid)::steps) end
8.10 | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa))
8.11 ((r, (f', am))::rts') =
8.12 @@ -77,7 +77,7 @@
8.13 val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am))
8.14 val is = RrlsState (f',f'',rss,rts)
8.15 val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
8.16 - val (p', cid, mout, pt') = generate1 thy m is p pt
8.17 + val (p', cid, mout, pt') = generate1 thy m (is, e_ctxt) p pt
8.18 in rts2steps ((m, mout, pt', p', cid)::steps)
8.19 ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
8.20
8.21 @@ -1108,13 +1108,13 @@
8.22 let (*val _=tracing("### assy: Ass ("^tac_2str m^", "^
8.23 term2str v'^")");*)
8.24 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
8.25 - (ScrState (E,l,a',v',S,true)) (p',p_) pt;
8.26 + (ScrState (E,l,a',v',S,true), e_ctxt) (p',p_) pt;
8.27 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
8.28 | AssWeak (m,v') =>
8.29 let (*val _=tracing("### assy: Ass Weak("^tac_2str m^", "^
8.30 term2str v'^")");*)
8.31 val (p'',c',f',pt') = generate1 (assoc_thy thy') m
8.32 - (ScrState (E,l,a',v',S,false)) (p',p_) pt;
8.33 + (ScrState (E,l,a',v',S,false), e_ctxt) (p',p_) pt;
8.34 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
8.35 | NotAss =>
8.36 ((*tracing("### assy, NotAss");*)
8.37 @@ -1125,7 +1125,7 @@
8.38 Appl m' =>
8.39 let val is = (E,l,a',tac_2res m',S,false(*FIXXXME*))
8.40 val (p'',c',f',pt') =
8.41 - generate1 (assoc_thy thy') m' (ScrState is) (p',p_) pt;
8.42 + generate1 (assoc_thy thy') m' (ScrState is, e_ctxt) (p',p_) pt;
8.43 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
8.44 | Notappl _ =>
8.45 (NasNap (v, E))
8.46 @@ -1328,39 +1328,14 @@
8.47 RrlsState (_,f'',rss,rts)) = (m, (p,p_), sc, is);
8.48 *)
8.49 fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p)
8.50 - (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts)) =
8.51 + (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
8.52 (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
8.53 [] => NotLocatable
8.54 | rts' =>
8.55 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
8.56 -(* val p as(p',p_)=(p,p_);val scr as Script(h $ body)=sc;val (E,l,a,v,S,bb)=is;
8.57 - locate_gen (thy':theory') (m:tac_) ((pt,p):ptree * pos')
8.58 - (scr,d) (E,l,a,v,S,bb);
8.59 - 9.6.03
8.60 - val ts = (thy',srls);
8.61 - val p = (p,p_);
8.62 - val (scr as Script (h $ body)) = (sc);
8.63 - val ScrState (E,l,a,v,S,b) = (is);
8.64
8.65 - val (ts as (thy',srls), m, (pt,p),
8.66 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b))) =
8.67 - ((thy',srls), m, (pt,(p,p_)), (sc,d), is);
8.68 - locate_gen (thy',srls) m (pt,p) (Script(h $ body),d)(ScrState(E,l,a,v,S,b));
8.69 -
8.70 - val (ts as (thy',srls), m, (pt,p),
8.71 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b))) =
8.72 - ((thy',srls), m', (pt,(lev_on p,Frm)), (sc,d), is');
8.73 -
8.74 - val (ts as (thy',srls), m, (pt,p),
8.75 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b))) =
8.76 - ((thy',srls), m', (pt,(p, Res)), (sc,d), is');
8.77 -
8.78 - val (ts as (thy',srls), m, (pt,p),
8.79 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b))) =
8.80 - ((thy',srls), m, (pt,(p,p_)), (sc,d), is);
8.81 - *)
8.82 | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos')
8.83 - (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b)) =
8.84 + (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
8.85 let (*val _= tracing("### locate_gen-----------------: is=");
8.86 val _= tracing( istate2str (ScrState (E,l,a,v,S,b)));
8.87 val _= tracing("### locate_gen: l= "^loc_2str l^", p= "^pos'2str p)*)
8.88 @@ -1388,7 +1363,7 @@
8.89 (*WN.12.03: noticed, that pos is also updated in assy !?!
8.90 instead take p' from Assoc ?????????????????????????????*)
8.91 val (p'',c'',f'',pt'') =
8.92 - generate1 thy m (ScrState is) (po',p_) pt;
8.93 + generate1 thy m (ScrState is, e_ctxt) (po',p_) pt;
8.94 (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*)
8.95 (*drop the intermediate steps !*)
8.96 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
8.97 @@ -1407,14 +1382,14 @@
8.98 ((*tracing"4### locate_gen Assoc after Fini";*)
8.99 if rew_only ss
8.100 then let val(p'',c'',f'',pt'') =
8.101 - generate1 thy m (ScrState is) p' pt;
8.102 + generate1 thy m (ScrState is, e_ctxt) p' pt;
8.103 (*drop the intermediate steps !*)
8.104 in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
8.105 else NotLocatable)
8.106 | _ => ((*tracing ("#### locate_gen: after Fini");*)
8.107 NotLocatable))
8.108 end
8.109 - | locate_gen _ m _ (sc,_) is =
8.110 + | locate_gen _ m _ (sc,_) (is, ctxt) =
8.111 error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
8.112 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is));
8.113
8.114 @@ -1775,24 +1750,24 @@
8.115 val (thy, (pt,p), Rfuns {next_rule=ne,...}, RrlsState (f,f',rss,_)) =
8.116 (thy', (pt',p'), sc, is');
8.117 *)
8.118 -fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_))=
8.119 - if f = f' then (End_Detail' (f',[])(*8.6.03*), Uistate,
8.120 +fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt)=
8.121 + if f = f' then (End_Detail' (f',[])(*8.6.03*), (Uistate, e_ctxt),
8.122 (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*)))
8.123 (*finished*)
8.124 else (case next_rule rss f of
8.125 - NONE => (Empty_Tac_, Uistate, (e_term, Sundef)) (*helpless*)
8.126 + NONE => (Empty_Tac_, (Uistate, e_ctxt), (e_term, Sundef)) (*helpless*)
8.127 (* val SOME (Thm (id,thm)) = next_rule rss f;
8.128 *)
8.129 | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) =>
8.130 (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false,
8.131 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])),
8.132 - Uistate, (e_term, Sundef))) (*next stac*)
8.133 + (Uistate, e_ctxt), (e_term, Sundef))) (*next stac*)
8.134
8.135 (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
8.136 ((thy',srls), (pt,pos), sc, is);
8.137 *)
8.138 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
8.139 - (ScrState (E,l,a,v,s,b)) =
8.140 + (ScrState (E,l,a,v,s,b), ctxt) =
8.141 ((*tracing("### next_tac-----------------: E= ");
8.142 tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
8.143 case if l=[] then appy thy ptp E [R] body NONE v
8.144 @@ -1802,13 +1777,13 @@
8.145 (true, p', _) =>
8.146 let val (_,pblID,_) = get_obj g_spec pt p';
8.147 in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
8.148 - e_istate, (v,s)) end
8.149 - | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), e_istate, (v,s)))
8.150 - | Napp _ => (Empty_Tac_, e_istate, (e_term, Sundef)) (*helpless*)
8.151 - | Appy (m', scrst as (_,_,_,v,_,_)) => (m', ScrState scrst,
8.152 + (e_istate, ctxt), (v,s)) end
8.153 + | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
8.154 + | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef)) (*helpless*)
8.155 + | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, e_ctxt),
8.156 (v, Sundef))) (*next stac*)
8.157
8.158 - | next_tac _ _ _ is = error ("next_tac: not impl for "^
8.159 + | next_tac _ _ _ (is, _) = error ("next_tac: not impl for "^
8.160 (istate2str is));
8.161
8.162
8.163 @@ -1849,7 +1824,7 @@
8.164 \formals: "^terms2str formals^"\n\
8.165 \actuals: "^terms2str actuals)
8.166 val env = relate_args [] formals actuals;
8.167 - in (ScrState (env,[],NONE,e_term,Safe,true), scr):istate * scr end;
8.168 + in (ScrState (env,[],NONE,e_term,Safe,true), e_ctxt, scr):istate * Proof.context * scr end;
8.169
8.170 (*.decide, where to get script/istate from:
8.171 (*1*) from PblObj.env: at begin of script if no init_form
8.172 @@ -1874,7 +1849,7 @@
8.173 val metID = get_obj g_metID pt p'
8.174 val {srls,...} = get_met metID
8.175 in (*if last_elem p = 0 (*nothing written to pt yet*)
8.176 - then let val (is, sc) = init_scrstate thy itms metID
8.177 + then let val (is, ctxt, sc) = init_scrstate thy itms metID
8.178 in (srls, is, sc) end
8.179 else*) (srls, get_istate pt (p,p_), (#scr o get_met) metID)
8.180 end
8.181 @@ -1889,15 +1864,15 @@
8.182 end;
8.183
8.184 (*.get script and istate from PblObj, see (*1*) above.*)
8.185 -fun from_pblobj' thy' (p,p_) pt =
8.186 +fun from_pblobj' thy' (p,p_) pt =
8.187 let val p' = par_pblobj pt p
8.188 val thy = assoc_thy thy'
8.189 val PblObj{meth=itms,...} = get_obj I pt p'
8.190 val metID = get_obj g_metID pt p'
8.191 val {srls,scr,...} = get_met metID
8.192 in if last_elem p = 0 (*nothing written to pt yet*)
8.193 - then let val (is, scr) = init_scrstate thy itms metID
8.194 - in (srls, is, scr) end
8.195 + then let val (is, ctxt, scr) = init_scrstate thy itms metID
8.196 + in (srls, (is, ctxt), scr) end
8.197 else (srls, get_istate pt (p,p_), scr)
8.198 end;
8.199
8.200 @@ -1923,7 +1898,7 @@
8.201 val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
8.202 else metID
8.203 val {scr=Script sc,srls,...} = get_met metID'
8.204 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
8.205 + val (ScrState (env,_,a,v,_,_), ctxt) = get_istate pt (p,p_);
8.206 in map ((stac2tac pt thy) o rep_stacexpr o #2 o
8.207 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
8.208 (*
8.209 @@ -1950,7 +1925,7 @@
8.210 then (thd3 o snd3) (get_obj g_origin pt pp)
8.211 else metID
8.212 val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
8.213 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
8.214 + val (ScrState (env,_,a,v,_,_), ctxt) = get_istate pt (p,p_)
8.215 val alltacs = (*we expect at least 1 stac in a script*)
8.216 map ((stac2tac pt thy) o rep_stacexpr o #2 o
8.217 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
9.1 --- a/src/Tools/isac/Interpret/solve.sml Sat Mar 19 15:18:10 2011 +0100
9.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Mar 21 00:32:53 2011 +0100
9.3 @@ -142,13 +142,13 @@
9.4 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
9.5 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
9.6 *)
9.7 -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _))
9.8 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _))
9.9 (pt:ptree, (pos as (p,_))) =
9.10 let val {srls,...} = get_met mI;
9.11 val PblObj{meth=itms,...} = get_obj I pt p;
9.12 val thy' = get_obj g_domID pt p;
9.13 val thy = assoc_thy thy';
9.14 - val (is as ScrState (env,_,_,_,_,_), sc) = init_scrstate thy itms mI;
9.15 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
9.16 val ini = init_form thy sc env;
9.17 val p = lev_dn p;
9.18 in
9.19 @@ -156,16 +156,16 @@
9.20 SOME t => (* val SOME t = ini;
9.21 *)
9.22 let val (pos,c,_,pt) =
9.23 - generate1 thy (Apply_Method' (mI, SOME t, is))
9.24 - is (lev_on p, Frm)(*implicit Take*) pt;
9.25 - in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is),
9.26 - ((lev_on p, Frm), is))], c, (pt,pos)):calcstate')
9.27 + generate1 thy (Apply_Method' (mI, SOME t, is, ctxt))
9.28 + (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
9.29 + in ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt),
9.30 + ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate')
9.31 end
9.32 | NONE => (*execute the first tac in the Script, compare solve m*)
9.33 - let val (m', is', _) = next_tac (thy', srls) (pt, (p, Res)) sc is;
9.34 + let val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
9.35 val d = e_rls (*FIXME: get simplifier from domID*);
9.36 in
9.37 - case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) is' of
9.38 + case locate_gen (thy',srls) m' (pt,(p, Res))(sc,d) (is', ctxt') of
9.39 Steps (is'', ss as (m'',f',pt',p',c')::_) =>
9.40 (* val Steps (is'', ss as (m'',f',pt',p',c')::_) =
9.41 locate_gen (thy',srls) m' (pt,(p,Res)) (sc,d) is';
9.42 @@ -175,7 +175,7 @@
9.43 let val (p,ps,f,pt) =
9.44 generate_hard (assoc_thy "Isac") m (p,Frm) pt;
9.45 in ("not-found-in-script",
9.46 - ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
9.47 + ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
9.48 (*just-before------------------------------------------------------
9.49 ("ok",([(Apply_Method mI,Apply_Method'(mI,NONE,e_istate),
9.50 (pos, is))],
9.51 @@ -189,7 +189,7 @@
9.52 val p' = lev_dn_ (p,Res);
9.53 val pt = update_metID pt (par_pblobj pt p) e_metID;
9.54 in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
9.55 - [(Empty_Tac, Empty_Tac_, (po, Uistate))], [], (pt,p'))) end
9.56 + [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end
9.57
9.58 (* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
9.59 ( m, (pt, pos));
9.60 @@ -204,20 +204,20 @@
9.61 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
9.62 val metID = get_obj g_metID pt pp;
9.63 val {srls=srls,scr=sc,...} = get_met metID;
9.64 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
9.65 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_);
9.66 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
9.67 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
9.68 val thy' = get_obj g_domID pt pp;
9.69 val thy = assoc_thy thy';
9.70 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
9.71 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
9.72 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
9.73
9.74 in if pp = [] then
9.75 let val is = ScrState (E,l,a,scval,scsaf,b)
9.76 val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
9.77 - val (pos,ps,f,pt) = generate1 thy tac_ is (pp,Res) pt;
9.78 + val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
9.79 in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
9.80 - [(Check_Postcond pI, tac_, ((pp,Res),is))], ps,(pt,pos))) end
9.81 + [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
9.82 else
9.83 let
9.84 (*resume script of parpbl, transfer value of subpbl-script*)
9.85 @@ -226,21 +226,21 @@
9.86 val thy = assoc_thy thy';
9.87 val metID = get_obj g_metID pt ppp;
9.88 val sc = (#scr o get_met) metID;
9.89 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm);
9.90 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm);
9.91 (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
9.92 val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
9.93 val _=tracing("### solve Check_postc, is'= "^
9.94 (istate2str (E,l,a,scval,scsaf,b)));*)
9.95 val ((p,p_),ps,f,pt) =
9.96 generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
9.97 - (ScrState (E,l,a,scval,scsaf,b)) (pp,Res) pt;
9.98 + (ScrState (E,l,a,scval,scsaf,b), ctxt) (pp,Res) pt;
9.99 (*val _=tracing("### solve Check_postc, is(pt')= "^
9.100 (istate2str (get_istate pt ([3],Res))));
9.101 val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) sc
9.102 (ScrState (E,l,a,scval,scsaf,b));*)
9.103 in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
9.104 ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
9.105 - ((pp,Res), ScrState (E,l,a,scval,scsaf,b)))],ps,(pt,(p,p_))))
9.106 + ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt)))],ps,(pt,(p,p_))))
9.107 end
9.108 end
9.109 (* val (msg, cs') =
9.110 @@ -256,7 +256,7 @@
9.111 | solve (_,End_Proof'') (pt, (p,p_)) =
9.112 ("end-proof",
9.113 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
9.114 - [(Empty_Tac,Empty_Tac_,(([],Res),Uistate))],[],(pt,(p,p_))))
9.115 + [(Empty_Tac,Empty_Tac_,(([],Res),(Uistate, e_ctxt)))],[],(pt,(p,p_))))
9.116
9.117 (*-----------vvvvvvvvvvv could be done by generate1 ?!?*)
9.118 | solve (_,End_Detail' t) (pt,(p,p_)) =
9.119 @@ -266,7 +266,7 @@
9.120 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
9.121 val thy' = get_obj g_domID pt pp
9.122 val (srls, is, sc) = from_pblobj' thy' pr pt
9.123 - val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
9.124 + val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
9.125 in ("ok", ((*((pp,Frm(*???*)),is,tac_),
9.126 Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
9.127 tac_2tac tac_, Sundef,*)
9.128 @@ -280,10 +280,10 @@
9.129 could be detail, too !!*)
9.130 then let val ((p,p_),ps,f,pt) =
9.131 generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
9.132 - m e_istate (p,p_) pt;
9.133 + m (e_istate, e_ctxt) (p,p_) pt;
9.134 in ("no-method-specified", (*Free_Solve*)
9.135 ((*((p,p_),Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*)
9.136 - [(Empty_Tac,Empty_Tac_, ((p,p_),Uistate))], ps, (pt,(p,p_)))) end
9.137 + [(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_)))) end
9.138 else
9.139 let
9.140 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.141 @@ -316,7 +316,7 @@
9.142
9.143 (*FIXME.WN050821 compare solve ... nxt_solv*)
9.144 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
9.145 -fun nxt_solv (Apply_Method' (mI,_,_)) _ (pt:ptree, pos as (p,_)) =
9.146 +fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
9.147 (* val ((Apply_Method' (mI,_,_)), _, (pt:ptree, pos as (p,_))) =
9.148 ((Apply_Method' (mI, NONE, e_istate)), e_istate, ptp);
9.149 *)
9.150 @@ -326,23 +326,23 @@
9.151 else complete_metitms oris probl [] ppc
9.152 val thy' = get_obj g_domID pt p;
9.153 val thy = assoc_thy thy';
9.154 - val (is as ScrState (env,_,_,_,_,_), scr) = init_scrstate thy itms mI;
9.155 + val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
9.156 val ini = init_form thy scr env;
9.157 in
9.158 case ini of
9.159 SOME t => (* val SOME t = ini;
9.160 *)
9.161 let val pos = ((lev_on o lev_dn) p, Frm)
9.162 - val tac_ = Apply_Method' (mI, SOME t, is);
9.163 + val tac_ = Apply_Method' (mI, SOME t, is, ctxt);
9.164 val (pos,c,_,pt) = (*implicit Take*)
9.165 - generate1 thy tac_ is pos pt
9.166 + generate1 thy tac_ (is, ctxt) pos pt
9.167 (*val _= ("### nxt_solv Apply_Method, pos= "^pos'2str (lev_on p,Frm));*)
9.168 - in ([(Apply_Method mI, tac_, (pos, is))], c, (pt, pos)):calcstate' end
9.169 + in ([(Apply_Method mI, tac_, (pos, (is, ctxt)))], c, (pt, pos)):calcstate' end
9.170 | NONE =>
9.171 - let val pt = update_env pt (fst pos) (SOME is)
9.172 + let val pt = update_env pt (fst pos) (SOME (is, ctxt))
9.173 val (tacis, c, ptp) = nxt_solve_ (pt, pos)
9.174 in (tacis @
9.175 - [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate), (pos, is))],
9.176 + [(Apply_Method mI, Apply_Method' (mI, NONE, e_istate, e_ctxt), (pos, (is, ctxt)))],
9.177 c, ptp) end
9.178 end
9.179 (* val ("Check_Postcond",Check_Postcond' (pI,_)) = (mI,m);
9.180 @@ -360,12 +360,12 @@
9.181 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
9.182 val metID = get_obj g_metID pt pp;
9.183 val {srls=srls,scr=sc,...} = get_met metID;
9.184 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (p,p_);
9.185 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_);
9.186 (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
9.187 val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
9.188 val thy' = get_obj g_domID pt pp;
9.189 val thy = assoc_thy thy';
9.190 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc is;
9.191 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
9.192 (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
9.193 in if pp = [] then
9.194 let val is = ScrState (E,l,a,scval,scsaf,b)
9.195 @@ -373,8 +373,8 @@
9.196 (*val _= tracing"### nxt_solv2 Apply_Method: stored is =";
9.197 val _= tracing(istate2str is);*)
9.198 val ((p,p_),ps,f,pt) =
9.199 - generate1 thy tac_ is (pp,Res) pt;
9.200 - in ([(Check_Postcond pI, tac_, ((pp,Res), is))],ps,(pt, (p,p_))) end
9.201 + generate1 thy tac_ (is, ctxt) (pp,Res) pt;
9.202 + in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
9.203 else
9.204 let
9.205 (*resume script of parpbl, transfer value of subpbl-script*)
9.206 @@ -383,14 +383,14 @@
9.207 val thy = assoc_thy thy';
9.208 val metID = get_obj g_metID pt ppp;
9.209 val {scr,...} = get_met metID;
9.210 - val is as ScrState (E,l,a,_,_,b) = get_istate pt (pp(*!/p/*),Frm)
9.211 + val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm)
9.212 val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
9.213 val is = ScrState (E,l,a,scval,scsaf,b)
9.214 (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";
9.215 val _= tracing(istate2str is);*)
9.216 - val ((p,p_),ps,f,pt) = generate1 thy tac_ is (pp, Res) pt;
9.217 + val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp, Res) pt;
9.218 (*val (nx,is',_) = next_tac (thy',srls) (pt,(p,p_)) scr is;WN050913*)
9.219 - in ([(Check_Postcond pI, tac_, ((pp, Res), is))], ps, (pt, (p,p_))) end
9.220 + in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, (p,p_))) end
9.221 end
9.222 (* tracing(istate2str(get_istate pt (p,p_)));
9.223 *)
9.224 @@ -503,8 +503,8 @@
9.225 val (ptp as (pt, (p,_))) = (pt, pos);
9.226 *)
9.227 let val (_,_,mI) = get_obj g_spec pt p;
9.228 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))
9.229 - e_istate ptp;
9.230 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
9.231 + (e_istate, e_ctxt) ptp;
9.232 in complete_solve auto (c@c') ptp end;
9.233 (*@@@ vvv @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
9.234 fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
9.235 @@ -528,8 +528,8 @@
9.236 | (_, c', ptp') => complete_solve auto (c@c') ptp'
9.237 and all_solve auto c (ptp as (pt, (p,_)): ptree * pos') =
9.238 let val (_,_,mI) = get_obj g_spec pt p
9.239 - val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate))
9.240 - e_istate ptp
9.241 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt))
9.242 + (e_istate, e_ctxt) ptp
9.243 in complete_solve auto (c@c') ptp end;
9.244
9.245 (*.aux.fun for detailrls with Rrls, reverse rewriting.*)
9.246 @@ -537,7 +537,7 @@
9.247 *)
9.248 fun rul_terms_2nds nds t [] = nds
9.249 | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
9.250 - (append_atomic [] e_istate t (rule2tac [] rule) res Complete EmptyPtree) ::
9.251 + (append_atomic [] (e_istate, e_ctxt) t (rule2tac [] rule) res Complete EmptyPtree) ::
9.252 (rul_terms_2nds nds t' rts);
9.253
9.254
9.255 @@ -562,10 +562,10 @@
9.256 (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
9.257 is wrong for simpl, but working ?!? *)
9.258 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*),
9.259 - SOME t, is)
9.260 + SOME t, is, e_ctxt)
9.261 val pos' = ((lev_on o lev_dn) p, Frm)
9.262 val thy = assoc_thy "Isac"
9.263 - val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
9.264 + val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, e_ctxt) pos' pt
9.265 val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
9.266 val newnds = children (get_nd pt'' p)
9.267 val pt''' = ins_chn newnds pt p
10.1 --- a/src/Tools/isac/Test_Some.thy Sat Mar 19 15:18:10 2011 +0100
10.2 +++ b/src/Tools/isac/Test_Some.thy Mon Mar 21 00:32:53 2011 +0100
10.3 @@ -17,9 +17,8 @@
10.4 (*..............................................########......................*)
10.5 *}
10.6
10.7 -ML {*parseNEW*}
10.8 -
10.9 -use"../../../test/Tools/isac/Interpret/mstools.sml";
10.10 +use "../../../test/Tools/isac/ProgLang/calculate.sml";
10.11 +use "../../../test/Tools/isac/Interpret/mathengine.sml";
10.12
10.13 end
10.14