intermed. ctxt ..: started check e_ctxt
TODOs:
# nxt_specif_additem: declare_constraints for ct (without dsc) into PblObj{ctxt, ...}
# Specify_Problem, _Method: declare_constraints from itms and add precond
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;
2.1 --- a/src/Tools/isac/Interpret/ctree.sml Sun May 15 12:36:29 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/ctree.sml Sun May 15 13:23:12 2011 +0200
2.3 @@ -1959,16 +1959,16 @@
2.4 );
2.5 (*TODO.WN050305 redesign the handling of istates*)
2.6 fun cappend_atomic pt p ist_res f r f' s =
2.7 - if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.8 - then (*after Take: transfer Frm and respective istate*)
2.9 - let val (ist_form, f) = (get_loc pt (p,Frm),
2.10 - get_obj g_form pt p)
2.11 - val (pt, cs) = cut_tree pt (p,Frm)
2.12 - val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
2.13 - val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2.14 - in (pt, cs) end
2.15 - else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2.16 -
2.17 + if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.18 + then (*after Take: transfer Frm and respective istate*)
2.19 + let
2.20 + val (ist_form, f) =
2.21 + (get_loc pt (p,Frm), get_obj g_form pt p)
2.22 + val (pt, cs) = cut_tree pt (p,Frm)
2.23 + val pt = append_atomic p (e_istate, e_ctxt) f r f' s pt
2.24 + val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
2.25 + in (pt, cs) end
2.26 + else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
2.27
2.28 (* called by Take *)
2.29 fun append_form p l f pt =
3.1 --- a/src/Tools/isac/Interpret/generate.sml Sun May 15 12:36:29 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/generate.sml Sun May 15 13:23:12 2011 +0200
3.3 @@ -264,13 +264,14 @@
3.4 case p_ of
3.5 Pbl => update_pbl pt p itmlist
3.6 | Met => update_met pt p itmlist)
3.7 -
3.8 + (*WN110515 probably declare_constraints with input item (without dsc) --
3.9 + -- important when specifying without formalisation*)
3.10 | generate1 thy (Add_Find' (_, itmlist)) _ (pos as (p,p_)) pt =
3.11 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
3.12 case p_ of
3.13 Pbl => update_pbl pt p itmlist
3.14 | Met => update_met pt p itmlist)
3.15 -
3.16 + (*WN110515 probably declare_constraints with input item (without dsc)*)
3.17 | generate1 thy (Add_Relation' (_, itmlist)) _ (pos as (p,p_)) pt =
3.18 (pos,[],Form' (PpcKF (0,EdUndef,0,Nundef,(Upblmet,itms2itemppc thy [][]))),
3.19 case p_ of
3.20 @@ -483,38 +484,28 @@
3.21 let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
3.22 val (pt,c) =
3.23 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
3.24 - val pt = update_ctxt pt p ctxt (*FIXME.WN110511*)
3.25 + val pt = update_ctxt pt p ctxt
3.26 val f = Syntax.string_of_term (thy2ctxt thy) f;
3.27 in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
3.28
3.29 | generate1 thy m' _ _ _ =
3.30 - error ("generate1: not impl.for "^(tac_2str m'))
3.31 -;
3.32 -
3.33 + error ("generate1: not impl.for "^(tac_2str m'));
3.34
3.35 fun generate_hard thy m' (p,p_) pt =
3.36 let
3.37 - val p = case p_ of Frm => p | Res => lev_on p
3.38 - | _ => error ("generate_hard: call by "^(pos'2str (p,p_)));
3.39 + val p =
3.40 + case p_ of
3.41 + Frm => p | Res => lev_on p
3.42 + | _ => error ("generate_hard: call by " ^ pos'2str (p,p_));
3.43 in generate1 thy m' (e_istate, e_ctxt) (p,p_) pt end;
3.44
3.45 -
3.46 -
3.47 (*tacis are in reverse order from nxt_solve_/specify_: last = fst to insert*)
3.48 -(* val (tacis, (pt, _)) = (tacis, ptp);
3.49 -
3.50 - val (tacis, (pt, c, _)) = (rev tacis, (pt, [], (p, Res)));
3.51 - *)
3.52 fun generate ([]: taci list) ptp = ptp
3.53 | generate tacis (pt, c, _:pos'(*!dropped!WN0504redesign generate/tacis?*))=
3.54 - let val (tacis', (_, tac_, (p, is))) = split_last tacis
3.55 - (* for recursion ...
3.56 - (tacis', (_, tac_, (p, is))) = split_last tacis';
3.57 - *)
3.58 - val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
3.59 - in generate tacis' (pt', c@c', p') end;
3.60 -
3.61 -
3.62 + let
3.63 + val (tacis', (_, tac_, (p, is))) = split_last tacis
3.64 + val (p',c',_,pt') = generate1 (assoc_thy "Isac") tac_ is p pt
3.65 + in generate tacis' (pt', c@c', p') end;
3.66
3.67 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
3.68 * of for connecting a user-input formula with the current calc-state. *