1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Sun Aug 27 16:09:04 2023 +0200
1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Sun Aug 27 16:48:03 2023 +0200
1.3 @@ -70,9 +70,9 @@
1.4 (*if*) pI = Problem.id_empty (*else*);
1.5 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
1.6 val (_, where_) =
1.7 - Pre_Conds.check_OLD ctxt where_rls where_
1.8 + Pre_Conds.check ctxt where_rls where_
1.9 (model, I_Model.OLD_to_TEST probl);
1.10 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.11 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.12 (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
1.13 val (_, _, (env_subst, env_eval)) =
1.14 of_max_variant model_patt i_model;
1.15 @@ -156,12 +156,12 @@
1.16 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
1.17 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
1.18 (*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\*)
1.19 -(*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
1.20 +(*\\------------------ adhoc inserted fun check ----------------------------------------//*)
1.21
1.22 val return_check_OLD =
1.23 - check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.24 -(*//////-------------- step into check_OLD -------------------------------------------------\\*)
1.25 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.26 + check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.27 +(*//////-------------- step into check -------------------------------------------------\\*)
1.28 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.29 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
1.30 val return_of_max_variant =
1.31 of_max_variant model_patt i_model;
1.32 @@ -181,7 +181,7 @@
1.33 |> distinct op =
1.34 val variants_separated = map (filter_variants' i_model) all_variants
1.35 val sums_corr = map (cnt_corrects) variants_separated
1.36 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
1.37 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
1.38 (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
1.39 val (_, max_variant) = hd (*..crude decision, up to improvement *)
1.40 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
1.41 @@ -246,8 +246,8 @@
1.42 ( *nth 2 equal_descr_pairs*)
1.43 (*+*)val [] = return_discern_typ;
1.44 (**)
1.45 - switch_type_TEST id ts;
1.46 -"~~~~~ fun switch_type_TEST , args:"; val (Const (descr_string, _), ts) = (descr, ts);
1.47 + switch_type id ts;
1.48 +"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
1.49
1.50 (*nth 1 equal_descr_pairs* )
1.51 val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
1.52 @@ -267,14 +267,14 @@
1.53 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
1.54 val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
1.55 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
1.56 -(*||||||-------------- contine check_OLD -----------------------------------------------------*)
1.57 +(*||||||-------------- contine check -----------------------------------------------------*)
1.58 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.59 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
1.60 val full_subst = if env_eval = [] then pres_subst_other
1.61 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
1.62 val evals = map (eval ctxt where_rls) full_subst
1.63 val return_ = (i_model_max, env_subst, env_eval)
1.64 -(*\\\\\\\------------- step into check_OLD -------------------------------------------------//*)
1.65 +(*\\\\\\\------------- step into check -------------------------------------------------//*)
1.66 val (preok, _) = return_check_OLD;
1.67
1.68 (*|||||--------------- contine for_problem ---------------------------------------------------*)
1.69 @@ -435,7 +435,7 @@
1.70 (* else *)
1.71 (* let *)
1.72 val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
1.73 - val (_, where_) = (*Pre_Conds.*)check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
1.74 + val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
1.75 (* in where_ end *)
1.76 val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
1.77 val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
1.78 @@ -489,7 +489,7 @@
1.79 (*//------------------ step into Step.by_tactic --------------------------------------------\\*)
1.80 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.81 val Applicable.Yes tac' =
1.82 - (*case*) check tac (pt, p) (*of*);
1.83 + (*case*) Specify_Step.check tac (pt, p) (*of*);
1.84 (*if*) Tactic.for_specify' tac' (*then*);
1.85 Step_Specify.by_tactic tac' ptp;
1.86 "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
1.87 @@ -559,8 +559,8 @@
1.88 val {model = mpc, ...} = MethodC.from_store ctxt cmI
1.89
1.90 val (preok, _) =
1.91 -Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.92 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.93 +Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.94 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.95 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
1.96
1.97 val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
1.98 @@ -571,7 +571,7 @@
1.99 |> distinct op =
1.100 val variants_separated = map (filter_variants' i_model) all_variants
1.101 val sums_corr = map (cnt_corrects) variants_separated
1.102 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
1.103 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
1.104 val (_, max_variant) = hd (*..crude decision, up to improvement *)
1.105 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
1.106 val i_model_max =
1.107 @@ -652,9 +652,9 @@
1.108 Free ("fixes", _)] = where_
1.109
1.110 val (preok, _) =
1.111 - Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.112 -(*///----------------- step into check_OLD -------------------------------------------------\\*)
1.113 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.114 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
1.115 +(*///----------------- step into check -------------------------------------------------\\*)
1.116 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
1.117 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
1.118 (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
1.119 (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
1.120 @@ -673,10 +673,10 @@
1.121 (*+*)val Type ("Real.real", []) = T2
1.122
1.123 val (_, _, (env_subst, env_eval)) = return_of_max_variant;
1.124 -(*|||----------------- contine check_OLD -----------------------------------------------------*)
1.125 +(*|||----------------- contine check -----------------------------------------------------*)
1.126 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.127
1.128 -(*|||----------------- contine check_OLD -----------------------------------------------------*)
1.129 +(*|||----------------- contine check -----------------------------------------------------*)
1.130 (*+*)val [(true, Const ("Orderings.ord_class.less", _) $
1.131 Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
1.132
1.133 @@ -687,7 +687,7 @@
1.134
1.135 val evals = map (eval ctxt where_rls) full_subst
1.136 val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
1.137 -(*\\\----------------- step into check_OLD -------------------------------------------------\\*)
1.138 +(*\\\----------------- step into check -------------------------------------------------\\*)
1.139
1.140 val (preok as true, _) = return_check_OLD
1.141 (*+---------------^^^^*)
1.142 @@ -708,7 +708,7 @@
1.143 Step.by_tactic tac (pt, p);
1.144 (*//------------------ step into Step_by_tactic --------------------------------------------\\*)
1.145 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.146 - (*case*) check tac (pt, p) (*of*);
1.147 + (*case*) Specify_Step.check tac (pt, p) (*of*);
1.148
1.149 (*||------------------ contine Step_by_tactic ------------------------------------------------*)
1.150 (*\\------------------ step into Step_by_tactic --------------------------------------------//*)
1.151 @@ -857,7 +857,7 @@
1.152 = (ctxt, oris, (o_refs, refs), (pbl, met));
1.153 val cmI = if mI = MethodC.id_empty then mI' else mI;
1.154 val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
1.155 - val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
1.156 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
1.157 val NONE =
1.158 (*case*) find_first (I_Model.is_error o #5) met (*of*);
1.159