38 val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single -> |
38 val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single -> |
39 (Model_Pattern.single * Model_Def.i_model_single_TEST) list |
39 (Model_Pattern.single * Model_Def.i_model_single_TEST) list |
40 val unchecked_OLD_to_TEST: term list -> (term * Position.T) list |
40 val unchecked_OLD_to_TEST: term list -> (term * Position.T) list |
41 |
41 |
42 val all_lhs_atoms: term list -> bool |
42 val all_lhs_atoms: term list -> bool |
|
43 (*/------- \<longrightarrow> pre-conditions*) |
|
44 val is_list_descr: Model_Pattern.descriptor -> bool |
|
45 val is_NObrack_list: Model_Pattern.descriptor -> Model_Pattern.values -> bool |
|
46 (*\------- \<longrightarrow> pre-conditions*) |
43 val handle_lists: term -> Model_Def.descriptor * term list -> Env.T; |
47 val handle_lists: term -> Model_Def.descriptor * term list -> Env.T; |
44 val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST |
48 val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST |
45 val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor; |
49 val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor; |
46 val discern_feedback: term -> Model_Def.i_model_feedback_TEST -> |
50 val discern_feedback: term -> Model_Def.i_model_feedback_TEST -> |
47 ((term * term) * (term * term)) list |
51 ((term * term) * (term * term)) list |
55 val get_dscr': Model_Def.i_model_feedback_TEST -> Model_Def.descriptor option |
59 val get_dscr': Model_Def.i_model_feedback_TEST -> Model_Def.descriptor option |
56 val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model_TEST -> |
60 val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model_TEST -> |
57 Model_Def.i_model_single_TEST |
61 Model_Def.i_model_single_TEST |
58 val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T -> |
62 val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T -> |
59 O_Model.T |
63 O_Model.T |
|
64 val get_dscr'': Model_Def.i_model_feedback_TEST -> Model_Pattern.descriptor |
|
65 val descriptor_exists: Model_Pattern.descriptor -> Model_Def.i_model_feedback_TEST -> bool |
60 (*\----- from isac_test for Minisubpbl*) |
66 (*\----- from isac_test for Minisubpbl*) |
61 |
67 |
62 \<^isac_test>\<open> |
68 \<^isac_test>\<open> |
63 (**) |
69 (**) |
64 \<close> |
70 \<close> |
159 NONE => false (*--------vvvvv*) |
165 NONE => false (*--------vvvvv*) |
160 | SOME descr' => descr' = descr) i_model |
166 | SOME descr' => descr' = descr) i_model |
161 in |
167 in |
162 (map (pair m_patt_single) equal_descr) |
168 (map (pair m_patt_single) equal_descr) |
163 end |
169 end |
|
170 |
|
171 (*OLD*) |
|
172 (*---*) |
|
173 fun descriptor_exists descr feedb = |
|
174 case get_dscr' feedb of |
|
175 SOME descr' => descr' = descr |
|
176 | NONE => raise ERROR "existing_description NONE" |
|
177 (*in case descriptor exists in this item*) |
|
178 fun get_dscr'' (Cor_TEST (descr, _)) = descr |
|
179 | get_dscr'' (Inc_TEST (descr, _)) = descr |
|
180 | get_dscr'' (Sup_TEST (descr, _)) = descr |
|
181 | get_dscr'' _ = raise ERROR "get_dscr'' from item without this description" |
|
182 (*NEW*) |
164 |
183 |
165 (* |
184 (* |
166 get an appropriate (description, variant)-item from i_model, otherwise return empty item, |
185 get an appropriate (description, variant)-item from i_model, otherwise return empty item, |
167 i.e. this function produces items with Sup. |
186 i.e. this function produces items with Sup. |
168 *) |
187 *) |
190 fun all_lhs_atoms ts = fold (curry and_) (map (fn t => |
209 fun all_lhs_atoms ts = fold (curry and_) (map (fn t => |
191 if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t)) |
210 if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t)) |
192 then TermC.is_atom (TermC.lhs t) |
211 then TermC.is_atom (TermC.lhs t) |
193 else false) ts) true |
212 else false) ts) true |
194 |
213 |
|
214 (*/------- \<longrightarrow> pre-conditions*) |
|
215 fun is_list_descr descr = |
|
216 case Model_Pattern.descr_type (type_of descr) of Model_Pattern.List _ => true | _ => false |
|
217 (*OLD* ) |
|
218 fun is_NObrack_list descr values = |
|
219 (*HACK: before introduction typedecl toreallNOpar, toboollNOpar*) |
|
220 let |
|
221 val (*maximum- example*)(max_descr, max_values) = |
|
222 (@{term AdditionalValues}, [@{term "u::real"}, @{term "v::real"}]) |
|
223 val (*begelinien- example 7.70*)(bieg_descr, bieg_values) = |
|
224 (@{term Randbedingungen}, |
|
225 [@{term "(y::real \<Rightarrow> real) 0 = (0::real)"}, @{term "(y::real \<Rightarrow> real) L = (0::real)"}, |
|
226 @{term "M_b 0 = (0::real)"}, @{term "M_b L = (0::real)"}]) |
|
227 in |
|
228 not |
|
229 ((descr = max_descr andalso subset op= (values, max_values)) orelse |
|
230 (descr = bieg_descr andalso subset op= (values, bieg_values))) |
|
231 end |
|
232 ( *---*) |
|
233 fun is_NObrack_list descr _ = |
|
234 (*HACK: before introduction typedecl toreallNObrack, toboollNObrack*) |
|
235 descr = @{term solutions} orelse descr = @{term solution} orelse descr = @{term Gleichungen} |
|
236 |
195 fun handle_lists id (descr, ts) = |
237 fun handle_lists id (descr, ts) = |
196 if Model_Pattern.is_list_descr descr |
238 if is_list_descr descr |
197 then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*) |
239 then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*) |
198 then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*) |
240 then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*) |
199 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))] |
241 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))] |
200 else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*) |
242 else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*) |
201 else if TermC.is_atom (Library.the_single ts) |
243 else if TermC.is_atom (Library.the_single ts) |
224 |
266 |
225 fun discern_typ _ (_, []) = [] |
267 fun discern_typ _ (_, []) = [] |
226 | discern_typ id (descr, ts) = |
268 | discern_typ id (descr, ts) = |
227 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*) |
269 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*) |
228 let |
270 let |
229 val ts = if Model_Pattern.is_list_descr descr |
271 val ts = if is_list_descr descr |
230 then if TermC.is_list (hd ts) |
272 then if TermC.is_list (hd ts) |
231 then ts |> map TermC.isalist2list |> flat |
273 then ts |> map TermC.isalist2list |> flat |
232 else ts |
274 else ts |
233 else ts |
275 else ts |
234 in |
276 in |