| changeset 60748 | d9bae125ba2a |
| parent 60747 | 2eff296ab809 |
| child 60751 | a4d734f7e02b |
| 60747:2eff296ab809 | 60748:d9bae125ba2a |
|---|---|
69 open Model_Def |
69 open Model_Def |
70 open Pre_Conds |
70 open Pre_Conds |
71 (**)open I_Model(**) |
71 (**)open I_Model(**) |
72 \<close> ML \<open> |
72 \<close> ML \<open> |
73 \<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*) |
73 \<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*) |
74 fun max_variants model_patt i_model = |
74 fun max_variants i_model = |
75 let |
75 let |
76 val all_variants = |
76 val all_variants = |
77 map (fn (_, variants, _, _, _) => variants) i_model |
77 map (fn (_, variants, _, _, _) => variants) i_model |
78 |> flat |
78 |> flat |
79 |> distinct op = |
79 |> distinct op = |
116 (*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * ) |
116 (*/-- fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------\ * ) |
117 (env_model, (env_subst, env_eval) |
117 (env_model, (env_subst, env_eval) |
118 ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *) |
118 ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *) |
119 end |
119 end |
120 ; |
120 ; |
121 max_variants: Model_Pattern.T -> Model_Def.i_model_TEST -> |
121 max_variants: Model_Def.i_model_TEST -> |
122 (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*) |
122 (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*) |
123 \<close> ML \<open> |
123 \<close> ML \<open> |
124 \<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*) |
124 \<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*) |
125 \<close> ML \<open> |
125 \<close> ML \<open> |
126 fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr |
126 fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr |
174 ; |
174 ; |
175 msg: variants -> feedback_TEST -> string |
175 msg: variants -> feedback_TEST -> string |
176 \<close> ML \<open> |
176 \<close> ML \<open> |
177 fun fill_method o_model pbl_imod met_patt = |
177 fun fill_method o_model pbl_imod met_patt = |
178 let |
178 let |
179 val (pbl_max_vnts, _) = max_variants met_patt pbl_imod; |
179 val (pbl_max_vnts, _) = max_variants pbl_imod; |
180 val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt |
180 val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt |
181 val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) => |
181 val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) => |
182 if is_empty_single_TEST i_single |
182 if is_empty_single_TEST i_single |
183 then |
183 then |
184 case get_descr_vnt' feedb pbl_max_vnts o_model of |
184 case get_descr_vnt' feedb pbl_max_vnts o_model of |
1186 \<close> ML \<open> |
1186 \<close> ML \<open> |
1187 (*old*)val ((_, pbl_max_vnt as 3, pbl_i_max), _, _) = I_Model.of_max_variant pbl_patt pbl_imod |
1187 (*old*)val ((_, pbl_max_vnt as 3, pbl_i_max), _, _) = I_Model.of_max_variant pbl_patt pbl_imod |
1188 (*new below step into*) |
1188 (*new below step into*) |
1189 |
1189 |
1190 val return_max_variants = |
1190 val return_max_variants = |
1191 (*I_Model.*)max_variants met_patt pbl_imod; |
1191 (*I_Model.*)max_variants pbl_imod; |
1192 \<close> ML \<open> (*////--------- step into max_variants ----------------------------------------------\\*) |
1192 \<close> ML \<open> (*////--------- step into max_variants ----------------------------------------------\\*) |
1193 (*////---------------- step into max_variants ----------------------------------------------\\*) |
1193 (*////---------------- step into max_variants ----------------------------------------------\\*) |
1194 "~~~~~ fun max_variants , args:"; val (model_patt, i_model) = (pbl_patt, pbl_imod); |
1194 "~~~~~ fun max_variants , args:"; val (model_patt, i_model) = (pbl_patt, pbl_imod); |
1195 \<close> ML \<open> |
1195 \<close> ML \<open> |
1196 val all_variants = |
1196 val all_variants = |
1265 val (pbl_max_vnts, pbl_max_imos) = return_max_variants |
1265 val (pbl_max_vnts, pbl_max_imos) = return_max_variants |
1266 \<close> ML \<open> |
1266 \<close> ML \<open> |
1267 \<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*) |
1267 \<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*) |
1268 (*|||----------------- continue fill_method --------------------------------------------------*) |
1268 (*|||----------------- continue fill_method --------------------------------------------------*) |
1269 \<close> ML \<open> |
1269 \<close> ML \<open> |
1270 val (pbl_max_vnts, pbl_max_imos) = (*I_Model.*)max_variants pbl_patt pbl_imod |
1270 val (pbl_max_vnts, pbl_max_imos) = (*I_Model.*)max_variants pbl_imod |
1271 ; |
1271 ; |
1272 (*+*)val [2, 1] = pbl_max_vnts; |
1272 (*+*)val [2, 1] = pbl_max_vnts; |
1273 (*-------pbl_max_imos is NONSENSE (*+*)if (pbl_max_imos ..*) |
1273 (*-------pbl_max_imos is NONSENSE (*+*)if (pbl_max_imos ..*) |
1274 (*+*)if (pbl_max_imos |> map (map (fn (no, vnts, _, _, _) => (no, vnts)))) = [ |
1274 (*+*)if (pbl_max_imos |> map (map (fn (no, vnts, _, _, _) => (no, vnts)))) = [ |
1275 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])], |
1275 [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])], |