1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 11 08:25:40 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 11 14:58:07 2011 +0200
1.3 @@ -723,41 +723,37 @@
1.4 (*. is the input term t known in oris ?
1.5 give feedback on all(?) strange input;
1.6 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
1.7 -(*WN.11.03: from lists*)
1.8 fun is_known ctxt sel ori t =
1.9 -(* val (ori,t)=(oris,term_of ct);
1.10 - *)
1.11 let
1.12 val _ = tracing ("RM is_known: t=" ^ term2str t);
1.13 val ots = (distinct o flat o (map #5)) (ori:ori list);
1.14 val oids = ((map (fst o dest_Free)) o distinct o
1.15 - flat o (map vars)) ots;
1.16 - val (d,ts(*,pval*)) = split_dts t;
1.17 + flat o (map vars)) ots;
1.18 + val (d, ts) = split_dts t;
1.19 val ids = map (fst o dest_Free)
1.20 ((distinct o (flat o (map vars))) ts);
1.21 in if (subtract op = oids ids) <> []
1.22 - then (("identifiers "^(strs2str' (subtract op = oids ids))^
1.23 - " not in example"), e_ori_, [])
1.24 + then (("identifiers "^(strs2str' (subtract op = oids ids)) ^
1.25 + " not in example"), e_ori_, [])
1.26 else
1.27 - if d = e_term
1.28 - then
1.29 - if not (subset op = (map typeless ts, map typeless ots))
1.30 - then (("terms '"^
1.31 - ((strs2str' o
1.32 - (map (Print_Mode.setmp [] (Syntax.string_of_term
1.33 - ctxt)))) ts)^
1.34 - "' not in example (typeless)"), e_ori_, [])
1.35 - else (case seek_orits ctxt sel ts ori of
1.36 - ("", ori_ as (_,_,_,d,ts), all) =>
1.37 - (case test_types ctxt (d,ts) of
1.38 - "" => ("", ori_, all)
1.39 - | msg => (msg, e_ori_, []))
1.40 - | (msg,_,_) => (msg, e_ori_, []))
1.41 - else
1.42 - if member op = (map #4 ori) d
1.43 - then seek_oridts ctxt sel (d,ts) ori
1.44 - else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.45 - " not in example", (0, [], sel, d, ts), [])
1.46 + if d = e_term
1.47 + then
1.48 + if not (subset op = (map typeless ts, map typeless ots))
1.49 + then (("terms '" ^ ((strs2str' o
1.50 + (map (Print_Mode.setmp [] (Syntax.string_of_term ctxt)))) ts) ^
1.51 + "' not in example (typeless)"), e_ori_, [])
1.52 + else
1.53 + (case seek_orits ctxt sel ts ori of
1.54 + ("", ori_ as (_,_,_,d,ts), all) =>
1.55 + (case test_types ctxt (d,ts) of
1.56 + "" => ("", ori_, all)
1.57 + | msg => (msg, e_ori_, []))
1.58 + | (msg,_,_) => (msg, e_ori_, []))
1.59 + else
1.60 + if member op = (map #4 ori) d
1.61 + then seek_oridts ctxt sel (d,ts) ori
1.62 + else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.63 + " not in example", (0, [], sel, d, ts), [])
1.64 end;
1.65
1.66
1.67 @@ -1097,7 +1093,7 @@
1.68 else pI' |> #ppc o get_pbt |> prep_ori fmz thy
1.69 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.70 (oris, (dI',pI',mI'),e_term)
1.71 - (*val pt = update_env pt [] (SOME (e_istate, ctxt)) GOON.WN110506*)
1.72 + (*val pt = update_env pt [] (SOME (e_istate, ctxt)) FIXME.WN110511*)
1.73 val {ppc, prls, where_, ...} = get_pbt pI'
1.74 val (pbl, pre, pb) = ([], [], false)
1.75 in
1.76 @@ -1250,75 +1246,58 @@
1.77 | specify m' _ _ _ =
1.78 error ("specify: not impl. for "^tac_2str m');
1.79
1.80 -(* val (sel, Add_Given ct, ptp as (pt,(p,Pbl))) = ("#Given", tac, ptp);
1.81 - val (sel, Add_Find ct, ptp as (pt,(p,Pbl))) = ("#Find", tac, ptp);
1.82 - *)
1.83 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) =
1.84 - let
1.85 - val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.86 - probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1.87 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.88 - val cpI = if pI = e_pblID then pI' else pI;
1.89 - val ctxt = get_ctxt pt (p, Pbl);
1.90 - in case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.91 - Add itm (*..union old input *) =>
1.92 -(* val Add itm = appl_add thy sel oris pbl ppc ct;
1.93 - *)
1.94 - let
1.95 - (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1.96 - val pbl' = insert_ppc thy itm pbl
1.97 - val (tac,tac_) =
1.98 - case sel of
1.99 - "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1.100 - | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.101 - | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.102 - val ((p,Pbl),c,_,pt') =
1.103 - generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1.104 - in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate' end
1.105 -
1.106 - | Err msg =>
1.107 - (*TODO.WN03 pass error-msgs to the frontend..
1.108 - FIXME ..and dont abuse a tactic for that purpose*)
1.109 - ([(Tac msg,
1.110 - Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.111 - (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.112 - end
1.113 + let
1.114 + val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
1.115 + probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1.116 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.117 + val cpI = if pI = e_pblID then pI' else pI;
1.118 + val ctxt = get_ctxt pt (p, Pbl); (*FIXME.WN110511 repair*)
1.119 + in
1.120 + case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.121 + Add itm (*..union old input *) =>
1.122 + let
1.123 + (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)
1.124 + val pbl' = insert_ppc thy itm pbl
1.125 + val (tac,tac_) =
1.126 + case sel of
1.127 + "#Given" => (Add_Given ct, Add_Given' (ct, pbl'))
1.128 + | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.129 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.130 + val ((p,Pbl),c,_,pt') =
1.131 + generate1 thy tac_ (Uistate, e_ctxt) (p,Pbl) pt
1.132 + in ([(tac,tac_,((p,Pbl),(Uistate, e_ctxt)))], c, (pt',(p,Pbl))):calcstate'
1.133 + end
1.134 + | Err msg =>
1.135 + (*TODO.WN03 pass error-msgs to the frontend..
1.136 + FIXME ..and dont abuse a tactic for that purpose*)
1.137 + ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.138 + (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.139 + end
1.140 + | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1.141 + let
1.142 + val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.143 + probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.144 + val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.145 + val cmI = if mI = e_metID then mI' else mI;
1.146 + val ctxt = get_ctxt pt (p,Met); (*FIXME.WN110511 repair*)
1.147 + in
1.148 + case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1.149 + Add itm (*..union old input *) =>
1.150 + let
1.151 + val met' = insert_ppc thy itm met;
1.152 + val (tac,tac_) =
1.153 + case sel of
1.154 + "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1.155 + | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.156 + | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.157 + val ((p,Met),c,_,pt') =
1.158 + generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1.159 + in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1.160 + | Err msg => ([(*tacis*)], [], ptp)
1.161 + (*nxt_me collects tacis until not hide; here just no progress*)
1.162 + end;
1.163
1.164 -(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1.165 - val (_,_,f,nxt',_,pt')= nxt_specif_additem sel ct (p,Met) c pt;
1.166 - *)
1.167 - | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) =
1.168 - let
1.169 - val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.170 - probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.171 - val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.172 - val cmI = if mI = e_metID then mI' else mI;
1.173 - val ctxt = get_ctxt pt (p,Met);
1.174 - in case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
1.175 - Add itm (*..union old input *) =>
1.176 - let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.177 - *)
1.178 - val met' = insert_ppc thy itm met;
1.179 - val (tac,tac_) =
1.180 - case sel of
1.181 - "#Given" => (Add_Given ct, Add_Given' (ct, met'))
1.182 - | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.183 - | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.184 - val ((p,Met),c,_,pt') =
1.185 - generate1 thy tac_ (Uistate, e_ctxt) (p,Met) pt
1.186 - in ([(tac,tac_,((p,Met), (Uistate, e_ctxt)))], c, (pt',(p,Met))) end
1.187 -
1.188 - | Err msg => ([(*tacis*)], [], ptp)
1.189 - (*nxt_me collects tacis until not hide; here just no progress*)
1.190 - end;
1.191 -
1.192 -(* ori
1.193 -val (msg,itm) = appl_add thy sel oris ppc ct;
1.194 -val (Cor(d,ts)) = #5 itm;
1.195 -map (atomty) ts;
1.196 -
1.197 -pre
1.198 -*)
1.199 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =
1.200 (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt)
1.201 handle _ => error ("ori2Coritm: dsc "^
1.202 @@ -1394,22 +1373,22 @@
1.203 (*WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg*)
1.204 (*WN.24.10.03 fun nxt_solv = ...................................??*)
1.205 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =
1.206 - let
1.207 - val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1.208 - val (dI, pI, mI) = some_spec ospec spec
1.209 - val thy = assoc_thy dI
1.210 - val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.211 - val {cas, ppc, ...} = get_pbt pI
1.212 - val pbl = init_pbl ppc (* fill in descriptions *)
1.213 - (*----------------if you think, this should be done by the Dialog
1.214 - in the java front-end, search there for WN060225-modelProblem----*)
1.215 - val (pbl, met) =
1.216 - case cas of NONE => (pbl, [])
1.217 - | _ => complete_mod_ (oris, mpc, ppc, probl)
1.218 - (*----------------------------------------------------------------*)
1.219 - val tac_ = Model_Problem' (pI, pbl, met)
1.220 - val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1.221 - in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1.222 + let
1.223 + val PblObj {origin = (oris, ospec, _), probl, spec, ...} = get_obj I pt p
1.224 + val (dI, pI, mI) = some_spec ospec spec
1.225 + val thy = assoc_thy dI
1.226 + val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)
1.227 + val {cas, ppc, ...} = get_pbt pI
1.228 + val pbl = init_pbl ppc (* fill in descriptions *)
1.229 + (*----------------if you think, this should be done by the Dialog
1.230 + in the java front-end, search there for WN060225-modelProblem----*)
1.231 + val (pbl, met) =
1.232 + case cas of NONE => (pbl, [])
1.233 + | _ => complete_mod_ (oris, mpc, ppc, probl)
1.234 + (*----------------------------------------------------------------*)
1.235 + val tac_ = Model_Problem' (pI, pbl, met)
1.236 + val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
1.237 + in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
1.238
1.239 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.240 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1.241 @@ -1417,92 +1396,101 @@
1.242
1.243 (*. called only if no_met is specified .*)
1.244 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
1.245 - let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1.246 - val opt = refine_ori oris pI
1.247 - in case opt of
1.248 - SOME pI' =>
1.249 - let val {met,ppc,...} = get_pbt pI'
1.250 - val pbl = init_pbl ppc
1.251 - (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.252 - val mI = if length met = 0 then e_metID else hd met
1.253 - val thy = assoc_thy dI
1.254 - val (pos,c,_,pt) =
1.255 - generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.256 - (Uistate, e_ctxt) pos pt
1.257 - in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.258 - (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1.259 - | NONE => ([], [], ptp)
1.260 - end
1.261 + let
1.262 + val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
1.263 + val opt = refine_ori oris pI
1.264 + in
1.265 + case opt of
1.266 + SOME pI' =>
1.267 + let
1.268 + val {met,ppc,...} = get_pbt pI'
1.269 + val pbl = init_pbl ppc
1.270 + (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
1.271 + val mI = if length met = 0 then e_metID else hd met
1.272 + val thy = assoc_thy dI
1.273 + val (pos,c,_,pt) =
1.274 + generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]))
1.275 + (Uistate, e_ctxt) pos pt
1.276 + in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.277 + (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.278 + end
1.279 + | NONE => ([], [], ptp)
1.280 + end
1.281
1.282 | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
1.283 - let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1.284 - probl, ...}) = get_obj I pt p
1.285 - val thy = if dI' = e_domID then dI else dI'
1.286 - in case refine_pbl (assoc_thy thy) pI probl of
1.287 - NONE => ([], [], ptp)
1.288 - | SOME (rfd as (pI',_)) =>
1.289 - let val (pos,c,_,pt) =
1.290 - generate1 (assoc_thy thy)
1.291 - (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.292 - in ([(Refine_Problem pI, Refine_Problem' rfd,
1.293 - (pos, (Uistate, e_ctxt)))], c, (pt,pos)) end
1.294 - end
1.295 + let
1.296 + val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ...}) = get_obj I pt p
1.297 + val thy = if dI' = e_domID then dI else dI'
1.298 + in
1.299 + case refine_pbl (assoc_thy thy) pI probl of
1.300 + NONE => ([], [], ptp)
1.301 + | SOME (rfd as (pI',_)) =>
1.302 + let
1.303 + val (pos,c,_,pt) = generate1 (assoc_thy thy)
1.304 + (Refine_Problem' rfd) (Uistate, e_ctxt) pos pt
1.305 + in ([(Refine_Problem pI, Refine_Problem' rfd,
1.306 + (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.307 + end
1.308 + end
1.309
1.310 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1.311 - let val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_),
1.312 - probl, ...}) = get_obj I pt p;
1.313 - val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.314 + let
1.315 + val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ...}) = get_obj I pt p;
1.316 + val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.317 val {ppc,where_,prls,...} = get_pbt pI
1.318 - val pbl as (_,(itms,_)) =
1.319 - if pI'=e_pblID andalso pI=e_pblID
1.320 - then (false, (init_pbl ppc, []))
1.321 - else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1.322 - (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.323 - val ((p,Pbl),c,_,pt)=
1.324 - generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1.325 - in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1.326 - (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1.327 + val pbl as (_,(itms,_)) =
1.328 + if pI'=e_pblID andalso pI=e_pblID
1.329 + then (false, (init_pbl ppc, []))
1.330 + else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)
1.331 + (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.332 + val ((p,Pbl),c,_,pt) =
1.333 + generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, e_ctxt) pos pt
1.334 + in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),
1.335 + (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1.336 + end
1.337
1.338 (*transfers oris (not required in pbl) to met-model for script-env
1.339 FIXME.WN.8.03: application of several mIDs to SAME model?*)
1.340 | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) =
1.341 - let val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI),
1.342 - meth=met, ...}) = get_obj I pt p;
1.343 - val {ppc,pre,prls,...} = get_met mID
1.344 - val thy = assoc_thy dI
1.345 - val oris = add_field' thy ppc oris;
1.346 - val dI'' = if dI=e_domID then dI' else dI;
1.347 - val pI'' = if pI = e_pblID then pI' else pI;
1.348 - val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1.349 - val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.350 - val (pos,c,_,pt)=
1.351 - generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.352 - in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1.353 - (pos,(Uistate, e_ctxt)))], c, (pt,pos)) end
1.354 + let
1.355 + val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), meth=met, ...}) = get_obj I pt p;
1.356 + val {ppc,pre,prls,...} = get_met mID
1.357 + val thy = assoc_thy dI
1.358 + val oris = add_field' thy ppc oris;
1.359 + val dI'' = if dI=e_domID then dI' else dI;
1.360 + val pI'' = if pI = e_pblID then pI' else pI;
1.361 + val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)
1.362 + val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;
1.363 + val (pos,c,_,pt)=
1.364 + generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, e_ctxt) pos pt
1.365 + in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),
1.366 + (pos,(Uistate, e_ctxt)))], c, (pt,pos))
1.367 + end
1.368
1.369 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =
1.370 - let val (dI',_,_) = get_obj g_spec pt p
1.371 - val (pos,c,_,pt) =
1.372 - generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1.373 - (Uistate, e_ctxt) pos pt
1.374 - in (*FIXXXME: check if pbl can still be parsed*)
1.375 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.376 - (pt, pos)) end
1.377 + let
1.378 + val (dI',_,_) = get_obj g_spec pt p
1.379 + val (pos,c,_,pt) =
1.380 + generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, e_ctxt) pos pt
1.381 + in (*FIXXXME: check if pbl can still be parsed*)
1.382 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.383 + (pt, pos))
1.384 + end
1.385
1.386 | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =
1.387 - let val (dI',_,_) = get_obj g_spec pt p
1.388 - val (pos,c,_,pt) =
1.389 - generate1 (assoc_thy "Isac") (Specify_Theory' dI)
1.390 - (Uistate, e_ctxt) pos pt
1.391 - in (*FIXXXME: check if met can still be parsed*)
1.392 - ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.393 - (pt, pos)) end
1.394 + let
1.395 + val (dI',_,_) = get_obj g_spec pt p
1.396 + val (pos,c,_,pt) =
1.397 + generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, e_ctxt) pos pt
1.398 + in (*FIXXXME: check if met can still be parsed*)
1.399 + ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, e_ctxt)))], c,
1.400 + (pt, pos))
1.401 + end
1.402
1.403 | nxt_specif m' _ =
1.404 error ("nxt_specif: not impl. for "^tac2str m');
1.405
1.406 -(*.get the values from oris; handle the term list w.r.t. penv.*)
1.407 -
1.408 +(* get the values from oris; handle the term list w.r.t. penv *)
1.409 local infix mem;
1.410 fun x mem [] = false
1.411 | x mem (y :: ys) = x = y orelse x mem ys;
1.412 @@ -1512,8 +1500,6 @@
1.413 (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
1.414 end;
1.415
1.416 -
1.417 -
1.418 (* create a calc-tree with oris via an cas.refined pbl *)
1.419 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1.420 if pI <> []
1.421 @@ -1568,7 +1554,7 @@
1.422 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1.423 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1.424 (pors, (dI, pI, mI), hdl)
1.425 - (* val pt = update_env pt [] (SOME (e_istate, pctxt)) GOON.WN110506*)
1.426 + (* val pt = update_env pt [] (SOME (e_istate, pctxt)) FIXME.WN110511*)
1.427 in ((pt, ([], Pbl)),
1.428 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.429 end;