1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 18 09:37:35 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 18 09:45:45 2011 +0200
1.3 @@ -1122,13 +1122,13 @@
1.4 (*. called only if no_met is specified .*)
1.5 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
1.6 let
1.7 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ...}) = get_obj I pt p;
1.8 + val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;
1.9 val {prls,met,ppc,thy,where_,...} = get_pbt pIre
1.10 val (domID, metID) =
1.11 (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.12 val ((p,_),_,_,pt) =
1.13 generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[]))
1.14 - (Uistate, e_ctxt) pos pt
1.15 + (Uistate, ctxt) pos pt
1.16 val (pbl, pre, pb) = ([], [], false)
1.17 in ((p, Pbl), (pos, Uistate),
1.18 Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.19 @@ -1137,9 +1137,10 @@
1.20 end
1.21
1.22 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1.23 - let
1.24 + let
1.25 + val ctxt = get_ctxt pt pos
1.26 val (pos,_,_,pt) =
1.27 - generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.28 + generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.29 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1.30 Model_Problem, Safe, pt)
1.31 end
1.32 @@ -1147,10 +1148,10 @@
1.33 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1.34 let
1.35 val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1.36 - meth=met, ...}) = get_obj I pt p;
1.37 + meth=met, ctxt, ...}) = get_obj I pt p;
1.38 val thy = assoc_thy dI
1.39 val ((p,Pbl),_,_,pt)=
1.40 - generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1.41 + generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt
1.42 val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.43 val mI'' = if mI=e_metID then mI' else mI;
1.44 val (_, nxt) =
1.45 @@ -1164,7 +1165,7 @@
1.46 | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1.47 let
1.48 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.49 - meth=met, ...}) = get_obj I pt p;
1.50 + meth=met, ctxt, ...}) = get_obj I pt p;
1.51 val {ppc,pre,prls,...} = get_met mID
1.52 val thy = assoc_thy dI
1.53 val oris = add_field' thy ppc oris;
1.54 @@ -1173,7 +1174,7 @@
1.55 val met = if met=[] then pbl else met;
1.56 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.57 val (pos, _, _, pt) =
1.58 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.59 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.60 val (_,nxt) =
1.61 nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1.62 ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1.63 @@ -1192,7 +1193,7 @@
1.64 val p_ = case p_ of Met => Met | _ => Pbl
1.65 val thy = assoc_thy domID;
1.66 val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1.67 - probl=pbl, spec=(dI,pI,mI), ...}) = get_obj I pt p;
1.68 + probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
1.69 val mppc = case p_ of Met => met | _ => pbl;
1.70 val cpI = if pI = e_pblID then pI' else pI;
1.71 val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1.72 @@ -1216,7 +1217,7 @@
1.73 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.74 let
1.75 val ((p,p_),_,_,pt) =
1.76 - generate1 thy (Specify_Theory' domID) (Uistate, e_ctxt) (p,p_) pt
1.77 + generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.78 val (p_,nxt) =
1.79 nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
1.80 in ((p,p_), (pos,Uistate),
1.81 @@ -1249,8 +1250,8 @@
1.82 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.83 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.84 val ((p,Pbl),c,_,pt') =
1.85 - generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1.86 - in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate'
1.87 + generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt
1.88 + in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate'
1.89 end
1.90 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.91 FIXME ..and dont abuse a tactic for that purpose*)
1.92 @@ -1275,8 +1276,8 @@
1.93 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.94 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.95 val ((p,Met),c,_,pt') =
1.96 - generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1.97 - in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1.98 + generate1 thy tac_ (Uistate, ctxt) (p,Met) pt
1.99 + in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end
1.100 | Err msg => ([(*tacis*)], [], ptp)
1.101 (*nxt_me collects tacis until not hide; here just no progress*)
1.102 end;
1.103 @@ -1357,7 +1358,7 @@
1.104 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1.105 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1.106 let
1.107 - val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1.108 + val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p
1.109 val (dI, pI, mI) = some_spec ospec spec
1.110 val thy = assoc_thy dI
1.111 val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.112 @@ -1370,7 +1371,7 @@
1.113 | _ => complete_mod_ (oris, mpc, ppc, probl)
1.114 (*----------------------------------------------------------------*)
1.115 val tac_ = Model_Problem' (pI, pbl, met)
1.116 - val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1.117 + val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt
1.118 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1.119
1.120 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.121 @@ -1380,7 +1381,7 @@
1.122 (*. called only if no_met is specified .*)
1.123 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1.124 let
1.125 - val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1.126 + val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p
1.127 val opt = refine_ori oris pI
1.128 in
1.129 case opt of
1.130 @@ -1393,7 +1394,7 @@
1.131 val thy = assoc_thy dI
1.132 val (pos,c,_,pt) =
1.133 generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.134 - (Uistate, e_ctxt) pos pt
1.135 + (Uistate, ctxt) pos pt
1.136 in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.137 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.138 end
1.139 @@ -1402,7 +1403,7 @@
1.140
1.141 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1.142 let
1.143 - val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ...}) = get_obj I pt p
1.144 + val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p
1.145 val thy = if dI' = e_domID then dI else dI'
1.146 in
1.147 case refine_pbl (assoc_thy thy) pI probl of
1.148 @@ -1410,7 +1411,7 @@
1.149 | SOME (rfd as (pI',_)) =>
1.150 let
1.151 val (pos,c,_,pt) = generate1 (assoc_thy thy)
1.152 - (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.153 + (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.154 in ([(Refine_Problem pI, Refine_Problem' rfd,
1.155 (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.156 end
1.157 @@ -1418,7 +1419,7 @@
1.158
1.159 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1.160 let
1.161 - val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ...}) = get_obj I pt p;
1.162 + val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;
1.163 val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.164 val {ppc,where_,prls,...} = get_pbt pI
1.165 val pbl as (_,(itms,_)) =
1.166 @@ -1427,7 +1428,7 @@
1.167 else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1.168 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.169 val ((p,Pbl),c,_,pt) =
1.170 - generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1.171 + generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt
1.172 in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1.173 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1.174 end
1.175 @@ -1437,7 +1438,7 @@
1.176 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1.177 let
1.178 val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.179 - meth=met, ...}) = get_obj I pt p;
1.180 + meth=met, ctxt, ...}) = get_obj I pt p;
1.181 val {ppc,pre,prls,...} = get_met mID
1.182 val thy = assoc_thy dI
1.183 val oris = add_field' thy ppc oris;
1.184 @@ -1446,28 +1447,30 @@
1.185 val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1.186 val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.187 val (pos,c,_,pt)=
1.188 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.189 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.190 in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1.191 (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1.192 end
1.193
1.194 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1.195 let
1.196 + val ctxt = get_ctxt pt pos
1.197 val (dI',_,_) = get_obj g_spec pt p
1.198 val (pos,c,_,pt) =
1.199 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, e_ctxt) pos pt
1.200 + generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.201 in (*FIXXXME: check if pbl can still be parsed*)
1.202 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.203 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1.204 (pt, pos))
1.205 end
1.206
1.207 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1.208 let
1.209 + val ctxt = get_ctxt pt pos
1.210 val (dI',_,_) = get_obj g_spec pt p
1.211 val (pos,c,_,pt) =
1.212 - generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, e_ctxt) pos pt
1.213 + generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.214 in (*FIXXXME: check if met can still be parsed*)
1.215 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.216 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,
1.217 (pt, pos))
1.218 end
1.219