71 (* val where_ = if pI = Problem.id_empty then []*) |
71 (* val where_ = if pI = Problem.id_empty then []*) |
72 (*if*) pI = Problem.id_empty (*else*); |
72 (*if*) pI = Problem.id_empty (*else*); |
73 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI |
73 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI |
74 val (_, where_) = |
74 val (_, where_) = |
75 Pre_Conds.check ctxt where_rls where_ |
75 Pre_Conds.check ctxt where_rls where_ |
76 (model, I_Model.OLD_to_POS probl); |
76 (model, I_Model.OLD_to probl); |
77 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
77 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
78 (ctxt, where_rls, where_, (model, I_Model.OLD_to_POS probl)); |
78 (ctxt, where_rls, where_, (model, I_Model.OLD_to probl)); |
79 val (env_model, (env_subst, env_eval)) = |
79 val (env_model, (env_subst, env_eval)) = |
80 make_environments model_patt i_model; |
80 make_environments model_patt i_model; |
81 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model); |
81 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model); |
82 (*\------------------- step into init_calc -------------------------------------------------//*) |
82 (*\------------------- step into init_calc -------------------------------------------------//*) |
83 val (p,_,f,nxt,_,pt) = return_init_calc; |
83 val (p,_,f,nxt,_,pt) = return_init_calc; |
109 (tac, (ctree, pos)); |
109 (tac, (ctree, pos)); |
110 val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of |
110 val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of |
111 Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI') |
111 Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI') |
112 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj" |
112 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj" |
113 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' |
113 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' |
114 val pbl = I_Model.init_POS ctxt o_model model_patt |
114 val pbl = I_Model.init ctxt o_model model_patt |
115 |
115 |
116 val return_check = |
116 val return_check = |
117 Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])); |
117 Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])); |
118 (*\\------------------ step into by_tactic -------------------------------------------------//*) |
118 (*\\------------------ step into by_tactic -------------------------------------------------//*) |
119 val (pt, p) = return_by_tactic; |
119 val (pt, p) = return_by_tactic; |
148 val ctxt = Ctree.get_ctxt pt pos; |
148 val ctxt = Ctree.get_ctxt pt pos; |
149 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
149 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
150 (*if*) p_ = Pos.Pbl (*then*); |
150 (*if*) p_ = Pos.Pbl (*then*); |
151 |
151 |
152 val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) = |
152 val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) = |
153 Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_POS met); |
153 Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to met); |
154 (*/////--------------- step into for_problem -----------------------------------------------\\*) |
154 (*/////--------------- step into for_problem -----------------------------------------------\\*) |
155 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) |
155 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) |
156 = (ctxt, oris, (o_refs, refs), (pbl, met)); |
156 = (ctxt, oris, (o_refs, refs), (pbl, met)); |
157 val cdI = if dI = ThyC.id_empty then dI' else dI; |
157 val cdI = if dI = ThyC.id_empty then dI' else dI; |
158 val cpI = if pI = Problem.id_empty then pI' else pI; |
158 val cpI = if pI = Problem.id_empty then pI' else pI; |
159 val cmI = if mI = MethodC.id_empty then mI' else mI; |
159 val cmI = if mI = MethodC.id_empty then mI' else mI; |
160 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
160 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
161 val {model = mpc, ...} = MethodC.from_store ctxt cmI; |
161 val {model = mpc, ...} = MethodC.from_store ctxt cmI; |
162 |
162 |
163 val return_check = |
163 val return_check = |
164 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_POS pbl); |
164 Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to pbl); |
165 (*//////-------------- step into check -------------------------------------------------\\*) |
165 (*//////-------------- step into check -------------------------------------------------\\*) |
166 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
166 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = |
167 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_POS pbl)); |
167 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to pbl)); |
168 val return_make_environments = |
168 val return_make_environments = |
169 make_environments model_patt i_model; |
169 make_environments model_patt i_model; |
170 (*///// //------------ step into of_max_variant --------------------------------------------\\*) |
170 (*///// //------------ step into of_max_variant --------------------------------------------\\*) |
171 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = |
171 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = |
172 (model_patt, i_model); |
172 (model_patt, i_model); |
173 |
173 |
174 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_POS Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_POS Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_POS AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_POS Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_POS SideConditions [] [__=__, __=__], Position.T))]" |
174 (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc SideConditions [] [__=__, __=__], Position.T))]" |
175 = i_model |> I_Model.to_string_POS ctxt |
175 = i_model |> I_Model.to_string ctxt |
176 val all_variants = |
176 val all_variants = |
177 map (fn (_, variants, _, _, _) => variants) i_model |
177 map (fn (_, variants, _, _, _) => variants) i_model |
178 |> flat |
178 |> flat |
179 |> distinct op = |
179 |> distinct op = |
180 val variants_separated = map (filter_variants' i_model) all_variants |
180 val variants_separated = map (filter_variants' i_model) all_variants |
190 (*!!!*) val ("#Given", (descr, term), pos) = |
190 (*!!!*) val ("#Given", (descr, term), pos) = |
191 Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none) |
191 Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none) |
192 (*!!!*) val patt = equal_descr_pairs |> hd |> #1 |
192 (*!!!*) val patt = equal_descr_pairs |> hd |> #1 |
193 (*!!!*)val equal_descr_pairs = |
193 (*!!!*)val equal_descr_pairs = |
194 (patt, |
194 (patt, |
195 (1, [1, 2, 3], true, "#Given", (Cor_POS ((descr, (*!*)TermC.isalist2list(*!*) term)), pos))) |
195 (1, [1, 2, 3], true, "#Given", (Cor ((descr, (*!*)TermC.isalist2list(*!*) term)), pos))) |
196 :: tl equal_descr_pairs |
196 :: tl equal_descr_pairs |
197 (*for building make_env_s -------------------------------------------------------------------/*) |
197 (*for building make_env_s -------------------------------------------------------------------/*) |
198 |
198 |
199 val env_model = make_env_model equal_descr_pairs; |
199 val env_model = make_env_model equal_descr_pairs; |
200 (*///// ///----------- step into make_env_model --------------------------------------------\\*) |
200 (*///// ///----------- step into make_env_model --------------------------------------------\\*) |
212 make_envs_preconds equal_givens; |
212 make_envs_preconds equal_givens; |
213 (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*) |
213 (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*) |
214 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens); |
214 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens); |
215 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) |
215 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) |
216 ; |
216 ; |
217 xxx: (Model_Pattern.single * I_Model.single_POS) -> ((term * term) * (term * term)) list; |
217 xxx: (Model_Pattern.single * I_Model.single) -> ((term * term) * (term * term)) list; |
218 val return_discern_feedback = |
218 val return_discern_feedback = |
219 discern_feedback id feedb; |
219 discern_feedback id feedb; |
220 (*nth 1 equal_descr_pairs* ) |
220 (*nth 1 equal_descr_pairs* ) |
221 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_POS ((descr, ts), _))) = (id, feedb); |
221 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor ((descr, ts), _))) = (id, feedb); |
222 ( *nth 2 equal_descr_pairs*) |
222 ( *nth 2 equal_descr_pairs*) |
223 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_POS ((descr, ts)))) = (id, feedb); |
223 "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc ((descr, ts)))) = (id, feedb); |
224 |
224 |
225 (*nth 1 equal_descr_pairs* ) |
225 (*nth 1 equal_descr_pairs* ) |
226 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), |
226 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), |
227 (Free ("r", typ3), value))] = return_discern_feedback |
227 (Free ("r", typ3), value))] = return_discern_feedback |
228 (*+*)val true = typ1 = typ2 |
228 (*+*)val true = typ1 = typ2 |
245 (**) |
245 (**) |
246 switch_type id ts; |
246 switch_type id ts; |
247 "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts); |
247 "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts); |
248 |
248 |
249 (*nth 1 equal_descr_pairs* ) |
249 (*nth 1 equal_descr_pairs* ) |
250 val return_switch_type_POS = Const (descr_string, ts |> hd |> TermC.lhs |> type_of) |
250 val return_switch_type = Const (descr_string, ts |> hd |> TermC.lhs |> type_of) |
251 |
251 |
252 (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_POS |
252 (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type |
253 (*+*)val Type ("Real.real", []) = typ |
253 (*+*)val Type ("Real.real", []) = typ |
254 ( *nth 2 equal_descr_pairs*) |
254 ( *nth 2 equal_descr_pairs*) |
255 (*+*)val return_switch_type_POS = descr |
255 (*+*)val return_switch_type = descr |
256 (**) |
256 (**) |
257 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*) |
257 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*) |
258 (*||||| ||------------ contine of_max_variant ------------------------------------------------*) |
258 (*||||| ||------------ contine of_max_variant ------------------------------------------------*) |
259 val subst_eval_list = make_envs_preconds equal_givens |
259 val subst_eval_list = make_envs_preconds equal_givens |
260 val (env_subst, env_eval) = split_list subst_eval_list |
260 val (env_subst, env_eval) = split_list subst_eval_list |
282 val NONE = |
282 val NONE = |
283 (*case*) find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl (*of*); |
283 (*case*) find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl (*of*); |
284 |
284 |
285 (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **) |
285 (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **) |
286 (**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*) |
286 (**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*) |
287 Specify.item_to_add ctxt oris (I_Model.OLD_to_POS pbl) (*of*); |
287 Specify.item_to_add ctxt oris (I_Model.OLD_to pbl) (*of*); |
288 (*///// /------------- step into item_to_add -----------------------------------------------\\*) |
288 (*///// /------------- step into item_to_add -----------------------------------------------\\*) |
289 (*==================== see test/../i_model.sml --- fun item_to_add ---========================*) |
289 (*==================== see test/../i_model.sml --- fun item_to_add ---========================*) |
290 (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*) |
290 (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*) |
291 val SOME (fd, ct') = return_item_to_add |
291 val SOME (fd, ct') = return_item_to_add |
292 (*+*)val ("#Given", "Constants [r = 7]") = (fd, ct') (*from NEW item_to_add*) |
292 (*+*)val ("#Given", "Constants [r = 7]") = (fd, ct') (*from NEW item_to_add*) |
361 (ctxt, i_model, all, ori', m_patt); |
361 (ctxt, i_model, all, ori', m_patt); |
362 val SOME (_, (_, pid)) = |
362 val SOME (_, (_, pid)) = |
363 (*case*) find_first (fn (_, (d', _)) => d = d') pbt |
363 (*case*) find_first (fn (_, (d', _)) => d = d') pbt |
364 val SOME (_, _, _, _, (feedb, _)) = |
364 val SOME (_, _, _, _, (feedb, _)) = |
365 (*case*) find_first (fn (_, _, _, f', (feedb, _)) => |
365 (*case*) find_first (fn (_, _, _, f', (feedb, _)) => |
366 f = f' andalso d = (descriptor_POS feedb)) itms |
366 f = f' andalso d = (descriptor feedb)) itms |
367 val ts' = inter op = (feedb_values feedb) ts |
367 val ts' = inter op = (feedb_values feedb) ts |
368 val false = |
368 val false = |
369 (*if*) subset op = (ts, ts') |
369 (*if*) subset op = (ts, ts') |
370 |
370 |
371 val return_is_notyet_input = ("", |
371 val return_is_notyet_input = ("", |
374 (feedb, pid, all, (i, v, f, d, subtract op = ts' ts)); |
374 (feedb, pid, all, (i, v, f, d, subtract op = ts' ts)); |
375 val ts' = union op = (feedb_values feedb) ts; |
375 val ts' = union op = (feedb_values feedb) ts; |
376 val pval = [Input_Descript.join'''' (d, ts')] |
376 val pval = [Input_Descript.join'''' (d, ts')] |
377 val complete = if eq_set op = (ts', all) then true else false |
377 val complete = if eq_set op = (ts', all) then true else false |
378 |
378 |
379 (*+*)val "Inc_POS Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_POS_to_string ctxt |
379 (*+*)val "Inc Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_to_string ctxt |
380 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |
380 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |
381 (*\\------------------ step into do_next ---------------------------------------------------//*) |
381 (*\\------------------ step into do_next ---------------------------------------------------//*) |
382 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next |
382 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next |
383 |
383 |
384 (*|------------------- continue with me_Model_Problem ----------------------------------------*) |
384 (*|------------------- continue with me_Model_Problem ----------------------------------------*) |
399 |
399 |
400 pt_model ppobj p_; |
400 pt_model ppobj p_; |
401 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), |
401 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), |
402 Pbl(*Frm,Pbl*)) = (ppobj, p_); |
402 Pbl(*Frm,Pbl*)) = (ppobj, p_); |
403 val (_, _, met_id) = References.select_input o_spec spec |
403 val (_, _, met_id) = References.select_input o_spec spec |
404 val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id) |
404 val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to probl) (Pos.Met, met_id) |
405 |
405 |
406 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to_POS probl, |
406 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to probl, |
407 (*where_*)[(*Problem.from_store in check*)], spec) |
407 (*where_*)[(*Problem.from_store in check*)], spec) |
408 |
408 |
409 (*|------------------- continue with TESTg_form ----------------------------------------------*) |
409 (*|------------------- continue with TESTg_form ----------------------------------------------*) |
410 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) = |
410 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) = |
411 (*case*) form (*of*); |
411 (*case*) form (*of*); |