diff -r 344eee0d80f7 -r e797d1bdfe37 test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml --- a/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml Mon Dec 11 16:18:42 2023 +0100 +++ b/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml Mon Dec 11 17:26:30 2023 +0100 @@ -73,9 +73,9 @@ val {where_rls, where_, model, ...} = Problem.from_store ctxt pI val (_, where_) = Pre_Conds.check ctxt where_rls where_ - (model, I_Model.OLD_to_POS probl); + (model, I_Model.OLD_to probl); "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = - (ctxt, where_rls, where_, (model, I_Model.OLD_to_POS probl)); + (ctxt, where_rls, where_, (model, I_Model.OLD_to probl)); val (env_model, (env_subst, env_eval)) = make_environments model_patt i_model; "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model); @@ -111,7 +111,7 @@ Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI') | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj" val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' - val pbl = I_Model.init_POS ctxt o_model model_patt + val pbl = I_Model.init ctxt o_model model_patt val return_check = Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])); @@ -150,7 +150,7 @@ (*if*) p_ = Pos.Pbl (*then*); val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) = - Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_POS met); + Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to met); (*/////--------------- step into for_problem -----------------------------------------------\\*) "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = (ctxt, oris, (o_refs, refs), (pbl, met)); @@ -161,18 +161,18 @@ val {model = mpc, ...} = MethodC.from_store ctxt cmI; val return_check = - Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_POS pbl); + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to pbl); (*//////-------------- step into check -------------------------------------------------\\*) "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_POS pbl)); + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to pbl)); val return_make_environments = make_environments model_patt i_model; (*///// //------------ step into of_max_variant --------------------------------------------\\*) "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model); -(*+*)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))]" - = i_model |> I_Model.to_string_POS ctxt +(*+*)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))]" + = i_model |> I_Model.to_string ctxt val all_variants = map (fn (_, variants, _, _, _) => variants) i_model |> flat @@ -192,7 +192,7 @@ (*!!!*) val patt = equal_descr_pairs |> hd |> #1 (*!!!*)val equal_descr_pairs = (patt, - (1, [1, 2, 3], true, "#Given", (Cor_POS ((descr, (*!*)TermC.isalist2list(*!*) term)), pos))) + (1, [1, 2, 3], true, "#Given", (Cor ((descr, (*!*)TermC.isalist2list(*!*) term)), pos))) :: tl equal_descr_pairs (*for building make_env_s -------------------------------------------------------------------/*) @@ -214,13 +214,13 @@ "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens); val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) ; -xxx: (Model_Pattern.single * I_Model.single_POS) -> ((term * term) * (term * term)) list; +xxx: (Model_Pattern.single * I_Model.single) -> ((term * term) * (term * term)) list; val return_discern_feedback = discern_feedback id feedb; (*nth 1 equal_descr_pairs* ) -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_POS ((descr, ts), _))) = (id, feedb); +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor ((descr, ts), _))) = (id, feedb); ( *nth 2 equal_descr_pairs*) -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_POS ((descr, ts)))) = (id, feedb); +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc ((descr, ts)))) = (id, feedb); (*nth 1 equal_descr_pairs* ) (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), @@ -247,12 +247,12 @@ "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts); (*nth 1 equal_descr_pairs* ) -val return_switch_type_POS = Const (descr_string, ts |> hd |> TermC.lhs |> type_of) +val return_switch_type = Const (descr_string, ts |> hd |> TermC.lhs |> type_of) -(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_POS +(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type (*+*)val Type ("Real.real", []) = typ ( *nth 2 equal_descr_pairs*) -(*+*)val return_switch_type_POS = descr +(*+*)val return_switch_type = descr (**) (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*) (*||||| ||------------ contine of_max_variant ------------------------------------------------*) @@ -284,7 +284,7 @@ (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **) (**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*) - Specify.item_to_add ctxt oris (I_Model.OLD_to_POS pbl) (*of*); + Specify.item_to_add ctxt oris (I_Model.OLD_to pbl) (*of*); (*///// /------------- step into item_to_add -----------------------------------------------\\*) (*==================== see test/../i_model.sml --- fun item_to_add ---========================*) (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*) @@ -363,7 +363,7 @@ (*case*) find_first (fn (_, (d', _)) => d = d') pbt val SOME (_, _, _, _, (feedb, _)) = (*case*) find_first (fn (_, _, _, f', (feedb, _)) => - f = f' andalso d = (descriptor_POS feedb)) itms + f = f' andalso d = (descriptor feedb)) itms val ts' = inter op = (feedb_values feedb) ts val false = (*if*) subset op = (ts, ts') @@ -376,7 +376,7 @@ val pval = [Input_Descript.join'''' (d, ts')] val complete = if eq_set op = (ts', all) then true else false -(*+*)val "Inc_POS Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_POS_to_string ctxt +(*+*)val "Inc Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_to_string ctxt (*\\\----------------- step into specify_do_next -------------------------------------------//*) (*\\------------------ step into do_next ---------------------------------------------------//*) val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next @@ -401,9 +401,9 @@ "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), Pbl(*Frm,Pbl*)) = (ppobj, p_); val (_, _, met_id) = References.select_input o_spec spec - val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id) + val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to probl) (Pos.Met, met_id) -val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to_POS probl, +val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to probl, (*where_*)[(*Problem.from_store in check*)], spec) (*|------------------- continue with TESTg_form ----------------------------------------------*)