1.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Sep 20 11:30:50 2023 +0200
1.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Sep 20 16:51:08 2023 +0200
1.3 @@ -56,27 +56,30 @@
1.4 -> message * single
1.5 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
1.6
1.7 +(*TODO: replace in pre-conditions.m, see fun max_variants + make_envs_preconds,
1.8 + see (** complete I_Model.T **) *)
1.9 val of_max_variant: Model_Pattern.T -> T_TEST ->
1.10 (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
1.11
1.12 -(*REN make_complete*)
1.13 + val add: single -> T -> T
1.14 + val s_make_complete: O_Model.T -> T_TEST * T_TEST -> Model_Pattern.T * Model_Pattern.T ->
1.15 + T_TEST * T_TEST
1.16 +(*^^^--- s_make_complete SHALL REPLACE ALL THESE ---vvv*)
1.17 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
1.18 - val add: single -> T -> T
1.19 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
1.20 -
1.21 -
1.22 + val complete': Model_Pattern.T -> O_Model.single -> single
1.23 + val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
1.24
1.25 val is_error: feedback -> bool
1.26 -(*REN complete_internal*)
1.27 - val complete': Model_Pattern.T -> O_Model.single -> single
1.28 -
1.29 - val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
1.30
1.31 val is_complete: T -> bool
1.32 val is_complete_variant: Model_Def.variant -> T_TEST-> bool
1.33 val to_p_model: theory -> feedback -> string
1.34
1.35 (*from isac_test for Minisubpbl*)
1.36 + val msg: variants -> feedback_TEST -> string
1.37 + val transfer_terms: O_Model.single -> single_TEST
1.38 +
1.39 val eq1: ''a -> 'b * (''a * 'c) -> bool
1.40 val filter_outs: O_Model.T -> T -> O_Model.T
1.41 val filter_outs_TEST: O_Model.T -> T_TEST -> O_Model.T
1.42 @@ -413,13 +416,10 @@
1.43 (** complete I_Model.T **)
1.44
1.45 (*
1.46 - Survey on completion of i-models. There are 2 cases:
1.47 - (1) the most general case covering allmost all others:
1.48 - I_Model.s_complete: transfer ideas from fill_method
1.49 - (2) case for refinement
1.50 - TODO: check old code
1.51 + Survey on completion of i-models.
1.52 + one most general version, , shall replace all old versions
1.53
1.54 - Divide functionality of I_Model.of_max_variant into parts in ordeer for re-use in is_complete
1.55 + Divide functionality of I_Model.of_max_variant into parts in order for re-use in is_complete
1.56 I_Model.max_variants
1.57 return variant list, because Problem#model might be insufficient to determine
1.58 variant of MethodC.#model (FunctionVariable a ! b)
1.59 @@ -560,4 +560,33 @@
1.60
1.61 val of_max_variant = Pre_Conds.of_max_variant
1.62
1.63 +fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
1.64 + let
1.65 + val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
1.66 + val i_from_pbl = map (fn (_, (descr, _)) =>
1.67 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
1.68 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.69 + if is_empty_single_TEST i_single
1.70 + then
1.71 + case Pre_Conds.get_descr_vnt' feedb pbl_max_vnts o_model of
1.72 + [] => raise ERROR (msg pbl_max_vnts feedb)
1.73 + | o_singles => map transfer_terms o_singles
1.74 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
1.75 +
1.76 + val i_from_met = map (fn (_, (descr, _)) =>
1.77 + (Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod)) met_patt
1.78 + val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
1.79 + val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
1.80 +
1.81 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
1.82 + if is_empty_single_TEST i_single
1.83 + then
1.84 + case Pre_Conds.get_descr_vnt' feedb [met_max_vnt] o_model of
1.85 + [] => raise ERROR (msg [met_max_vnt] feedb)
1.86 + | o_singles => map transfer_terms o_singles
1.87 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
1.88 + in
1.89 + (pbl_from_o_model, met_from_pbl)
1.90 + end
1.91 +
1.92 (**)end(**);
2.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 11:30:50 2023 +0200
2.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 16:51:08 2023 +0200
2.3 @@ -21,6 +21,8 @@
2.4 val max_variant: Model_Def.i_model -> Model_Def.variant
2.5 val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
2.6
2.7 +(*TODO: replace in pre-conditions.m, see fun max_variants + make_envs_preconds,
2.8 + see i-model.sml (** complete I_Model.T **) *)
2.9 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
2.10 (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
2.11 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
3.1 --- a/test/Tools/isac/Specify/i-model.sml Wed Sep 20 11:30:50 2023 +0200
3.2 +++ b/test/Tools/isac/Specify/i-model.sml Wed Sep 20 16:51:08 2023 +0200
3.3 @@ -10,6 +10,7 @@
3.4 "----------- build I_Model.init_TEST -----------------------------------------------------------";
3.5 "----------- exercise preparing I_Model.is_complete --------------------------------------------";
3.6 "----------- build I_Model.is_complete_OLD -----------------------------------------------------";
3.7 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
3.8 "-----------------------------------------------------------------------------------------------";
3.9 "-----------------------------------------------------------------------------------------------";
3.10 "-----------------------------------------------------------------------------------------------";
3.11 @@ -288,3 +289,163 @@
3.12 (*/------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------\*)
3.13 (*\------------------- test on OLD algorithm (with I_Model.T_TEST) --------------------------/*)
3.14 ( *\----- reactivate with CS "remove sep_variants_envs"-----/*)
3.15 +
3.16 +
3.17 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
3.18 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
3.19 +"----------- build I_Model.s_make_complete -----------------------------------------------------";
3.20 +val (_(*example text*),
3.21 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
3.22 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
3.23 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
3.24 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
3.25 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
3.26 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
3.27 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
3.28 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
3.29 + "ErrorBound (\<epsilon> = (0::real))" :: []),
3.30 + refs as ("Diff_App",
3.31 + ["univariate_calculus", "Optimisation"],
3.32 + ["Optimisation", "by_univariate_calculus"])))
3.33 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
3.34 +
3.35 +val c = [];
3.36 +val (p,_,f,nxt,_,pt) =
3.37 + Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
3.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.39 +
3.40 +(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
3.41 +val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
3.42 + PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
3.43 + => (o_model, (pbl_imod, met_imod), (pI, mI))
3.44 + | _ => raise ERROR ""
3.45 +
3.46 +val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
3.47 +val {model = met_patt, ...} = MethodC.from_store ctxt mI;
3.48 +
3.49 +val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
3.50 + (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
3.51 + [@{term "[r = (7::real)]"}]), Position.none)),
3.52 + (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
3.53 + [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
3.54 +
3.55 +val met_imod = [ (*1 item for creating code*)
3.56 +(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
3.57 +;
3.58 +(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
3.59 +(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
3.60 +(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
3.61 +(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
3.62 +(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
3.63 +(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
3.64 +(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
3.65 +(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
3.66 +(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
3.67 +(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
3.68 +(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
3.69 +(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
3.70 +(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
3.71 +then () else error "setup test data for I_Model.s_make_complete CHANGED";
3.72 +(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
3.73 +
3.74 +val return_s_make_complete =
3.75 + s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
3.76 +(*/------------------- step into s_make_complete -------------------------------------------\\*)
3.77 +"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
3.78 + (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
3.79 + val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
3.80 + val i_from_pbl = map (fn (_, (descr, _)) =>
3.81 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
3.82 +
3.83 +(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
3.84 +"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
3.85 + (@{term Constants}, pbl_max_vnts, pbl_imod);
3.86 + val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
3.87 + | SOME descr' => if descr = descr' then true else false) i_model
3.88 +;
3.89 +(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr: I_Model.T_TEST
3.90 +;
3.91 +val return_get_descr_vnt_1 =
3.92 + case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
3.93 + [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
3.94 + | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
3.95 +(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
3.96 +
3.97 +(*|------------------- continue s_make_complete ----------------------------------------------*)
3.98 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
3.99 + if is_empty_single_TEST i_single
3.100 + then
3.101 + case get_descr_vnt' feedb pbl_max_vnts o_model of
3.102 +(*-----------^^^^^^^^^^^^^^-----------------------------*)
3.103 + [] => raise ERROR (msg pbl_max_vnts feedb)
3.104 + | o_singles => map transfer_terms o_singles
3.105 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
3.106 +
3.107 +(*+*)val [2, 1] = vnts;
3.108 +(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
3.109 + "(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
3.110 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
3.111 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
3.112 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
3.113 + "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
3.114 +then () else error "pbl_from_o_model CHANGED"
3.115 +
3.116 +(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
3.117 +"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
3.118 + (*if*) is_empty_single_TEST i_single (*else*);
3.119 + get_descr_vnt' feedb pbl_max_vnts o_model;
3.120 +
3.121 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
3.122 + if is_empty_single_TEST i_single
3.123 + then
3.124 + case get_descr_vnt' feedb pbl_max_vnts o_model of
3.125 +(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
3.126 + [] => raise ERROR (msg pbl_max_vnts feedb)
3.127 + | o_singles => map transfer_terms o_singles
3.128 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
3.129 +(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
3.130 +
3.131 +(*|------------------- continue s_make_complete ----------------------------------------------*)
3.132 + val i_from_met = map (fn (_, (descr, _)) =>
3.133 + (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt
3.134 +;
3.135 +(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
3.136 + "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
3.137 + "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
3.138 + "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
3.139 + "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
3.140 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
3.141 +(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
3.142 + "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
3.143 + "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
3.144 + "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
3.145 +(*+*)then () else error "s_make_complete: from_met CHANGED";
3.146 +;
3.147 + val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
3.148 +(*+*)val [2] = met_max_vnts
3.149 +
3.150 + val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
3.151 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
3.152 + if is_empty_single_TEST i_single
3.153 + then
3.154 + case get_descr_vnt' feedb [met_max_vnt] o_model of
3.155 + [] => raise ERROR (msg [met_max_vnt] feedb)
3.156 + | o_singles => map transfer_terms o_singles
3.157 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
3.158 +;
3.159 +(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
3.160 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
3.161 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
3.162 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
3.163 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
3.164 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
3.165 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
3.166 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
3.167 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
3.168 +(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
3.169 +;
3.170 +val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
3.171 +(*\------------------- step into s_make_complete -------------------------------------------//*)
3.172 +;
3.173 +if return_s_make_complete = return_s_make_complete_step
3.174 +then () else error "s_make_complete: stewise construction <> value of fun"
4.1 --- a/test/Tools/isac/Test_Theory.thy Wed Sep 20 11:30:50 2023 +0200
4.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Sep 20 16:51:08 2023 +0200
4.3 @@ -18,6 +18,9 @@
4.4 declare [[ML_print_depth = 999]]
4.5 declare [[ML_exception_trace]]
4.6 \<close>
4.7 +(** )
4.8 + (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
4.9 +( **)
4.10 ML \<open>
4.11 \<close> ML \<open>
4.12 "~~~~~ fun xxx , args:"; val () = ();
4.13 @@ -32,6 +35,11 @@
4.14 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
4.15 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
4.16
4.17 +\<close> ML \<open> (*//----------- setup test data for XXXXX -------------------------------------------\\*)
4.18 +(*//------------------ setup test data for XXXXX -------------------------------------------\\*)
4.19 +(*\\------------------ setup test data for XXXXX -------------------------------------------//*)
4.20 +\<close> ML \<open> (*\\----------- setup test data for XXXXX -------------------------------------------//*)
4.21 +
4.22 val return_XXXXX = "XXXXX"
4.23 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
4.24 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
4.25 @@ -66,9 +74,26 @@
4.26 (*T_TEST*)
4.27 (*T_TESTnew*)
4.28
4.29 +(**)
4.30 +open Ctree
4.31 +open Pos;
4.32 +open TermC;
4.33 +open Istate;
4.34 +open Tactic;
4.35 +open P_Model
4.36 +open Rewrite;
4.37 +open Step;
4.38 +open LItool;
4.39 +open LI;
4.40 +open Test_Code
4.41 +open Specify
4.42 +(**)
4.43 open Model_Def
4.44 +(**)
4.45 open Pre_Conds
4.46 -(**)open I_Model(**)
4.47 +(**)
4.48 +open I_Model
4.49 +(**)
4.50 \<close> ML \<open>
4.51 \<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*)
4.52 fun max_variants i_model =
4.53 @@ -86,7 +111,7 @@
4.54 |> map snd
4.55 val option_sequence = map
4.56 (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
4.57 -(*das ist UNSINN .., siehe (*+*)if (pbl_max_imos*)
4.58 +(*das ist UNSINN'+ UNNOETIG WEGLASSEN, .., siehe (*+*)if (pbl_max_imos*)
4.59 val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
4.60 if is_some pos_in_sum_variant_s then i_model else [])
4.61 (option_sequence ~~ variants_separated)
4.62 @@ -118,13 +143,14 @@
4.63 ( *\--fun make_envs_preconds: 1 max_i_model can be determined only together with meth --------/ *)
4.64 end
4.65 ;
4.66 -max_variants: Model_Def.i_model_TEST ->
4.67 +(*of_max_variant*)
4.68 + max_variants: (*Model_Pattern.T -> *) Model_Def.i_model_TEST ->
4.69 (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*)
4.70 \<close> ML \<open>
4.71 \<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*)
4.72 \<close> ML \<open>
4.73 -fun get_dscr' (Cor_TEST ((descr, _), _)) = SOME descr
4.74 - | get_dscr' (Inc_TEST ((descr, _), _)) = SOME descr
4.75 +fun get_dscr' (Cor_TEST (descr, _)) = SOME descr
4.76 + | get_dscr' (Inc_TEST (descr, _)) = SOME descr
4.77 | get_dscr' (Sup_TEST (descr, _)) = SOME descr
4.78 | get_dscr' _ = NONE
4.79 (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)
4.80 @@ -134,39 +160,41 @@
4.81 \<close> ML \<open>
4.82 fun get_descr (_, _, _, _, (feedb, _)) =
4.83 case get_dscr' feedb of NONE => NONE | some_descr => some_descr
4.84 -(* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single ->
4.85 - (Model_Pattern.single * I_Model.single_TEST) list*)
4.86 -\<close> ML \<open>
4.87 +;
4.88 get_descr: single_TEST -> descriptor option;
4.89
4.90 \<close> ML \<open>
4.91 -(*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*)
4.92 fun get_descr_vnt descr vnts i_model =
4.93 let
4.94 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
4.95 | SOME descr' => if descr = descr' then true else false) i_model
4.96 in
4.97 - case find_first (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
4.98 - SOME item => item
4.99 - | NONE => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
4.100 + case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
4.101 + [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
4.102 + | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
4.103 end
4.104 ;
4.105 get_descr_vnt: descriptor -> variants -> T_TEST -> single_TEST
4.106 \<close> ML \<open>
4.107 \<close> ML \<open> (*\<longrightarrow> i-model.sml*)
4.108 \<close> ML \<open>
4.109 -(*
4.110 +fun transfer_terms (i, vnts, m_field, descr, ts) =
4.111 + (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
4.112 +;
4.113 +transfer_terms: O_Model.single -> I_Model.single_TEST
4.114 +\<close> ML \<open>
4.115 +(*
4.116 get an appropriate (description, variant) item from o_model;
4.117 called in case of item in met_imod is_empty_single_TEST
4.118 (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
4.119 *)
4.120 fun get_descr_vnt' feedb vnts o_model =
4.121 -find_first (fn (_, vnts', _, descr', _) =>
4.122 + filter (fn (_, vnts', _, descr', _) =>
4.123 case get_dscr' feedb of
4.124 SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
4.125 | NONE => false) o_model
4.126 ;
4.127 -get_descr_vnt': feedback_TEST -> variants -> O_Model.T -> O_Model.single option
4.128 +get_descr_vnt': feedback_TEST -> variants -> O_Model.T -> O_Model.T
4.129 \<close> ML \<open>
4.130 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
4.131 "variants " ^ ints2str' vnts ^ " and descriptor " ^
4.132 @@ -182,15 +210,52 @@
4.133 if is_empty_single_TEST i_single
4.134 then
4.135 case get_descr_vnt' feedb pbl_max_vnts o_model of
4.136 - NONE => raise ERROR (msg pbl_max_vnts feedb)
4.137 - | SOME (i, vnts, m_field, descr, ts) =>
4.138 - (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
4.139 - else i_single (*fetched before from pbl_imod*))) from_pbl
4.140 + [] => raise ERROR (msg pbl_max_vnts feedb)
4.141 + | o_singles => map transfer_terms o_singles
4.142 + else [i_single (*fetched before from pbl_imod*)])) from_pbl
4.143 in
4.144 - from_o_model
4.145 + from_o_model |> flat
4.146 end
4.147 ;
4.148 -fill_method: O_Model.T -> I_Model.T_TEST -> Model_Pattern.T -> I_Model.T_TEST
4.149 +fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
4.150 +\<close> ML \<open>
4.151 +\<close> ML \<open>
4.152 +\<close> ML \<open> (* \<longrightarrow> i-model.sml*)
4.153 +\<close> ML \<open>
4.154 +fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
4.155 + let
4.156 + val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
4.157 + val i_from_pbl = map (fn (_, (descr, _)) =>
4.158 + (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
4.159 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
4.160 + if is_empty_single_TEST i_single
4.161 + then
4.162 + case get_descr_vnt' feedb pbl_max_vnts o_model of
4.163 + [] => raise ERROR (msg pbl_max_vnts feedb)
4.164 + | o_singles => map transfer_terms o_singles
4.165 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
4.166 +
4.167 + val i_from_met = map (fn (_, (descr, _)) =>
4.168 + (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt
4.169 + val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
4.170 + val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
4.171 +
4.172 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
4.173 + if is_empty_single_TEST i_single
4.174 + then
4.175 + case get_descr_vnt' feedb [met_max_vnt] o_model of
4.176 + [] => raise ERROR (msg [met_max_vnt] feedb)
4.177 + | o_singles => map transfer_terms o_singles
4.178 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
4.179 + in
4.180 + (pbl_from_o_model, met_from_pbl)
4.181 + end
4.182 +\<close> ML \<open>
4.183 +;
4.184 +s_make_complete: O_Model.T -> I_Model.T_TEST * I_Model.T_TEST -> Model_Pattern.T * Model_Pattern.T ->
4.185 + I_Model.T_TEST * I_Model.T_TEST
4.186 +\<close> ML \<open>
4.187 +\<close> ML \<open>
4.188 \<close> ML \<open>
4.189 \<close> ML \<open> (*\<longrightarrow> lucas-interpreter.sml*)
4.190 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
4.191 @@ -204,32 +269,18 @@
4.192 \<close> ML \<open>
4.193 \<close>
4.194
4.195 -(** )ML_file "Minisubpbl/150a-add-given-Maximum.sml" ( ** )check file with test under repair below( **)
4.196 section \<open>===================================================================================\<close>
4.197 -section \<open>===== Minisubpbl/150a-add-given-Maximum.sml ======================================\<close>
4.198 +section \<open>===== i-model.sml .s_complete =====================================================\<close>
4.199 ML \<open>
4.200 \<close> ML \<open>
4.201 -(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
4.202 - Author: Walther Neuper 1105
4.203 - (c) copyright due to lincense terms.
4.204 -
4.205 -COMPARE Specify/specify.sml --- specify-phase: low level functions ---
4.206 -
4.207 -ATTENTION: the file creates buffer overflow if copied in one piece !
4.208 -
4.209 -Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
4.210 - in order not to get lost while working in Test_Some etc,
4.211 - re-introduce ML (*--- step into XXXXX ---*) and Co.
4.212 - and use Sidekick for orientation.
4.213 - Nesting is indicated by /--- //-- ///- at the left margin of the comments.
4.214 -*)
4.215 -
4.216 -open Ctree;
4.217 +(* most general case: user activates some <complete specification> *)
4.218 +\<close> ML \<open>
4.219 +(*---vvvvv these would overwrite above definition ^^^* )
4.220 +open Ctree
4.221 open Pos;
4.222 open TermC;
4.223 open Istate;
4.224 open Tactic;
4.225 -open I_Model;
4.226 open P_Model
4.227 open Rewrite;
4.228 open Step;
4.229 @@ -237,8 +288,10 @@
4.230 open LI;
4.231 open Test_Code
4.232 open Specify
4.233 -open ME_Misc
4.234 +open Model_Def
4.235 open Pre_Conds;
4.236 +open I_Model;
4.237 +( **)
4.238
4.239 val (_(*example text*),
4.240 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
4.241 @@ -256,1159 +309,163 @@
4.242 = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
4.243
4.244 val c = [];
4.245 -val return_init_calc =
4.246 - Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
4.247 -(*/------------------- step into init_calc -------------------------------------------------\\*)
4.248 -"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
4.249 - (@{context}, [(model, refs)]);
4.250 - val thy = thy_id |> ThyC.get_theory ctxt
4.251 - val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
4.252 - val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
4.253 - val f =
4.254 - TESTg_form ctxt (pt,p);
4.255 -"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
4.256 - val (form, _, _) =
4.257 - ME_Misc.pt_extract ctxt ptp;
4.258 -"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
4.259 - val ppobj = Ctree.get_obj I pt p
4.260 - val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
4.261 - (*if*) Ctree.is_pblobj ppobj (*then*);
4.262 - pt_model ppobj p_ ;
4.263 -"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
4.264 - (ppobj, p_);
4.265 - val (_, pI, _) = Ctree.get_somespec' spec spec';
4.266 -(* val where_ = if pI = Problem.id_empty then []*)
4.267 - (*if*) pI = Problem.id_empty (*else*);
4.268 - val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
4.269 - val (_, where_) =
4.270 - Pre_Conds.check ctxt where_rls where_
4.271 - (model, I_Model.OLD_to_TEST probl);
4.272 -"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
4.273 - (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
4.274 - val (_, _, (env_subst, env_eval)) =
4.275 - of_max_variant model_patt i_model;
4.276 -"~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);
4.277 -(*\------------------- step into init_calc -------------------------------------------------//*)
4.278 -val (p,_,f,nxt,_,pt) = return_init_calc;
4.279 -
4.280 -(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
4.281 -(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
4.282 -(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
4.283 -(*+*)val [] = probl
4.284 -
4.285 -val return_me_Model_Problem =
4.286 - me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
4.287 -(*/------------------- step into me Model_Problem ------------------------------------------\\*)
4.288 -"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
4.289 - val ctxt = Ctree.get_ctxt pt p
4.290 -val return_by_tactic = case
4.291 - Step.by_tactic tac (pt,p) of
4.292 - ("ok", (_, _, ptp)) => ptp;
4.293 -
4.294 -(*//------------------ step into by_tactic -------------------------------------------------\\*)
4.295 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
4.296 -val Applicable.Yes tac' = (*case*)
4.297 - Step.check tac (pt, p) (*of*);
4.298 -(*+*)val Model_Problem' _ = tac';
4.299 -"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
4.300 - (*if*) Tactic.for_specify tac (*then*);
4.301 -
4.302 -Specify_Step.check tac (ctree, pos);
4.303 -"~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
4.304 - (tac, (ctree, pos));
4.305 - val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of
4.306 - Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)
4.307 - val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
4.308 - val pbl = I_Model.init_TEST o_model model_patt;
4.309 -
4.310 -val return_check =
4.311 - Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
4.312 -(*\\------------------ step into by_tactic -------------------------------------------------//*)
4.313 -val (pt, p) = return_by_tactic;
4.314 -
4.315 -val return_do_next = (*case*)
4.316 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.317 -(*//------------------ step into do_next ---------------------------------------------------\\*)
4.318 -"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
4.319 - (p, ((pt, e_pos'),[]));
4.320 - val pIopt = get_pblID (pt,ip);
4.321 - (*if*) ip = ([],Res); (* = false*)
4.322 - val _ = (*case*) tacis (*of*);
4.323 - val SOME _ = (*case*) pIopt (*of*);
4.324 -
4.325 - val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
4.326 - Step.switch_specify_solve p_ (pt, ip);
4.327 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.328 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.329 -
4.330 - val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
4.331 - Step.specify_do_next (pt, input_pos);
4.332 -(*///----------------- step into specify_do_next -------------------------------------------\\*)
4.333 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
4.334 -
4.335 -(* val (_, (p_', tac)) =*)
4.336 -val return_find_next_step = (*keep for continuing specify_do_next*)
4.337 - Specify.find_next_step ptp;
4.338 -(*////---------------- step into find_next_step --------------------------------------------\\*)
4.339 -"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
4.340 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
4.341 - spec = refs, ...} = Calc.specify_data (pt, pos);
4.342 - val ctxt = Ctree.get_ctxt pt pos;
4.343 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
4.344 - (*if*) p_ = Pos.Pbl (*then*);
4.345 -
4.346 - Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
4.347 -(*/////--------------- step into for_problem -----------------------------------------------\\*)
4.348 -"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
4.349 - = (ctxt, oris, (o_refs, refs), (pbl, met));
4.350 - val cdI = if dI = ThyC.id_empty then dI' else dI;
4.351 - val cpI = if pI = Problem.id_empty then pI' else pI;
4.352 - val cmI = if mI = MethodC.id_empty then mI' else mI;
4.353 - val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
4.354 - val {model = mpc, ...} = MethodC.from_store ctxt cmI;
4.355 -
4.356 - val return_check_OLD =
4.357 - check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
4.358 -(*//////-------------- step into check -------------------------------------------------\\*)
4.359 -"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
4.360 - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
4.361 - val return_of_max_variant =
4.362 - of_max_variant model_patt i_model;
4.363 -(*///// //------------ step into of_max_variant --------------------------------------------\\*)
4.364 -"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
4.365 - (model_patt, i_model);
4.366 -
4.367 -(*+*)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))]"
4.368 - = i_model |> I_Model.to_string_TEST @{context}
4.369 - val all_variants =
4.370 - map (fn (_, variants, _, _, _) => variants) i_model
4.371 - |> flat
4.372 - |> distinct op =
4.373 - val variants_separated = map (filter_variants' i_model) all_variants
4.374 - val sums_corr = map (cnt_corrects) variants_separated
4.375 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
4.376 -(*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
4.377 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
4.378 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
4.379 - val i_model_max =
4.380 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
4.381 - val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
4.382 -(*for building make_env_s -------------------------------------------------------------------\*)
4.383 -(*!!!*) val ("#Given", (descr, term), pos) =
4.384 - Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
4.385 -(*!!!*) val patt = equal_descr_pairs |> hd |> #1
4.386 -(*!!!*)val equal_descr_pairs =
4.387 - (patt,
4.388 - (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term),
4.389 - (TermC.empty, [])), pos)))
4.390 - :: tl equal_descr_pairs
4.391 -(*for building make_env_s -------------------------------------------------------------------/*)
4.392 -
4.393 - val env_model = make_env_model equal_descr_pairs;
4.394 -(*///// ///----------- step into make_env_model --------------------------------------------\\*)
4.395 -"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
4.396 -
4.397 -val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
4.398 - => (mk_env_model id feedb));
4.399 -val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
4.400 -(*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
4.401 -(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
4.402 -
4.403 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
4.404 - val subst_eval_list = make_envs_preconds equal_givens
4.405 -val return_make_envs_preconds =
4.406 - make_envs_preconds equal_givens;
4.407 -(*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
4.408 -"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
4.409 -val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
4.410 -;
4.411 -xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;
4.412 -val return_discern_feedback =
4.413 - discern_feedback id feedb;
4.414 -(*nth 1 equal_descr_pairs* )
4.415 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
4.416 -( *nth 2 equal_descr_pairs*)
4.417 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts), _))) = (id, feedb);
4.418 -
4.419 -(*nth 1 equal_descr_pairs* )
4.420 -(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
4.421 - (Free ("r", typ3), value))] = return_discern_feedback
4.422 -(*+*)val true = typ1 = typ2
4.423 -(*+*)val true = typ3 = HOLogic.realT
4.424 -(*+*)val "7" = UnparseC.term @{context} value
4.425 -( *nth 2 equal_descr_pairs*)
4.426 -(*+*)val [] = return_discern_feedback
4.427 -
4.428 -val return_discern_typ =
4.429 - discern_typ id (descr, ts);
4.430 -"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
4.431 -(*nth 1 equal_descr_pairs* )
4.432 -(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
4.433 - (Free ("r", typ3), value))] = return_discern_typ
4.434 -(*+*)val true = typ1 = typ2
4.435 -(*+*)val true = typ3 = HOLogic.realT
4.436 -(*+*)val "7" = UnparseC.term @{context} value
4.437 -( *nth 2 equal_descr_pairs*)
4.438 -(*+*)val [] = return_discern_typ;
4.439 -(**)
4.440 - switch_type id ts;
4.441 -"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
4.442 -
4.443 -(*nth 1 equal_descr_pairs* )
4.444 -val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
4.445 -
4.446 -(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST
4.447 -(*+*)val Type ("Real.real", []) = typ
4.448 -( *nth 2 equal_descr_pairs*)
4.449 -(*+*)val return_switch_type_TEST = descr
4.450 -(**)
4.451 -(*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
4.452 -
4.453 -(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
4.454 - val subst_eval_list = make_envs_preconds equal_givens
4.455 - val (env_subst, env_eval) = split_list subst_eval_list
4.456 -
4.457 -val return_of_max_variant = ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
4.458 - = length model_patt, max_variant, i_model_max),
4.459 - env_model, (env_subst, env_eval));
4.460 -return_of_max_variant: (bool * variant * T_TEST) * Env.T * (env_subst * env_eval);
4.461 -(*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
4.462 - val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant
4.463 -(*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
4.464 - val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
4.465 -(*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
4.466 -(*||||||-------------- contine check -----------------------------------------------------*)
4.467 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
4.468 - val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
4.469 - val full_subst = if env_eval = [] then pres_subst_other
4.470 - else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
4.471 - val evals = map (eval ctxt where_rls) full_subst
4.472 -val return_ = (i_model_max, env_subst, env_eval)
4.473 -(*\\\\\\\------------- step into check -------------------------------------------------//*)
4.474 -val (preok, _) = return_check_OLD;
4.475 -
4.476 -(*|||||--------------- contine for_problem ---------------------------------------------------*)
4.477 - (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
4.478 - (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
4.479 -val NONE =
4.480 - (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
4.481 -
4.482 - (*case*)
4.483 - Specify.item_to_add (ThyC.get_theory ctxt
4.484 - (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
4.485 -"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
4.486 - = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
4.487 - fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
4.488 - | false_and_not_Sup (_, _, false, _, _) = true
4.489 - | false_and_not_Sup _ = false
4.490 -
4.491 - val v = if itms = [] then 1 else Pre_Conds.max_variant itms
4.492 - val vors = if v = 0 then oris
4.493 - else filter ((fn variant =>
4.494 - fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
4.495 - v) oris
4.496 -
4.497 -(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"])]"
4.498 -(*+*) = vors |> O_Model.to_string @{context}
4.499 -
4.500 - val vits = if v = 0 then itms (* because of dsc without dat *)
4.501 - else filter ((fn variant =>
4.502 - fn (_, variants, _, _, _) => member op= variants variant)
4.503 - v) itms; (* itms..vat *)
4.504 -
4.505 - val icl = filter false_and_not_Sup vits; (* incomplete *)
4.506 -
4.507 - (*if*) icl = [] (*else*);
4.508 -(*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
4.509 - = icl |> I_Model.to_string @{context}
4.510 -(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"
4.511 - = hd icl |> I_Model.single_to_string @{context}
4.512 -
4.513 -(*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
4.514 -(*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
4.515 -(*++*)val [] = I_Model.o_model_values feedback
4.516 -
4.517 -(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"])]"
4.518 -(*+*) = vors |> O_Model.to_string @{context}
4.519 -
4.520 -val SOME ori =
4.521 - (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
4.522 - d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
4.523 - (hd icl)) vors (*of*);
4.524 -
4.525 -(*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
4.526 -(*+*) ori |> O_Model.single_to_string @{context}
4.527 -(*\\\\\--------------- step into for_problem -----------------------------------------------//*)
4.528 -(*\\\\---------------- step into find_next_step --------------------------------------------//*)
4.529 -(*|||----------------- continuing specify_do_next --------------------------------------------*)
4.530 -val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
4.531 -
4.532 - val ist_ctxt = Ctree.get_loc pt (p, p_)
4.533 -(*+*)val Add_Given "Constants [r = 7]" = tac
4.534 -val _ =
4.535 - (*case*) tac (*of*);
4.536 -
4.537 -Step_Specify.by_tactic_input tac (pt, (p, p_'));
4.538 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
4.539 - (tac, (pt, (p, p_')));
4.540 -
4.541 - Specify.by_Add_ "#Given" ct ptp;
4.542 -"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
4.543 - ("#Given", ct, ptp);
4.544 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
4.545 - val (i_model, m_patt) =
4.546 - if p_ = Pos.Met then
4.547 - (met,
4.548 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
4.549 - else
4.550 - (pbl,
4.551 - (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
4.552 -
4.553 - (*case*)
4.554 - I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
4.555 -"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
4.556 - (ctxt, m_field, oris, i_model, m_patt, ct);
4.557 - val (t as (descriptor $ _)) = Syntax.read_term ctxt str
4.558 -
4.559 -(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
4.560 -
4.561 - val SOME m_field' =
4.562 - (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
4.563 - (*if*) m_field <> m_field' (*else*);
4.564 -
4.565 -(*+*)val "#Given" = m_field; val "#Given" = m_field'
4.566 -
4.567 -val ("", ori', all) =
4.568 - (*case*) O_Model.contains ctxt m_field o_model t (*of*);
4.569 -
4.570 -(*+*)val (_, _, _, _, vals) = hd o_model;
4.571 -(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
4.572 -(*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
4.573 -(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
4.574 -(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
4.575 -(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
4.576 -(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
4.577 -(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
4.578 -(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
4.579 -(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
4.580 -(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
4.581 -(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
4.582 -(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
4.583 -(*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
4.584 -
4.585 - (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
4.586 -"~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
4.587 - (ctxt, i_model, all, ori', m_patt);
4.588 -val SOME (_, (_, pid)) =
4.589 - (*case*) find_first (eq1 d) pbt (*of*);
4.590 -(*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
4.591 -val SOME (_, _, _, _, itm_) =
4.592 - (*case*) find_first (eq3 f d) itms (*of*);
4.593 -val ts' = inter op = (o_model_values itm_) ts;
4.594 - (*if*) subset op = (ts, ts') (*else*);
4.595 -val return_is_notyet_input = ("",
4.596 - ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
4.597 -"~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
4.598 - (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
4.599 - val ts' = union op = (o_model_values itm_) ts;
4.600 - val pval = [Input_Descript.join'''' (d, ts')]
4.601 - val complete = if eq_set op = (ts', all) then true else false
4.602 -
4.603 -(*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context}
4.604 -(*\\\----------------- step into specify_do_next -------------------------------------------//*)
4.605 -(*\\------------------ step into do_next ---------------------------------------------------//*)
4.606 -val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
4.607 -
4.608 -(*|------------------- continue with me_Model_Problem ----------------------------------------*)
4.609 -
4.610 -val tacis as (_::_) =
4.611 - (*case*) ts (*of*);
4.612 - val (tac, _, _) = last_elem tacis
4.613 -
4.614 -val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
4.615 -(*//------------------ step into TESTg_form ------------------------------------------------\\*)
4.616 -"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
4.617 -
4.618 - val (form, _, _) =
4.619 - ME_Misc.pt_extract ctxt ptp;
4.620 -"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
4.621 - val ppobj = Ctree.get_obj I pt p
4.622 - val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
4.623 - (*if*) Ctree.is_pblobj ppobj (*then*);
4.624 -
4.625 - pt_model ppobj p_;
4.626 -"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}),
4.627 - Pbl(*Frm,Pbl*)) = (ppobj, p_);
4.628 - val (_, pI, _) = Ctree.get_somespec' spec spec';
4.629 - (*if*) pI = Problem.id_empty (*else*);
4.630 -(* val where_ = if pI = Problem.id_empty then []*)
4.631 -(* else *)
4.632 -(* let *)
4.633 - val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
4.634 - val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
4.635 -(* in where_ end *)
4.636 - val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
4.637 -val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
4.638 -
4.639 -(*|------------------- continue with TESTg_form ----------------------------------------------*)
4.640 -val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
4.641 - (*case*) form (*of*);
4.642 - Test_Out.PpcKF ( (Test_Out.Problem [],
4.643 - P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
4.644 -
4.645 - P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
4.646 -"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
4.647 - fun coll model [] = model
4.648 - | coll model ((_, _, _, field, itm_) :: itms) =
4.649 - coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
4.650 -
4.651 - val gfr = coll P_Model.empty itms;
4.652 -"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
4.653 - = (P_Model.empty, itms);
4.654 -
4.655 -(*+*)val 4 = length itms;
4.656 -(*+*)val itm = nth 1 itms;
4.657 -
4.658 - coll P_Model.empty [itm];
4.659 -"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
4.660 - = (P_Model.empty, [itm]);
4.661 -
4.662 - (add_sel_ppc thy field model (item_from_feedback thy itm_));
4.663 -"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
4.664 - = (thy, field, model, (item_from_feedback thy itm_));
4.665 -
4.666 - P_Model.item_from_feedback thy itm_;
4.667 -"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
4.668 - P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
4.669 -(*\\------------------ step into TESTg_form ------------------------------------------------//*)
4.670 -(*\------------------- step into me Model_Problem ------------------------------------------//*)
4.671 -val (p, _, f, nxt, _, pt) = return_me_Model_Problem
4.672 -
4.673 -(*-------------------- contine me's ----------------------------------------------------------*)
4.674 -val return_me_add_find_Constants = me nxt p c pt;
4.675 - val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
4.676 -(*/------------------- step into me_add_find_Constants -------------------------------------\\*)
4.677 -"~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
4.678 - (nxt, p, c, pt);
4.679 - val ctxt = Ctree.get_ctxt pt p
4.680 -(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
4.681 - ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
4.682 -(*-------------------------------------------^^--*)
4.683 -val return_step_by_tactic = (*case*)
4.684 - Step.by_tactic tac (pt, p) (*of*);
4.685 -(*//------------------ step into Step.by_tactic --------------------------------------------\\*)
4.686 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
4.687 -val Applicable.Yes tac' =
4.688 - (*case*) Specify_Step.check tac (pt, p) (*of*);
4.689 - (*if*) Tactic.for_specify' tac' (*then*);
4.690 -Step_Specify.by_tactic tac' ptp;
4.691 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
4.692 -
4.693 - Specify.by_Add_ "#Given" ct (pt, p);
4.694 -"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
4.695 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
4.696 -(* val (i_model, m_patt) =*)
4.697 - (*if*) p_ = Pos.Met (*else*);
4.698 -val return_by_Add_ =
4.699 - (pbl,
4.700 - (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
4.701 -val I_Model.Add i_single =
4.702 - (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
4.703 -
4.704 - val i_model' =
4.705 - I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
4.706 -"~~~~~ fun add_single , args:"; val (thy, itm, model) =
4.707 - ((Proof_Context.theory_of ctxt), i_single, i_model);
4.708 - fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
4.709 - | eq_untouched _ _ = false
4.710 - val model' = case I_Model.seek_ppc (#1 itm) model of
4.711 - SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
4.712 -
4.713 -(*||------------------ contine Step.by_tactic ------------------------------------------------*)
4.714 -(*\\------------------ step into Step.by_tactic --------------------------------------------//*)
4.715 -val ("ok", (_, _, ptp)) = return_step_by_tactic;
4.716 -
4.717 - val (pt, p) = ptp;
4.718 - (*case*)
4.719 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.720 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
4.721 - (p, ((pt, Pos.e_pos'), []));
4.722 - (*if*) Pos.on_calc_end ip (*else*);
4.723 - val (_, probl_id, _) = Calc.references (pt, p);
4.724 -val _ =
4.725 - (*case*) tacis (*of*);
4.726 - (*if*) probl_id = Problem.id_empty (*else*);
4.727 -
4.728 - switch_specify_solve p_ (pt, ip);
4.729 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.730 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.731 -
4.732 - specify_do_next (pt, input_pos);
4.733 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
4.734 - val (_, (p_', tac)) =
4.735 - Specify.find_next_step ptp;
4.736 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
4.737 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
4.738 - spec = refs, ...} = Calc.specify_data (pt, pos);
4.739 - val ctxt = Ctree.get_ctxt pt pos;
4.740 -
4.741 -(*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _
4.742 - = pbl
4.743 -(*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts;
4.744 -(*-----ML-^------^-HOL*)
4.745 -
4.746 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
4.747 - (*if*) p_ = Pos.Pbl (*then*);
4.748 -
4.749 - for_problem ctxt oris (o_refs, refs) (pbl, met);
4.750 -"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
4.751 - (ctxt, oris, (o_refs, refs), (pbl, met));
4.752 - val cpI = if pI = Problem.id_empty then pI' else pI;
4.753 - val cmI = if mI = MethodC.id_empty then mI' else mI;
4.754 - val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
4.755 - val {model = mpc, ...} = MethodC.from_store ctxt cmI
4.756 -
4.757 - val (preok, _) =
4.758 -Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
4.759 -"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
4.760 - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
4.761 -
4.762 - val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
4.763 -"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
4.764 - val all_variants =
4.765 - map (fn (_, variants, _, _, _) => variants) i_model
4.766 - |> flat
4.767 - |> distinct op =
4.768 - val variants_separated = map (filter_variants' i_model) all_variants
4.769 - val sums_corr = map (cnt_corrects) variants_separated
4.770 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
4.771 - val (_, max_variant) = hd (*..crude decision, up to improvement *)
4.772 - (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
4.773 - val i_model_max =
4.774 - filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
4.775 - val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
4.776 - val env_model = make_env_model equal_descr_pairs
4.777 - val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
4.778 -
4.779 - val subst_eval_list =
4.780 - make_envs_preconds equal_givens;
4.781 -"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
4.782 -val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>
4.783 - discern_feedback id feedb)
4.784 -val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;
4.785 -"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
4.786 -
4.787 - discern_typ id (descr, ts);
4.788 -"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
4.789 -(*|------------------- contine me_add_find_Constants -----------------------------------------*)
4.790 -(*\------------------- step into me_add_find_Constants -------------------------------------//*)
4.791 -val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
4.792 -(*/########################## before destroying elementwise input of lists ##################\* )
4.793 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
4.794 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
4.795 -( *\########################## before destroying elementwise input of lists ##################/*)
4.796 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;
4.797 -
4.798 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
4.799 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;
4.800 -val return_me_Add_Relation_SideConditions
4.801 - = me nxt p c pt;
4.802 -(*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*)
4.803 -(*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
4.804 -"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
4.805 - val ctxt = Ctree.get_ctxt pt p;
4.806 -(**) val (pt, p) = (**)
4.807 - (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
4.808 -(**) ("ok", (_, _, ptp)) => ptp (**) ;
4.809 -
4.810 - (*case*)
4.811 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.812 -(*//------------------ step into do_next ---------------------------------------------------\\*)
4.813 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
4.814 - = (p, ((pt, Pos.e_pos'), [])) (*of*);
4.815 - (*if*) Pos.on_calc_end ip (*else*);
4.816 - val (_, probl_id, _) = Calc.references (pt, p);
4.817 - (*case*) tacis (*of*);
4.818 - (*if*) probl_id = Problem.id_empty (*else*);
4.819 -
4.820 - Step.switch_specify_solve p_ (pt, ip);
4.821 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.822 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.823 - Step.specify_do_next (pt, input_pos);
4.824 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
4.825 -(*isa------ERROR: Refine_Problem INSTEAD
4.826 - isa2: Specify_Theory "Diff_App"*)
4.827 - val (_, (p_', tac as Specify_Theory "Diff_App")) =
4.828 -(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
4.829 - Specify.find_next_step ptp;
4.830 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
4.831 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
4.832 - spec = refs, ...} = Calc.specify_data (pt, pos);
4.833 - val ctxt = Ctree.get_ctxt pt pos;
4.834 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
4.835 - (*if*) p_ = Pos.Pbl (*then*);
4.836 -
4.837 -val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =
4.838 -(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
4.839 - for_problem ctxt oris (o_refs, refs) (pbl, met);
4.840 -"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
4.841 - (ctxt, oris, (o_refs, refs), (pbl, met));
4.842 - val cpI = if pI = Problem.id_empty then pI' else pI;
4.843 - val cmI = if mI = MethodC.id_empty then mI' else mI;
4.844 - val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
4.845 - val {model = mpc, ...} = MethodC.from_store ctxt cmI
4.846 -
4.847 -(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
4.848 - Free ("fixes", _)] = where_
4.849 -
4.850 - val (preok, _) =
4.851 - Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
4.852 -(*///----------------- step into check -------------------------------------------------\\*)
4.853 -"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
4.854 - (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
4.855 -(*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
4.856 -(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
4.857 -(*+*) = model_patt |> Model_Pattern.to_string @{context}
4.858 -(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
4.859 - = i_model |> I_Model.to_string_TEST @{context}
4.860 -
4.861 -val return_of_max_variant as (_, _, (env_subst, env_eval)) =
4.862 - of_max_variant model_patt i_model
4.863 -
4.864 -(*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
4.865 -(*+*)val Type ("Real.real", []) = T1
4.866 -(*+*)val Type ("Real.real", []) = T2
4.867 -
4.868 -(*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
4.869 -(*+*)val Type ("Real.real", []) = T2
4.870 -
4.871 -val (_, _, (env_subst, env_eval)) = return_of_max_variant;
4.872 -(*|||----------------- contine check -----------------------------------------------------*)
4.873 - val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
4.874 -
4.875 -(*|||----------------- contine check -----------------------------------------------------*)
4.876 -(*+*)val [(true, Const ("Orderings.ord_class.less", _) $
4.877 - Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
4.878 -
4.879 - val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
4.880 -(*+*)val [(true,
4.881 - Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
4.882 - (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
4.883 -
4.884 - val evals = map (eval ctxt where_rls) full_subst
4.885 -val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
4.886 -(*\\\----------------- step into check -------------------------------------------------\\*)
4.887 -
4.888 - val (preok as true, _) = return_check_OLD
4.889 -(*+---------------^^^^*)
4.890 -(*\\------------------ step into do_next ---------------------------------------------------\\*)
4.891 -(*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
4.892 -val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
4.893 - val Specify_Theory "Diff_App" = nxt;
4.894 -
4.895 -val return_me_Specify_Theory
4.896 - = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
4.897 -(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
4.898 -"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
4.899 - val ctxt = Ctree.get_ctxt pt p;
4.900 -(* val (pt, p) = *)
4.901 - (*case*) Step.by_tactic tac (pt, p) (*of*);
4.902 -(* ("ok", (_, _, ptp)) => ptp *)
4.903 -val return_Step_by_tactic =
4.904 - Step.by_tactic tac (pt, p);
4.905 -(*//------------------ step into Step_by_tactic --------------------------------------------\\*)
4.906 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
4.907 - (*case*) Specify_Step.check tac (pt, p) (*of*);
4.908 -
4.909 -(*||------------------ contine Step_by_tactic ------------------------------------------------*)
4.910 -(*\\------------------ step into Step_by_tactic --------------------------------------------//*)
4.911 -
4.912 -val ("ok", (_, _, ptp)) = return_Step_by_tactic;
4.913 -(*|------------------- continue me Specify_Theory --------------------------------------------*)
4.914 -
4.915 -val ("ok", (ts as (_, _, _) :: _, _, _)) =
4.916 - (*case*)
4.917 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.918 -(*//------------------ step into do_next ---------------------------------------------------\\*)
4.919 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
4.920 - = (p, ((pt, Pos.e_pos'), [])) (*of*);
4.921 - (*if*) Pos.on_calc_end ip (*else*);
4.922 - val (_, probl_id, _) = Calc.references (pt, p);
4.923 -val _ =
4.924 - (*case*) tacis (*of*);
4.925 - (*if*) probl_id = Problem.id_empty (*else*);
4.926 -
4.927 - Step.switch_specify_solve p_ (pt, ip);
4.928 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.929 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.930 -
4.931 - Step.specify_do_next (pt, input_pos);
4.932 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
4.933 - val (_, (p_', tac)) = Specify.find_next_step ptp
4.934 - val ist_ctxt = Ctree.get_loc pt (p, p_);
4.935 - (*case*) tac (*of*);
4.936 -
4.937 -Step_Specify.by_tactic_input tac (pt, (p, p_'));
4.938 -(*+*)val Specify_Theory "Diff_App" = tac;
4.939 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
4.940 - = (tac, (pt, (p, p_')));
4.941 - val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
4.942 - PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
4.943 - (oris, dI, dI', pI', probl, ctxt)
4.944 - val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
4.945 - val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
4.946 -(*\\------------------ step into do_next ---------------------------------------------------//*)
4.947 -(*\------------------- step into me Specify_Theory -----------------------------------------//*)
4.948 -val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
4.949 -
4.950 -val return_me_Specify_Problem (* keep for continuing me *)
4.951 - = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
4.952 -(*/------------------- step into me Specify_Problem ----------------------------------------\\*)
4.953 -"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
4.954 - val ctxt = Ctree.get_ctxt pt p
4.955 -
4.956 -(** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
4.957 -(**) val return_by_tactic =(**) (*case*)
4.958 - Step.by_tactic tac (pt, p) (*of*);
4.959 -(*//------------------ step into by_tactic -------------------------------------------------\\*)
4.960 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
4.961 -
4.962 - (*case*)
4.963 - Step.check tac (pt, p) (*of*);
4.964 -"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
4.965 - (*if*) Tactic.for_specify tac (*then*);
4.966 -
4.967 -Specify_Step.check tac (ctree, pos);
4.968 -"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
4.969 - = (tac, (ctree, pos));
4.970 - val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
4.971 - Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
4.972 - => (oris, dI, pI, dI', pI', itms)
4.973 - val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
4.974 -(*\\------------------ step into by_tactic -------------------------------------------------//*)
4.975 -val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
4.976 -
4.977 - (*case*)
4.978 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.979 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
4.980 - (*if*) Pos.on_calc_end ip (*else*);
4.981 - val (_, probl_id, _) = Calc.references (pt, p);
4.982 -val _ =
4.983 - (*case*) tacis (*of*);
4.984 - (*if*) probl_id = Problem.id_empty (*else*);
4.985 -
4.986 - Step.switch_specify_solve p_ (pt, ip);
4.987 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.988 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.989 -
4.990 - Step.specify_do_next (pt, input_pos);
4.991 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
4.992 - val (_, (p_', tac)) = Specify.find_next_step ptp
4.993 - val ist_ctxt = Ctree.get_loc pt (p, p_)
4.994 -val _ =
4.995 - (*case*) tac (*of*);
4.996 -
4.997 -Step_Specify.by_tactic_input tac (pt, (p, p_'));
4.998 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
4.999 - = (tac, (pt, (p, p_')));
4.1000 -
4.1001 - val (o_model, ctxt, i_model) =
4.1002 -Specify_Step.complete_for id (pt, pos);
4.1003 -"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
4.1004 - val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
4.1005 - ...} = Calc.specify_data (ctree, pos);
4.1006 - val ctxt = Ctree.get_ctxt ctree pos
4.1007 - val (dI, _, _) = References.select_input o_refs refs;
4.1008 - val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
4.1009 - val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
4.1010 - val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
4.1011 - val thy = ThyC.get_theory ctxt dI
4.1012 - val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
4.1013 -(*\------------------- step into me Specify_Problem ----------------------------------------//*)
4.1014 -val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
4.1015 -
4.1016 -val return_me_Add_Given_FunctionVariable
4.1017 - = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
4.1018 -(*/------------------- step into me Specify_Method -----------------------------------------\\*)
4.1019 -"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
4.1020 - val ctxt = Ctree.get_ctxt pt p
4.1021 - val (pt, p) =
4.1022 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
4.1023 - case Step.by_tactic tac (pt, p) of
4.1024 - ("ok", (_, _, ptp)) => ptp;
4.1025 -
4.1026 - (*case*)
4.1027 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.1028 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
4.1029 - (*if*) Pos.on_calc_end ip (*else*);
4.1030 - val (_, probl_id, _) = Calc.references (pt, p);
4.1031 -val _ =
4.1032 - (*case*) tacis (*of*);
4.1033 - (*if*) probl_id = Problem.id_empty (*else*);
4.1034 -
4.1035 - Step.switch_specify_solve p_ (pt, ip);
4.1036 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.1037 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.1038 -
4.1039 - Step.specify_do_next (pt, input_pos);
4.1040 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
4.1041 -
4.1042 - val (_, (p_', tac)) =
4.1043 - Specify.find_next_step ptp;
4.1044 -"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
4.1045 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
4.1046 - spec = refs, ...} = Calc.specify_data (pt, pos);
4.1047 - val ctxt = Ctree.get_ctxt pt pos;
4.1048 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
4.1049 - (*if*) p_ = Pos.Pbl (*else*);
4.1050 -
4.1051 - Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
4.1052 -"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
4.1053 - = (ctxt, oris, (o_refs, refs), (pbl, met));
4.1054 - val cmI = if mI = MethodC.id_empty then mI' else mI;
4.1055 - val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
4.1056 - val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
4.1057 -val NONE =
4.1058 - (*case*) find_first (I_Model.is_error o #5) met (*of*);
4.1059 -
4.1060 - (*case*)
4.1061 - Specify.item_to_add (ThyC.get_theory ctxt
4.1062 - (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
4.1063 -"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
4.1064 - = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
4.1065 -(*\------------------- step into me Specify_Method -----------------------------------------//*)
4.1066 -val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
4.1067 -
4.1068 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
4.1069 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
4.1070 -
4.1071 -(* ------------------- step into UNTIL A PROGRAM IS REQUIRED (not yet impl. ---------------- )*)
4.1072 -\<close> ML \<open>(*/------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
4.1073 -(*/------------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
4.1074 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
4.1075 - val ctxt = Ctree.get_ctxt pt p
4.1076 - val (pt, p) =
4.1077 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
4.1078 - case Step.by_tactic tac (pt, p) of
4.1079 - ("ok", (_, _, ptp)) => ptp;
4.1080 -(*ERROR due to missing program in creating the environment from formal args* )
4.1081 - (*case*)
4.1082 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
4.1083 -( *ERROR*)
4.1084 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) =
4.1085 - (p, ((pt, Pos.e_pos'), []));
4.1086 - (*if*) Pos.on_calc_end ip (*else*);
4.1087 - val (_, probl_id, _) = Calc.references (pt, p);
4.1088 -val _ =
4.1089 - (*case*) tacis (*of*);
4.1090 - (*if*) probl_id = Problem.id_empty (*else*);
4.1091 -
4.1092 -(*ERROR due to missing program in creating the environment from formal args* )
4.1093 - switch_specify_solve p_ (pt, ip);
4.1094 -( *ERROR*)
4.1095 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
4.1096 - (*if*) Pos.on_specification ([], state_pos) (*then*);
4.1097 -
4.1098 -(*ERROR due to missing program in creating the environment from formal args* )
4.1099 - specify_do_next (pt, input_pos)
4.1100 -( *ERROR*)
4.1101 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
4.1102 - val (_, (p_', tac as Apply_Method ["Optimisation", "by_univariate_calculus"])) =
4.1103 - (*-------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not yet impl.*)
4.1104 - Specify.find_next_step ptp
4.1105 - val ist_ctxt = Ctree.get_loc pt (p, p_)
4.1106 -
4.1107 -val Tactic.Apply_Method (mI as ["Optimisation", "by_univariate_calculus"]) =
4.1108 - (*case*) tac (*of*);
4.1109 -(*ERROR due to missing program in creating the environment from formal args* )
4.1110 - LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
4.1111 - ist_ctxt (pt, (p, p_'))
4.1112 -( *ERROR*)
4.1113 -\<close> ML \<open> (*//----------- step into by_tactic -------------------------------------------------\\*)
4.1114 -(*//------------------ step into by_tactic -------------------------------------------------\\*)
4.1115 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
4.1116 - ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
4.1117 -(*new*)val (itms, oris, pI, probl) = case get_obj I pt p of
4.1118 -(*new*) PblObj {meth = itms, origin = (oris, (_, pI, _), _), probl, ...} => (itms, oris, pI, probl)
4.1119 +val (p,_,f,nxt,_,pt) =
4.1120 + Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
4.1121 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
4.1122 +\<close> ML \<open>
4.1123 +\<close> ML \<open> (*//----------- setup test data for I_Model.s_make_complete -------------------------\\*)
4.1124 +(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
4.1125 +val (o_model, (pbl_imod, met_imod), (pI, mI)) = case get_obj I pt (fst p) of
4.1126 + PblObj {meth = met_imod, origin = (o_model, (_, pI, mI), _), probl = pbl_imod, ...}
4.1127 + => (o_model, (pbl_imod, met_imod), (pI, mI))
4.1128 | _ => raise ERROR ""
4.1129 \<close> ML \<open>
4.1130 -(*new*)val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
4.1131 -(*new*)val {model = met_patt, ...} = MethodC.from_store ctxt mI;
4.1132 - (*if*) itms <> [] (*then*);
4.1133 -\<close> text \<open>(*old*)
4.1134 -(*old*)val itms =
4.1135 - I_Model.complete oris probl [] met_patt;
4.1136 -\<close> ML \<open>(*new*)
4.1137 -(*new*)val itms =
4.1138 - (*I_Model.*)fill_method oris (I_Model.OLD_to_TEST probl) met_patt;
4.1139 +val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
4.1140 +val {model = met_patt, ...} = MethodC.from_store ctxt mI;
4.1141 \<close> ML \<open>
4.1142 -val return_fill_method = fill_method oris (I_Model.OLD_to_TEST probl) met_patt;
4.1143 -\<close> ML \<open> (*///---------- step into fill_method -----------------------------------------------\\*)
4.1144 -(*///----------------- step into fill_method -----------------------------------------------\\*)
4.1145 -"~~~~~ fun fill_method , args:"; val (o_model, pbl_imod, met_patt) =
4.1146 - (oris, I_Model.OLD_to_TEST probl, met_patt);
4.1147 +val pbl_imod = [ (*2 items for creating code ---> variants [1, 2]*)
4.1148 + (1, [1, 2, 3], true, "#undef", (Cor_TEST (@{term Constants},
4.1149 + [@{term "[r = (7::real)]"}]), Position.none)),
4.1150 + (1, [1, 2], true, "#undef", (Cor_TEST (@{term SideConditions},
4.1151 + [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]), Position.none))]
4.1152 +\<close> ML \<open>
4.1153 +val met_imod = [ (*1 item for creating code*)
4.1154 +(8, [2], true, "#undef", (Cor_TEST (@{term FunctionVariable}, [@{term "b::real"}]), Position.none))]
4.1155 \<close> ML \<open>
4.1156 (*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
4.1157 - "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
4.1158 - "(2, [\"1\", \"2\", \"3\"], #Given, Maximum, [\"A\"]), \n" ^
4.1159 - "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
4.1160 - "(4, [\"1\", \"2\", \"3\"], #Given, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
4.1161 - "(5, [\"1\", \"2\"], #Given, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
4.1162 -(*ERROR----------------------------------------------------------^^^^^*)
4.1163 - "(6, [\"3\"], #Given, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
4.1164 - "(7, [\"1\"], #Given, FunctionVariable, [\"a\"]), \n" ^
4.1165 - "(8, [\"2\"], #Given, FunctionVariable, [\"b\"]), \n" ^
4.1166 - "(9, [\"3\"], #Given, FunctionVariable, [\"\<alpha>\"]), \n" ^
4.1167 - "(10, [\"1\", \"2\"], #Given, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
4.1168 - "(11, [\"3\"], #Given, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
4.1169 - "(12, [\"1\", \"2\", \"3\"], #Given, ErrorBound, [\"\<epsilon> = 0\"])]"
4.1170 -then () else error "complete_TEST: init. o_model CHANGED"
4.1171 +(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
4.1172 +(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
4.1173 +(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
4.1174 +(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
4.1175 +(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
4.1176 +(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
4.1177 +(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
4.1178 +(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
4.1179 +(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
4.1180 +(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
4.1181 +(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
4.1182 +(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
4.1183 +then () else error "setup test data for I_Model.s_make_complete CHANGED";
4.1184 +(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
4.1185 +\<close> ML \<open> (*\\----------- setup test data for I_Model.s_make_complete -------------------------//*)
4.1186 \<close> ML \<open>
4.1187 -(*+*)if (pbl_imod |> I_Model.to_string_TEST @{context}) = "[\n" ^
4.1188 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1189 +val return_s_make_complete =
4.1190 + s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
4.1191 +\<close> ML \<open> (*/------------ step into s_make_complete -------------------------------------------\\*)
4.1192 +(*/------------------- step into s_make_complete -------------------------------------------\\*)
4.1193 +(*.....~~~ fill_method....*)
4.1194 +"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
4.1195 + (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
4.1196 +\<close> ML \<open>
4.1197 + val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
4.1198 +\<close> ML \<open>
4.1199 + val i_from_pbl = map (fn (_, (descr, _)) =>
4.1200 + (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
4.1201 +\<close> ML \<open> (*//----------- step into get_descr_vnt ---------------------------------------------\\*)
4.1202 +(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
4.1203 +"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
4.1204 + (@{term Constants}, pbl_max_vnts, pbl_imod);
4.1205 +\<close> ML \<open>
4.1206 + val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
4.1207 + | SOME descr' => if descr = descr' then true else false) i_model
4.1208 +\<close> ML \<open>
4.1209 +(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr
4.1210 +(*+*): I_Model.T_TEST
4.1211 +\<close> ML \<open>
4.1212 +val return_get_descr_vnt_1 =
4.1213 + case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
4.1214 + [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
4.1215 + | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
4.1216 +(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
4.1217 +\<close> ML \<open> (*\\----------- step into get_descr_vnt ---------------------------------------------//*)
4.1218 +\<close> ML \<open>
4.1219 +\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
4.1220 +(*|------------------- continue s_make_complete ----------------------------------------------*)
4.1221 +\<close> ML \<open>
4.1222 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
4.1223 + if is_empty_single_TEST i_single
4.1224 + then
4.1225 + case get_descr_vnt' feedb pbl_max_vnts o_model of
4.1226 +(*-----------^^^^^^^^^^^^^^-----------------------------*)
4.1227 + [] => raise ERROR (msg pbl_max_vnts feedb)
4.1228 + | o_singles => map transfer_terms o_singles
4.1229 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
4.1230 +\<close> ML \<open>
4.1231 +(*+*)val [2, 1] = vnts;
4.1232 +(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
4.1233 + "(1, [1, 2, 3], true ,#undef, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1234 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1235 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1236 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1237 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
4.1238 -(*ERROR----------------------------------------------------------------^^^^^*)
4.1239 -then () else error "complete_TEST: init. pbl_imod CHANGED";
4.1240 + "(1, [1, 2], true ,#undef, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
4.1241 +then () else error "pbl_from_o_model CHANGED"
4.1242 \<close> ML \<open>
4.1243 -(*+*)if (met_patt |> Model_Pattern.to_string @{context}) = "[\"" ^
4.1244 - "(#Given, (Constants, fixes))\", \"" ^
4.1245 - "(#Given, (Maximum, maxx))\", \"" ^
4.1246 - "(#Given, (Extremum, extr))\", \"" ^
4.1247 - "(#Given, (SideConditions, sideconds))\", \"" ^
4.1248 - "(#Given, (FunctionVariable, funvar))\", \"" ^
4.1249 - "(#Given, (Input_Descript.Domain, doma))\", \"" ^
4.1250 - "(#Given, (ErrorBound, err))\", \"" ^
4.1251 - "(#Find, (AdditionalValues, vals))\"]"
4.1252 -then () else error "complete_TEST: init. met_patt CHANGED";
4.1253 \<close> ML \<open>
4.1254 -(*old*)val ((_, pbl_max_vnt as 3, pbl_i_max), _, _) = I_Model.of_max_variant pbl_patt pbl_imod
4.1255 -(*new below step into*)
4.1256 +\<close> ML \<open> (*//----------- step into map ((fn i_single -----------------------------------------\\*)
4.1257 +(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
4.1258 +"~~~~~ fun map ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) = (nth 1 i_from_pbl);
4.1259 + (*if*) is_empty_single_TEST i_single (*else*);
4.1260 + get_descr_vnt' feedb pbl_max_vnts o_model;
4.1261
4.1262 -val return_max_variants =
4.1263 -(*I_Model.*)max_variants pbl_imod;
4.1264 -\<close> ML \<open> (*////--------- step into max_variants ----------------------------------------------\\*)
4.1265 -(*////---------------- step into max_variants ----------------------------------------------\\*)
4.1266 -"~~~~~ fun max_variants , args:"; val (model_patt, i_model) = (pbl_patt, pbl_imod);
4.1267 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
4.1268 + if is_empty_single_TEST i_single
4.1269 + then
4.1270 + case get_descr_vnt' feedb pbl_max_vnts o_model of
4.1271 +(*---------- ^^^^^^^^^^^^^^ ----------------------------*)
4.1272 + [] => raise ERROR (msg pbl_max_vnts feedb)
4.1273 + | o_singles => map transfer_terms o_singles
4.1274 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
4.1275 \<close> ML \<open>
4.1276 - val all_variants =
4.1277 - map (fn (_, variants, _, _, _) => variants) i_model
4.1278 - |> flat
4.1279 - |> distinct op =
4.1280 +\<close> ML \<open> (*\\----------- step into map ((fn i_single -----------------------------------------//*)
4.1281 +(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
4.1282 +
4.1283 +\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
4.1284 +(*|------------------- continue s_make_complete ----------------------------------------------*)
4.1285 \<close> ML \<open>
4.1286 -(*+*)val [1, 2, 3] = all_variants
4.1287 + val i_from_met = map (fn (_, (descr, _)) =>
4.1288 + (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt
4.1289 \<close> ML \<open>
4.1290 - val variants_separated = map (filter_variants' i_model) all_variants
4.1291 +(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
4.1292 + "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
4.1293 + "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
4.1294 + "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
4.1295 + "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
4.1296 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
4.1297 +(*---there is 1 item already input -^^^^^^^^^^^^^^^^^^*)
4.1298 + "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
4.1299 + "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
4.1300 + "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
4.1301 +(*+*)then () else error "s_make_complete: from_met CHANGED";
4.1302 \<close> ML \<open>
4.1303 -(*+*)if map (I_Model.to_string_TEST @{context}) variants_separated =
4.1304 - ["[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1305 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1306 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1307 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1308 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
4.1309 - "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1310 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1311 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1312 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1313 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
4.1314 - "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1315 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1316 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1317 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"]
4.1318 -then () else error "of_max_variant: variants_separated CHANGED"
4.1319 + val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
4.1320 +(*+*)val [2] = met_max_vnts
4.1321 \<close> ML \<open>
4.1322 - val sums_corr = map (cnt_corrects) variants_separated
4.1323 -(*+*)val [5, 5, 4] = sums_corr
4.1324 + val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
4.1325 \<close> ML \<open>
4.1326 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
4.1327 -(*+*)val [(5(*--- items with Cor_TEST in variant ---*), 1), (5, 2), (4, 3)] = sum_variant_s
4.1328 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
4.1329 + if is_empty_single_TEST i_single
4.1330 + then
4.1331 + case get_descr_vnt' feedb [met_max_vnt] o_model of
4.1332 + [] => raise ERROR (msg [met_max_vnt] feedb)
4.1333 + | o_singles => map transfer_terms o_singles
4.1334 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
4.1335 \<close> ML \<open>
4.1336 - val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
4.1337 -(*+*)val [(5, 2), (5, 1), (4, 3)] = max_first
4.1338 -\<close> ML \<open>
4.1339 - val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
4.1340 - |> map snd
4.1341 -(*+*)val [2, 1] = maxes
4.1342 -\<close> ML \<open>
4.1343 - val option_sequence = map
4.1344 - (fn (_, vnt) => if (member (op =) maxes vnt) then SOME vnt else NONE) sum_variant_s
4.1345 -(*+*)val [SOME 1, SOME 2, NONE] = option_sequence
4.1346 -\<close> ML \<open>
4.1347 - val max_i_models = map (fn (pos_in_sum_variant_s, i_model) =>
4.1348 - if is_some pos_in_sum_variant_s then i_model else [])
4.1349 - (option_sequence ~~ variants_separated)
4.1350 - |> filter_out (fn place_holder => place_holder = []);
4.1351 -(*+*)if map (I_Model.to_string_TEST @{context}) max_i_models = [
4.1352 - "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1353 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1354 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1355 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1356 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
4.1357 - "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1358 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1359 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1360 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1361 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"]
4.1362 -then () else error "of_max_variant: resulting max_i_models CHANGED"
4.1363 -\<close> ML \<open>
4.1364 -(*+*)if length max_i_models = length maxes
4.1365 -(*+*)then () else error "of_max_variant: resulting max_i_models AND maxes OF UNEQUAL LENGTH"
4.1366 -\<close> ML \<open>
4.1367 -val return_max_variants_step = (maxes, max_i_models)
4.1368 -\<close> ML \<open>
4.1369 -(*+*)if return_max_variants_step = return_max_variants
4.1370 -(*+*)then () else error "max_variants CHANGED"
4.1371 -\<close> ML \<open> (*\\\\--------- step into max_variants ----------------------------------------------//*)
4.1372 -(*\\\\---------------- step into max_variants ----------------------------------------------//*)
4.1373 -val (pbl_max_vnts, pbl_max_imos) = return_max_variants
4.1374 -\<close> ML \<open>
4.1375 -\<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*)
4.1376 -(*|||----------------- continue fill_method --------------------------------------------------*)
4.1377 -\<close> ML \<open>
4.1378 - val (pbl_max_vnts, pbl_max_imos) = (*I_Model.*)max_variants pbl_imod
4.1379 -;
4.1380 -(*+*)val [2, 1] = pbl_max_vnts;
4.1381 -(*-------pbl_max_imos is NONSENSE (*+*)if (pbl_max_imos ..*)
4.1382 -(*+*)if (pbl_max_imos |> map (map (fn (no, vnts, _, _, _) => (no, vnts)))) = [
4.1383 - [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])],
4.1384 - [(1, [1, 2, 3]), (2, [1, 2, 3]), (3, [1, 2, 3]), (4, [1, 2, 3]), (5, [1, 2])]]
4.1385 -(*+*)then () else error "of_max_variant: RESULT pbl_max_imos CHANGED";
4.1386 -\<close> ML \<open>
4.1387 - (*we maintain the sequence of items in model_patt for sequence of formals*)
4.1388 - val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr maxes pbl_imod) met_patt
4.1389 -;
4.1390 -(*+*)if (from_pbl |> to_string_TEST @{context}) = "[\n" ^
4.1391 +(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
4.1392 "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1393 "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1394 "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1395 "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
4.1396 - "(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n" ^
4.1397 - "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
4.1398 - "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
4.1399 -(*RESULT OF program ---------------------AdditionalValues [u, v]-------------------------*)
4.1400 + "(8, [2], true ,#undef, (Cor_TEST FunctionVariable b , pen2str, Position.T)), \n" ^
4.1401 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
4.1402 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
4.1403 "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
4.1404 -(*+*)then () else error "get_descr_vntL result CHANGED";
4.1405 +(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
4.1406 \<close> ML \<open>
4.1407 -\<close> ML \<open>
4.1408 -\<close> ML \<open> (*////--------- step into get_descr_vnt' --------------------------------------------\\*)
4.1409 -(*////---------------- step into get_descr_vnt' --------------------------------------------\\*)
4.1410 -\<close> ML \<open>
4.1411 -"~~~~~ fun get_descr_vnt' , args:"; val (feedb, vnts, o_model) =
4.1412 - (Sup_TEST (@{term FunctionVariable}, [@{term "a::real"}]), maxes, o_model);
4.1413 -\<close> ML \<open>
4.1414 -(*+*)val "(7, [\"1\"], #Given, FunctionVariable, [\"a\"])"
4.1415 -(*+*) = (get_descr_vnt' feedb vnts o_model |> the |> O_Model.single_to_string @{context});
4.1416 -\<close> ML \<open>
4.1417 - val (_, vnts', _, descr', ts) = nth 7 o_model
4.1418 - val (_, _, _, _, (feedb, _)) = nth 5 from_pbl
4.1419 -\<close> ML \<open>
4.1420 -(*+*)val SOME (Const ("Input_Descript.FunctionVariable", _)) = get_dscr' feedb
4.1421 -\<close> ML \<open>
4.1422 -(*+*)val xxx = (fn (_, vnts', _, descr', _) =>
4.1423 - case get_dscr' feedb of
4.1424 - SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false)
4.1425 -(*+*);
4.1426 -(*+*)xxx: O_Model.single -> bool
4.1427 -\<close> ML \<open>
4.1428 -(*+*)val SOME (7, [1], "#Given", Const ("Input_Descript.FunctionVariable", _), [Free ("a", _)])
4.1429 - = find_first (fn (_, vnts', _, descr', _) =>
4.1430 - case get_dscr' feedb of
4.1431 - SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
4.1432 - | NONE => false) o_model
4.1433 -\<close> ML \<open>
4.1434 -(*\\\\---------------- step into get_descr_vnt' --------------------------------------------//*)
4.1435 -\<close> ML \<open> (*\\\\--------- step into get_descr_vnt' --------------------------------------------//*)
4.1436 -\<close> ML \<open>
4.1437 -\<close> ML \<open> (*|||---------- continue fill_method --------------------------------------------------*)
4.1438 -(*|||----------------- continue fill_method --------------------------------------------------*)
4.1439 -\<close> ML \<open>
4.1440 - val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
4.1441 - if is_empty_single_TEST i_single
4.1442 - then
4.1443 - case get_descr_vnt' feedb vnts o_model of
4.1444 - NONE => raise ERROR (msg vnts feedb)
4.1445 - | SOME (i, vnts, m_field, descr, ts) =>
4.1446 - (i, vnts, true, m_field, (Cor_TEST ((descr, ts), (TermC.empty, [])), Position.none))
4.1447 - else i_single (*fetched before from pbl_imod*))) from_pbl
4.1448 -\<close> ML \<open>
4.1449 -\<close> ML \<open>
4.1450 -(*+*)val 8 = length from_o_model;
4.1451 -(*+*)if (from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
4.1452 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1453 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1454 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
4.1455 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
4.1456 - "(7, [1], true ,#Given, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
4.1457 - "(10, [1, 2], true ,#Given, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
4.1458 - "(12, [1, 2, 3], true ,#Given, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
4.1459 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
4.1460 -then () else error "RESULT of fill_method CHANGED"
4.1461 -\<close> ML \<open>
4.1462 -(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
4.1463 -(*from_pbl*)"(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
4.1464 -(*from_pbl*)"(2, [\"1\", \"2\", \"3\"], #Given, Maximum, [\"A\"]), \n" ^
4.1465 -(*from_pbl*)"(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
4.1466 -(*from_pbl*)"(4, [\"1\", \"2\", \"3\"], #Given, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
4.1467 -(*from_pbl*)"(5, [\"1\", \"2\"], #Given, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
4.1468 - "(6, [\"3\"], #Given, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
4.1469 -
4.1470 -(*from_omo*)"(7, [\"1\"], #Given, FunctionVariable, [\"a\"]), \n" ^ (*..both in intersection *)
4.1471 -(*from_omo*)"(8, [\"2\"], #Given, FunctionVariable, [\"b\"]), \n" ^ (*..both in intersection *)
4.1472 - "(9, [\"3\"], #Given, FunctionVariable, [\"\<alpha>\"]), \n" ^
4.1473 -(*from_omo*)"(10, [\"1\", \"2\"], #Given, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
4.1474 - "(11, [\"3\"], #Given, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
4.1475 -(*from_omo*)"(12, [\"1\", \"2\", \"3\"], #Given, ErrorBound, [\"\<epsilon> = 0\"])]"
4.1476 -(*^^^^^^^^ these should go to met_imod: COME "from_pbl" OR "from o_model-------------------------*)
4.1477 -then () else error "CHANGED o_model with items to add marked"
4.1478 -\<close> ML \<open>
4.1479 -\<close> ML \<open>(*new*)
4.1480 -(*new*)val itms =
4.1481 - (*I_Model.*)fill_method oris (I_Model.OLD_to_TEST probl) met_patt;
4.1482 -\<close> ML \<open>
4.1483 -\<close> ML \<open>
4.1484 -\<close> ML \<open>
4.1485 -\<close> ML \<open> (*\\\---------- step into fill_method -----------------------------------------------//*)
4.1486 -(*\\\----------------- step into fill_method -----------------------------------------------//*)
4.1487 -\<close> ML \<open>
4.1488 -\<close> ML \<open>(*||------------ continue by_tactic ----------------------------------------------------*)
4.1489 -(*||------------------ continue by_tactic ----------------------------------------------------*)
4.1490 -\<close> ML \<open>(*new*)
4.1491 -(*new*)val itms = return_fill_method
4.1492 -\<close> ML \<open>
4.1493 -\<close> ML \<open> (*\\----------- step into by_tactic -------------------------------------------------//*)
4.1494 -(*\\------------------ step into by_tactic -------------------------------------------------//*)
4.1495 -\<close> ML \<open>
4.1496 -(*GOON 2 after 1:
4.1497 - * of_max_variant returns hd maxes (works by chance for the example)
4.1498 - * do the same ^^^ with MethodC
4.1499 - * take the MethodC.model from the intersection of respective maxes
4.1500 - * if intersection = [] then message calling for interactive resolution
4.1501 - *)
4.1502 -\<close> ML \<open>
4.1503 -\<close> ML \<open>
4.1504 -\<close> text \<open> (*beim verschieben*)
4.1505 -val ((pbl_max_vnt, pbl_i_max), _, _) = return_of_max_variant;
4.1506 -\<close> ML \<open>
4.1507 -\<close> ML \<open>
4.1508 -\<close> text \<open> (*itermediate test result, before starting*)
4.1509 -(*+*) (pbl_i_max |> I_Model.to_string_TEST @ {context}) = "[\n" ^
4.1510 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
4.1511 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
4.1512 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
4.1513 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T))]"
4.1514 -\<close> ML \<open>
4.1515 -\<close> ML \<open>
4.1516 -\<close> text \<open>
4.1517 -(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,true ,#Given ,Cor FunctionVariable a , pen2str), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
4.1518 - = itms |> I_Model.to_string @ {context}
4.1519 -(*+*)val 8 = length itms
4.1520 -(*+*)val 8 = length model
4.1521 -\<close> ML \<open>(*\------------- step into me_Add_Given_ErrorBound------------------------------------//*)
4.1522 -(*\------------------- step into me_Add_Given_ErrorBound------------------------------------//*)
4.1523 -
4.1524 -
4.1525 +val return_s_make_complete_step = (pbl_from_o_model, met_from_pbl)
4.1526 +\<close> ML \<open> (*\------------ step into s_make_complete -------------------------------------------//*)
4.1527 +(*\------------------- step into s_make_complete -------------------------------------------//*)
4.1528 +if return_s_make_complete = return_s_make_complete_step
4.1529 +then () else error "s_make_complete: stewise construction <> value of fun"
4.1530 \<close> ML \<open>
4.1531 \<close>
4.1532