1.1 --- a/TODO.md Thu Oct 26 10:29:17 2023 +0200
1.2 +++ b/TODO.md Sun Oct 29 07:14:14 2023 +0100
1.3 @@ -52,6 +52,7 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 +* WN: reconsider design max_variants/_TEST
1.8 * WN: (*/---with M_Model.match_itms_oris broken elementwise input to lists---\*)
1.9 (*\---with M_Model.match_itms_oris broken elementwise input to lists---/*)
1.10 several tests marked in Test_Isac.thy, which have out-comments.
2.1 --- a/src/Tools/isac/Build_Isac.thy Thu Oct 26 10:29:17 2023 +0200
2.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Oct 29 07:14:14 2023 +0100
2.3 @@ -181,9 +181,9 @@
2.4 As next step we go bottom up from Thy_Info.get_theory and remove it.
2.5 Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
2.6 \<close>
2.7 -(** ) (* evaluated in Test_Isac/_Short *)
2.8 +(**) (* evaluated in Test_Isac/_Short *)
2.9 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
2.10 -(*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml"*)
2.11 +(*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" (*still in Test_Theory*)*)
2.12 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
2.13 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
2.14 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
2.15 @@ -216,7 +216,7 @@
2.16 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/preliminary.sml"
2.17 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/calculation.sml"
2.18 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/vscode-example.sml"
2.19 -( **)
2.20 +(**)
2.21
2.22 (* evaluated in Test_Isac/_Short *)
2.23
2.24 @@ -275,11 +275,11 @@
2.25 \<close> ML \<open>
2.26
2.27 \<close> ML \<open>
2.28 -I_Model.TEST_to_OLD
2.29 -\<close> ML \<open>
2.30 +I_Model.TEST_to_OLD ;
2.31 I_Model.OLD_to_TEST
2.32 -\<close>
2.33 (*OLD*)
2.34 (*---*)
2.35 (*NEW*)
2.36 +\<close> ML \<open>
2.37 +\<close>
2.38 end
3.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Thu Oct 26 10:29:17 2023 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Sun Oct 29 07:14:14 2023 +0100
3.3 @@ -49,7 +49,6 @@
3.4
3.5 val member_vnt: variants -> variant -> bool
3.6 val max_variants: o_model -> i_model_TEST -> variants
3.7 - val max_variant_TEST: i_model_TEST -> variant
3.8
3.9 (*from isac_test for Minisubpbl*)
3.10 val all_variants: ('a * variants * 'c * 'd * 'e) list -> variants
3.11 @@ -145,50 +144,61 @@
3.12 |> distinct op =
3.13 fun filter_variants' i_singles n =
3.14 filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
3.15 +
3.16 +(*OLD*)
3.17 +(*---*)
3.18 +fun some_input (Cor_TEST _) = true
3.19 + | some_input (Inc_TEST (_, _::_)) = true
3.20 + | some_input (Syn_TEST _) = true
3.21 + | some_input _ = false
3.22 +(*NEW*)
3.23 +
3.24 +(*OLD*)
3.25 fun cnt_corrects i_model =
3.26 fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
3.27 +(*---*)
3.28 +fun cnt_corrects i_model =
3.29 + fold (curry op +) (map (fn (_, _, _, _, (feedb, _)) =>
3.30 + if some_input feedb then 1 else 0) i_model) 0;
3.31 +(*NEW*)
3.32 fun arrange_args [] _ = []
3.33 | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all))
3.34
3.35 -(*for cases with only one i_model *)
3.36 -(*TODO: with vvv--- and vvv- max_variants replace Pre_Conds.max_variant *)
3.37 -fun max_variant_TEST i_model =
3.38 - let
3.39 - val all_variants =
3.40 - map (fn (_, variants, _, _, _) => variants) i_model
3.41 - |> flat
3.42 - |> distinct op =
3.43 - val variants_separated = map (filter_variants' i_model) all_variants
3.44 - val sums_corr = map (cnt_corrects) variants_separated
3.45 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
3.46 +(*in case of i_model max_variants = [] we take of o_model all_variants *)
3.47 +(*
3.48 + reconsider design:
3.49 + ?a? take all_variants from o_model and consider feedback only in i_model
3.50 + ?b? only consider non-empty items
3.51 + ?c? start with met_patt; pbl_patt only for Problem.is_complete
3.52 +*)
3.53 +fun max_variants o_model i_model =
3.54 + let
3.55 +(*OLD*)
3.56 + val all_variants =
3.57 + map (fn (_, variants, _, _, _) => variants) i_model
3.58 + |> flat
3.59 + |> distinct op =
3.60 +(*---* )
3.61 + val all_variants = (*we do not count empty items (not yet input)*)
3.62 + map (fn (_, _, _, _, (Inc_TEST (_, []), _)) => []
3.63 + | (_, variants, _, _, _) => variants) i_model
3.64 + |> flat
3.65 + |> distinct op =
3.66 +( *NEW*)
3.67 + val variants_separated = map (filter_variants' i_model) all_variants
3.68 + val sums_corr = map (cnt_corrects) variants_separated
3.69 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
3.70
3.71 - val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
3.72 - val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
3.73 - |> map snd
3.74 - in
3.75 - hd maxes
3.76 - end
3.77 -(*in case of i_model max_variants = [] we take of o_model all_variants *)
3.78 -fun max_variants o_model i_model =
3.79 - let
3.80 - val all_variants =
3.81 - map (fn (_, variants, _, _, _) => variants) i_model
3.82 - |> flat
3.83 - |> distinct op =
3.84 - val variants_separated = map (filter_variants' i_model) all_variants
3.85 - val sums_corr = map (cnt_corrects) variants_separated
3.86 - val sum_variant_s = arrange_args sums_corr (1, all_variants)
3.87 -
3.88 - val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
3.89 - val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
3.90 - |> map snd
3.91 - in
3.92 - if maxes = []
3.93 - then map (fn (_, variants, _, _, _) => variants) o_model
3.94 - |> flat
3.95 - |> distinct op =
3.96 - else maxes
3.97 - end
3.98 + val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
3.99 + val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
3.100 + |> map snd
3.101 + in
3.102 + if maxes = []
3.103 + then map (fn (_, variants, _, _, _) => variants) o_model
3.104 + |> flat
3.105 + |> distinct op =
3.106 + else maxes
3.107 + end
3.108
3.109
3.110 (** definitions for O_Model.T **)
4.1 --- a/src/Tools/isac/Specify/i-model.sml Thu Oct 26 10:29:17 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/i-model.sml Sun Oct 29 07:14:14 2023 +0100
4.3 @@ -25,6 +25,7 @@
4.4 type variants
4.5 type m_field
4.6 type descriptor
4.7 + type values
4.8
4.9 datatype feedback = datatype Model_Def.i_model_feedback
4.10 datatype feedback_TEST = datatype Model_Def.i_model_feedback_TEST
4.11 @@ -49,6 +50,8 @@
4.12 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
4.13 val descriptor: feedback -> descriptor
4.14 val descriptor_TEST: feedback_TEST -> descriptor
4.15 + val values: feedback -> values option
4.16 + val values_TEST: feedback_TEST -> values option
4.17 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
4.18 val o_model_values: feedback -> O_Model.values
4.19 val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
4.20 @@ -73,8 +76,7 @@
4.21 val feedback_to_string: Proof.context -> feedback -> string
4.22 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
4.23
4.24 - val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list ->
4.25 - 'a * 'b * bool * string * feedback
4.26 + val ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single
4.27 val seek_ppc: int -> T -> single option
4.28 val overwrite_ppc: theory -> single -> T -> T
4.29 (*\----- from isac_test for Minisubpbl*)
4.30 @@ -97,6 +99,7 @@
4.31 type variants = Model_Def.variants;
4.32 type m_field = Model_Def.m_field;
4.33 type descriptor = Model_Def.descriptor;
4.34 +type values = Model_Def.values
4.35
4.36 type T = Model_Def.i_model_single list;
4.37 (* for developing input from PIDE, we use T_TEST with these ideas:
4.38 @@ -237,6 +240,18 @@
4.39 | descriptor_TEST (Inc_TEST (d, _)) = d
4.40 | descriptor_TEST (Sup_TEST (d, _)) = d
4.41
4.42 +fun values (Cor ((_ , ts), _)) = SOME ts
4.43 + | values (Syn _) = NONE
4.44 + | values (Typ _) = NONE
4.45 + | values (Inc ((_, ts), _)) = SOME ts
4.46 + | values (Sup (_, ts)) = SOME ts
4.47 + | values (Mis (_, t)) = SOME [t]
4.48 + | values _ = raise ERROR "descriptor: uncovered case in fun.def.";
4.49 +fun values_TEST (Cor_TEST (_, ts)) = SOME ts
4.50 + | values_TEST (Syn_TEST _) = NONE
4.51 + | values_TEST (Inc_TEST (_, ts)) = SOME ts
4.52 + | values_TEST (Sup_TEST (_, ts)) = SOME ts
4.53 +
4.54 fun descr_pairs_to_string ctxt equal_descr_pairs =
4.55 (map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
4.56 |> pair2str) equal_descr_pairs)
5.1 --- a/test/Tools/isac/Test_Theory.thy Thu Oct 26 10:29:17 2023 +0200
5.2 +++ b/test/Tools/isac/Test_Theory.thy Sun Oct 29 07:14:14 2023 +0100
5.3 @@ -31,6 +31,7 @@
5.4 "xx"
5.5 ^ "xxx" (*+*) (*+++*) (*keep for continuing YYYYY*) (*isa*) (*isa2*) (**)
5.6
5.7 +\<close> ML \<open> (*--------------locate below ~~~ fun XXXXX, asap shift into separate section above ----*)
5.8 \<close> ML \<open> (*//----------- build fun XXXXX -----------------------------------------------------\\*)
5.9 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
5.10 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
5.11 @@ -44,14 +45,21 @@
5.12 val return_XXXXX = "XXXXX"
5.13 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
5.14 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
5.15 -\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
5.16 -(*||------------------ contine XXXXX ---------------------------------------------------------*)
5.17 +\<close> ML \<open> (*||----------- contine.. XXXXX -------------------------------------------------------*)
5.18 +(*||------------------ contine.. XXXXX -------------------------------------------------------*)
5.19 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
5.20 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
5.21 val "XXXXX" = return_XXXXX;
5.22
5.23 (* final test ... ----------------------------------------------------------------------------*)
5.24
5.25 +\<close> ML \<open>(*//############ @ {context} within fun XXXXX ----------------------------------\\*)
5.26 +(*//################## @ {context} within fun XXXXX ---------------------------------------\\* )
5.27 +(*-------------------- there must not be > ML < inbetween-------------------------------------*)
5.28 +( *\\################# @ {context} within fun XXXXX ----------------------------------------//*)
5.29 +\<close> ML \<open>(*\\############ @ {context} within fun XXXXX -----------------------------------//*)
5.30 +
5.31 +
5.32 \<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
5.33 (*//------------------ inserted hidden code ------------------------------------------------\\*)
5.34 (*\\------------------ inserted hidden code ------------------------------------------------//*)
5.35 @@ -69,19 +77,128 @@
5.36 \<close>
5.37
5.38 section \<open>===================================================================================\<close>
5.39 -section \<open>===== ============================================================================\<close>
5.40 +section \<open>===== --- build fun item_to_add ---================================================\<close>
5.41 ML \<open>
5.42 \<close> ML \<open>
5.43 +open Ctree;
5.44 +open Pos;
5.45 +open TermC;
5.46 +open Istate;
5.47 +open Tactic;
5.48 +open I_Model;
5.49 +open P_Model
5.50 +open Rewrite;
5.51 +open Step;
5.52 +open LItool;
5.53 +open LI;
5.54 +open Test_Code
5.55 +open Specify
5.56 +open ME_Misc
5.57 +open Pre_Conds;
5.58 +\<close> ML \<open> (*//----------- build fun item_to_add -----------------------------------------------\\*)
5.59 +(*//------------------ build fun item_to_add -----------------------------------------------\\*)
5.60 +\<close> ML \<open> (*shift this block up in separate section a.s.a.p*)
5.61 +\<close> ML \<open>
5.62 +\<close> ML \<open>(*\<longrightarrow> model-def.sml*)
5.63 +fun some_input (Cor_TEST _) = true
5.64 + | some_input (Inc_TEST (_, _::_)) = true
5.65 + | some_input (Syn_TEST _) = true
5.66 + | some_input _ = false
5.67 +;
5.68 +some_input: feedback_TEST -> bool
5.69 +\<close> ML \<open>
5.70 +(*OLD*)
5.71 +fun cnt_corrects i_model =
5.72 + fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
5.73 +(*---* )
5.74 +fun cnt_correct i_model =
5.75 + fold (curry op +) (map (fn (_, _, _, _, (feedb, _)) =>
5.76 + if some_input feedb then 1 else 0) i_model) 0;
5.77 +( *NEW*)
5.78 +\<close> ML \<open>(*\<longrightarrow> model-def.sml*)
5.79 +fun arrange_args [] _ = []
5.80 + | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all))
5.81 +\<close> ML \<open>
5.82 +\<close> ML \<open>(*\<longrightarrow> model-def.sml*)
5.83 +(*OLD*)
5.84 +(*---*)
5.85 +fun max_variants o_model i_model =
5.86 + let
5.87 +(*OLD*)
5.88 + val all_variants =
5.89 + map (fn (_, variants, _, _, _) => variants) i_model
5.90 + |> flat
5.91 + |> distinct op =
5.92 +(*---* )
5.93 + val all_variants = (*we do not count empty items (not yet input)*)
5.94 + map (fn (_, _, _, _, (Inc_TEST (_, []), _)) => []
5.95 + | (_, variants, _, _, _) => variants) i_model
5.96 + |> flat
5.97 + |> distinct op =
5.98 +( *NEW*)
5.99 + val variants_separated = map (filter_variants' i_model) all_variants
5.100 + val sums_corr = map (cnt_corrects) variants_separated
5.101 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
5.102 +
5.103 + val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.104 + val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
5.105 + |> map snd
5.106 + in
5.107 + if maxes = []
5.108 + then map (fn (_, variants, _, _, _) => variants) o_model
5.109 + |> flat
5.110 + |> distinct op =
5.111 + else maxes
5.112 + end
5.113 +\<close> ML \<open> (*\<longrightarrow> model-def.sml*)
5.114 +fun descriptor_exists descr feedb =
5.115 + case get_dscr' feedb of
5.116 + SOME descr' => descr' = descr
5.117 + | NONE => raise ERROR "existing_description NONE"
5.118 +;
5.119 +descriptor_exists: descriptor -> I_Model.feedback_TEST -> bool
5.120 +\<close> ML \<open>
5.121 +\<close> ML \<open> (*\<longrightarrow> i-model.sml*)
5.122 +(*in item_to_add prefers items with incomplete lists *)
5.123 +fun prior_to_select i_model =
5.124 + let
5.125 + (* ? problem with Const ("Input_Descript.solutions", _) ? *)
5.126 + val filt = (fn (_, _, _, _, (Inc_TEST (descr, _::_) , _)) => Model_Pattern.is_list_descr descr
5.127 + | _ => false)
5.128 + in
5.129 + (filter filt i_model) @ (filter_out filt i_model)
5.130 + end
5.131 +;
5.132 +prior_to_select: I_Model.T_TEST -> I_Model.T_TEST
5.133 +\<close> ML \<open>
5.134 +(*
5.135 + Select an item from o_model not yet input to i_model and add it to i_model.
5.136 + Prefer items with incomplete lists.
5.137 +*)
5.138 +fun item_to_add ctxt o_model i_model =
5.139 + let
5.140 + val m_field = "#Given"
5.141 + val term_as_string = "Constants [r = 7]"
5.142 + in
5.143 + SOME (m_field, term_as_string)
5.144 + end
5.145 +\<close> ML \<open>
5.146 +item_to_add: Proof.context -> O_Model.T -> Model_Pattern.T ->
5.147 + (Model_Def.m_field * TermC.as_string) option
5.148 +\<close> ML \<open>
5.149 +\<close> ML \<open>
5.150 +(*\\------------------ build fun item_to_add -----------------------------------------------//*)
5.151 +\<close> ML \<open> (*\\----------- build fun item_to_add -----------------------------------------------//*)
5.152
5.153 \<close> ML \<open>
5.154 \<close>
5.155
5.156 -(*ML_file "Minisubpbl/150a-add-given-Maximum.sml"*)
5.157 +(*ML_file "Minisubpbl/100a-init-rootpbl-Maximum.sml"*)
5.158 section \<open>===================================================================================\<close>
5.159 -section \<open>===== "Minisubpbl/150a-add-given-Maximum.sml" ====================================\<close>
5.160 +section \<open>===== "Minisubpbl/100a-init-rootpbl-Maximum.sml" ==================================\<close>
5.161 ML \<open>
5.162 \<close> ML \<open>
5.163 -(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
5.164 +(* Title: "Minisubpbl/100a-init-rootpbl-Maximum.sml"
5.165 Author: Walther Neuper 1105
5.166 (c) copyright due to lincense terms.
5.167
5.168 @@ -170,7 +287,8 @@
5.169
5.170 val return_me_Model_Problem =
5.171 me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
5.172 -(*/------------------- step into me Model_Problem ------------------------------------------\\*)
5.173 +\<close> ML \<open>(*/------------- step into me_Model_Problem ------------------------------------------\\*)
5.174 +(*/------------------- step into me_Model_Problem ------------------------------------------\\*)
5.175 "~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
5.176 val ctxt = Ctree.get_ctxt pt p
5.177 val return_by_tactic = case
5.178 @@ -229,7 +347,10 @@
5.179 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.180 (*if*) p_ = Pos.Pbl (*then*);
5.181
5.182 +\<close> ML \<open>
5.183 +val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) =
5.184 Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
5.185 +\<close> ML \<open>
5.186 (*/////--------------- step into for_problem -----------------------------------------------\\*)
5.187 "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
5.188 = (ctxt, oris, (o_refs, refs), (pbl, met));
5.189 @@ -239,8 +360,8 @@
5.190 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
5.191 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
5.192
5.193 - val return_check_OLD =
5.194 - check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
5.195 + val return_check =
5.196 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
5.197 (*//////-------------- step into check -------------------------------------------------\\*)
5.198 "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
5.199 (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
5.200 @@ -343,83 +464,161 @@
5.201 (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
5.202 val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
5.203 (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
5.204 -(*||||||-------------- contine check -----------------------------------------------------*)
5.205 +(*||||| |------------- contine check -----------------------------------------------------*)
5.206 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
5.207 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
5.208 val full_subst = if env_eval = [] then pres_subst_other
5.209 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
5.210 val evals = map (eval ctxt where_rls) full_subst
5.211 val return_ = (i_model_max, env_subst, env_eval)
5.212 -(*\\\\\\\------------- step into check -------------------------------------------------//*)
5.213 -val (preok, _) = return_check_OLD;
5.214 +(*\\\\\ \------------- step into check -----------------------------------------------------//*)
5.215 +val (preok, _) = return_check;
5.216
5.217 +\<close> ML \<open>(*|||||--------- contine for_problem ---------------------------------------------------*)
5.218 (*|||||--------------- contine for_problem ---------------------------------------------------*)
5.219 +val false =
5.220 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
5.221 +val false =
5.222 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
5.223 val NONE =
5.224 (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
5.225
5.226 - (*case*)
5.227 - Specify.item_to_add (ThyC.get_theory ctxt
5.228 +\<close> ML \<open>
5.229 +(**)val return_item_to_add =(**)
5.230 +(** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **)
5.231 + (*case*) item_to_add (ThyC.get_theory ctxt
5.232 (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
5.233 +\<close> ML \<open> (*///// /------ step into item_to_add -----------------------------------------------\\*)
5.234 +(*///// /--------------- step into item_to_add -----------------------------------------------\\*)
5.235 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
5.236 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
5.237 -\<close> ML \<open> (*//----------- build fun item_to_add -----------------------------------------------\\*)
5.238 -(*//------------------ build fun item_to_add -----------------------------------------------\\*)
5.239 -\<close> ML \<open> (*shift this block up in separate section a.s.a.p*)
5.240 \<close> ML \<open>
5.241 +(*+*)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]\"]), \n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
5.242 + = oris |> O_Model.to_string @{context}
5.243 +(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
5.244 + = pbt |> Model_Pattern.to_string @{context}
5.245 +(*+*)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)]"
5.246 + = itms |> I_Model.to_string @{context}
5.247 \<close> ML \<open>
5.248 \<close> ML \<open>
5.249 +"~~~~~ fun item_to_add NEW, args:"; val (ctxt, o_model, i_model) =
5.250 + (@{context}, oris, I_Model.OLD_to_TEST itms)
5.251 \<close> ML \<open>
5.252 \<close> ML \<open>
5.253 \<close> ML \<open>
5.254 +val return_item_to_add_step = SOME (I_Model.get_field_term thy ori (hd icl));
5.255 +"~~~~~ fun item_to_add NEW, args:"; val (ctxt, o_model, i_model) =
5.256 + (@{context}, oris, I_Model.OLD_to_TEST itms);
5.257 +"~~~~~ fun item_to_add NEW CODE BUILD, args:"; val (ctxt, o_model, i_model) =
5.258 + (@{context}, oris, I_Model.OLD_to_TEST
5.259 + (Library.take 4 itms @
5.260 + [(5, [3], false, "#Relate", Inc ((@{term SideConditions},
5.261 + [@{term "(u::real) / 2 = r * sin \<alpha>"}]), (TermC.empty, []) ))]))
5.262 \<close> ML \<open>
5.263 +(*+*)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, [3], false ,#Relate, (Inc_TEST SideConditions (u div 2 = r * sin \<alpha>) , pen2str, Position.T))]"
5.264 + = i_model |> I_Model.to_string_TEST @{context}
5.265 +\<close> ML \<open> (*//----------- build fun max_variants_TEST -----------------------------------------\\*)
5.266 +(*//------------------ build fun max_variants_TEST -----------------------------------------\\*)
5.267 \<close> ML \<open>
5.268 + val all_variants as [3] =
5.269 + map (fn (_, _, _, _, (Inc_TEST (_, []), _)) => []
5.270 + | (_, variants, _, _, _) => variants) i_model
5.271 + |> flat
5.272 + |> distinct op =
5.273 \<close> ML \<open>
5.274 + val variants_separated = map (filter_variants' i_model) all_variants
5.275 \<close> ML \<open>
5.276 -(*\\------------------ build fun item_to_add -----------------------------------------------//*)
5.277 -\<close> ML \<open> (*\\----------- build fun item_to_add -----------------------------------------------//*)
5.278 - fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
5.279 - | false_and_not_Sup (_, _, false, _, _) = true
5.280 - | false_and_not_Sup _ = false
5.281 +(*+*)length variants_separated
5.282 +\<close> ML \<open>
5.283 +\<close> ML \<open>
5.284 + val sums_corr as [1] = map (Model_Def.cnt_corrects) variants_separated
5.285 +\<close> ML \<open>
5.286 + val sum_variant_s as [(1, 3)] = arrange_args sums_corr (1, all_variants)
5.287 +\<close> ML \<open>
5.288 + val max_first as [(1, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.289 +\<close> ML \<open>
5.290 + val maxes as [3] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
5.291 + |> map snd
5.292 +\<close> ML \<open>
5.293 +val return_max_variants = maxes
5.294 +\<close> ML \<open>
5.295 +(*\\------------------ build fun max_variants_TEST -----------------------------------------//*)
5.296 +\<close> ML \<open> (*\\----------- build fun max_variants_TEST -----------------------------------------//*)
5.297 +\<close> ML \<open>
5.298 +\<close> ML \<open>(*for that --vvvvvv--- reason we probably need a new max_variants_TEST ---^^^^^*)
5.299 + val max_vnt as 3 = last_elem ((*Model_Def.*)max_variants_TEST o_model i_model)
5.300 +\<close> ML \<open>
5.301 + val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model
5.302 +\<close> ML \<open>
5.303 + val i_to_select = i_model
5.304 + |> filter_out (fn (_, vnts, _, _, (Cor_TEST _, _)) => member op= vnts max_vnt | _ => false)
5.305 + |> prior_to_select
5.306 + |> hd
5.307 +\<close> ML \<open>
5.308 +get_dscr';
5.309 +ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> I_Model.single;
5.310 +\<close> text \<open>
5.311 +val (max_vnt, descr, ts) = (3, @{term SideConditions}, [@{term "(u::real) / 2 = r * sin \<alpha>"}])
5.312 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
5.313 +\<close> ML \<open>
5.314 +"~~~~~ fun fill_from_o , args:"; val (o_model, (i, vnts, bool, m_field, (feedb, pos))) =
5.315 + (o_vnts, (*i_to_select*) (1, [1, 2, 3], false, "#Given", (Inc_TEST (descr, ts), Position.none)));
5.316 +\<close> ML \<open>
5.317 + val all_values =
5.318 + case find_first (fn (_, _, _, descr', _) => descriptor_exists descr' feedb) o_model of
5.319 + SOME (_, _, _, _, ts) => ts
5.320 + | NONE => raise ERROR "xxxxx"
5.321 +\<close> ML \<open>
5.322 +(*+*)val xxx = all_values |> UnparseC.terms @{context}
5.323 +\<close> text \<open>
5.324 + if Model_Pattern.is_list_descr descr
5.325 + then
5.326 + let
5.327 + val miss = subtract op= (I_Model.values_TEST feedb) (*TODO*)
5.328 + in
5.329 + []
5.330 + end
5.331 + else all_values
5.332 +\<close> ML \<open>
5.333 +\<close> ML \<open>
5.334 +\<close> ML \<open>
5.335 +\<close> ML \<open> (*if Model_Pattern.is_list_descr*)
5.336 +val (o_ts, i_ts) = ([1,2,3], [2,3])
5.337 +\<close> ML \<open>
5.338 + val miss = subtract op= i_ts o_ts
5.339 +\<close> ML \<open>
5.340 +\<close> ML \<open>
5.341 +\<close> ML \<open>
5.342 +\<close> ML \<open>
5.343 +\<close> ML \<open>
5.344 +(*o_model contains appropriate variants only. Observe inclomplete lists *)
5.345 +fun fill_from_o o_model (i, vnts, bool, m_field, (feedb, pos)) =
5.346 + let
5.347 + val all_ts =
5.348 + case find_first (fn (_, _, _, descr', _) => descr' = (*feedb*) descr) o_model of
5.349 + SOME (_, _, _, _, ts) => ts
5.350 + | NONE => raise ERROR "xxxxx"
5.351 + in
5.352 + 123
5.353 + end
5.354 +\<close> ML \<open>
5.355 +\<close> ML \<open> (*----------^^^ new code --------------------------------------------------------------*)
5.356 +\<close> ML \<open>
5.357 +(*+*)val SOME ("#Given", "Constants [r = 7]") = return_item_to_add_step
5.358 +val true = return_item_to_add_step = return_item_to_add
5.359 +(*\\\\\ \------------- step into item_to_add -----------------------------------------------//*)
5.360 +\<close> ML \<open> (*\\\\\ \------ step into item_to_add -----------------------------------------------//*)
5.361 +val SOME (fd, ct') = return_item_to_add
5.362
5.363 - val v = if itms = [] then 1 else Pre_Conds.max_variant itms
5.364 - val vors = if v = 0 then oris
5.365 - else filter ((fn variant =>
5.366 - fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
5.367 - v) oris
5.368 -
5.369 -(*+*)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]\"])]"
5.370 -(*+*) = vors |> O_Model.to_string @{context}
5.371 -
5.372 - val vits = if v = 0 then itms (* because of dsc without dat *)
5.373 - else filter ((fn variant =>
5.374 - fn (_, variants, _, _, _) => member op= variants variant)
5.375 - v) itms; (* itms..vat *)
5.376 -
5.377 - val icl = filter false_and_not_Sup vits; (* incomplete *)
5.378 -
5.379 - (*if*) icl = [] (*else*);
5.380 -(*+*)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)]"
5.381 - = icl |> I_Model.to_string @{context}
5.382 -(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"
5.383 - = hd icl |> I_Model.single_to_string @{context}
5.384 -
5.385 -(*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
5.386 -(*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
5.387 -(*++*)val [] = I_Model.o_model_values feedback
5.388 -
5.389 -(*+*)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]\"])]"
5.390 -(*+*) = vors |> O_Model.to_string @{context}
5.391 -
5.392 -val SOME ori =
5.393 - (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
5.394 - d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
5.395 - (hd icl)) vors (*of*);
5.396 -
5.397 -(*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
5.398 -(*+*) ori |> O_Model.single_to_string @{context}
5.399 +\<close> ML \<open>(*|||||--------- continue.. for_problem ------------------------------------------------*)
5.400 +(*|||||--------------- continue.. for_problem ------------------------------------------------*)
5.401 +val return_for_problem_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]"))
5.402 + = ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
5.403 +(** )return_for_problem_step = return_for_problem( *..would require equality types*)
5.404 +\<close> ML \<open>(*\\\\\--------- step into for_problem -----------------------------------------------//*)
5.405 (*\\\\\--------------- step into for_problem -----------------------------------------------//*)
5.406 +val return_find_next_step = return_for_problem
5.407 +\<close> ML \<open>(*\\\\---------- step into find_next_step --------------------------------------------//*)
5.408 (*\\\\---------------- step into find_next_step --------------------------------------------//*)
5.409 (*|||----------------- continuing specify_do_next --------------------------------------------*)
5.410 val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
5.411 @@ -556,13 +755,115 @@
5.412 "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
5.413 P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
5.414 (*\\------------------ step into TESTg_form ------------------------------------------------//*)
5.415 -(*\------------------- step into me Model_Problem ------------------------------------------//*)
5.416 +\<close> ML \<open>(*\------------- step into me_Model_Problem ------------------------------------------//*)
5.417 +(*\------------------- step into me_Model_Problem ------------------------------------------//*)
5.418 val (p, _, f, nxt, _, pt) = return_me_Model_Problem
5.419
5.420 (*-------------------- contine me's ----------------------------------------------------------*)
5.421 val return_me_add_find_Constants = me nxt p c pt;
5.422 val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
5.423 (*/------------------- step into me_add_find_Constants -------------------------------------\\*)
5.424 +
5.425 +\<close> ML \<open>
5.426 +\<close>
5.427 +
5.428 +(*ML_file "Minisubpbl/150a-add-given-Maximum.sml"*)
5.429 +section \<open>===================================================================================\<close>
5.430 +section \<open>===== "Minisubpbl/150a-add-given-Maximum.sml" ====================================\<close>
5.431 +ML \<open>
5.432 +\<close> ML \<open>
5.433 +(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
5.434 + Author: Walther Neuper 1105
5.435 + (c) copyright due to lincense terms.
5.436 +
5.437 +COMPARE Specify/specify.sml --- specify-phase: low level functions ---
5.438 +
5.439 +ATTENTION: the file creates buffer overflow if copied in one piece !
5.440 +
5.441 +Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
5.442 + in order not to get lost while working in Test_Some etc,
5.443 + re-introduce ML (*--- step into XXXXX ---*) and Co.
5.444 + and use Sidekick for orientation.
5.445 + Nesting is indicated by /--- //-- ///- at the left margin of the comments.
5.446 +*)
5.447 +
5.448 +open Ctree;
5.449 +open Pos;
5.450 +open TermC;
5.451 +open Istate;
5.452 +open Tactic;
5.453 +open I_Model;
5.454 +open P_Model
5.455 +open Rewrite;
5.456 +open Step;
5.457 +open LItool;
5.458 +open LI;
5.459 +open Test_Code
5.460 +open Specify
5.461 +open ME_Misc
5.462 +open Pre_Conds;
5.463 +
5.464 +val (_(*example text*),
5.465 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
5.466 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
5.467 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
5.468 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
5.469 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
5.470 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
5.471 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
5.472 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
5.473 + "ErrorBound (\<epsilon> = (0::real))" :: []),
5.474 + refs as ("Diff_App",
5.475 + ["univariate_calculus", "Optimisation"],
5.476 + ["Optimisation", "by_univariate_calculus"])))
5.477 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
5.478 +
5.479 +val c = [];
5.480 +val return_init_calc =
5.481 + Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
5.482 +(*/------------------- step into init_calc -------------------------------------------------\\*)
5.483 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
5.484 + (@{context}, [(model, refs)]);
5.485 + val thy = thy_id |> ThyC.get_theory ctxt
5.486 + val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
5.487 + val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
5.488 + val f =
5.489 + TESTg_form ctxt (pt,p);
5.490 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
5.491 + val (form, _, _) =
5.492 + ME_Misc.pt_extract ctxt ptp;
5.493 +"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
5.494 + val ppobj = Ctree.get_obj I pt p
5.495 + val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
5.496 + (*if*) Ctree.is_pblobj ppobj (*then*);
5.497 + pt_model ppobj p_ ;
5.498 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
5.499 + (ppobj, p_);
5.500 + val (_, pI, _) = Ctree.get_somespec' spec spec';
5.501 +(* val where_ = if pI = Problem.id_empty then []*)
5.502 + (*if*) pI = Problem.id_empty (*else*);
5.503 + val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
5.504 + val (_, where_) =
5.505 + Pre_Conds.check ctxt where_rls where_
5.506 + (model, I_Model.OLD_to_TEST probl);
5.507 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
5.508 + (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
5.509 + val (env_model, (env_subst, env_eval)) =
5.510 + make_environments model_patt i_model;
5.511 +"~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
5.512 +(*\------------------- step into init_calc -------------------------------------------------//*)
5.513 +val (p,_,f,nxt,_,pt) = return_init_calc;
5.514 +
5.515 +(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
5.516 +(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
5.517 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
5.518 +(*+*)val [] = probl
5.519 +
5.520 +val (p, _, f, nxt, _, pt) = me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
5.521 +val return_me_add_find_Constants
5.522 + = me nxt p c pt; val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
5.523 +\<close> ML \<open>
5.524 +(*/------------------- step into me_add_find_Constants -------------------------------------\\*)
5.525 "~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
5.526 (nxt, p, c, pt);
5.527 val ctxt = Ctree.get_ctxt pt p
5.528 @@ -582,9 +883,10 @@
5.529 Specify.by_Add_ "#Given" ct (pt, p);
5.530 "~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
5.531 val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
5.532 -(* val (i_model, m_patt) =*)
5.533 +
5.534 +val false =
5.535 (*if*) p_ = Pos.Met (*else*);
5.536 -val return_by_Add_ =
5.537 +val (i_model, m_patt) =
5.538 (pbl,
5.539 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
5.540 val I_Model.Add i_single =
5.541 @@ -783,7 +1085,8 @@
5.542
5.543 val return_me_Specify_Theory
5.544 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
5.545 -(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
5.546 +\<close> ML \<open>(*/------------- step into me_Specify_Theory -----------------------------------------\\*)
5.547 +(*/------------------- step into me_Specify_Theory -----------------------------------------\\*)
5.548 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.549 val ctxt = Ctree.get_ctxt pt p;
5.550 (* val (pt, p) = *)
5.551 @@ -833,7 +1136,8 @@
5.552 val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
5.553 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
5.554 (*\\------------------ step into do_next ---------------------------------------------------//*)
5.555 -(*\------------------- step into me Specify_Theory -----------------------------------------//*)
5.556 +\<close> ML \<open>(*\------------- step into me_Specify_Theory -----------------------------------------//*)
5.557 +(*\------------------- step into me_Specify_Theory -----------------------------------------//*)
5.558 val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
5.559
5.560 val return_me_Specify_Problem (* keep for continuing me *)
5.561 @@ -888,11 +1192,9 @@
5.562 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
5.563 = (tac, (pt, (p, p_')));
5.564
5.565 -\<close> ML \<open>
5.566 (**)val return_complete_for =(**)
5.567 (** ) val (o_model, ctxt, i_model) =( **)
5.568 Specify_Step.complete_for id (pt, pos);
5.569 -\<close> ML \<open> (*//----------- step into complete_for ----------------------------------------------\\*)
5.570 (*//------------------ step into complete_for ----------------------------------------------\\*)
5.571 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
5.572
5.573 @@ -912,7 +1214,7 @@
5.574 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
5.575 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
5.576 (*NEW*)
5.577 -\<close> ML \<open>
5.578 +
5.579 (**)val return_match_itms_oris = (**)
5.580 (** )val (_, (i_model, _)) = ( **)
5.581 (*OLD* )
5.582 @@ -921,21 +1223,56 @@
5.583 M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
5.584 (m_patt, where_, where_rls);
5.585 (*NEW*)
5.586 -\<close> ML \<open> (*///---------- step into match_itms_oris -------------------------------------------\\*)
5.587 +\<close> ML \<open>(*//############ @ {context} within fun match_itms_oris ------------------------------\\*)
5.588 +(*//################## @ {context} within fun match_itms_oris -----------------------------\\*)
5.589 (*///----------------- step into match_itms_oris -------------------------------------------\\*)
5.590 -\<close> ML \<open> (*\<longrightarrow> m-match.sml*)
5.591 "~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
5.592 (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls));
5.593 -\<close> ML \<open>
5.594 +
5.595 (**)val return_fill_method =(**)
5.596 (** )val met_imod =( **)
5.597 fill_method o_model (pbl_imod, met_imod) m_patt;
5.598 -\<close> ML \<open> (*////-------- step into fill_method -----------------------------------------------\\*)
5.599 (*////--------------- step into fill_method -----------------------------------------------\\*)
5.600 "~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
5.601 (o_model, (pbl_imod, met_imod), m_patt);
5.602
5.603 - val pbl_max_vnts as [2, 1] = Model_Def.max_variants o_model pbl_imod
5.604 +(*+*)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))]"
5.605 + = pbl_imod |> I_Model.to_string_TEST @{context}
5.606 +(*+*)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))]"
5.607 + = met_imod |> I_Model.to_string_TEST @{context}
5.608 +
5.609 +(**)val return_max_variants =(**)
5.610 +(** )val pbl_max_vnts as [2, 1] =( **)
5.611 + Model_Def.max_variants o_model pbl_imod
5.612 +\<close> ML \<open> (*//----------- step into max_variants ----------------------------------------------\\*)
5.613 +(*//------------------ step into max_variants ----------------------------------------------\\*)
5.614 +"~~~~~ fun max_variants , args:"; val (o_model, i_model) = (o_model, pbl_imod);
5.615 +\<close> ML \<open>
5.616 + val all_variants as [1, 2, 3] =
5.617 + map (fn (_, variants, _, _, _) => variants) i_model
5.618 + |> flat
5.619 + |> distinct op =
5.620 +\<close> ML \<open>
5.621 + val variants_separated = map (filter_variants' i_model) all_variants
5.622 +(*+*)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))]",
5.623 + "[\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))]",
5.624 + "[\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))]"]
5.625 + = variants_separated |> map (I_Model.to_string_TEST @{context})
5.626 +
5.627 + val sums_corr as [5, 5, 4] = map (cnt_corrects) variants_separated
5.628 + (*----------------#--#--#*)
5.629 + (*---------------------^-------^-------^*)
5.630 + val sum_variant_s as [(5, 1), (5, 2), (4, 3)] = arrange_args sums_corr (1, all_variants)
5.631 + val max_first as [(5, 2), (5, 1), (4, 3)] = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.632 + (*----------------##====--##====--//////---------^^^^*)
5.633 + (*------------^--^-#-------#*)
5.634 + val maxes as [2, 1] = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
5.635 + |> map snd
5.636 +val return_max_variants = maxes
5.637 +(*\\------------------ step into max_variants ----------------------------------------------//*)
5.638 +\<close> ML \<open> (*\\----------- step into max_variants ----------------------------------------------//*)
5.639 +val pbl_max_vnts as [2, 1] = return_max_variants;
5.640 +
5.641 (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
5.642 val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
5.643 Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
5.644 @@ -946,17 +1283,18 @@
5.645 val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
5.646 (*add items from pbl_imod (without overwriting existing items in met_imod)*)
5.647
5.648 -val return_add_other = map (
5.649 +\<close> ML \<open>
5.650 +val return_add_other = map (
5.651 add_other max_vnt pbl_imod) i_from_met;
5.652 -\<close> ML \<open> (*/////------- step into add_other -------------------------------------------------\\*)
5.653 +(*+*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
5.654 + = return_add_other |> I_Model.to_string_TEST @{context};
5.655 (*/////-------------- step into add_other -------------------------------------------------\\*)
5.656 "~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) =
5.657 (max_vnt, pbl_imod, nth 5 i_from_met);
5.658 -\<close> ML \<open>
5.659 +
5.660 (*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
5.661 -\<close> ML \<open>
5.662 +
5.663 val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
5.664 -\<close> ML \<open>
5.665 val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
5.666 get_dscr' feedb1
5.667 val true =
5.668 @@ -967,59 +1305,45 @@
5.669 find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of
5.670 NONE => false
5.671 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
5.672 -\<close> ML \<open>
5.673 +
5.674 val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
5.675 val check as true = return_add_other_1 = nth 5 return_add_other
5.676 -\<close> ML \<open> (*\\\\\------- step into add_other -------------------------------------------------//*)
5.677 (*\\\\\-------------- step into add_other -------------------------------------------------//*)
5.678 val i_from_pbl = return_add_other
5.679 -\<close> ML \<open>
5.680 -\<close> ML \<open> (*\\\\--------- step into fill_method -----------------------------------------------//*)
5.681 (*\\\\---------------- step into fill_method -----------------------------------------------//*)
5.682 val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
5.683 -\<close> ML \<open>
5.684 +
5.685 (*+MET: dropped ALL DUE TO is_empty_single_TEST*)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(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)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]" =
5.686 return_fill_method_step |> I_Model.to_string_TEST @{context}
5.687 -\<close> ML \<open>
5.688 (*+*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
5.689 = return_fill_method |> I_Model.to_string_TEST @{context};
5.690 -\<close> ML \<open>
5.691 -return_fill_method_step = return_fill_method (*latter is correct, did not investigate further*)
5.692 +return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)
5.693 (*\\\----------------- step into match_itms_oris -------------------------------------------//*)
5.694 -\<close> ML \<open> (*\\\---------- step into match_itms_oris -------------------------------------------//*)
5.695 +(*\\################# @ {context} within fun match_itms_oris ------------------------------//*)
5.696 +\<close> ML \<open>(*\\############ @ {context} within fun match_itms_oris ------------------------------//*)
5.697 val (_, (i_model, _)) = return_match_itms_oris;
5.698 -\<close> ML \<open>
5.699 -\<close> ML \<open>(*||------------ continue. complete_for ------------------------------------------------*)
5.700 +
5.701 (*||------------------ continue. complete_for ------------------------------------------------*)
5.702 val (o_model, ctxt, i_model) = return_complete_for
5.703 -\<close> ML \<open>
5.704 -(*+*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
5.705 - = i_model |> I_Model.to_string_TEST @{context}
5.706 -\<close> ML \<open>
5.707 -(*
5.708 -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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
5.709 - = i_model |> I_Model.to_string @{context}
5.710 -*)
5.711 +(*+isa*)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(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)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
5.712 + = i_model |> I_Model.to_string_TEST @{context}(*+isa*)
5.713 (*+isa2:MET.Mis* ) 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] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =
5.714 i_model |> I_Model.to_string @{context} ( *+isa2*)
5.715 -\<close> ML \<open> (*\\----------- step into complete_for ----------------------------------------------//*)
5.716 (*\\------------------ step into complete_for ----------------------------------------------//*)
5.717 val (o_model, ctxt, i_model) = return_complete_for
5.718 -\<close> ML \<open>
5.719 -\<close> ML \<open> (*|------------ continue. complete_for ------------------------------------------------*)
5.720 +
5.721 (*|------------------- continue. complete_for ------------------------------------------------*)
5.722 val return_complete_for_step = (o_model', ctxt', i_model)
5.723 -\<close> ML \<open>
5.724 +
5.725 val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
5.726 val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
5.727 -\<close> ML \<open>
5.728 -if (o_model'_step, i_model_step) = (o_model', i_model)
5.729 -then () else error "return_complete_for_step <> return_complete_for";
5.730 +;
5.731 +(*+*)if (o_model'_step, i_model_step) = (o_model', i_model)
5.732 +(*+*)then () else error "return_complete_for_step <> return_complete_for";
5.733 \<close> ML \<open>(*\------------- step into me Specify_Problem ----------------------------------------//*)
5.734 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
5.735 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
5.736
5.737 -\<close> ML \<open>
5.738 val return_me_Specify_Method
5.739 = me nxt p c pt; val Add_Given "FunctionVariable b" = #4 return_me_Specify_Method;
5.740 (*/------------------- step into me_Specify_Method -----------------------------------------\\*)
5.741 @@ -1033,7 +1357,6 @@
5.742 case Step.by_tactic tac (pt, p) of
5.743 ("ok", (_, _, ptp)) => ptp;
5.744
5.745 -\<close> ML \<open>
5.746 (*quick step into --> me_Specify_Method*)
5.747 (*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
5.748 (* Step.by_tactic*)
5.749 @@ -1046,16 +1369,14 @@
5.750 "~~~~~ fun complete_for , args:"; val () = ();
5.751 (* M_Match.match_itms_oris*)
5.752 "~~~~~ fun match_itms_oris , args:"; val () = ();
5.753 -\<close> ML \<open>
5.754 -(*+*)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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
5.755 - = get_obj g_met pt (fst p) |> I_Model.to_string @{context};
5.756 -\<close> text \<open>
5.757 -(*+isa: METHOD.drop* )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)]" =( *+isaALLcorrect*)
5.758 -(*+isa2:METHOD.Mis*)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] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =(*isa2*)
5.759 - get_obj g_met pt (fst p) |> I_Model.to_string @ {context};
5.760 -\<close> ML \<open>
5.761
5.762 \<close> ML \<open>
5.763 +(*+isa*)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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
5.764 +(*+isa*)
5.765 +(*+isa2* )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] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"
5.766 +( *+isa2*)
5.767 + = get_obj g_met pt (fst p) |> I_Model.to_string @{context};
5.768 +
5.769 (*case*)
5.770 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.771 (*//------------------ step into Step.do_next ----------------------------------------------\\*)
5.772 @@ -1084,13 +1405,12 @@
5.773 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.774 (*if*) p_ = Pos.Pbl (*else*);
5.775
5.776 -\<close> ML \<open>
5.777 -(*+*)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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
5.778 +(*+isa*)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(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(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
5.779 +(*+isa*)
5.780 +(*isa2* )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] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"
5.781 +( *isa2*)
5.782 = met |> I_Model.to_string @{context};
5.783 -(*isa2* )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] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"
5.784 - =( *isa2*) met |> I_Model.to_string @{context};
5.785
5.786 -\<close> ML \<open>
5.787 (*isa2*)val ("dummy", (Met, Add_Given "FunctionVariable b")) =(*isa2*)
5.788 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
5.789 (*///// /------------- step into Step.for_method -------------------------------------------\\*)