1.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Mar 21 00:32:53 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Apr 04 11:05:07 2011 +0200
1.3 @@ -15,7 +15,7 @@
1.4 val all_modspec : ptree * pos' -> ptree * pos'
1.5 datatype appl = Appl of tac_ | Notappl of string
1.6 val appl_add :
1.7 - theory ->
1.8 + Proof.context ->
1.9 string ->
1.10 SpecifyTools.ori list ->
1.11 SpecifyTools.itm list ->
1.12 @@ -90,13 +90,13 @@
1.13 val is_error : SpecifyTools.itm_ -> bool
1.14 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
1.15 val is_known :
1.16 - theory ->
1.17 + Proof.context ->
1.18 string ->
1.19 SpecifyTools.ori list ->
1.20 Term.term -> string * SpecifyTools.ori * Term.term list
1.21 val is_list_type : Term.typ -> bool
1.22 val is_notyet_input :
1.23 - theory ->
1.24 + Proof.context ->
1.25 SpecifyTools.itm list ->
1.26 Term.term list ->
1.27 SpecifyTools.ori ->
1.28 @@ -142,7 +142,6 @@
1.29 val ori2Coritm :
1.30 pat list -> ori -> itm
1.31 val ori_2itm :
1.32 - 'a ->
1.33 SpecifyTools.itm_ ->
1.34 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
1.35 val overwrite_ppc :
1.36 @@ -169,7 +168,7 @@
1.37 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.38 -> string * SpecifyTools.ori * Term.term list
1.39 val seek_orits :
1.40 - theory ->
1.41 + Proof.context ->
1.42 string ->
1.43 Term.term list ->
1.44 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.45 @@ -193,7 +192,7 @@
1.46 ptree ->
1.47 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
1.48 val tag_form : theory -> term * term -> term
1.49 - val test_types : theory -> Term.term * Term.term list -> string
1.50 + val test_types : Proof.context -> Term.term * Term.term list -> string
1.51 val typeless : Term.term -> Term.term
1.52 val unbound_ppc : term SpecifyTools.ppc -> Term.term list
1.53 val vals_of_oris : SpecifyTools.ori list -> Term.term list
1.54 @@ -277,40 +276,35 @@
1.55
1.56 (*.to an input (d,ts) find the according ori and insert the ts.*)
1.57 (*WN.11.03: + dont take first inter<>[]*)
1.58 -fun seek_oridts thy sel (d,ts) [] =
1.59 - ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
1.60 - (comp_dts thy (d,ts))) ^
1.61 +fun seek_oridts ctxt sel (d,ts) [] =
1.62 + ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
1.63 + (comp_dts (d,ts))) ^
1.64 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
1.65 [])
1.66 - | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.67 - if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.68 - then if sel = sel'
1.69 + | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
1.70 + if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
1.71 then ("",
1.72 (id,vat,sel,d, inter op = ts ts'):ori,
1.73 ts')
1.74 - else ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
1.75 - (comp_dts thy (d,ts))) ^ " not for " ^ sel,
1.76 - e_ori_,
1.77 - [])
1.78 - else seek_oridts thy sel (d,ts) oris;
1.79 + else seek_oridts ctxt sel (d,ts) oris;
1.80
1.81 (*.to an input (_,ts) find the according ori and insert the ts.*)
1.82 -fun seek_orits thy sel ts [] =
1.83 +fun seek_orits ctxt sel ts [] =
1.84 ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
1.85 - (thy2ctxt thy))) ts) ^
1.86 + ctxt)) ts) ^
1.87 "') not found in oris (typed)", e_ori_, [])
1.88 - | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.89 + | seek_orits ctxt sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
1.90 if sel = sel' andalso (inter op = ts ts') <> []
1.91 then if sel = sel'
1.92 then ("",
1.93 (id,vat,sel,d, inter op = ts ts'):ori,
1.94 ts')
1.95 else (((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.96 - (thy2ctxt thy)))) ts)
1.97 + ctxt))) ts)
1.98 ^ " not for " ^ sel,
1.99 e_ori_,
1.100 [])
1.101 - else seek_orits thy sel ts oris;
1.102 + else seek_orits ctxt sel ts oris;
1.103 (* false
1.104 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
1.105 > seek_orits thy sel ts [(id,vat,sel',d,ts')];
1.106 @@ -479,21 +473,19 @@
1.107 (* val (_,_,fd,d,ts) = hd miss;
1.108 *)
1.109 fun getr_ct thy ((_, _, fd, d, ts) : ori) =
1.110 - (fd, (Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy))) o
1.111 - (comp_dts thy)) (d,[hd ts]) : cterm');
1.112 -(* val t = comp_dts thy (d,[hd ts]);
1.113 + (fd, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) o
1.114 + comp_dts) (d,[hd ts]) : cterm');
1.115 +(* val t = comp_dts (d,[hd ts]);
1.116 *)
1.117
1.118 (* get a term from ori, notyet input in itm.
1.119 the term from ori is thrown back to a string in order to reuse
1.120 machinery for immediate input by the user. *)
1.121 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.122 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.123 - (comp_dts thy))
1.124 + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.125 (d, subtract op = (ts_in itm_) ts) : cterm');
1.126 fun geti_ct thy ((_, _, _, d, ts) : ori) ((_, _, _, fd, itm_) : itm) =
1.127 - (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o
1.128 - (comp_dts thy))
1.129 + (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts)
1.130 (d, subtract op = (ts_in itm_) ts) : cterm');
1.131
1.132 (* in FE dsc, not dat: this is in itms ...*)
1.133 @@ -519,7 +511,7 @@
1.134 (f,(d,_))::itms =>
1.135 SOME (f : string,
1.136 ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) o
1.137 - comp_dts thy) (d, []) : cterm')
1.138 + comp_dts) (d, []) : cterm')
1.139 | _ => NONE end
1.140
1.141 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
1.142 @@ -642,10 +634,10 @@
1.143 (*. update the itm_ already input, all..from ori .*)
1.144 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
1.145 *)
1.146 -fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) =
1.147 +fun ori_2itm itm_ pid all ((id,vt,fd,d,ts):ori) =
1.148 let
1.149 val ts' = union op = (ts_in itm_) ts;
1.150 - val pval = pbl_ids' thy d ts'
1.151 + val pval = pbl_ids' d ts'
1.152 (*WN.9.5.03: FIXXXME [#0, epsilon]
1.153 here would upd_penv be called for [#0, epsilon] etc. *)
1.154 val complete = if eq_set op = (ts', all) then true else false;
1.155 @@ -685,7 +677,7 @@
1.156 (4) -"- <> empty --- new: ori(ts) \\ inter .*)
1.157 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');
1.158 *)
1.159 -fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.160 +fun is_notyet_input ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =
1.161 case find_first (eq1 d) pbt of
1.162 SOME (_,(_,pid)) =>(* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
1.163 val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;
1.164 @@ -696,29 +688,28 @@
1.165 val ts' = inter op = (ts_in itm_) ts;
1.166 in if subset op = (ts, ts')
1.167 then (((strs2str' o
1.168 - map (Print_Mode.setmp [] (Syntax.string_of_term
1.169 - (thy2ctxt thy)))) ts') ^
1.170 + map (Print_Mode.setmp [] (Syntax.string_of_term ctxt))) ts') ^
1.171 " already input", e_itm) (*2*)
1.172 else ("",
1.173 - ori_2itm thy itm_ pid all (i,v,f,d,
1.174 + ori_2itm itm_ pid all (i,v,f,d,
1.175 subtract op = ts' ts)) (*3,4*)
1.176 end
1.177 - | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[])))
1.178 + | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[])))
1.179 pid all (i,v,f,d,ts)) (*1*)
1.180 )
1.181 - | NONE => ("", ori_2itm thy (Sup (d,ts))
1.182 + | NONE => ("", ori_2itm (Sup (d,ts))
1.183 e_term all (i,v,f,d,ts));
1.184
1.185 -fun test_types thy (d,ts) =
1.186 +fun test_types ctxt (d,ts) =
1.187 let
1.188 (*val s = !show_types; val _ = show_types:= true;*)
1.189 - val opt = (try (comp_dts thy)) (d,ts);
1.190 + val opt = (try comp_dts) (d,ts);
1.191 val msg = case opt of
1.192 SOME _ => ""
1.193 - | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d) ^
1.194 + | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.195 " " ^
1.196 ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
1.197 - (thy2ctxt thy)))) ts)
1.198 + ctxt))) ts)
1.199 ^ " is illtyped");
1.200 (*val _ = show_types:= s*)
1.201 in msg end;
1.202 @@ -736,7 +727,7 @@
1.203 give feedback on all(?) strange input;
1.204 return _all_ terms already input to this item (e.g. valuesFor a,b) .*)
1.205 (*WN.11.03: from lists*)
1.206 -fun is_known thy sel ori t =
1.207 +fun is_known ctxt sel ori t =
1.208 (* val (ori,t)=(oris,term_of ct);
1.209 *)
1.210 let
1.211 @@ -744,7 +735,7 @@
1.212 val ots = (distinct o flat o (map #5)) (ori:ori list);
1.213 val oids = ((map (fst o dest_Free)) o distinct o
1.214 flat o (map vars)) ots;
1.215 - val (d,ts(*,pval*)) = split_dts thy t;
1.216 + val (d,ts(*,pval*)) = split_dts t;
1.217 val ids = map (fst o dest_Free)
1.218 ((distinct o (flat o (map vars))) ts);
1.219 in if (subtract op = oids ids) <> []
1.220 @@ -757,19 +748,18 @@
1.221 then (("terms '"^
1.222 ((strs2str' o
1.223 (map (Print_Mode.setmp [] (Syntax.string_of_term
1.224 - (thy2ctxt thy))))) ts)^
1.225 + ctxt)))) ts)^
1.226 "' not in example (typeless)"), e_ori_, [])
1.227 - else (case seek_orits thy sel ts ori of
1.228 + else (case seek_orits ctxt sel ts ori of
1.229 ("", ori_ as (_,_,_,d,ts), all) =>
1.230 - (case test_types thy (d,ts) of
1.231 + (case test_types ctxt (d,ts) of
1.232 "" => ("", ori_, all)
1.233 | msg => (msg, e_ori_, []))
1.234 | (msg,_,_) => (msg, e_ori_, []))
1.235 else
1.236 if member op = (map #4 ori) d
1.237 - then seek_oridts thy sel (d,ts) ori
1.238 - else ((Print_Mode.setmp [] (Syntax.string_of_term
1.239 - (thy2ctxt thy)) d) ^
1.240 + then seek_oridts ctxt sel (d,ts) ori
1.241 + else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^
1.242 " not in example", (0, [], sel, d, ts), [])
1.243 end;
1.244
1.245 @@ -783,61 +773,45 @@
1.246 (** add an item to the model; check wrt. oris and pbt **)
1.247 (* in contrary to oris<>[] below, this part handles user-input
1.248 extremely acceptive, i.e. accept input instead error-msg *)
1.249 -fun appl_add thy sel ([]:ori list) ppc pbt ct' =
1.250 -(* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);
1.251 - !!!! 28.8.01: env tested _minimally_ !!!
1.252 - *)
1.253 - let
1.254 - val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));
1.255 - in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)
1.256 - NONE => Add (i,[],false,sel,Syn ct')
1.257 -(* val (SOME ct) = parse thy ct';
1.258 - *)
1.259 - | SOME ct =>
1.260 +fun appl_add ctxt sel [] ppc pbt t =
1.261 let
1.262 - val (d,ts(*,pval*)) = split_dts thy (term_of ct);
1.263 - in if d = e_term
1.264 - then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))
1.265 -
1.266 - else
1.267 - (case find_first (eq1 d) pbt of
1.268 - NONE => Add (i,[],true,sel,Sup ((d,ts)))
1.269 - | SOME (f,(_,id)) =>
1.270 -(* val SOME (f,(_,id)) = find_first (eq1 d) pbt;
1.271 - *)
1.272 - let
1.273 - fun eq2 d ((i,_,_,_,itm_):itm) =
1.274 - (d = (d_in itm_)) andalso i<>0;
1.275 - in case find_first (eq2 d) ppc of
1.276 - NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)
1.277 - pbl_ids' thy d ts)))
1.278 - | SOME (i',_,_,_,itm_) =>
1.279 -(* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;
1.280 - val NONE = find_first (eq2 d) ppc;
1.281 - *)
1.282 - if is_list_dsc d
1.283 - then let val ts = union op = ts (ts_in itm_)
1.284 - in Add (if ts_in itm_ = [] then i else i',
1.285 - [],true,f,Cor ((d, ts), (id, (*pval*)
1.286 - pbl_ids' thy d ts)))
1.287 - end
1.288 - else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)
1.289 - pbl_ids' thy d ts)))
1.290 - end
1.291 - )
1.292 + val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
1.293 + in case parseNEW ctxt t of
1.294 + NONE => Add (i, [], false, sel, Syn t)
1.295 + | SOME t' =>
1.296 + let val (d, ts) = split_dts t';
1.297 + in if d = e_term then
1.298 + Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
1.299 + (case find_first (eq1 d) pbt of
1.300 + NONE => Add (i, [], true, sel, Sup (d,ts))
1.301 + | SOME (f, (_, id)) =>
1.302 + let fun eq2 d (i, _, _, _, itm_) =
1.303 + d = (d_in itm_) andalso i <> 0;
1.304 + in case find_first (eq2 d) ppc of
1.305 + NONE => Add (i, [], true, f,
1.306 + Cor ((d, ts), (id, pbl_ids' d ts))
1.307 + )
1.308 + | SOME (i', _, _, _, itm_) => if is_list_dsc d then
1.309 + let
1.310 + val in_itm = ts_in itm_;
1.311 + val ts' = union op = ts in_itm;
1.312 + val i'' = if in_itm = [] then i else i';
1.313 + in Add (i'', [], true, f,
1.314 + Cor ((d, ts'), (id, pbl_ids' d ts'))
1.315 + )
1.316 + end else
1.317 + Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.318 + end)
1.319 + end
1.320 end
1.321 - end
1.322 -(* add ct to ppc *)
1.323 -(*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)
1.324 - | appl_add thy sel oris ppc pbt (*only for upd_envv*) str =
1.325 - case parse thy str of
1.326 - NONE => Err ("syntax error in " ^ str)
1.327 - | SOME t => case is_known thy sel oris (term_of t) of
1.328 - ("", ori', all) =>
1.329 - (case is_notyet_input thy ppc all ori' pbt of
1.330 - ("", itm) => Add itm
1.331 - | (msg, _) => Err msg)
1.332 - | (msg, _, _) => Err msg;
1.333 + | appl_add ctxt sel oris ppc pbt str =
1.334 + case parseNEW ctxt str of
1.335 + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.336 + | SOME t => case is_known ctxt sel oris t of
1.337 + ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
1.338 + ("", itm) => Add itm
1.339 + | (msg, _) => Err msg)
1.340 + | (msg, _, _) => Err msg;
1.341 (*
1.342 > val (msg,itm) = is_notyet_input thy ppc all ori';
1.343 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
1.344 @@ -1043,8 +1017,8 @@
1.345 (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
1.346 val cpI = if pI = e_pblID then pI' else pI;
1.347 val cmI = if mI = e_metID then mI' else mI;
1.348 - val {ppc,pre,prls,...} = get_met cmI
1.349 - in case appl_add thy sel oris met ppc ct of
1.350 + val {ppc,pre,prls,...} = get_met cmI;
1.351 + in case appl_add (thy2ctxt thy) sel oris met ppc ct of
1.352 Add itm (*..union old input *) =>
1.353 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.354 *)
1.355 @@ -1077,7 +1051,7 @@
1.356 end
1.357 (* val (p,_) = p;
1.358 *)
1.359 -| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt =
1.360 +| specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt =
1.361 let
1.362 val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
1.363 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.364 @@ -1085,7 +1059,7 @@
1.365 val cpI = if pI = e_pblID then pI' else pI;
1.366 val cmI = if mI = e_metID then mI' else mI;
1.367 val {ppc,where_,prls,...} = get_pbt cpI;
1.368 - in case appl_add thy sel oris pbl ppc ct of
1.369 + in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
1.370 Add itm (*..union old input *) =>
1.371 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1.372 *)
1.373 @@ -1138,9 +1112,10 @@
1.374 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.375 let (* either """"""""""""""" all empty or complete *)
1.376 val thy = assoc_thy dI';
1.377 + val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
1.378 val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
1.379 - else prep_ori fmz thy ((#ppc o get_pbt) pI');
1.380 - val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
1.381 + else istate_;
1.382 + val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.383 (oris,(dI',pI',mI'),e_term);
1.384 val {ppc,prls,where_,...} = get_pbt pI'
1.385 (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1.386 @@ -1317,7 +1292,7 @@
1.387 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
1.388 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.389 val cpI = if pI = e_pblID then pI' else pI;
1.390 - in case appl_add thy sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.391 + in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
1.392 Add itm (*..union old input *) =>
1.393 (* val Add itm = appl_add thy sel oris pbl ppc ct;
1.394 *)
1.395 @@ -1350,7 +1325,7 @@
1.396 probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
1.397 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
1.398 val cmI = if mI = e_metID then mI' else mI;
1.399 - in case appl_add thy sel oris met ((#ppc o get_met) cmI) ct of
1.400 + in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
1.401 Add itm (*..union old input *) =>
1.402 let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
1.403 *)
1.404 @@ -1579,7 +1554,7 @@
1.405 val thy = assoc_thy dI
1.406 val mI = if mI = [] then hd met else mI
1.407 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.408 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.409 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.410 ([], (dI,pI,mI), hdl)
1.411 val pt = update_spec pt [] (dI,pI,mI)
1.412 val pits = init_pbl' ppc
1.413 @@ -1588,12 +1563,12 @@
1.414 else if mI <> [] then (* from met-browser *)
1.415 let val {ppc,...} = get_met mI
1.416 val dI = if dI = "" then "Isac" else dI
1.417 - val thy = assoc_thy dI
1.418 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.419 - ([], (dI,pI,mI), e_term(*FIXME met*))
1.420 - val pt = update_spec pt [] (dI,pI,mI)
1.421 - val mits = init_pbl' ppc
1.422 - val pt = update_met pt [] mits
1.423 + val thy = assoc_thy dI;
1.424 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.425 + ([], (dI,pI,mI), e_term(*FIXME met*));
1.426 + val pt = update_spec pt [] (dI,pI,mI);
1.427 + val mits = init_pbl' ppc;
1.428 + val pt = update_met pt [] mits;
1.429 in ((pt, ([], Met)), []) : calcstate end
1.430 else (* new example, pepare for interactive modeling *)
1.431 let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.432 @@ -1604,18 +1579,19 @@
1.433 val thy = assoc_thy dI
1.434 val (pI, pors, mI) =
1.435 if mI = ["no_met"]
1.436 - then let val pors = prep_ori fmz thy ((#ppc o get_pbt) pI)
1.437 + then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
1.438 val pI' = refine_ori' pors pI;
1.439 in (pI', pors(*refinement over models with diff.precond only*),
1.440 (hd o #met o get_pbt) pI') end
1.441 - else (pI, prep_ori fmz thy ((#ppc o get_pbt) pI), mI)
1.442 + else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
1.443 val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.444 val dI = theory2theory' (maxthy thy thy');
1.445 + val ctxt = prep_ori fmz thy ppc |> #2;
1.446 val hdl = case cas of
1.447 NONE => pblterm dI pI
1.448 | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1.449 - ~~~ vals_of_oris pors) t
1.450 - val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
1.451 + ~~~ vals_of_oris pors) t;
1.452 + val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
1.453 (pors, (dI, pI, mI), hdl)
1.454 in ((pt, ([], Pbl)),
1.455 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.456 @@ -1814,7 +1790,7 @@
1.457 ...}) = get_obj I pt p;
1.458 val thy = assoc_thy dI;
1.459 val {ppc,...} = get_met mI;
1.460 - val mors = prep_ori fmz_ thy ppc;
1.461 + val mors = prep_ori fmz_ thy ppc |> #1;
1.462 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.463 val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.464 val pt = update_spec pt p (dI,pI,mI);