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
19 val empty_single: single
24 datatype feedback = datatype Model_Def.i_model_feedback
25 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
29 val feedback_to_string': feedback -> string
30 val feedback_to_string: Proof.context -> feedback -> string
32 val feedback_to_string'_TEST: Proof.context -> feedback_TEST -> string
33 val feedback_TEST_to_string: feedback_TEST -> string
34 val single_to_string: Proof.context -> single -> string
35 val single_to_string_TEST: Proof.context -> single_TEST -> string
36 val to_string: Proof.context -> T -> string
37 val to_string_TEST: Proof.context -> T_TEST -> string
38 val feedback_OLD_to_TEST: feedback -> feedback_TEST
40 datatype add_single = Add of single | Err of string
41 val init: Model_Pattern.T -> T
42 val init_TEST: O_Model.T -> Model_Pattern.T -> T_TEST
43 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
44 TermC.as_string -> add_single
45 val add_single: theory -> single -> T -> T
47 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
48 val descriptor: feedback -> descriptor
49 val descriptor_TEST: feedback_TEST -> descriptor
50 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
51 val o_model_values: feedback -> O_Model.values
52 val variables: T -> term list
53 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
55 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
57 val penvval_in: feedback -> term list
59 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
60 val add: single -> T -> T
61 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
62 val is_error: feedback -> bool
63 val complete': Model_Pattern.T -> O_Model.single -> single
65 val is_complete: T -> bool
66 val to_p_model: theory -> feedback -> string
67 val eq1: ''a -> 'b * (''a * 'c) -> bool
70 val is_complete_OLD: Proof.context -> Model_Pattern.T -> Rule_Def.rule_set ->
71 Pre_Conds.unchecked -> T_TEST -> variants option
73 val is_complete_variant: int -> T_TEST-> bool
76 val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
78 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
79 Model_Def.i_model_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
82 (*from isac_test for Minisubpbl*)
83 val penv_to_string: Proof.context -> T -> string
84 val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list ->
85 'a * 'b * bool * string * feedback
86 (* ...Minisubpbl... *)
87 val seek_ppc: int -> T -> single option
88 val overwrite_ppc: theory -> single -> T -> T
98 structure I_Model(**) : INTERACTION_MODEL(**) =
104 type variant = Model_Def.variant;
105 type variants = Model_Def.variants;
106 type m_field = Model_Def.m_field;
107 type descriptor = Model_Def.descriptor;
109 type T = Model_Def.i_model_single list;
110 (* for developing input from PIDE, we use T_TEST with these ideas:
111 (1) the new structure is as close to old T, because we want to preserve the old tests
112 (2) after development (with *_TEST) of essential parts of the Specification's semantics,
113 we adapt the old tests to the new T_TEST
114 (3) together with adaption of the tests we remove the *_TEST
116 type T_TEST = Model_Def.i_model_single_TEST list;
117 datatype feedback = datatype Model_Def.i_model_feedback;
118 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;
119 type single = Model_Def.i_model_single;
120 type single_TEST = Model_Def.i_model_single_TEST;
121 val empty_single = Model_Def.i_model_empty;
123 val empty_TEST = []: T_TEST;
124 fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST ((d, ts), penv))
125 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
126 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
127 | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST ((d, ts), penv))
128 | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
129 | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
130 (UnparseC.term (ContextC.for_ERROR ()) pid))
131 | feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)
132 fun OLD_to_TEST i_old =
133 map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
135 fun feedback_TEST_to_OLD (Model_Def.Cor_TEST ((d, ts), penv)) = (Cor ((d, ts), penv))
136 | feedback_TEST_to_OLD (Model_Def.Syn_TEST c) = (Syn c)
137 | feedback_TEST_to_OLD (Model_Def.Inc_TEST ((d, ts), penv)) = (Inc ((d, ts), penv))
138 | feedback_TEST_to_OLD (Model_Def.Sup_TEST (d, ts)) = (Sup (d, ts))
139 fun TEST_to_OLD i_model =
140 map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_TEST_to_OLD e)) i_model
143 type message = string;
145 fun pen2str ctxt (t, ts) =
146 pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term ctxt)) ts);
148 fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
149 "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
150 | feedback_to_string _ (Syn c) = "Syn " ^ c
151 | feedback_to_string _ (Typ c) = "Typ " ^ c
152 | feedback_to_string ctxt (Inc ((d, ts), penv)) =
153 "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
154 | feedback_to_string ctxt (Sup (d, ts)) =
155 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
156 | feedback_to_string ctxt (Mis (d, pid)) =
157 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
158 | feedback_to_string _ (Par s) = "Trm "^s;
160 fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) =
161 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
162 | feedback_to_string_TEST _ (Syn_TEST c) =
164 | feedback_to_string_TEST ctxt (Inc_TEST ((d, []), penv)) =
165 "Inc_TEST " ^ UnparseC.term ctxt d ^ " " ^ Model_Pattern.empty_for d
166 | feedback_to_string_TEST ctxt (Inc_TEST ((d, ts), penv)) =
167 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
168 | feedback_to_string_TEST ctxt (Sup_TEST (d, ts)) =
169 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
171 fun feedback_to_string' t = feedback_to_string (ContextC.for_ERROR ()) t;
172 fun feedback_to_string'_TEST _ t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
173 fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
175 fun single_to_string ctxt (i, is, b, s, itm_) =
176 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
177 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
178 fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
179 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
180 s ^ ", (" ^ feedback_to_string'_TEST ctxt itm_ ^ ", Position.T))";
182 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
183 fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
186 (** make a Tactic.T **)
188 fun make_tactic m_field (term_as_string, i_model) =
190 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
191 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
192 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
193 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
196 (** initialise a model **)
200 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
201 in map pbt2itm pbt end
205 * Now the Model in Specification is intialised such that the placement of items can be
206 maximally stable during interactive input to the Specification.
207 * Template.show provides the initial output to the user and thus determines what will be parsed
208 by Outer_Syntax later during interaction.
209 * The relation between O_Model.T and I_Model.T becomes much simpler.
212 fun pat_to_item o_model (_, (descriptor, _)) =
213 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
214 NONE => raise ERROR "I_Model.pat_to_item_TEST with NONE"
215 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
216 (Inc_TEST ((descr, []), (descr, [])), Position.none))
217 fun init_TEST o_model model_patt =
219 val pre_items = map (pat_to_item o_model) model_patt
221 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
224 (*########################* )
225 val init = init_TEST see Test_Theory.thy
226 ( *########################*)
228 (** check input on a model **)
230 (*/---------------- old code before I_Model.T_TEST -------------------------------------------\* )
232 ( *\---------------- old code before I_Model.T_TEST -------------------------------------------/*)
234 (*/---------------- new code with I_Model.T_TEST ---------------------------------------------\*)
235 (*\---------------- new code with I_Model.T_TEST ---------------------------------------------/*)
237 (*/---------------- old code -----------------------------------------------------------------\*)
238 fun o_model_values (Cor ((_, ts), _)) = ts
239 | o_model_values (Syn _) = []
240 | o_model_values (Typ _) = []
241 | o_model_values (Inc ((_, ts), _)) = ts
242 | o_model_values (Sup (_, ts)) = ts
243 | o_model_values (Mis _) = []
244 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
246 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
247 fun descriptor (Cor ((d ,_), _)) = d
248 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
249 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
250 | descriptor (Inc ((d, _), _)) = d
251 | descriptor (Sup (d, _)) = d
252 | descriptor (Mis (d, _)) = d
253 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
254 fun descriptor_TEST (Cor_TEST ((d ,_), _)) = d
255 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
256 | descriptor_TEST (Inc_TEST ((d, _), _)) = d
257 | descriptor_TEST (Sup_TEST (d, _)) = d
258 | descriptor_TEST _ = raise ERROR "descriptor_TEST: uncovered case in fun.def.";
260 fun descr_pairs_to_string ctxt equal_descr_pairs =
261 (map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
262 |> pair2str) equal_descr_pairs)
265 (*val string_of_descr_values: term * (term list) -> string
266 fun string_of_descr_values (d, ts) = pair2str (UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.terms ts);*)
267 fun penvval_in (Cor ((d, _), (_, ts))) = (**)[Input_Descript.join'''' (d, ts)](** )------(**)[]( **)
268 | penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
269 | penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
270 | penvval_in (Inc (_, (_, ts))) = (**)ts(** )------------------------------------------(**)[]( **)
271 | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ string_of_descr_values dts);*) [])
272 | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
273 pair2str(UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.term (ContextC.for_ERROR ()) t));*) [])
274 | penvval_in _ = raise ERROR "penvval_in: uncovered case in fun.def.";
276 fun variables itms = itms |> Pre_Conds.environment |> map snd
278 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
280 (* get a term from O_Model, notyet input in I_Model.
281 the term from O_Model is thrown back to a string in order to reuse
282 machinery for immediate input by the user. *)
283 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
284 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
286 (* update the itm_ already input, all..from ori *)
287 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
289 val ts' = union op = (o_model_values itm_) ts;
290 val pval = [Input_Descript.join'''' (d, ts')]
291 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
292 val complete = if eq_set op = (ts', all) then true else false
296 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
297 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
298 | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
299 | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
302 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
303 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
304 | (Sup (d,ts')) => (*4.9.01 lost env*)
305 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
306 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
307 (* 28.1.00: not completely clear ---^^^ etc.*)
308 | (Mis _) => (* 4.9.01: Mis just copied *)
310 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
311 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
312 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string' i)
315 fun eq1 d (_, (d', _)) = (d = d')
316 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
318 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
319 case find_first (eq1 d) pbt of
320 SOME (_, (_, pid)) =>
321 (case find_first (eq3 f d) itms of
322 SOME (_, _, _, _, itm_) =>
323 let val ts' = inter op = (o_model_values itm_) ts
325 if subset op = (ts, ts')
326 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
327 else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
329 | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
330 | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
332 datatype add_single =
333 Add of single (* return-value of check_single *)
334 | Err of string (* error-message *)
337 Create feedback for input of TermC.as_string to m_field;
338 check w.r.t. O_Model.T and Model_Pattern.T.
339 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
340 check_single is extremely permissive.
342 (*will come directly from PIDE -----------------vvvvvvvvvvv
343 in case t comes from Step.specify_do_next -----------vvv = Position.none*)
344 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
346 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
347 (*/------------ replace by ParseC.term_position -----------\*)
348 val t = Syntax.read_term ctxt ct
349 handle ERROR msg => error (msg (*^ Position.here pos*))
350 (*\------------ replace by ParseC.term_position -----------/*)
351 (*NONE => Add (i, [], false, m_field, Syn ct)*)
352 val (d, ts) = Input_Descript.split t
354 if d = TermC.empty then
355 Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
357 (case find_first (eq1 d) m_patt of
358 NONE => Add (i, [], true, m_field, Sup (d,ts))
359 | SOME (f, (_, id)) =>
361 fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
363 case find_first (eq2 d) i_model of
364 NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
365 | SOME (i', _, _, _, itm_) =>
366 if Input_Descript.for_list d then
368 val in_itm = o_model_values itm_
369 val ts' = union op = ts in_itm
370 val i'' = if in_itm = [] then i else i'
371 in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
372 else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
375 (* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
376 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
377 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
379 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
380 handle ERROR msg => error (msg (*^ Position.here pp*))
381 (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
383 case Model_Pattern.get_field descriptor m_patt of
384 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
385 UnparseC.term ctxt descriptor ^ "\"")
387 if m_field <> m_field' then
388 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
389 "\" not for field \"" ^ m_field ^ "\"")
391 case O_Model.contains ctxt m_field o_model t of
393 (case is_notyet_input ctxt i_model all ori' m_patt of
395 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
396 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
402 fun overwrite_ppc thy itm model =
404 fun repl _ (_, _, _, _, itm_) [] =
405 raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_
407 | repl model' itm (p :: model) =
409 then model' @ [itm] @ model
410 else repl (model' @ [p]) itm model
411 in repl [] itm model end
413 (* find_first item with #1 equal to id *)
414 fun seek_ppc _ [] = NONE
415 | seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model
417 (* 10.3.00: insert the already compiled itm into model;
418 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
419 fun add_single thy itm model =
421 fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)
422 | eq_untouched _ _ = false
423 val model' = case seek_ppc (#1 itm) model of
424 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
425 | NONE => (model @ [itm])
426 in filter_out (eq_untouched ((descriptor o #5) itm)) model' end
428 fun complete' pbt (i, v, f, d, ts) =
429 case \<^try>\<open> (i, v, true, f, Cor ((d, ts),
430 ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)
433 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
435 (* filter out oris which have same description in itms *)
436 fun filter_outs oris [] = oris
437 | filter_outs oris (i::itms) =
439 val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris
444 (* filter oris which are in pbt, too *)
445 fun filter_pbt oris pbt =
447 val dscs = map (fst o snd) pbt
449 filter ((member op= dscs) o (#4)) oris
452 fun is_error (Cor _) = false
453 | is_error (Sup _) = false
454 | is_error (Inc _) = false
455 | is_error (Mis _) = false
458 (*create output-string for itm_*)
459 fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
460 | to_p_model _ (Syn c) = c
461 | to_p_model _ (Typ c) = c
462 | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
463 | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
464 | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid
465 | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
467 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)
469 (* insert_ppc = add for appl_add', input_icalhd 11.03,
470 handles superfluous items carelessly *)
471 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
473 (* combine itms from pbl + met and complete them wrt. pbt *)
474 (* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
475 fun complete oris pits mits met =
477 val vat = Pre_Conds.max_variant pits;
478 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
479 val ors = filter ((member_swap op= vat) o (#2)) oris
480 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
482 itms @ (map (complete' met) os)
484 val complete_Test = complete
486 (* complete model and guard of a calc-head *)
487 fun complete_method (oris, mpc, model, probl) =
489 val pits = filter_out ((curry op= false) o (#3)) probl
490 val vat = if probl = [] then 1 else Pre_Conds.max_variant probl
491 val pors = filter ((member_swap op = vat) o (#2)) oris
492 val pors = filter_outs pors pits (*which are in pbl already*)
493 val pors = (filter_pbt pors model) (*which are in pbt, too*)
494 val pits = pits @ (map (complete' model) pors)
495 val mits = complete oris pits [] mpc
498 (* TODO: also check if all elements are I_Model.Cor *)
499 fun is_complete ([]: T) = false
500 | is_complete itms = foldl and_ (true, (map #3 itms))
503 (** is_complete_OLD for PIDE **)
506 "OLD" means: this code will adapted to maintain the old texts.
507 Parts of the code will be required for Template.show etc.
510 fun is_complete_variant no_model_items i_model =
511 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
514 fun is_complete_OLD ctxt model_patt where_rls pres i_model =
516 val no_model_items = length model_patt
517 val variants_envs = Pre_Conds.sep_variants_envs model_patt i_model;
518 val result_all_variants = map
519 (fn ((i_model, env_subst, env_eval), variant) =>
520 if fst (Pre_Conds.check_variant_envs ctxt where_rls pres env_subst env_eval)
521 andalso is_complete_variant no_model_items i_model
522 then SOME [variant] else NONE) variants_envs
524 if forall is_none result_all_variants
526 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
530 val of_max_variant = Pre_Conds.of_max_variant
532 (*get_penv: single -> (term * term list) list*)
533 fun get_penv (_, _, _, _, Cor (_, elem)) = [elem]
534 | get_penv (_, _, _, _, Inc (_, elem)) = [elem]
536 fun penv_to_string ctxt i_model = map get_penv i_model
538 |> map (fn (t, ts) => pair2str (UnparseC.term ctxt t, UnparseC.terms ctxt ts))