1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sat Mar 19 15:18:10 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Mar 21 00:32:53 2011 +0100
1.3 @@ -206,11 +206,11 @@
1.4
1.5
1.6
1.7 -(*---------------------------------------------------------------------*)
1.8 +(*---------------------------------------------------------------------
1.9 structure CalcHead (**): CALC_HEAD(**) =
1.10
1.11 struct
1.12 -(*---------------------------------------------------------------------*)
1.13 +---------------------------------------------------------------------*)
1.14
1.15 (* datatypes *)
1.16
1.17 @@ -1055,7 +1055,7 @@
1.18 "#Given" => Add_Given' (ct, met')
1.19 | "#Find" => Add_Find' (ct, met')
1.20 | "#Relate"=> Add_Relation'(ct, met'))
1.21 - Uistate (p,Met) pt
1.22 + (Uistate, e_ctxt) (p,Met) pt
1.23 val pre' = check_preconds thy prls pre met'
1.24 val pb = foldl and_ (true, map fst pre')
1.25 (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
1.26 @@ -1097,7 +1097,7 @@
1.27 "#Given" => Add_Given' (ct, pbl')
1.28 | "#Find" => Add_Find' (ct, pbl')
1.29 | "#Relate"=> Add_Relation'(ct, pbl'))
1.30 - Uistate (p,Pbl) pt
1.31 + (Uistate, e_ctxt) (p,Pbl) pt
1.32 val pre = check_preconds thy prls where_ pbl'
1.33 val pb = foldl and_ (true, map fst pre)
1.34 (*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
1.35 @@ -1140,7 +1140,7 @@
1.36 val thy = assoc_thy dI';
1.37 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1.38 else prep_ori fmz thy ((#ppc o get_pbt) pI');
1.39 - val (pt,c) = cappend_problem e_ptree [] e_istate (fmz,(dI',pI',mI'))
1.40 + val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1.41 (oris,(dI',pI',mI'),e_term);
1.42 val {ppc,prls,where_,...} = get_pbt pI'
1.43 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1.44 @@ -1173,7 +1173,7 @@
1.45 val pre = check_preconds thy prls where_ pbl
1.46 val pb = foldl and_ (true, map fst pre)
1.47 val ((p,_),_,_,pt) =
1.48 - generate1 thy (Model_Problem'([],pbl,met)) Uistate pos pt
1.49 + generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1.50 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.51 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.52 in ((p,Pbl), ((p,p_),Uistate),
1.53 @@ -1197,7 +1197,7 @@
1.54 if length met = 0 then e_metID else hd met)
1.55 val ((p,_),_,_,pt) =
1.56 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1.57 - Uistate pos pt
1.58 + (Uistate, e_ctxt) pos pt
1.59 (*val pre = check_preconds thy prls where_ pbl
1.60 val pb = foldl and_ (true, map fst pre)*)
1.61 val (pbl, pre, pb) = ([], [], false)
1.62 @@ -1208,7 +1208,7 @@
1.63
1.64 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1.65 let val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1.66 - (Refine_Problem' rfd) Uistate pos pt
1.67 + (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.68 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1.69 Model_Problem, Safe, pt) end
1.70
1.71 @@ -1222,7 +1222,7 @@
1.72 val pt = update_pblID pt p pI;*)
1.73 val thy = assoc_thy dI
1.74 val ((p,Pbl),_,_,pt)=
1.75 - generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
1.76 + generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1.77 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.78 val mI'' = if mI=e_metID then mI' else mI;
1.79 (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1.80 @@ -1250,7 +1250,7 @@
1.81 (*val pt = update_met pt p itms;
1.82 val pt = update_metID pt p mID*)
1.83 val (pos,_,_,pt)=
1.84 - generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1.85 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.86 (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1.87 val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1.88 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1.89 @@ -1294,7 +1294,7 @@
1.90 let
1.91 (*val pt = update_domID pt p domID;11.8.03*)
1.92 val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1.93 - Uistate (p,p_) pt
1.94 + (Uistate, e_ctxt) (p,p_) pt
1.95 (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1.96 val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1.97 (ppc,mpc) (domID,pI,mI);
1.98 @@ -1330,15 +1330,15 @@
1.99 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.100 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.101 val ((p,Pbl),c,_,pt') =
1.102 - generate1 thy tac_ Uistate (p,Pbl) pt
1.103 - in ([(tac,tac_,((p,Pbl),Uistate))], c, (pt',(p,Pbl))):calcstate' end
1.104 + generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1.105 + in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1.106
1.107 | Err msg =>
1.108 (*TODO.WN03 pass error-msgs to the frontend..
1.109 FIXME ..and dont abuse a tactic for that purpose*)
1.110 ([(Tac msg,
1.111 Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.112 - (e_pos', e_istate))], [], ptp)
1.113 + (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.114 end
1.115
1.116 (* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1.117 @@ -1361,8 +1361,8 @@
1.118 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.119 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.120 val ((p,Met),c,_,pt') =
1.121 - generate1 thy tac_ Uistate (p,Met) pt
1.122 - in ([(tac,tac_,((p,Met), Uistate))], c, (pt',(p,Met))) end
1.123 + generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1.124 + in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1.125
1.126 | Err msg => ([(*tacis*)], [], ptp)
1.127 (*nxt_me collects tacis until not hide; here just no progress*)
1.128 @@ -1463,8 +1463,8 @@
1.129 | _ => complete_mod_ (oris, mpc, ppc, probl)
1.130 (*----------------------------------------------------------------*)
1.131 val tac_ = Model_Problem' (pI, pbl, met)
1.132 - val (pos,c,_,pt) = generate1 thy tac_ Uistate pos pt
1.133 - in ([(tac,tac_, (pos, Uistate))], c, (pt,pos)):calcstate' end
1.134 + val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1.135 + in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1.136
1.137 (* val Add_Find ct = tac;
1.138 *)
1.139 @@ -1485,9 +1485,9 @@
1.140 val thy = assoc_thy dI
1.141 val (pos,c,_,pt) =
1.142 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.143 - Uistate pos pt
1.144 + (Uistate, e_ctxt) pos pt
1.145 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.146 - (pos, Uistate))], c, (pt,pos)) end
1.147 + (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1.148 | NONE => ([], [], ptp)
1.149 end
1.150
1.151 @@ -1500,9 +1500,9 @@
1.152 | SOME (rfd as (pI',_)) =>
1.153 let val (pos,c,_,pt) =
1.154 generate1 (assoc_thy thy)
1.155 - (Refine_Problem' rfd) Uistate pos pt
1.156 + (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.157 in ([(Refine_Problem pI, Refine_Problem' rfd,
1.158 - (pos, Uistate))], c, (pt,pos)) end
1.159 + (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1.160 end
1.161
1.162 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1.163 @@ -1516,9 +1516,9 @@
1.164 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1.165 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.166 val ((p,Pbl),c,_,pt)=
1.167 - generate1 thy (Specify_Problem' (pI, pbl)) Uistate pos pt
1.168 + generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1.169 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1.170 - (pos,Uistate))], c, (pt,pos)) end
1.171 + (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1.172
1.173 (*transfers oris (not required in pbl) to met-model for script-env
1.174 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1.175 @@ -1533,26 +1533,26 @@
1.176 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1.177 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.178 val (pos,c,_,pt)=
1.179 - generate1 thy (Specify_Method' (mID, oris, itms)) Uistate pos pt
1.180 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.181 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1.182 - (pos,Uistate))], c, (pt,pos)) end
1.183 + (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1.184
1.185 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1.186 let val (dI',_,_) = get_obj g_spec pt p
1.187 val (pos,c,_,pt) =
1.188 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1.189 - Uistate pos pt
1.190 + (Uistate, e_ctxt) pos pt
1.191 in (*FIXXXME: check if pbl can still be parsed*)
1.192 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1.193 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.194 (pt, pos)) end
1.195
1.196 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1.197 let val (dI',_,_) = get_obj g_spec pt p
1.198 val (pos,c,_,pt) =
1.199 generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1.200 - Uistate pos pt
1.201 + (Uistate, e_ctxt) pos pt
1.202 in (*FIXXXME: check if met can still be parsed*)
1.203 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,Uistate))], c,
1.204 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.205 (pt, pos)) end
1.206
1.207 | nxt_specif m' _ =
1.208 @@ -1579,7 +1579,7 @@
1.209 val thy = assoc_thy dI
1.210 val mI = if mI = [] then hd met else mI
1.211 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.212 - val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1.213 + val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.214 ([], (dI,pI,mI), hdl)
1.215 val pt = update_spec pt [] (dI,pI,mI)
1.216 val pits = init_pbl' ppc
1.217 @@ -1589,14 +1589,14 @@
1.218 let val {ppc,...} = get_met mI
1.219 val dI = if dI = "" then "Isac" else dI
1.220 val thy = assoc_thy dI
1.221 - val (pt,_) = cappend_problem e_ptree [] e_istate ([], (dI,pI,mI))
1.222 + val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.223 ([], (dI,pI,mI), e_term(*FIXME met*))
1.224 val pt = update_spec pt [] (dI,pI,mI)
1.225 val mits = init_pbl' ppc
1.226 val pt = update_met pt [] mits
1.227 in ((pt, ([], Met)), []) : calcstate end
1.228 else (* new example, pepare for interactive modeling *)
1.229 - let val (pt,_) = cappend_problem e_ptree [] e_istate ([], e_spec)
1.230 + let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.231 ([], e_spec, e_term)
1.232 in ((pt,([],Pbl)), []) : calcstate end
1.233 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1.234 @@ -1615,7 +1615,7 @@
1.235 NONE => pblterm dI pI
1.236 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1.237 ~~~ vals_of_oris pors) t
1.238 - val (pt, _) = cappend_problem e_ptree [] e_istate (fmz, (dI, pI, mI))
1.239 + val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1.240 (pors, (dI, pI, mI), hdl)
1.241 in ((pt, ([], Pbl)),
1.242 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.243 @@ -2090,9 +2090,9 @@
1.244 val pt = update_spec pt p e_spec
1.245 in (pt, (p,Pbl):pos') end;
1.246
1.247 -(*---------------------------------------------------------------------*)
1.248 +(*---------------------------------------------------------------------
1.249 end
1.250
1.251 open CalcHead;
1.252 -(*---------------------------------------------------------------------*)
1.253 +---------------------------------------------------------------------*)
1.254