152 fun get_descr (_, _, _, _, (feedb, _)) = |
152 fun get_descr (_, _, _, _, (feedb, _)) = |
153 case get_dscr' feedb of NONE => NONE | some_descr => some_descr |
153 case get_dscr' feedb of NONE => NONE | some_descr => some_descr |
154 (* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single -> (Model_Pattern.single * I_Model.single_TEST) list*) |
154 (* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single -> (Model_Pattern.single * I_Model.single_TEST) list*) |
155 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) = |
155 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) = |
156 let |
156 let |
157 val equal_variants = |
157 val equal_descr = |
158 filter (fn i_single => case get_descr i_single of |
158 filter (fn i_single => case get_descr i_single of |
159 NONE => false (*--------vvvvv*) |
159 NONE => false (*--------vvvvv*) |
160 | SOME descr' => descr' = descr) (*probl_POS*) i_model |
160 | SOME descr' => descr' = descr) i_model |
161 in |
161 in |
162 (map (pair m_patt_single) equal_variants) |
162 (map (pair m_patt_single) equal_descr) |
163 end |
163 end |
164 |
164 |
165 (*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*) |
165 (* |
|
166 get an appropriate (description, variant)-item from i_model, otherwise return empty item, |
|
167 i.e. this function produces items with Sup. |
|
168 *) |
166 fun get_descr_vnt descr vnts i_model = |
169 fun get_descr_vnt descr vnts i_model = |
167 let |
170 let |
168 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false |
171 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false |
169 | SOME descr' => if descr = descr' then true else false) i_model |
172 | SOME descr' => if descr = descr' then true else false) i_model |
170 in |
173 in |