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_POS: T -> T_POS
14 val TEST_to_OLD: T_POS -> T
20 val empty_single: single
21 val empty_single_POS: single_POS
22 val is_empty_single_POS: single_POS -> bool
30 datatype feedback = datatype Model_Def.i_model_feedback
31 datatype feedback_POS = datatype Model_Def.i_model_feedback_POS
32 val feedback_empty_POS: Model_Def.i_model_feedback_POS
37 val single_to_string: Proof.context -> single -> string
38 val single_to_string_POS: Proof.context -> single_POS -> string
39 val single_to_string_POS': single_POS -> string
40 val to_string: Proof.context -> T -> string
41 val to_string_POS: Proof.context -> T_POS -> string
43 val feedback_OLD_to_POS: feedback -> feedback_POS
44 val feedback_POS_to_OLD: feedback_POS -> feedback
45 val OLD_to_POS_single: single -> single_POS
46 val TEST_to_OLD_single: single_POS -> single
48 datatype add_single = Add of single_POS | Err of string
49 val init: Model_Pattern.T -> T
50 val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
51 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
52 TermC.as_string -> add_single
53 val add_single: theory -> single_POS -> T_POS -> T_POS
55 val make_tactic: m_field -> TermC.as_string * T_POS -> Tactic.T
57 val descriptor: feedback -> descriptor
58 val descriptor_POS: feedback_POS -> descriptor
59 val values: feedback -> values option
60 val get_values: T_POS -> values list
61 val o_model_values: feedback -> values
62 val feedb_values: feedback_POS -> values
63 val order_by_patt: Model_Pattern.T -> T_POS ->T_POS
64 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
65 val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
66 val is_notyet_input: Proof.context -> T_POS -> O_Model.values -> O_Model.single ->
67 Model_Pattern.T -> message * single_POS
68 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
70 val fill_from_o: O_Model.T -> single_POS -> single_POS option
72 val add_other: variant -> T_POS -> single_POS -> single_POS
73 val fill_method: O_Model.T -> T_POS * T_POS-> Model_Pattern.T -> T_POS
74 val s_make_complete: Proof.context -> O_Model.T -> T_POS * T_POS -> Problem.id * MethodC.id ->
76 val s_are_complete: Proof.context -> O_Model.T -> T_POS * T_POS -> Problem.id * MethodC.id -> bool
78 val is_error: feedback_POS -> bool
79 val to_p_model: theory -> feedback_POS -> string
81 (*/----- from isac_test for Minisubpbl*)
82 val msg: variants -> feedback_POS -> string
83 val transfer_terms: O_Model.single -> single_POS
85 val feedback_to_string: Proof.context -> feedback -> string
86 val feedback_POS_to_string: Proof.context -> feedback_POS -> string
87 val descr_vals_to_string: Proof.context -> descriptor * values -> string
88 val feedb_args_to_string: Proof.context -> feedback_POS -> string
90 val ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> single_POS
91 val seek_ppc: int -> single_POS list -> single_POS option
92 val overwrite_ppc: theory -> single_POS -> T_POS -> T_POS
93 (*\----- from isac_test for Minisubpbl*)
96 (*copy "from isac_test for Minisubpbl" here*)
103 structure I_Model(**) : INTERACTION_MODEL(**) =
109 type variant = Model_Def.variant;
110 type variants = Model_Def.variants;
111 type m_field = Model_Def.m_field;
112 type descriptor = Model_Def.descriptor;
113 type values = Model_Def.values
115 type T = Model_Def.i_model_single list;
116 (* for developing input from PIDE, we use T_POS with these ideas:
117 (1) the new structure is as close to old T, because we want to preserve the old tests
118 (2) after development (with *_POS) of essential parts of the Specification's semantics,
119 we adapt the old tests to the new T_POS
120 (3) together with adaption of the tests we remove the *_POS
122 type T_POS = Model_Def.i_model_single_POS list;
123 datatype feedback = datatype Model_Def.i_model_feedback;
124 datatype feedback_POS = datatype Model_Def.i_model_feedback_POS;
125 val feedback_empty_POS = Model_Def.feedback_empty_POS
126 type single = Model_Def.i_model_single;
127 type single_POS = Model_Def.i_model_single_POS;
128 val empty_single = Model_Def.i_model_empty;
129 val empty_single_POS = Model_Def.i_model_empty_POS;
130 fun is_empty_single_POS (0, [], false, "i_model_empty", _) = true
131 | is_empty_single_POS _ = false
134 val empty_POS = []: T_POS;
139 fun feedback_OLD_to_POS (Cor ((d, ts), _)) = (Model_Def.Cor_POS (d, ts))
140 | feedback_OLD_to_POS (Syn c) = (Model_Def.Syn_POS c)
141 | feedback_OLD_to_POS (Typ c) = (Model_Def.Syn_POS c)
142 | feedback_OLD_to_POS (Inc ((d, ts), _)) = (Model_Def.Inc_POS (d, ts))
143 | feedback_OLD_to_POS (Sup (d, ts)) = (Model_Def.Sup_POS (d, ts))
144 | feedback_OLD_to_POS (Mis (d, pid)) = Model_Def.Syn_POS ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
145 (UnparseC.term (ContextC.for_ERROR ()) pid))
146 | feedback_OLD_to_POS (Par s) = (Model_Def.Syn_POS s)
147 fun OLD_to_POS_single (a, b, c, d, e) = (a, b, c, d, (feedback_OLD_to_POS e, Position.none))
148 fun OLD_to_POS i_old = map OLD_to_POS_single i_old
150 fun feedback_POS_to_OLD (Model_Def.Cor_POS (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
151 | feedback_POS_to_OLD (Model_Def.Syn_POS c) = (Syn c)
152 | feedback_POS_to_OLD (Model_Def.Inc_POS (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
153 | feedback_POS_to_OLD (Model_Def.Sup_POS (d, ts)) = (Sup (d, ts))
154 fun TEST_to_OLD_single (a, b, c, d, (e, _)) = (a, b, c, d, feedback_POS_to_OLD e)
155 fun TEST_to_OLD i_model = map TEST_to_OLD_single i_model
157 type message = string;
159 fun feedback_to_string ctxt (Cor ((d, ts), _)) =
160 "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
161 | feedback_to_string _ (Syn c) = "Syn " ^ c
162 | feedback_to_string _ (Typ c) = "Typ " ^ c
163 | feedback_to_string ctxt (Inc ((d, ts), _)) =
164 "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
165 | feedback_to_string ctxt (Sup (d, ts)) =
166 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
167 | feedback_to_string ctxt (Mis (d, pid)) =
168 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
169 | feedback_to_string _ (Par s) = "Trm "^s;
171 fun feedback_POS_to_string ctxt (Cor_POS (d, ts)) =
172 "Cor_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
173 | feedback_POS_to_string _ (Syn_POS c) =
175 | feedback_POS_to_string ctxt (Inc_POS (d, [])) =
176 "Inc_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
177 Model_Pattern.empty_for d
178 | feedback_POS_to_string ctxt (Inc_POS (d, ts)) =
179 "Inc_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
180 | feedback_POS_to_string ctxt (Sup_POS (d, ts)) =
181 "Sup_POS " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
183 fun descr_vals_to_string ctxt (descr, values) =
184 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
186 (*prepare for presentation to user; thus Syn_POS does NOT raise an exn*)
187 fun feedb_args_to_string ctxt (Cor_POS (descr, values)) =
188 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
189 | feedb_args_to_string _ (Syn_POS str) = str
190 | feedb_args_to_string ctxt (Inc_POS (descr, [])) =
191 UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr
192 | feedb_args_to_string ctxt (Inc_POS (descr, values)) =
193 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
194 | feedb_args_to_string ctxt (Sup_POS (descr, values)) =
195 UnparseC.term ctxt (descr $ Model_Def.values_to_present values)
197 fun single_to_string ctxt (i, is, b, s, itm_) =
198 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
199 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
200 fun single_to_string_POS ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
201 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
202 s ^ ", (" ^ feedback_POS_to_string ctxt itm_ ^ ", Position.T))";
203 fun single_to_string_POS' (i, is, b, s, (itm_, _(*Position.T*))) =
204 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
205 s ^ ", (" ^ feedback_POS_to_string (ContextC.for_ERROR ()) itm_ ^ ", Position.T))";
207 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
208 fun to_string_POS ctxt itms = strs2str' (map (linefeed o (single_to_string_POS ctxt)) itms);
211 (** make a Tactic.T **)
213 fun make_tactic m_field (term_as_string, i_model) =
215 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
216 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
217 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
218 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
221 (** initialise a model **)
225 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
226 in map pbt2itm pbt end
230 * Now the Model in Specification is intialised such that the placement of items can be
231 maximally stable during interactive input to the Specification.
232 * Template.show provides the initial output to the user and thus determines what will be parsed
233 by Outer_Syntax later during interaction.
234 * The relation between O_Model.T and I_Model.T becomes much simpler.
237 fun patt_to_item ctxt o_model (_, (descriptor, _)) =
238 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
239 NONE => raise ERROR ("I_Model.patt_to_item NONE for " ^ UnparseC.term ctxt descriptor)
240 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
241 (Inc_POS (descr, []), Position.none))
242 fun init_POS ctxt o_model model_patt =
244 val pre_items = map (patt_to_item ctxt o_model) model_patt
246 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
250 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
251 (*DANGEROUS: do NOT use "UnIqE_tErM" *)
252 fun descriptor (Cor ((d ,_), _)) = d
253 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
254 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
255 | descriptor (Inc ((d, _), _)) = d
256 | descriptor (Sup (d, _)) = d
257 | descriptor (Mis (d, _)) = d
258 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
259 (*DANGEROUS: do NOT use "UnIqE_tErM" *)
260 fun descriptor_POS (Cor_POS (d ,_)) = d
261 | descriptor_POS (Syn_POS _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
262 | descriptor_POS (Inc_POS (d, _)) = d
263 | descriptor_POS (Sup_POS (d, _)) = d
265 fun values (Cor ((_ , ts), _)) = SOME ts
266 | values (Syn _) = NONE
267 | values (Typ _) = NONE
268 | values (Inc ((_, ts), _)) = SOME ts
269 | values (Sup (_, ts)) = SOME ts
270 | values (Mis (_, t)) = SOME [t]
271 | values _ = raise ERROR "descriptor: uncovered case in fun.def.";
272 fun o_model_values (Cor ((_, ts), _)) = ts
273 | o_model_values (Syn _) = []
274 | o_model_values (Typ _) = []
275 | o_model_values (Inc ((_, ts), _)) = ts
276 | o_model_values (Sup (_, ts)) = ts
277 | o_model_values (Mis _) = []
278 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
280 fun feedb_values (Cor_POS (_, ts)) = ts
281 | feedb_values (Syn_POS _) = raise ERROR "feedb_values NOT for Syn_POS"
282 | feedb_values (Inc_POS (_, ts)) = ts
283 | feedb_values (Sup_POS (_, ts)) = ts
285 (*assumption: i_model has filtered max_vnt*)
287 fun order_by_pa i_model (_, (descr, _ )) =
288 case find_first (fn (_, _, _, _, (feedb, _)) => descr = descriptor_POS feedb) i_model of
289 SOME i_single => [i_single]
292 fun order_by_patt model_patt i_model = model_patt |> map (order_by_pa i_model) |> flat
294 fun feedb_vals (Cor_POS (_, ts)) = [ts]
295 | feedb_vals (Syn_POS _) = []
296 | feedb_vals (Inc_POS (_, ts)) = [ts]
297 | feedb_vals (Sup_POS (_, ts)) = [ts]
298 fun get_values i_model =
299 map (fn (_, _, _, _, (feedb, _)) => feedb_vals feedb) i_model
302 fun descr_pairs_to_string ctxt equal_descr_pairs =
303 (map (fn (a, b) => pair (Model_Pattern.single_to_string ctxt a) (single_to_string_POS ctxt b)
304 |> pair2str) equal_descr_pairs)
307 fun variables model_patt i_model =
308 Pre_Conds.environment_POS model_patt i_model
312 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
314 (* get a term from O_Model, notyet input in I_Model.
315 the term from O_Model is thrown back to a string in order to reuse
316 machinery for immediate input by the user. *)
317 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
318 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
320 (*update the itm_ already input, all..from ori*)
321 fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) =
323 val ts' = union op = (feedb_values feedb) ts;
324 val complete = if eq_set op = (ts', all) then true else false
327 Cor_POS _ => if fd = "#undef"
328 then (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
329 else (id, vt, complete, fd, (Cor_POS (d, ts'), Position.none))
330 | Inc_POS _ => if complete
331 then (id, vt, true, fd, (Cor_POS (d, ts'), Position.none))
332 else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))
333 | Sup_POS (d, ts') =>
334 (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
335 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
339 (** find next step **)
341 (*old code kept for test/*)
342 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
343 case find_first (fn (_, (d', _)) => d = d') pbt of
344 SOME (_, (_, pid)) =>
345 (case find_first (fn (_, _, _, f', (feedb, _)) =>
346 f = f' andalso d = (descriptor_POS feedb)) itms of
347 SOME (_, _, _, _, (feedb, _)) =>
349 val ts' = inter op = (feedb_values feedb) ts
351 if subset op = (ts, ts')
352 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
353 else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))
355 | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
356 | NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
358 datatype add_single =
359 Add of single_POS (* return-value of check_single *)
360 | Err of string (* error-message *)
363 Create feedback for input of TermC.as_string to m_field;
364 check w.r.t. O_Model.T and Model_Pattern.T.
365 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
366 check_single is extremely permissive.
368 (*will come directly from PIDE -----------------vvvvvvvvvvv
369 in case t comes from Step.specify_do_next -----------vvv = Position.none*)
370 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
372 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
373 (*/------------ replace by ParseC.term_position -----------\*)
374 val t = Syntax.read_term ctxt ct
375 handle ERROR msg => error (msg (*^ Position.here pos*))
376 (*\------------ replace by ParseC.term_position -----------/*)
377 (*NONE => Add (i, [], false, m_field, Syn ct)*)
378 val (d, ts) = Input_Descript.split t
380 (*if d = TermC.empty then .. *)
381 (case find_first (fn (_, (d', _)) => d = d') m_patt of
382 NONE => Add (i, [], true, m_field, (Sup_POS (d,ts), Position.none))
383 | SOME (f, (_, id)) =>
384 case find_first (fn (i, _, _, _, feedb) => d = (descriptor feedb) andalso i <> 0) i_model of
386 Add (i, [], true, f, (Cor_POS (d, ts), Position.none))
387 | SOME (i', _, _, _, itm_) =>
388 if Input_Descript.for_list d then
390 val in_itm = o_model_values itm_
391 val ts' = union op = ts in_itm
392 val i'' = if in_itm = [] then i else i'
393 in Add (i'', [], true, f, (Cor_POS (d, ts'), Position.none)) end
394 else Add (i', [], true, f, (Cor_POS (d, ts), Position.none)))
396 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
397 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
399 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
400 handle ERROR msg => error (msg (*TODO: ^ Position.here pp*))
401 (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
403 case Model_Pattern.get_field descriptor m_patt of
404 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
405 UnparseC.term ctxt descriptor ^ "\"")
407 if m_field <> m_field' then
408 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
409 "\" not for field \"" ^ m_field ^ "\"")
411 case O_Model.contains ctxt m_field o_model t of
413 (case is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt of
415 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
416 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
422 fun overwrite_ppc thy itm model =
424 fun repl _ (_, _, _, _, (itm_, _)) [] =
425 raise ERROR ("overwrite_ppc: " ^ feedback_POS_to_string (Proof_Context.init_global thy) itm_
427 | repl model' itm (p :: model) =
429 then model' @ [itm] @ model
430 else repl (model' @ [p]) itm model
431 in repl [] itm model end
433 (*find_first item with #1 equal to id*)
434 fun seek_ppc _ [] = NONE
435 | seek_ppc id (p :: model) = if id = #1 (p: single_POS) then SOME p else seek_ppc id model
437 (* 10.3.00: insert the parsed itm into model;
438 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
439 fun add_single thy itm model =
441 fun eq_untouched d (0, _, _, _, (itm_, _)) = (d = descriptor_POS itm_)
442 | eq_untouched _ _ = false
443 val model' = case seek_ppc (#1 itm) model of
444 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
445 | NONE => (model @ [itm])
446 in filter_out (eq_untouched ((descriptor_POS o #1 o #5) itm)) model' end
449 (** complete I_Model.T **)
451 fun s_are_complete _ _ ([], _) _ = false
452 | s_are_complete _ _ (_, []) _ = false
453 | s_are_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
455 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
456 val met_max_vnts = Model_Def.max_variants o_model met_imod
457 val max_vnts = inter op= pbl_max_vnts met_max_vnts
458 val max_vnt = if max_vnts = []
459 then raise ERROR "I_Model.s_are_complete: request user to review met_imod"
462 val (pbl_imod', met_imod') = (
463 filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) pbl_imod,
464 filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) met_imod)
466 val (pbl_check, _) = Pre_Conds.check_internal ctxt pbl_imod' (Pos.Pbl, pbl_id)
467 val (met_check, _) = Pre_Conds.check_internal ctxt met_imod' (Pos.Met, met_id)
469 pbl_check andalso met_check
472 fun is_error (Cor_POS _) = false
473 | is_error (Sup_POS _) = false
474 | is_error (Inc_POS _) = false
475 | is_error (Syn_POS _) = true
477 (*create output-string for itm*)
478 fun to_p_model thy (Cor_POS (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
479 | to_p_model _ (Syn_POS c) = c
480 | to_p_model thy (Inc_POS (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
481 | to_p_model thy (Sup_POS (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
483 fun fill_from_o o_model (i, vnts, bool, _, (feedb, pos)) =
485 val (m_field, all_values) =
486 case find_first (fn (_, _, _, descr', _) => Model_Def.descriptor_exists descr' feedb) o_model of
487 SOME (_, _, m_field, _, ts) => (m_field, ts)
488 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
489 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
491 (*---------------vvvvvvvvvvvvv MV if TermC.is_list all_value-----*)
492 if Model_Def.is_list_descr descr
495 val already_input = feedb |> feedb_values
496 val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
497 val ts = already_input @ [hd miss]
499 if length all_values = length ts
500 then SOME (i, vnts, bool, m_field, (Cor_POS (descr, [Model_Def.values_to_present ts]), pos))
501 else SOME (i, vnts, bool, m_field, (Inc_POS (descr, [Model_Def.values_to_present ts]), pos))
503 else SOME (i, vnts, bool, m_field, (Cor_POS (descr, all_values(*only 1 term*)), pos))
507 in case there is an item in i2_model(= met) with Sup_POS,
508 find_first an appropriate (variant, descriptor) item in i1_model(= pbl) and add it instead Sup_POS,
509 otherwise keep the items of i2_model.
511 fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_POS (descr2, ts2), pos2)) =
512 (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Model_Def.get_dscr_opt feedb1 of
514 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
516 (i2, [max_vnt], bool2, m_field2, (Sup_POS (descr2, ts2), pos2)) (*the present in i2_model*)
517 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
518 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
520 (*fill method from items already input*)
521 fun fill_method o_model (pbl_imod, met_imod) met_patt =
523 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
524 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
525 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
526 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
528 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
529 val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts);
530 (*add items from pbl_imod (without overwriting existing items in met_imod)*)
532 map (add_other max_vnt pbl_imod) i_from_met
535 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
536 "variants " ^ ints2str' vnts ^ " and descriptor " ^
537 (feedb |> Model_Def.get_dscr_opt |> the |> UnparseC.term (ContextC.for_ERROR ()))
538 fun transfer_terms (i, vnts, m_field, descr, ts) =
539 (i, vnts, true, m_field, (Cor_POS (descr, ts), Position.none))
540 fun s_make_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
542 val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
543 val {model = met_patt, ...} = MethodC.from_store ctxt met_id;
544 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
545 val i_from_pbl = map (fn (_, (descr, _)) =>
546 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
547 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
548 if is_empty_single_POS i_single
550 case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
551 [] => raise ERROR (msg pbl_max_vnts feedb)
552 | o_singles => map transfer_terms o_singles
553 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
555 val i_from_met = map (fn (_, (descr, _)) =>
556 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
557 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
558 val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
560 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
561 if is_empty_single_POS i_single
563 case Pre_Conds.get_descr_vnt' feedb [max_vnt] o_model of
564 [] => raise ERROR (msg [max_vnt] feedb)
565 | o_singles => map transfer_terms o_singles
566 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
568 (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,