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
30 datatype feedback = datatype Model_Def.i_model_feedback
31 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
32 val feedback_empty_TEST: Model_Def.i_model_feedback_TEST
37 val single_to_string: Proof.context -> single -> string
38 val single_to_string_TEST: Proof.context -> single_TEST -> string
39 val single_to_string_TEST': single_TEST -> string
40 val to_string: Proof.context -> T -> string
41 val to_string_TEST: Proof.context -> T_TEST -> string
43 val feedback_OLD_to_TEST: feedback -> feedback_TEST
45 datatype add_single = Add of single | Err of string
46 val init: Model_Pattern.T -> T
47 val init_TEST: Proof.context -> O_Model.T -> Model_Pattern.T -> T_TEST
48 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
49 TermC.as_string -> add_single
50 val add_single: theory -> single -> T -> T
52 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
53 val descriptor: feedback -> descriptor
54 val descriptor_TEST: feedback_TEST -> descriptor
55 val values: feedback -> values option
56 val o_model_values: feedback -> values
57 val values_TEST': feedback_TEST -> values
58 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
59 val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
60 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
62 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
65 val add: single -> T -> T
66 val handle_atom: values -> values
68 val unpack_values: descriptor * values -> values
69 val fill_from_o: O_Model.T -> single_TEST -> single_TEST option
73 val add_other: variant -> T_TEST -> single_TEST -> single_TEST
74 val fill_method: O_Model.T -> T_TEST * T_TEST-> Model_Pattern.T -> T_TEST
75 val s_make_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id ->
77 val s_are_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id -> bool
79 val is_error: feedback -> bool
80 val to_p_model: theory -> feedback -> string
81 (*/----- from isac_test for Minisubpbl*)
82 val msg: variants -> feedback_TEST -> string
83 val transfer_terms: O_Model.single -> single_TEST
85 val eq1: ''a -> 'b * (''a * 'c) -> bool
86 val feedback_to_string: Proof.context -> feedback -> string
88 val feedback_NEW_to_string: Proof.context -> feedback_TEST -> string
90 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
91 val descr_vals_to_string: Proof.context -> descriptor * values -> string
92 val feedb_args_to_string: Proof.context -> feedback_TEST -> string
95 val ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single
96 val seek_ppc: int -> T -> single option
97 val overwrite_ppc: theory -> single -> T -> T
98 (*\----- from isac_test for Minisubpbl*)
108 structure I_Model(**) : INTERACTION_MODEL(**) =
114 type variant = Model_Def.variant;
115 type variants = Model_Def.variants;
116 type m_field = Model_Def.m_field;
117 type descriptor = Model_Def.descriptor;
118 type values = Model_Def.values
120 type T = Model_Def.i_model_single list;
121 (* for developing input from PIDE, we use T_TEST with these ideas:
122 (1) the new structure is as close to old T, because we want to preserve the old tests
123 (2) after development (with *_TEST) of essential parts of the Specification's semantics,
124 we adapt the old tests to the new T_TEST
125 (3) together with adaption of the tests we remove the *_TEST
127 type T_TEST = Model_Def.i_model_single_TEST list;
128 datatype feedback = datatype Model_Def.i_model_feedback;
129 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;
130 val feedback_empty_TEST = Model_Def.feedback_empty_TEST
131 type single = Model_Def.i_model_single;
132 type single_TEST = Model_Def.i_model_single_TEST;
133 val empty_single = Model_Def.i_model_empty;
134 val empty_single_TEST = Model_Def.i_model_empty_TEST;
135 fun is_empty_single_TEST (0, [], false, "i_model_empty", _) = true
136 | is_empty_single_TEST _ = false
139 val empty_TEST = []: T_TEST;
144 fun feedback_OLD_to_TEST (Cor ((d, ts), _)) = (Model_Def.Cor_TEST (d, ts))
145 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
146 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
147 | feedback_OLD_to_TEST (Inc ((d, ts), _)) = (Model_Def.Inc_TEST (d, ts))
148 | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
149 | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
150 (UnparseC.term (ContextC.for_ERROR ()) pid))
151 | feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)
152 fun OLD_to_TEST i_old =
153 map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
155 fun feedback_TEST_to_OLD (Model_Def.Cor_TEST (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
156 | feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)
157 | feedback_TEST_to_OLD (Model_Def.Inc_TEST (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
158 | feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))
159 fun TEST_to_OLD i_model =
160 map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model
162 type message = string;
164 fun feedback_to_string ctxt (Cor ((d, ts), _)) =
165 "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
166 | feedback_to_string _ (Syn c) = "Syn " ^ c
167 | feedback_to_string _ (Typ c) = "Typ " ^ c
168 | feedback_to_string ctxt (Inc ((d, ts), _)) =
169 "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
170 | feedback_to_string ctxt (Sup (d, ts)) =
171 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
172 | feedback_to_string ctxt (Mis (d, pid)) =
173 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
174 | feedback_to_string _ (Par s) = "Trm "^s;
176 fun feedback_TEST_to_string ctxt (Cor_TEST (d, ts)) =
177 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
178 | feedback_TEST_to_string _ (Syn_TEST c) =
180 | feedback_TEST_to_string ctxt (Inc_TEST (d, [])) =
181 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, [])) ^ " " ^
182 Model_Pattern.empty_for d
183 | feedback_TEST_to_string ctxt (Inc_TEST (d, ts)) =
184 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " , pen2str"
185 | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
186 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
189 fun descr_vals_to_string ctxt (descr, values) =
190 if Model_Def.is_list_descr descr
191 then if Pre_Conds.is_NObrack_list descr
192 then UnparseC.term ctxt descr ^ " " ^ UnparseC.terms_NObrack ctxt values
193 else UnparseC.term ctxt descr ^ " " ^ UnparseC.terms ctxt values
194 else if TermC.is_atom (hd values)
195 then UnparseC.term ctxt descr ^ " " ^ UnparseC.term ctxt (hd values)
196 else UnparseC.term ctxt descr ^ " (" ^ UnparseC.term ctxt (hd values) ^ ")"
198 fun descr_vals_to_string ctxt (descr, values) =
199 UnparseC.term ctxt (descr $ Model_Def.dest_values values)
202 (*prepare for presentation to user; thus Syn_TEST does NOT raise an exn*)
204 fun feedb_args_to_string ctxt (Cor_TEST (descr, values)) = descr_vals_to_string ctxt (descr, values)
205 | feedb_args_to_string _ (Syn_TEST str) = str
206 | feedb_args_to_string ctxt (Inc_TEST (descr, [])) =
207 UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr
208 | feedb_args_to_string ctxt (Inc_TEST (descr, values)) = descr_vals_to_string ctxt (descr, values)
209 | feedb_args_to_string ctxt (Sup_TEST (descr, values)) = descr_vals_to_string ctxt (descr, values)
211 fun feedb_args_to_string ctxt (Cor_TEST (descr, values)) =
212 UnparseC.term ctxt (descr $ Model_Def.dest_values values)
213 | feedb_args_to_string _ (Syn_TEST str) = str
214 | feedb_args_to_string ctxt (Inc_TEST (descr, [])) =
215 UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr
216 | feedb_args_to_string ctxt (Inc_TEST (descr, values)) =
217 UnparseC.term ctxt (descr $ Model_Def.dest_values values)
218 | feedb_args_to_string ctxt (Sup_TEST (descr, values)) =
219 UnparseC.term ctxt (descr $ Model_Def.dest_values values)
222 fun single_to_string ctxt (i, is, b, s, itm_) =
223 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
224 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
225 fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
226 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
227 s ^ ", (" ^ feedback_TEST_to_string ctxt itm_ ^ ", Position.T))";
228 fun single_to_string_TEST' (i, is, b, s, (itm_, _(*Position.T*))) =
229 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
230 s ^ ", (" ^ feedback_TEST_to_string (ContextC.for_ERROR ()) itm_ ^ ", Position.T))";
232 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
233 fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
236 (** make a Tactic.T **)
238 fun make_tactic m_field (term_as_string, i_model) =
240 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
241 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
242 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
243 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
246 (** initialise a model **)
250 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
251 in map pbt2itm pbt end
255 * Now the Model in Specification is intialised such that the placement of items can be
256 maximally stable during interactive input to the Specification.
257 * Template.show provides the initial output to the user and thus determines what will be parsed
258 by Outer_Syntax later during interaction.
259 * The relation between O_Model.T and I_Model.T becomes much simpler.
262 fun pat_to_item ctxt o_model (_, (descriptor, _)) =
263 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
264 NONE => raise ERROR ("I_Model.pat_to_item NONE for " ^ UnparseC.term ctxt descriptor)
265 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
266 (Inc_TEST (descr, []), Position.none))
267 fun init_TEST ctxt o_model model_patt =
269 val pre_items = map (pat_to_item ctxt o_model) model_patt
271 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
275 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
276 fun descriptor (Cor ((d ,_), _)) = d
277 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
278 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
279 | descriptor (Inc ((d, _), _)) = d
280 | descriptor (Sup (d, _)) = d
281 | descriptor (Mis (d, _)) = d
282 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
283 fun descriptor_TEST (Cor_TEST (d ,_)) = d
284 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
285 | descriptor_TEST (Inc_TEST (d, _)) = d
286 | descriptor_TEST (Sup_TEST (d, _)) = d
288 fun values (Cor ((_ , ts), _)) = SOME ts
289 | values (Syn _) = NONE
290 | values (Typ _) = NONE
291 | values (Inc ((_, ts), _)) = SOME ts
292 | values (Sup (_, ts)) = SOME ts
293 | values (Mis (_, t)) = SOME [t]
294 | values _ = raise ERROR "descriptor: uncovered case in fun.def.";
295 fun o_model_values (Cor ((_, ts), _)) = ts
296 | o_model_values (Syn _) = []
297 | o_model_values (Typ _) = []
298 | o_model_values (Inc ((_, ts), _)) = ts
299 | o_model_values (Sup (_, ts)) = ts
300 | o_model_values (Mis _) = []
301 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
302 fun values_TEST' (Cor_TEST (_, ts)) = ts
303 | values_TEST' (Syn_TEST _) = raise ERROR "values_TEST' NOT for Syn_TEST"
304 | values_TEST' (Inc_TEST (_, ts)) = ts
305 | values_TEST' (Sup_TEST (_, ts)) = ts
307 fun descr_pairs_to_string ctxt equal_descr_pairs =
308 (map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
309 |> pair2str) equal_descr_pairs)
312 fun variables model_patt i_model =
313 Pre_Conds.environment_TEST model_patt i_model
316 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
318 (* get a term from O_Model, notyet input in I_Model.
319 the term from O_Model is thrown back to a string in order to reuse
320 machinery for immediate input by the user. *)
321 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
322 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
324 (*update the itm_ already input, all..from ori*)
325 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
327 val ts' = union op = (o_model_values itm_) ts;
328 val pval = [Input_Descript.join'''' (d, ts')]
329 (*WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc*)
330 val complete = if eq_set op = (ts', all) then true else false
334 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
335 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
336 | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
337 | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
340 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
341 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
342 | (Sup (d,ts')) => (*4.9.01 lost env*)
343 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
344 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
345 (* 28.1.00: not completely clear ---^^^ etc.*)
346 | (Mis _) => (* 4.9.01: Mis just copied *)
348 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
349 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
350 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string (ContextC.for_ERROR ()) i)
354 (** find next step **)
356 fun eq1 d (_, (d', _)) = (d = d')
357 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
359 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
360 case find_first (eq1 d) pbt of
361 SOME (_, (_, pid)) =>
362 (case find_first (eq3 f d) itms of
363 SOME (_, _, _, _, itm_) =>
364 let val ts' = inter op = (o_model_values itm_) ts
366 if subset op = (ts, ts')
367 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
368 else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
370 | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
371 | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
373 datatype add_single =
374 Add of single (* return-value of check_single *)
375 | Err of string (* error-message *)
378 Create feedback for input of TermC.as_string to m_field;
379 check w.r.t. O_Model.T and Model_Pattern.T.
380 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
381 check_single is extremely permissive.
383 (*will come directly from PIDE -----------------vvvvvvvvvvv
384 in case t comes from Step.specify_do_next -----------vvv = Position.none*)
385 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
387 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
388 (*/------------ replace by ParseC.term_position -----------\*)
389 val t = Syntax.read_term ctxt ct
390 handle ERROR msg => error (msg (*^ Position.here pos*))
391 (*\------------ replace by ParseC.term_position -----------/*)
392 (*NONE => Add (i, [], false, m_field, Syn ct)*)
393 val (d, ts) = Input_Descript.split t
395 if d = TermC.empty then
396 Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
398 (case find_first (eq1 d) m_patt of
399 NONE => Add (i, [], true, m_field, Sup (d,ts))
400 | SOME (f, (_, id)) =>
402 fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
404 case find_first (eq2 d) i_model of
405 NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
406 | SOME (i', _, _, _, itm_) =>
407 if Input_Descript.for_list d then
409 val in_itm = o_model_values itm_
410 val ts' = union op = ts in_itm
411 val i'' = if in_itm = [] then i else i'
412 in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
413 else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
416 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
417 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
419 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
420 handle ERROR msg => error (msg (*TODO: ^ Position.here pp*))
421 (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
423 case Model_Pattern.get_field descriptor m_patt of
424 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
425 UnparseC.term ctxt descriptor ^ "\"")
427 if m_field <> m_field' then
428 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
429 "\" not for field \"" ^ m_field ^ "\"")
431 case O_Model.contains ctxt m_field o_model t of
433 (case is_notyet_input ctxt i_model all ori' m_patt of
435 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
436 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
442 fun overwrite_ppc thy itm model =
444 fun repl _ (_, _, _, _, itm_) [] =
445 raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_
447 | repl model' itm (p :: model) =
449 then model' @ [itm] @ model
450 else repl (model' @ [p]) itm model
451 in repl [] itm model end
453 (*find_first item with #1 equal to id*)
454 fun seek_ppc _ [] = NONE
455 | seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model
457 (* 10.3.00: insert the parsed itm into model;
458 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
459 fun add_single thy itm model =
461 fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)
462 | eq_untouched _ _ = false
463 val model' = case seek_ppc (#1 itm) model of
464 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
465 | NONE => (model @ [itm])
466 in filter_out (eq_untouched ((descriptor o #5) itm)) model' end
469 (** complete I_Model.T **)
471 fun s_are_complete _ _ ([], _) _ = false
472 | s_are_complete _ _ (_, []) _ = false
473 | s_are_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
475 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
476 val met_max_vnts = Model_Def.max_variants o_model met_imod
477 val max_vnts = inter op= pbl_max_vnts met_max_vnts
478 val max_vnt = if max_vnts = []
479 then raise ERROR "I_Model.s_are_complete: request user to review met_imod"
482 val (pbl_imod', met_imod') = (
483 filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) pbl_imod,
484 filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts) met_imod)
486 val (pbl_check, _) = Pre_Conds.check_internal ctxt pbl_imod' (Pos.Pbl, pbl_id)
487 val (met_check, _) = Pre_Conds.check_internal ctxt met_imod' (Pos.Met, met_id)
489 pbl_check andalso met_check
492 fun is_error (Cor _) = false
493 | is_error (Sup _) = false
494 | is_error (Inc _) = false
495 | is_error (Mis _) = false
499 (*create output-string for itm*)
500 fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
501 | to_p_model _ (Syn c) = c
502 | to_p_model _ (Typ c) = c
503 | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
504 | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
505 | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid
506 | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
508 (*see feedback_NEW_to_string, descr_vals_to_string*)
512 fun handle_atom [t] = [t]
513 | handle_atom ts = [TermC.list2isalist (type_of (hd ts)) ts]
516 atoms like Solutions (L::bool list);
517 precondition: arguments are of type list; according to type of descriptor
519 fun handle_atom [t] = [t]
520 | handle_atom ts = ts |> map TermC.isalist2list |> flat
524 fun is_NObrack_list (Const ("Input_Descript.solutions", _)) = true
525 | is_NObrack_list (Const ("EqSystem.solution", _)) = true
526 | is_NObrack_list (Const ("Biegelinie.Gleichungen", _)) = true
527 | is_NObrack_list _ = false
528 fun unpack_values (descr, [t]) =
529 if Model_Def.is_list_descr descr
530 then if is_NObrack_list descr
532 else t |> TermC.isalist2list
534 | unpack_values (_, ts) = ts |> map TermC.isalist2list |> flat
539 fun fill_from_o o_model (i, vnts, bool, _, (feedb, pos)) =
541 val (m_field, all_value) =
542 case find_first (fn (_, _, _, descr', _) => Pre_Conds.descriptor_exists descr' feedb) o_model of
543 SOME (_, _, m_field, _, ts) => (m_field, ts)
544 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
545 val descr = Pre_Conds.get_dscr'' feedb (*i_single has been filtered appropriately*)
547 if Model_Def.is_list_descr descr
550 val all_value' = unpack_values (descr, all_value)
551 val already_input = feedb |> values_TEST' |> map TermC.isalist2list |> flat
552 val miss = subtract op= already_input all_value'
553 val present = already_input @ [hd miss]
555 if length all_value' = length present
556 then SOME (i, vnts, bool, m_field, (Cor_TEST (descr, present), pos))
557 else SOME (i, vnts, bool, m_field, (Inc_TEST (descr, present), pos))
559 else SOME (i, vnts, bool, m_field, (Cor_TEST (descr, all_value), pos))
562 fun fill_from_o o_model (i, vnts, bool, _, (feedb, pos)) =
564 val (m_field, all_values) =
565 case find_first (fn (_, _, _, descr', _) => Pre_Conds.descriptor_exists descr' feedb) o_model of
566 SOME (_, _, m_field, _, ts) => (m_field, ts)
567 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
568 val descr = Pre_Conds.get_dscr'' feedb (*i_single has been filtered appropriately*)
570 (*---------------vvvvvvvvvvvvv MV if TermC-is_list all_value-----*)
571 if Model_Def.is_list_descr descr
574 val already_input = feedb |> values_TEST'
575 val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
576 val ts = already_input @ [hd miss]
578 if length all_values = length ts
579 then SOME (i, vnts, bool, m_field, (Cor_TEST (descr, [Model_Def.dest_values ts]), pos))
580 else SOME (i, vnts, bool, m_field, (Inc_TEST (descr, [Model_Def.dest_values ts]), pos))
582 else SOME (i, vnts, bool, m_field, (Cor_TEST (descr, all_values(*only 1 term*)), pos))
587 in case there is an item in i2_model(= met) with Sup_TEST,
588 find_first an appropriate (variant, descriptor) item in i1_model(= pbl) and add it instead Sup_TEST,
589 otherwise keep the items of i2_model.
591 fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) =
592 (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Pre_Conds.get_dscr' feedb1 of
594 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
596 (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*)
597 | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
598 | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
600 fun fill_method o_model (pbl_imod, met_imod) met_patt =
602 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
603 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
604 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
605 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
607 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
608 val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts);
609 (*add items from pbl_imod (without overwriting existing items in met_imod)*)
611 map (add_other max_vnt pbl_imod) i_from_met
614 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
615 "variants " ^ ints2str' vnts ^ " and descriptor " ^
616 (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
617 fun transfer_terms (i, vnts, m_field, descr, ts) =
618 (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
619 fun s_make_complete ctxt o_model (pbl_imod, met_imod) (pbl_id, met_id) =
621 val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id;
622 val {model = met_patt, ...} = MethodC.from_store ctxt met_id;
623 val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
624 val i_from_pbl = map (fn (_, (descr, _)) =>
625 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
626 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
627 if is_empty_single_TEST i_single
629 case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
630 [] => raise ERROR (msg pbl_max_vnts feedb)
631 | o_singles => map transfer_terms o_singles
632 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
634 val i_from_met = map (fn (_, (descr, _)) =>
635 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
636 val met_max_vnts = Model_Def.max_variants o_model i_from_met;
637 val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
639 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
640 if is_empty_single_TEST i_single
642 case Pre_Conds.get_descr_vnt' feedb [max_vnt] o_model of
643 [] => raise ERROR (msg [max_vnt] feedb)
644 | o_singles => map transfer_terms o_singles
645 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
647 (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,