1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sun May 15 12:36:29 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sun May 15 13:23:12 2011 +0200
1.3 @@ -1075,29 +1075,29 @@
1.4 end;
1.5
1.6 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.7 - let (* either """"""""""""""" all empty or complete *)
1.8 - val thy = assoc_thy dI';
1.9 - val (oris, ctxt) =
1.10 - if dI' = e_domID orelse pI' = e_pblID
1.11 - then ([], e_ctxt)
1.12 - else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1.13 - val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.14 - (oris, (dI',pI',mI'),e_term)
1.15 - val pt = update_ctxt pt [] ctxt (*FIXME.WN110511*)
1.16 - val {ppc, prls, where_, ...} = get_pbt pI'
1.17 - val (pbl, pre, pb) = ([], [], false)
1.18 - in
1.19 - case mI' of
1.20 - ["no_met"] =>
1.21 - (([], Pbl), (([], Pbl), Uistate),
1.22 - Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.23 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.24 - Refine_Tacitly pI', Safe, pt)
1.25 - | _ =>
1.26 - (([], Pbl), (([], Pbl), Uistate),
1.27 - Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.28 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.29 - Model_Problem, Safe, pt)
1.30 + let (* either """"""""""""""" all empty or complete *)
1.31 + val thy = assoc_thy dI';
1.32 + val (oris, ctxt) =
1.33 + if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1.34 + then ([], e_ctxt)
1.35 + else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1.36 + val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.37 + (oris, (dI',pI',mI'),e_term)
1.38 + val pt = update_ctxt pt [] ctxt
1.39 + val {ppc, prls, where_, ...} = get_pbt pI'
1.40 + val (pbl, pre, pb) = ([], [], false)
1.41 + in
1.42 + case mI' of
1.43 + ["no_met"] =>
1.44 + (([], Pbl), (([], Pbl), Uistate),
1.45 + Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.46 + (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.47 + Refine_Tacitly pI', Safe, pt)
1.48 + | _ =>
1.49 + (([], Pbl), (([], Pbl), Uistate),
1.50 + Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.51 + (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.52 + Model_Problem, Safe, pt)
1.53 end
1.54
1.55 (*ONLY for STARTING modeling phase*)
1.56 @@ -1109,7 +1109,8 @@
1.57 val {ppc,prls,where_,...} = get_pbt pI'
1.58 val pre = check_preconds thy prls where_ pbl
1.59 val pb = foldl and_ (true, map fst pre)
1.60 - val ((p,_),_,_,pt) = generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1.61 + val ((p,_),_,_,pt) =
1.62 + generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
1.63 val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
1.64 (ppc,(#ppc o get_met) mI') (dI',pI',mI');
1.65 in ((p, Pbl), ((p, p_), Uistate),
1.66 @@ -1137,103 +1138,99 @@
1.67
1.68 | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =
1.69 let
1.70 - val (pos,_,_,pt) = generate1 (assoc_thy "Isac")
1.71 - (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.72 + val (pos,_,_,pt) =
1.73 + generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.74 in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd),
1.75 Model_Problem, Safe, pt)
1.76 end
1.77 + (*WN110515 initialise ctxt again from itms and add preconds*)
1.78 + | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1.79 + let
1.80 + val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1.81 + meth=met, ...}) = get_obj I pt p;
1.82 + val thy = assoc_thy dI
1.83 + val ((p,Pbl),_,_,pt)=
1.84 + generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1.85 + val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.86 + val mI'' = if mI=e_metID then mI' else mI;
1.87 + val (_, nxt) =
1.88 + nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1.89 + ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1.90 + in ((p,Pbl), (pos,Uistate),
1.91 + Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),
1.92 + nxt, Safe, pt)
1.93 + end
1.94 + (*WN110515 initialise ctxt again from itms and add preconds*)
1.95 + | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1.96 + let
1.97 + val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.98 + meth=met, ...}) = get_obj I pt p;
1.99 + val {ppc,pre,prls,...} = get_met mID
1.100 + val thy = assoc_thy dI
1.101 + val oris = add_field' thy ppc oris;
1.102 + val dI'' = if dI=e_domID then dI' else dI;
1.103 + val pI'' = if pI = e_pblID then pI' else pI;
1.104 + val met = if met=[] then pbl else met;
1.105 + val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.106 + val (pos, _, _, pt) =
1.107 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.108 + val (_,nxt) =
1.109 + nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1.110 + ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1.111 + in (pos, (pos,Uistate),
1.112 + Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.113 + (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.114 + nxt, Safe, pt)
1.115 + end
1.116
1.117 - | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =
1.118 - let val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI),
1.119 - meth=met, ...}) = get_obj I pt p;
1.120 - val thy = assoc_thy dI
1.121 - val ((p,Pbl),_,_,pt)=
1.122 - generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, e_ctxt) pos pt
1.123 - val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
1.124 - val mI'' = if mI=e_metID then mI' else mI;
1.125 - (*val _=tracing("@@@ specify (Specify_Problem) before nxt_spec")*)
1.126 - val (_,nxt) = nxt_spec Pbl ok oris (dI',pI',mI') (itms, met)
1.127 - ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);
1.128 - in ((p,Pbl), (pos,Uistate),
1.129 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.130 - (Problem pI, itms2itemppc dI'' itms pre))),
1.131 - nxt, Safe, pt) end
1.132 -(* val Specify_Method' mID = nxt; val (p,_) = p;
1.133 - val Specify_Method' mID = m;
1.134 - specify (Specify_Method' mID) (p,p_) c pt;
1.135 - *)
1.136 - | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =
1.137 - let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.138 - meth=met, ...}) = get_obj I pt p;
1.139 - val {ppc,pre,prls,...} = get_met mID
1.140 - val thy = assoc_thy dI
1.141 - val oris = add_field' thy ppc oris;
1.142 - (*val pt = update_oris pt p oris; 20.3.02: repl. "#undef"*)
1.143 - val dI'' = if dI=e_domID then dI' else dI;
1.144 - val pI'' = if pI = e_pblID then pI' else pI;
1.145 - val met = if met=[] then pbl else met;
1.146 - val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.147 - (*val pt = update_met pt p itms;
1.148 - val pt = update_metID pt p mID*)
1.149 - val (pos,_,_,pt)=
1.150 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.151 - (*val _=tracing("@@@ specify (Specify_Method) before nxt_spec")*)
1.152 - val (_,nxt) = nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms)
1.153 - ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);
1.154 - in (pos, (pos,Uistate),
1.155 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
1.156 - (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),
1.157 - nxt, Safe, pt) end
1.158 -(* val Add_Find' ct = nxt; val sel = "#Find";
1.159 - *)
1.160 | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt
1.161 | specify (Add_Find' ct) p c pt = specify_additem "#Find" ct p c pt
1.162 | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt
1.163 -(* val Specify_Theory' domID = m;
1.164 - val (Specify_Theory' domID, (p,p_)) = (m, pos);
1.165 - *)
1.166 +
1.167 | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =
1.168 - let val p_ = case p_ of Met => Met | _ => Pbl
1.169 - val thy = assoc_thy domID;
1.170 - val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1.171 - probl=pbl, spec=(dI,pI,mI), ...}) = get_obj I pt p;
1.172 - val mppc = case p_ of Met => met | _ => pbl;
1.173 - val cpI = if pI = e_pblID then pI' else pI;
1.174 - val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1.175 - val cmI = if mI = e_metID then mI' else mI;
1.176 - val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1.177 - val pre =
1.178 - case p_ of
1.179 - Met => (check_preconds thy mer mwh met)
1.180 - | _ => (check_preconds thy per pwh pbl)
1.181 - val pb = foldl and_ (true, map fst pre)
1.182 - in if domID = dI
1.183 - then let
1.184 - (*val _=tracing("@@@ specify (Specify_Theory) THEN before nxt_spec")*)
1.185 - val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1.186 - (pbl,met) (ppc,mpc) (dI,pI,mI);
1.187 - in ((p,p_), (pos,Uistate),
1.188 - Form'(PpcKF (0,EdUndef,(length p), Nundef,
1.189 - (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.190 - nxt,Safe,pt) end
1.191 - else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.192 - let
1.193 - (*val pt = update_domID pt p domID;11.8.03*)
1.194 - val ((p,p_),_,_,pt) = generate1 thy (Specify_Theory' domID)
1.195 - (Uistate, e_ctxt) (p,p_) pt
1.196 - (*val _=tracing("@@@ specify (Specify_Theory) ELSE before nxt_spec")*)
1.197 - val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') (pbl,met)
1.198 - (ppc,mpc) (domID,pI,mI);
1.199 - in ((p,p_), (pos,Uistate),
1.200 - Form' (PpcKF (0, EdUndef, (length p),Nundef,
1.201 - (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.202 - nxt, Safe,pt) end
1.203 - end
1.204 -(* itms2itemppc thy [](*mpc*) pre
1.205 - *)
1.206 + let
1.207 + val p_ = case p_ of Met => Met | _ => Pbl
1.208 + val thy = assoc_thy domID;
1.209 + val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,
1.210 + probl=pbl, spec=(dI,pI,mI), ...}) = get_obj I pt p;
1.211 + val mppc = case p_ of Met => met | _ => pbl;
1.212 + val cpI = if pI = e_pblID then pI' else pI;
1.213 + val {prls=per,ppc,where_=pwh,...} = get_pbt cpI
1.214 + val cmI = if mI = e_metID then mI' else mI;
1.215 + val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI
1.216 + val pre =
1.217 + case p_ of
1.218 + Met => (check_preconds thy mer mwh met)
1.219 + | _ => (check_preconds thy per pwh pbl)
1.220 + val pb = foldl and_ (true, map fst pre)
1.221 + in
1.222 + if domID = dI
1.223 + then
1.224 + let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI')
1.225 + (pbl,met) (ppc,mpc) (dI,pI,mI);
1.226 + in ((p,p_), (pos,Uistate),
1.227 + Form'(PpcKF (0,EdUndef,(length p), Nundef,
1.228 + (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.229 + nxt,Safe,pt)
1.230 + end
1.231 + else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.232 + let
1.233 + val ((p,p_),_,_,pt) =
1.234 + generate1 thy (Specify_Theory' domID) (Uistate, e_ctxt) (p,p_) pt
1.235 + val (p_,nxt) =
1.236 + nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);
1.237 + in ((p,p_), (pos,Uistate),
1.238 + Form' (PpcKF (0, EdUndef, (length p),Nundef,
1.239 + (header p_ pI cmI, itms2itemppc thy mppc pre))),
1.240 + nxt, Safe,pt)
1.241 + end
1.242 + end
1.243 +
1.244 | specify m' _ _ _ =
1.245 - error ("specify: not impl. for "^tac_2str m');
1.246 + error ("specify: not impl. for " ^ tac_2str m');
1.247
1.248 +(*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
1.249 + -- for input from scratch*)
1.250 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1.251 let
1.252 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.253 @@ -1255,12 +1252,12 @@
1.254 generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1.255 in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate'
1.256 end
1.257 - | Err msg =>
1.258 - (*TODO.WN03 pass error-msgs to the frontend..
1.259 - FIXME ..and dont abuse a tactic for that purpose*)
1.260 + | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.261 + FIXME ..and dont abuse a tactic for that purpose*)
1.262 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.263 (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.264 end
1.265 +
1.266 | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1.267 let
1.268 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.269 @@ -1541,7 +1538,7 @@
1.270 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1.271 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1.272 (pors, (dI, pI, mI), hdl)
1.273 - val pt = update_ctxt pt [] pctxt (* FIXME.WN110511*)
1.274 + val pt = update_ctxt pt [] pctxt
1.275 in ((pt, ([], Pbl)),
1.276 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.277 end;