1.1 --- a/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml Fri Dec 01 05:51:18 2023 +0100
1.2 +++ b/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml Fri Dec 01 06:08:22 2023 +0100
1.3 @@ -73,9 +73,9 @@
1.4 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
1.5 val (_, where_) =
1.6 Pre_Conds.check ctxt where_rls where_
1.7 - (model, I_Model.OLD_to_TEST probl);
1.8 + (model, I_Model.OLD_to_POS probl);
1.9 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.10 - (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
1.11 + (ctxt, where_rls, where_, (model, I_Model.OLD_to_POS probl));
1.12 val (env_model, (env_subst, env_eval)) =
1.13 make_environments model_patt i_model;
1.14 "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
1.15 @@ -111,7 +111,7 @@
1.16 Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
1.17 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
1.18 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
1.19 - val pbl = I_Model.init_TEST ctxt o_model model_patt
1.20 + val pbl = I_Model.init_POS ctxt o_model model_patt
1.21
1.22 val return_check =
1.23 Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
1.24 @@ -150,7 +150,7 @@
1.25 (*if*) p_ = Pos.Pbl (*then*);
1.26
1.27 val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) =
1.28 - Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met);
1.29 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_POS met);
1.30 (*/////--------------- step into for_problem -----------------------------------------------\\*)
1.31 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
1.32 = (ctxt, oris, (o_refs, refs), (pbl, met));
1.33 @@ -161,18 +161,18 @@
1.34 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
1.35
1.36 val return_check =
1.37 - Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.38 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_POS pbl);
1.39 (*//////-------------- step into check -------------------------------------------------\\*)
1.40 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.41 - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
1.42 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_POS pbl));
1.43 val return_make_environments =
1.44 make_environments model_patt i_model;
1.45 (*///// //------------ step into of_max_variant --------------------------------------------\\*)
1.46 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
1.47 (model_patt, i_model);
1.48
1.49 -(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
1.50 - = i_model |> I_Model.to_string_TEST ctxt
1.51 +(*+*)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))]"
1.52 + = i_model |> I_Model.to_string_POS ctxt
1.53 val all_variants =
1.54 map (fn (_, variants, _, _, _) => variants) i_model
1.55 |> flat
1.56 @@ -192,7 +192,7 @@
1.57 (*!!!*) val patt = equal_descr_pairs |> hd |> #1
1.58 (*!!!*)val equal_descr_pairs =
1.59 (patt,
1.60 - (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term)), pos)))
1.61 + (1, [1, 2, 3], true, "#Given", (Cor_POS ((descr, (*!*)TermC.isalist2list(*!*) term)), pos)))
1.62 :: tl equal_descr_pairs
1.63 (*for building make_env_s -------------------------------------------------------------------/*)
1.64
1.65 @@ -214,13 +214,13 @@
1.66 "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
1.67 val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
1.68 ;
1.69 -xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;
1.70 +xxx: (Model_Pattern.single * I_Model.single_POS) -> ((term * term) * (term * term)) list;
1.71 val return_discern_feedback =
1.72 discern_feedback id feedb;
1.73 (*nth 1 equal_descr_pairs* )
1.74 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
1.75 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_POS ((descr, ts), _))) = (id, feedb);
1.76 ( *nth 2 equal_descr_pairs*)
1.77 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts)))) = (id, feedb);
1.78 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_POS ((descr, ts)))) = (id, feedb);
1.79
1.80 (*nth 1 equal_descr_pairs* )
1.81 (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
1.82 @@ -247,12 +247,12 @@
1.83 "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
1.84
1.85 (*nth 1 equal_descr_pairs* )
1.86 -val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
1.87 +val return_switch_type_POS = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
1.88
1.89 -(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST
1.90 +(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_POS
1.91 (*+*)val Type ("Real.real", []) = typ
1.92 ( *nth 2 equal_descr_pairs*)
1.93 -(*+*)val return_switch_type_TEST = descr
1.94 +(*+*)val return_switch_type_POS = descr
1.95 (**)
1.96 (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
1.97 (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
1.98 @@ -284,7 +284,7 @@
1.99
1.100 (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **)
1.101 (**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*)
1.102 - Specify.item_to_add ctxt oris (I_Model.OLD_to_TEST pbl) (*of*);
1.103 + Specify.item_to_add ctxt oris (I_Model.OLD_to_POS pbl) (*of*);
1.104 (*///// /------------- step into item_to_add -----------------------------------------------\\*)
1.105 (*==================== see test/../i_model.sml --- fun item_to_add ---========================*)
1.106 (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*)
1.107 @@ -399,7 +399,7 @@
1.108 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}),
1.109 Pbl(*Frm,Pbl*)) = (ppobj, p_);
1.110 val (_, _, met_id) = References.select_input o_spec spec
1.111 - val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id)
1.112 + val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id)
1.113 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
1.114
1.115 (*|------------------- continue with TESTg_form ----------------------------------------------*)