1.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 26 18:02:22 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 26 19:29:09 2022 +0200
1.3 @@ -108,9 +108,156 @@
1.4 \<close> ML \<open>
1.5 \<close>
1.6
1.7 -section \<open>===================================================================================\<close>
1.8 +section \<open>====--- VSCode example with Step.specify_do_next ---===============================\<close>
1.9 ML \<open>
1.10 \<close> ML \<open>
1.11 +(**** VSCode example with Step.specify_do_next ########################################### ****)
1.12 +"----------- VSCode example with Step.specify_do_next ------------------------------------------";
1.13 +"----------- VSCode example with Step.specify_do_next ------------------------------------------";
1.14 +val c = []:cid;
1.15 +val fmz = [
1.16 +(*Problem model:*)
1.17 + "Constants [r = (7::real)]", "Maximum A", "AdditionalValues [u, v]",
1.18 + "Extremum (A = 2 * u * v - u \<up> 2)",
1.19 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.20 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]",
1.21 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]",
1.22 +(*MethodC model:*)
1.23 + "FunctionVariable a", "FunctionVariable b", "FunctionVariable \<alpha>",
1.24 + "Domain {0 <..< r}",
1.25 + "Domain {0 <..< r}",
1.26 + "Domain {0 <..< \<pi> / 2}",
1.27 + "ErrorBound (\<epsilon> = (0::real))"
1.28 +]: TermC.as_string list;
1.29 +if (fmz |> map (TermC.parseNEW @{context}) |> filter is_some |> length) = 14
1.30 +then () else error "Formalise.model not parsed completely";
1.31 +
1.32 +val refs =
1.33 +("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]);
1.34 +\<close> ML \<open>
1.35 +(*/------- start example as usual in tests ---------------------------------------------------* )
1.36 +val (p,_,f, nxt,_,pt) = CalcTreeTEST [(fmz, refs)];
1.37 +val ptp = (pt, p);
1.38 +( *-------- outcomment EITHER above OR below --------------------------------------------------*)
1.39 +case get_example "Diff_App/No.123 a" of
1.40 + (_, ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: _,
1.41 + ("Diff_App", ["univariate_calculus", "Optimisation"] ,["Optimisation", "by_univariate_calculus"])))
1.42 + => ()
1.43 +| _ => error "intermed. example_store CHANGED";
1.44 +val p = ([], Pbl);
1.45 +val pt = update_state (*here we have Ctree.EmptyPtree and thus call init_ctree*)
1.46 +("Diff_App/No.123 a",
1.47 + (* Problem.parse_model_input results in markup, which is accepted by \<open>fun update_state\<close>, too:
1.48 + Constants [r = 7] *)
1.49 + ( [("#Given", ["Constants [r = 7]"]),
1.50 + ("#Where", ["0 < r"]),
1.51 + ("#Find", ["Maximum A", "AdditionalValues [u, v]"]),
1.52 + ("#Relate", ["Extremum A = 2 * u * v - u \<up> 2",
1.53 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"])
1.54 + ],
1.55 + ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"])
1.56 + (*References_Def.explode_id ^^^^^^^^^^^^^^^^^^^^^^, ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.57 + )
1.58 +) Ctree.EmptyPtree;
1.59 +val ptp = (pt, p);
1.60 +(*\------- start example as required in VSCode_Example.thy -----------------------------------*)
1.61 +
1.62 +\<close> ML \<open>
1.63 +(*** stepwise Specification: Problem model================================================= ***)
1.64 +(** ) we drop this step, because the user shall be presented a (empty) Model ... ( ** )
1.65 +val ("ok", ([(Model_Problem, Model_Problem' (["univariate_calculus", "Optimisation"], _, _), _)], _, ptp))
1.66 + = Step.specify_do_next ptp;
1.67 +( **)
1.68 +val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
1.69 + = Step.specify_do_next ptp;
1.70 +val ("ok", ([(Add_Find "Maximum A", _, _)], _, ptp))
1.71 + = Step.specify_do_next ptp;
1.72 +val ("ok", ([(Add_Find "AdditionalValues [u]", _, _)], _, ptp))
1.73 + = Step.specify_do_next ptp;
1.74 +val ("ok", ([(Add_Find "AdditionalValues [v]", _, _)], _, ptp))
1.75 + = Step.specify_do_next ptp;
1.76 +val ("ok", ([(Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)", _, _)], _, ptp))
1.77 + = Step.specify_do_next ptp;
1.78 +val ("ok", ([(Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
1.79 + = Step.specify_do_next ptp;
1.80 +
1.81 +(*** Problem model is complete ============================================================ ***)
1.82 +val PblObj {probl, ...} = get_obj I (fst ptp) [];
1.83 +if I_Model.to_string @{context} probl = "[\n" ^
1.84 + "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
1.85 + "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
1.86 + "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
1.87 + "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
1.88 + "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]))]"
1.89 +then () else error "I_Model.to_string probl CHANGED";
1.90 +
1.91 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
1.92 +\<close> ML \<open> (*with update_state*)
1.93 +(* already been input -------vvvvvvvvvvvvvvvvvvv: code in check_input is missing*)
1.94 +(*+*)val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], _, ptp))
1.95 + = (**) Step.specify_do_next ptp;
1.96 +\<close> ML \<open> (*with update_state*)
1.97 +(*+*)val ("ERROR I_Model.check_single: \"Maximum A\"\" not for field \"#Find\"", ([], [], ptp))
1.98 + = (**) Step.specify_do_next ptp;
1.99 +\<close> ML \<open>
1.100 +\<close> text \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
1.101 +(*** Specification of References ========================================================== ***)
1.102 +val ("ok", ([(Specify_Theory "Diff_App", _, _)], _, ptp))
1.103 + = Step.specify_do_next ptp;
1.104 +val ("ok", ([(Specify_Problem ["univariate_calculus", "Optimisation"], _, _)], _, ptp))
1.105 + = Step.specify_do_next ptp;
1.106 +val ("ok", ([(Specify_Method ["Optimisation", "by_univariate_calculus"], _, _)], _, ptp))
1.107 + = Step.specify_do_next ptp;
1.108 +\<close> text \<open>
1.109 +
1.110 +(*** stepwise Specification: MethodC model ================================================ ***)
1.111 +val ("ok", ([(Add_Given "FunctionVariable a", _, _)], _, ptp))
1.112 + = Step.specify_do_next ptp;
1.113 +val ("ok", ([(Add_Given "Input_Descript.Domain {0<..<r}", _, _)], _, ptp))
1.114 + = Step.specify_do_next ptp;
1.115 +val ("ok", ([(Add_Given "ErrorBound (\<epsilon> = 0)", _, _)], _, ptp))
1.116 + = Step.specify_do_next ptp;
1.117 +
1.118 +(*** Specification of Problem and MethodC model is complete =============================== ***)
1.119 +\<close> ML \<open>
1.120 +val PblObj {meth, ...} = get_obj I (fst ptp) [];
1.121 +\<close> ML \<open>
1.122 +(*+*)I_Model.to_string @{context} meth
1.123 +\<close> text \<open> (*with update_state*)
1.124 +if I_Model.to_string @ {context} meth = ("[\n" ^
1.125 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
1.126 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
1.127 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
1.128 + "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
1.129 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
1.130 +------ these are from Biegelinie: utterly wrong.
1.131 + "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
1.132 + "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]")
1.133 +then () else error "";
1.134 +\<close> ML \<open>
1.135 +\<close> text \<open> (*with *)
1.136 +if I_Model.to_string @ {context} meth = "[\n" ^
1.137 + "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] ,(fixes, [[r = 7]])), \n" ^
1.138 + "(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A ,(maxx, [A])), \n" ^
1.139 + "(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] ,(vals, [[u, v]])), \n" ^
1.140 + "(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2])), \n" ^
1.141 + "(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]])), \n" ^
1.142 + "(7 ,[1] ,true ,#Given ,Cor FunctionVariable a ,(funvar, [a])), \n" ^
1.143 + "(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} ,(doma, [{0<..<r}])), \n" ^
1.144 + "(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) ,(err, [\<epsilon> = 0]))]"
1.145 +then () else error "I_Model.to_string meth CHANGED";
1.146 +
1.147 +(*** Solution starts ====================================================================== ***)
1.148 +(*---
1.149 +Step.specify_do_next ptp;
1.150 +(*ERinROR in creating the environment from formal args. of partial_function "Diff_App.univar_optimisation"
1.151 +and the actual args., ie. items of the guard of "["Optimisation", "by_univariate_calculus"]" by "assoc_by_type":
1.152 +formal arg "err" of type "bool" doesn't mach an actual arg.
1.153 +with:
1.154 +7 formal args: ["fixes", "maxx", "extr", "sideconds", "funvar", "doma", "err"]
1.155 +7 actual args: ["[r = 7]", "A", "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", "a", "{0<..<r}", "\<epsilon> = 0", "[u, v]"]
1.156 + with types: ["bool list", "real", "bool list", "real", "real set", "bool", "real list"]*)
1.157 +---*)
1.158 \<close> ML \<open>
1.159 \<close> ML \<open>
1.160 \<close>