1 (* Title: Specify/i-model.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 \<open>I_Model\<close> serves students' interactive modelling and gives feedback in the specify-phase.
8 signature INTERACTION_MODEL =
13 val OLD_to_TEST: T -> T_TEST
14 val TEST_to_OLD: T_TEST -> T
16 val empty_TEST: T_TEST
20 val empty_single: single
21 val empty_single_TEST: single_TEST
22 val is_empty_single_TEST: single_TEST -> bool
29 datatype feedback = datatype Model_Def.i_model_feedback
30 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
31 val feedback_empty_TEST: Model_Def.i_model_feedback_TEST
36 val single_to_string: Proof.context -> single -> string
37 val single_to_string_TEST: Proof.context -> single_TEST -> string
38 val to_string: Proof.context -> T -> string
39 val to_string_TEST: Proof.context -> T_TEST -> string
40 val feedback_OLD_to_TEST: feedback -> feedback_TEST
42 datatype add_single = Add of single | Err of string
43 val init: Model_Pattern.T -> T
44 val init_TEST: O_Model.T -> Model_Pattern.T -> T_TEST
45 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
46 TermC.as_string -> add_single
47 val add_single: theory -> single -> T -> T
49 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
50 val descriptor: feedback -> descriptor
51 val descriptor_TEST: feedback_TEST -> descriptor
52 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
53 val o_model_values: feedback -> O_Model.values
54 val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
55 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
57 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
59 (*TODO: replace in pre-conditions.m, see fun max_variants + make_envs_preconds,
60 see (** complete I_Model.T **) *)
61 val of_max_variant: Model_Pattern.T -> T_TEST ->
62 (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
64 val add: single -> T -> T
65 val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
68 val is_error: feedback -> bool
69 val is_complete: T -> bool
70 val is_complete_variant: Model_Def.variant -> T_TEST-> bool
71 val to_p_model: theory -> feedback -> string
73 (*from isac_test for Minisubpbl*)
74 val msg: variants -> feedback_TEST -> string
75 val transfer_terms: O_Model.single -> single_TEST
77 val eq1: ''a -> 'b * (''a * 'c) -> bool
78 val filter_outs: O_Model.T -> T -> O_Model.T
79 val filter_outs_TEST: O_Model.T -> T_TEST -> O_Model.T
80 val feedback_to_string: Proof.context -> feedback -> string
81 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
83 val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list ->
84 'a * 'b * bool * string * feedback
85 val seek_ppc: int -> T -> single option
86 val overwrite_ppc: theory -> single -> T -> T
96 structure I_Model(**) : INTERACTION_MODEL(**) =
102 type variant = Model_Def.variant;
103 type variants = Model_Def.variants;
104 type m_field = Model_Def.m_field;
105 type descriptor = Model_Def.descriptor;
107 type T = Model_Def.i_model_single list;
108 (* for developing input from PIDE, we use T_TEST with these ideas:
109 (1) the new structure is as close to old T, because we want to preserve the old tests
110 (2) after development (with *_TEST) of essential parts of the Specification's semantics,
111 we adapt the old tests to the new T_TEST
112 (3) together with adaption of the tests we remove the *_TEST
114 type T_TEST = Model_Def.i_model_single_TEST list;
115 datatype feedback = datatype Model_Def.i_model_feedback;
116 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;
117 val feedback_empty_TEST = Model_Def.feedback_empty_TEST
118 type single = Model_Def.i_model_single;
119 type single_TEST = Model_Def.i_model_single_TEST;
120 val empty_single = Model_Def.i_model_empty;
121 val empty_single_TEST = Model_Def.i_model_empty_TEST;
122 fun is_empty_single_TEST (0, [], false, "i_model_empty", _) = true
123 | is_empty_single_TEST _ = false
126 val empty_TEST = []: T_TEST;
131 fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST (d, ts))
132 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
133 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
134 | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST (d, ts))
135 | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
136 | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
137 (UnparseC.term (ContextC.for_ERROR ()) pid))
138 | feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)
139 fun OLD_to_TEST i_old =
140 map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
142 fun feedback_TEST_to_OLD (Model_Def.Cor_TEST (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
143 | feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)
144 | feedback_TEST_to_OLD (Model_Def.Inc_TEST (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
145 | feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))
146 fun TEST_to_OLD i_model =
147 map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model
149 type message = string;
151 fun feedback_to_string ctxt (Cor ((d, ts), _)) =
152 "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
153 | feedback_to_string _ (Syn c) = "Syn " ^ c
154 | feedback_to_string _ (Typ c) = "Typ " ^ c
155 | feedback_to_string ctxt (Inc ((d, ts), _)) =
156 "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
157 | feedback_to_string ctxt (Sup (d, ts)) =
158 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
159 | feedback_to_string ctxt (Mis (d, pid)) =
160 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
161 | feedback_to_string _ (Par s) = "Trm "^s;
164 fun feedback_TEST_to_string ctxt (Cor_TEST (d, ts)) =
165 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
166 | feedback_TEST_to_string _ (Syn_TEST c) =
168 | feedback_TEST_to_string ctxt (Inc_TEST (d, [])) =
169 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
170 Model_Pattern.empty_for d
171 | feedback_TEST_to_string ctxt (Inc_TEST (d, ts)) =
172 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
173 | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
174 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
176 fun single_to_string ctxt (i, is, b, s, itm_) =
177 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
178 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
179 fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
180 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
181 s ^ ", (" ^ feedback_TEST_to_string ctxt itm_ ^ ", Position.T))";
183 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
184 fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
187 (** make a Tactic.T **)
189 fun make_tactic m_field (term_as_string, i_model) =
191 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
192 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
193 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
194 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
197 (** initialise a model **)
201 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
202 in map pbt2itm pbt end
206 * Now the Model in Specification is intialised such that the placement of items can be
207 maximally stable during interactive input to the Specification.
208 * Template.show provides the initial output to the user and thus determines what will be parsed
209 by Outer_Syntax later during interaction.
210 * The relation between O_Model.T and I_Model.T becomes much simpler.
213 fun pat_to_item o_model (_, (descriptor, _)) =
214 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
215 NONE => raise ERROR "I_Model.pat_to_item_TEST with NONE"
216 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
217 (Inc_TEST (descr, []), Position.none))
218 fun init_TEST o_model model_patt =
220 val pre_items = map (pat_to_item o_model) model_patt
222 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
225 (*/---------------- old code -----------------------------------------------------------------\*)
226 fun o_model_values (Cor ((_, ts), _)) = ts
227 | o_model_values (Syn _) = []
228 | o_model_values (Typ _) = []
229 | o_model_values (Inc ((_, ts), _)) = ts
230 | o_model_values (Sup (_, ts)) = ts
231 | o_model_values (Mis _) = []
232 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
234 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
235 fun descriptor (Cor ((d ,_), _)) = d
236 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
237 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
238 | descriptor (Inc ((d, _), _)) = d
239 | descriptor (Sup (d, _)) = d
240 | descriptor (Mis (d, _)) = d
241 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
242 fun descriptor_TEST (Cor_TEST (d ,_)) = d
243 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
244 | descriptor_TEST (Inc_TEST (d, _)) = d
245 | descriptor_TEST (Sup_TEST (d, _)) = d
247 fun descr_pairs_to_string ctxt equal_descr_pairs =
248 (map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
249 |> pair2str) equal_descr_pairs)
252 fun variables model_patt i_model =
253 Pre_Conds.environment_TEST model_patt i_model
256 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
258 (* get a term from O_Model, notyet input in I_Model.
259 the term from O_Model is thrown back to a string in order to reuse
260 machinery for immediate input by the user. *)
261 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
262 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
264 (*update the itm_ already input, all..from ori*)
265 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
267 val ts' = union op = (o_model_values itm_) ts;
268 val pval = [Input_Descript.join'''' (d, ts')]
269 (*WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc*)
270 val complete = if eq_set op = (ts', all) then true else false
274 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
275 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
276 | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
277 | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
280 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
281 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
282 | (Sup (d,ts')) => (*4.9.01 lost env*)
283 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
284 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
285 (* 28.1.00: not completely clear ---^^^ etc.*)
286 | (Mis _) => (* 4.9.01: Mis just copied *)
288 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
289 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
290 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string (ContextC.for_ERROR ()) i)
294 (** find next step **)
296 fun eq1 d (_, (d', _)) = (d = d')
297 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
299 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
300 case find_first (eq1 d) pbt of
301 SOME (_, (_, pid)) =>
302 (case find_first (eq3 f d) itms of
303 SOME (_, _, _, _, itm_) =>
304 let val ts' = inter op = (o_model_values itm_) ts
306 if subset op = (ts, ts')
307 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
308 else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
310 | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
311 | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
313 datatype add_single =
314 Add of single (* return-value of check_single *)
315 | Err of string (* error-message *)
318 Create feedback for input of TermC.as_string to m_field;
319 check w.r.t. O_Model.T and Model_Pattern.T.
320 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
321 check_single is extremely permissive.
323 (*will come directly from PIDE -----------------vvvvvvvvvvv
324 in case t comes from Step.specify_do_next -----------vvv = Position.none*)
325 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
327 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
328 (*/------------ replace by ParseC.term_position -----------\*)
329 val t = Syntax.read_term ctxt ct
330 handle ERROR msg => error (msg (*^ Position.here pos*))
331 (*\------------ replace by ParseC.term_position -----------/*)
332 (*NONE => Add (i, [], false, m_field, Syn ct)*)
333 val (d, ts) = Input_Descript.split t
335 if d = TermC.empty then
336 Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
338 (case find_first (eq1 d) m_patt of
339 NONE => Add (i, [], true, m_field, Sup (d,ts))
340 | SOME (f, (_, id)) =>
342 fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
344 case find_first (eq2 d) i_model of
345 NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
346 | SOME (i', _, _, _, itm_) =>
347 if Input_Descript.for_list d then
349 val in_itm = o_model_values itm_
350 val ts' = union op = ts in_itm
351 val i'' = if in_itm = [] then i else i'
352 in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
353 else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
356 (*for MethodC: #undef completed vvvvv vvvvvv term_as_string*)
357 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
358 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
360 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
361 handle ERROR msg => error (msg (*TODO: ^ Position.here pp*))
362 (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
364 case Model_Pattern.get_field descriptor m_patt of
365 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
366 UnparseC.term ctxt descriptor ^ "\"")
368 if m_field <> m_field' then
369 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
370 "\" not for field \"" ^ m_field ^ "\"")
372 case O_Model.contains ctxt m_field o_model t of
374 (case is_notyet_input ctxt i_model all ori' m_patt of
376 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
377 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
383 fun overwrite_ppc thy itm model =
385 fun repl _ (_, _, _, _, itm_) [] =
386 raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_
388 | repl model' itm (p :: model) =
390 then model' @ [itm] @ model
391 else repl (model' @ [p]) itm model
392 in repl [] itm model end
394 (*find_first item with #1 equal to id*)
395 fun seek_ppc _ [] = NONE
396 | seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model
398 (* 10.3.00: insert the already compiled itm into model;
399 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
400 fun add_single thy itm model =
402 fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)
403 | eq_untouched _ _ = false
404 val model' = case seek_ppc (#1 itm) model of
405 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
406 | NONE => (model @ [itm])
407 in filter_out (eq_untouched ((descriptor o #5) itm)) model' end
410 (** complete I_Model.T **)
413 Survey on completion of i-models.
414 one most general version, I_Model.s_make_complete, shall replace all old versions
416 Divide functionality of I_Model.of_max_variant into parts in order for re-use in is_complete
418 return variant list, because Problem#model might be insufficient to determine
419 variant of MethodC.#model (FunctionVariable a ! b)
420 + (Model_Pattern.single * I_Model.single) list for make_environments
421 ^^NO: need ONLY max_variants
422 Pre_Conds.make_environments
425 Coordination with I_Model.is_complete:
426 uses I_Model.max_variants, Pre_Conds.make_environments for Pre_Conds.check
427 determines by use of both models independently (?)
430 fun complete' pbt (i, v, f, d, ts) =
431 case \<^try>\<open> (i, v, true, f, Cor ((d, ts),
432 ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)
435 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
437 (*filter out oris which have same description in itms*)
438 (* ---------------------------------- type problems ---vv---------vv
439 fun filter_outs oris [] = oris
440 | filter_outs oris (i::itms) =
442 val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris
449 fun filter_outs oris [] = oris
450 | filter_outs oris (i::itms) =
452 val ors = filter_out ((curry op = ((descriptor o
453 (#5: single -> feedback)) i)) o
454 (#4: O_Model.single -> O_Model.descriptor)) oris
459 fun filter_outs_TEST oris [] = oris
460 | filter_outs_TEST oris (i::itms) =
462 val ors = filter_out ((curry op = ((descriptor_TEST o
463 ((#1 o #5): single_TEST -> feedback_TEST) ) i) ) o
464 (#4: O_Model.single -> O_Model.descriptor) ) oris
466 filter_outs_TEST ors itms
470 fun is_error (Cor _) = false
471 | is_error (Sup _) = false
472 | is_error (Inc _) = false
473 | is_error (Mis _) = false
476 (*create output-string for itm*)
477 fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
478 | to_p_model _ (Syn c) = c
479 | to_p_model _ (Typ c) = c
480 | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
481 | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
482 | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid
483 | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
485 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)
487 (* insert_ppc = add for appl_add', input_icalhd 11.03,
488 handles superfluous items carelessly *)
489 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
491 (*TODO: also check if all elements are I_Model.Cor*)
492 fun is_complete ([]: T) = false
493 | is_complete itms = foldl and_ (true, (map #3 itms))
495 (*for PIDE: are all feedback Cor ? MISSING: Pre_Conds.check *)
496 fun is_complete_variant no_model_items i_model =
497 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
499 val of_max_variant = Pre_Conds.of_max_variant
501 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
502 "variants " ^ ints2str' vnts ^ " and descriptor " ^
503 (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
504 fun transfer_terms (i, vnts, m_field, descr, ts) =
505 (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
506 fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
508 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
509 val i_from_pbl = map (fn (_, (descr, _)) =>
510 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
511 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
512 if is_empty_single_TEST i_single
514 case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
515 [] => raise ERROR (msg pbl_max_vnts feedb)
516 | o_singles => map transfer_terms o_singles
517 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
519 val i_from_met = map (fn (_, (descr, _)) =>
520 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
521 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
522 val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
524 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
525 if is_empty_single_TEST i_single
527 case Pre_Conds.get_descr_vnt' feedb [max_vnt] o_model of
528 [] => raise ERROR (msg [max_vnt] feedb)
529 | o_singles => map transfer_terms o_singles
530 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
532 (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,