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
15 val empty_TEST: T_TEST
18 val empty_single: single
23 datatype feedback = datatype Model_Def.i_model_feedback
24 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
28 val feedback_to_string': feedback -> string
29 val feedback_to_string: Proof.context -> feedback -> string
31 val feedback_to_string'_TEST: Proof.context -> feedback_TEST -> string
32 val feedback_TEST_to_string: feedback_TEST -> string
33 val single_to_string: Proof.context -> single -> string
34 val single_to_string_TEST: Proof.context -> single_TEST -> string
35 val to_string: Proof.context -> T -> string
36 val to_string_TEST: Proof.context -> T_TEST -> string
37 val feedback_OLD_to_TEST: feedback -> feedback_TEST
39 datatype add_single = Add of single | Err of string
40 val init: Model_Pattern.T -> T
41 val init_TEST: O_Model.T -> Model_Pattern.T -> T_TEST
42 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
43 TermC.as_string -> add_single
44 val add_single: theory -> single -> T -> T
46 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
47 val descriptor: feedback -> descriptor
48 val descriptor_TEST: feedback_TEST -> descriptor
49 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
50 val o_model_values: feedback -> O_Model.values
51 val variables: T -> term list
52 val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
54 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
56 val penvval_in: feedback -> term list
58 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
59 val add: single -> T -> T
60 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
61 val is_error: feedback -> bool
62 val complete': Model_Pattern.T -> O_Model.single -> single
64 val is_complete: T -> bool
65 val to_p_model: theory -> feedback -> string
66 val eq1: ''a -> 'b * (''a * 'c) -> bool
68 val is_complete_OLD: Proof.context -> Model_Pattern.T -> Rule_Def.rule_set ->
69 Pre_Conds.unchecked -> T_TEST -> variants option
70 val is_complete_variant: int -> T_TEST-> bool
72 val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
74 (*from isac_test for Minisubpbl*)
75 val penv_to_string: Proof.context -> T -> string
84 structure I_Model(**) : INTERACTION_MODEL(**) =
90 type variant = Model_Def.variant;
91 type variants = Model_Def.variants;
92 type m_field = Model_Def.m_field;
93 type descriptor = Model_Def.descriptor;
95 type T = Model_Def.i_model_single list;
96 (* for developing input from PIDE, we use T_TEST with these ideas:
97 (1) the new structure is as close to old T, because we want to preserve the old tests
98 (2) after development (with *_TEST) of essential parts of the Specification's semantics,
99 we adapt the old tests to the new T_TEST
100 (3) together with adaption of the tests we remove the *_TEST
102 type T_TEST = Model_Def.i_model_single_TEST list;
103 datatype feedback = datatype Model_Def.i_model_feedback;
104 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST;
105 type single = Model_Def.i_model_single;
106 type single_TEST = Model_Def.i_model_single_TEST;
107 val empty_single = Model_Def.i_model_empty;
109 val empty_TEST = []: T_TEST;
110 fun feedback_OLD_to_TEST (Cor ((d, ts), penv)) = (Model_Def.Cor_TEST ((d, ts), penv))
111 | feedback_OLD_to_TEST (Syn c) = (Model_Def.Syn_TEST c)
112 | feedback_OLD_to_TEST (Typ c) = (Model_Def.Syn_TEST c)
113 | feedback_OLD_to_TEST (Inc ((d, ts), penv)) = (Model_Def.Inc_TEST ((d, ts), penv))
114 | feedback_OLD_to_TEST (Sup (d, ts)) = (Model_Def.Sup_TEST (d, ts))
115 | feedback_OLD_to_TEST (Mis (d, pid)) = Model_Def.Syn_TEST ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
116 (UnparseC.term (ContextC.for_ERROR ()) pid))
117 | feedback_OLD_to_TEST (Par s) = (Model_Def.Syn_TEST s)
118 fun OLD_to_TEST i_old =
119 map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_TEST e, Position.none))) i_old
122 type message = string;
124 fun pen2str ctxt (t, ts) =
125 pair2str (UnparseC.term ctxt t, (strs2str' o map (UnparseC.term ctxt)) ts);
127 fun feedback_to_string ctxt (Cor ((d, ts), penv)) =
128 "Cor " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
129 | feedback_to_string _ (Syn c) = "Syn " ^ c
130 | feedback_to_string _ (Typ c) = "Typ " ^ c
131 | feedback_to_string ctxt (Inc ((d, ts), penv)) =
132 "Inc " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
133 | feedback_to_string ctxt (Sup (d, ts)) =
134 "Sup " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
135 | feedback_to_string ctxt (Mis (d, pid)) =
136 "Mis " ^ UnparseC.term ctxt d ^ " " ^ UnparseC.term ctxt pid
137 | feedback_to_string _ (Par s) = "Trm "^s;
139 fun feedback_to_string_TEST ctxt (Cor_TEST ((d, ts), penv)) =
140 "Cor_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
141 | feedback_to_string_TEST ctxt (Inp_TEST (descriptor, format)) =
142 "Inp_TEST " ^ UnparseC.term ctxt descriptor ^ " " ^ format
143 | feedback_to_string_TEST _ (Syn_TEST c) =
145 | feedback_to_string_TEST ctxt (Inc_TEST ((d, ts), penv)) =
146 "Inc_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts)) ^ " ," ^ pen2str ctxt penv
147 | feedback_to_string_TEST ctxt (Sup_TEST (d, ts)) =
148 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
150 fun feedback_to_string' t = feedback_to_string (ContextC.for_ERROR ()) t;
151 fun feedback_to_string'_TEST _ t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
152 fun feedback_TEST_to_string t = feedback_to_string_TEST (ContextC.for_ERROR ()) t;
154 fun single_to_string ctxt (i, is, b, s, itm_) =
155 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
156 s ^ " ," ^ feedback_to_string ctxt itm_ ^ ")";
157 fun single_to_string_TEST ctxt (i, is, b, s, (itm_, _(*Position.T*))) =
158 "(" ^ string_of_int i ^ ", " ^ ints2str' is ^ ", " ^ bool2str b ^ " ," ^
159 s ^ ", (" ^ feedback_to_string'_TEST ctxt itm_ ^ ", Position.T))";
161 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
162 fun to_string_TEST ctxt itms = strs2str' (map (linefeed o (single_to_string_TEST ctxt)) itms);
165 (** make a Tactic.T **)
167 fun make_tactic m_field (term_as_string, i_model) =
169 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
170 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
171 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
172 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
175 (** initialise a model **)
179 fun pbt2itm (f, (d, _)) = (0, [], false, f, Inc ((d, []), (TermC.empty, [])))
180 in map pbt2itm pbt end
184 * Now the Model in Specification is intialised such that the placement of items can be
185 maximally stable during interactive input to the Specification.
186 * Template.show provides the initial output to the user and thus determines what will be parsed
187 by Outer_Syntax later during interaction.
188 * The relation between O_Model.T and I_Model.T becomes much simpler.
191 fun pat_to_item o_model (_, (descriptor, _)) =
192 case find_first (fn (_, _, _, desc, _) => desc = descriptor) o_model of
193 NONE => raise ERROR "I_Model.pat_to_item_TEST with NONE"
194 | SOME (_, variants, m_field, descr, _) => (variants, false, m_field,
195 (Inp_TEST (descr, Model_Pattern.empty_for (type_of descriptor)), Position.none))
196 fun init_TEST o_model model_patt =
198 val pre_items = map (pat_to_item o_model) model_patt
200 O_Model.add_enumerate pre_items |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e))
203 (*########################* )
204 val init = init_TEST see Test_Theory.thy
205 ( *########################*)
207 (** check input on a model **)
209 (*/---------------- old code before I_Model.T_TEST -------------------------------------------\* )
211 ( *\---------------- old code before I_Model.T_TEST -------------------------------------------/*)
213 (*/---------------- new code with I_Model.T_TEST ---------------------------------------------\*)
214 (*\---------------- new code with I_Model.T_TEST ---------------------------------------------/*)
216 (*/---------------- old code -----------------------------------------------------------------\*)
217 fun o_model_values (Cor ((_, ts), _)) = ts
218 | o_model_values (Syn _) = []
219 | o_model_values (Typ _) = []
220 | o_model_values (Inc ((_, ts), _)) = ts
221 | o_model_values (Sup (_, ts)) = ts
222 | o_model_values (Mis _) = []
223 | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
225 val unique = Syntax.read_term\<^context> "UnIqE_tErM";
226 fun descriptor (Cor ((d ,_), _)) = d
227 | descriptor (Syn _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
228 | descriptor (Typ _) = ((*tracing ("*** descriptor: Typ ("^c^")");*) unique)
229 | descriptor (Inc ((d, _), _)) = d
230 | descriptor (Sup (d, _)) = d
231 | descriptor (Mis (d, _)) = d
232 | descriptor _ = raise ERROR "descriptor: uncovered case in fun.def.";
233 fun descriptor_TEST (Cor_TEST ((d ,_), _)) = d
234 | descriptor_TEST (Inp_TEST (d, _)) = d
235 | descriptor_TEST (Syn_TEST _) = ((*tracing ("*** descriptor: Syn ("^c^")");*) unique)
236 | descriptor_TEST (Inc_TEST ((d, _), _)) = d
237 | descriptor_TEST (Sup_TEST (d, _)) = d
238 | descriptor_TEST _ = raise ERROR "descriptor_TEST: uncovered case in fun.def.";
240 fun descr_pairs_to_string ctxt equal_descr_pairs =
241 (map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
242 |> pair2str) equal_descr_pairs)
245 (*val string_of_descr_values: term * (term list) -> string
246 fun string_of_descr_values (d, ts) = pair2str (UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.terms ts);*)
247 fun penvval_in (Cor ((d, _), (_, ts))) = (**)[Input_Descript.join'''' (d, ts)](** )------(**)[]( **)
248 | penvval_in (Syn (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
249 | penvval_in (Typ (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
250 | penvval_in (Inc (_, (_, ts))) = (**)ts(** )------------------------------------------(**)[]( **)
251 | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ string_of_descr_values dts);*) [])
252 | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
253 pair2str(UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.term (ContextC.for_ERROR ()) t));*) [])
254 | penvval_in _ = raise ERROR "penvval_in: uncovered case in fun.def.";
256 fun variables itms = itms |> Pre_Conds.environment |> map snd
258 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
260 (* get a term from O_Model, notyet input in I_Model.
261 the term from O_Model is thrown back to a string in order to reuse
262 machinery for immediate input by the user. *)
263 fun get_field_term thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
264 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
266 (* update the itm_ already input, all..from ori *)
267 fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
269 val ts' = union op = (o_model_values itm_) ts;
270 val pval = [Input_Descript.join'''' (d, ts')]
271 (* WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc *)
272 val complete = if eq_set op = (ts', all) then true else false
276 (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
277 else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
278 | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
279 | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
282 then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
283 else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
284 | (Sup (d,ts')) => (*4.9.01 lost env*)
285 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
286 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
287 (* 28.1.00: not completely clear ---^^^ etc.*)
288 | (Mis _) => (* 4.9.01: Mis just copied *)
290 then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
291 else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
292 | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string' i)
295 fun eq1 d (_, (d', _)) = (d = d')
296 fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
298 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
299 case find_first (eq1 d) pbt of
300 SOME (_, (_, pid)) =>
301 (case find_first (eq3 f d) itms of
302 SOME (_, _, _, _, itm_) =>
303 let val ts' = inter op = (o_model_values itm_) ts
305 if subset op = (ts, ts')
306 then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
307 else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
309 | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
310 | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
312 datatype add_single =
313 Add of single (* return-value of check_single *)
314 | Err of string (* error-message *)
317 Create feedback for input of TermC.as_string to m_field;
318 check w.r.t. O_Model.T and Model_Pattern.T.
319 In case of O_Model.T = [] (i.e. no data for user-guidance in Formalise.T)
320 check_single is extremely permissive.
322 (*will come directly from PIDE -----------------vvvvvvvvvvv
323 in case t comes from Step.specify_do_next -----------vvv = Position.none*)
324 fun check_single ctxt m_field [] i_model m_patt (ct(*, pos*)) =
326 val i = 1 + (if i_model = [] then 0 else map #1 i_model |> maxl)
327 (*/------------ replace by ParseC.term_position -----------\*)
328 val t = Syntax.read_term ctxt ct
329 handle ERROR msg => error (msg (*^ Position.here pos*))
330 (*\------------ replace by ParseC.term_position -----------/*)
331 (*NONE => Add (i, [], false, m_field, Syn ct)*)
332 val (d, ts) = Input_Descript.split t
334 if d = TermC.empty then
335 Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
337 (case find_first (eq1 d) m_patt of
338 NONE => Add (i, [], true, m_field, Sup (d,ts))
339 | SOME (f, (_, id)) =>
341 fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
343 case find_first (eq2 d) i_model of
344 NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
345 | SOME (i', _, _, _, itm_) =>
346 if Input_Descript.for_list d then
348 val in_itm = o_model_values itm_
349 val ts' = union op = ts in_itm
350 val i'' = if in_itm = [] then i else i'
351 in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
352 else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
355 (* for MethodC: #undef completed vvvvv vvvvvv term_as_string *)
356 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
357 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
359 val (t as (descriptor $ _)) = Syntax.read_term ctxt str
360 handle ERROR msg => error (msg (*^ Position.here pp*))
361 (*old code: NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")*)
363 case Model_Pattern.get_field descriptor m_patt of
364 NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
365 UnparseC.term ctxt descriptor ^ "\"")
367 if m_field <> m_field' then
368 Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term ctxt t ^ "\"" ^
369 "\" not for field \"" ^ m_field ^ "\"")
371 case O_Model.contains ctxt m_field o_model t of
373 (case is_notyet_input ctxt i_model all ori' m_patt of
375 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
376 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
382 fun overwrite_ppc thy itm model =
384 fun repl _ (_, _, _, _, itm_) [] =
385 raise ERROR ("overwrite_ppc: " ^ feedback_to_string (Proof_Context.init_global thy) itm_
387 | repl model' itm (p :: model) =
389 then model' @ [itm] @ model
390 else repl (model' @ [p]) itm model
391 in repl [] itm model end
393 (* find_first item with #1 equal to id *)
394 fun seek_ppc _ [] = NONE
395 | seek_ppc id (p :: model) = if id = #1 (p: single) then SOME p else seek_ppc id model
397 (* 10.3.00: insert the already compiled itm into model;
398 ev. filter_out untouched (in FE: (0,...)) item related to insert-item *)
399 fun add_single thy itm model =
401 fun eq_untouched d (0, _, _, _, itm_) = (d = descriptor itm_)
402 | eq_untouched _ _ = false
403 val model' = case seek_ppc (#1 itm) model of
404 SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
405 | NONE => (model @ [itm])
406 in filter_out (eq_untouched ((descriptor o #5) itm)) model' end
408 fun complete' pbt (i, v, f, d, ts) =
409 case \<^try>\<open> (i, v, true, f, Cor ((d, ts),
410 ((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) pbt |> the |> snd |> snd, ts)
413 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
415 (* filter out oris which have same description in itms *)
416 fun filter_outs oris [] = oris
417 | filter_outs oris (i::itms) =
419 val ors = filter_out ((curry op = ((descriptor o #5) i)) o (#4)) oris
424 (* filter oris which are in pbt, too *)
425 fun filter_pbt oris pbt =
427 val dscs = map (fst o snd) pbt
429 filter ((member op= dscs) o (#4)) oris
432 fun is_error (Cor _) = false
433 | is_error (Sup _) = false
434 | is_error (Inc _) = false
435 | is_error (Mis _) = false
438 (*create output-string for itm_*)
439 fun to_p_model thy (Cor ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
440 | to_p_model _ (Syn c) = c
441 | to_p_model _ (Typ c) = c
442 | to_p_model thy (Inc ((d, ts), _)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
443 | to_p_model thy (Sup (d, ts)) = UnparseC.term_in_thy thy (Input_Descript.join (d, ts))
444 | to_p_model thy (Mis (d, pid)) = UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid
445 | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
447 fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)
449 (* insert_ppc = add for appl_add', input_icalhd 11.03,
450 handles superfluous items carelessly *)
451 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
453 (* combine itms from pbl + met and complete them wrt. pbt *)
454 (* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
455 fun complete oris pits mits met =
457 val vat = Pre_Conds.max_variant pits;
458 val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
459 val ors = filter ((member_swap op= vat) o (#2)) oris
460 val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
462 itms @ (map (complete' met) os)
464 val complete_Test = complete
466 (* complete model and guard of a calc-head *)
467 fun complete_method (oris, mpc, model, probl) =
469 val pits = filter_out ((curry op= false) o (#3)) probl
470 val vat = if probl = [] then 1 else Pre_Conds.max_variant probl
471 val pors = filter ((member_swap op = vat) o (#2)) oris
472 val pors = filter_outs pors pits (*which are in pbl already*)
473 val pors = (filter_pbt pors model) (*which are in pbt, too*)
474 val pits = pits @ (map (complete' model) pors)
475 val mits = complete oris pits [] mpc
478 (* TODO: also check if all elements are I_Model.Cor *)
479 fun is_complete ([]: T) = false
480 | is_complete itms = foldl and_ (true, (map #3 itms))
483 (** is_complete_OLD for PIDE **)
486 "OLD" means: this code will adapted to maintain the old texts.
487 Parts of the code will be required for Template.show etc.
490 fun is_complete_variant no_model_items i_model =
491 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
493 fun is_complete_OLD ctxt model_patt where_rls pres i_model =
495 val no_model_items = length model_patt
496 val variants_envs = Pre_Conds.sep_variants_envs model_patt i_model;
497 val result_all_variants = map
498 (fn ((i_model, env_subst, env_eval), variant) =>
499 if fst (Pre_Conds.check_variant_envs ctxt where_rls pres env_subst env_eval)
500 andalso is_complete_variant no_model_items i_model
501 then SOME [variant] else NONE) variants_envs
503 if forall is_none result_all_variants
505 else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
508 val of_max_variant = Pre_Conds.of_max_variant
510 (*get_penv: single -> (term * term list) list*)
511 fun get_penv (_, _, _, _, Cor (_, elem)) = [elem]
512 | get_penv (_, _, _, _, Inc (_, elem)) = [elem]
514 fun penv_to_string ctxt i_model = map get_penv i_model
516 |> map (fn (t, ts) => pair2str (UnparseC.term ctxt t, UnparseC.terms ctxt ts))